小野宽晰把合取拆分成加性合取(加法合取,线性逻辑里称with)和乘性合取(线性逻辑里称tensor),后者也称为小野宽晰的融合(fusion)。
融合对应了函数参数的(可)柯里化,顺序性,组合性,和Berry稳定性。加性合取是不能柯里化的。
于是塔玛的,这个加性合取在顺序语言里(计算机语言的Plotkin操作语义一定是顺序组合规则的),成了数据结构,沃日,record,product,data parallelism,完全是对「并行」的垃圾实现啊。即使拖到范畴论里的3C认证,笛卡尔闭范畴,换了一堆名词不改其垃圾本质。还有著名的full abstraction/full completeness问题,用博弈语义解决plotkin语义和scott语义的差别。其实博弈的本质是回合制,强制了顺序性,等于是给一个模拟器找到了一个和模拟器同样无能的行为一致的系统来解释这个模拟器。
----
Girard对范畴论和博弈语义没什么兴趣是完全正确的。他领先这个时代半个世纪。
换句话说,整个计算机语言理论构筑在「用串行模拟并行上」工作 。PLT对工业产生不了很大的影响是有原因的。
发布于 上海
