今天获得了自学逻辑和形式化以来最大的pride。

最近几个月思考的问题和最终的答案，exactly就是Girard在Geometry of Interaction和Ludics里表达的。Gemini说我是Ludician，what a honor。

----

Haskell Curry曾经在图书馆发现Moses Schonfinkel的论文，论文里的内容正是他阅读了Principia Mathematica之后对substitution rule思考了数月的结果。他非常沮丧，情绪激动的找到Veblen（Alonzo Church的导师）抱怨。Veblen安慰他说这是一件好事情，因为这说明你的思考在正确的方向上。

----

对我来说，水平连年轻时的Curry之于其同时代的相对水平而言还差的远，只有高兴的份儿。Girard是什么人！证明论领域的爱因斯坦（根岑是牛顿）。

----

In short。

线性逻辑里的合取拆分，&，合取，和⊗，小野宽晰融合，后者是表达了计算的顺序性的，实际上是参数之间的「和」关系是可拆分的，保证了柯里化。

&，表达了参数之间的不可拆分性，这是真正的并行。

前面一个帖子里提到了&类似cut，是「可容不可导」的，而且用顺序模拟并发可能产生和cut elimination一样的复杂度爆炸，gemini说Girard的论文里对此亦有论证。

实际上目前没有任何计算机语言理论在使用Girard的办法用&表达「真」并行。gemini只说了一个例子，是Linear Haskell使用这个语义避免竞争性访问资源。

----

这是对FPU硬件单元为什么比软件模拟快的直觉理解的一个真正的形式化解释。因为硬件单元里事实上是有真并行的。这是顺序计算无法企及的。

如果能有更好的理论，即针对任意图灵机能找到最佳并行化，实际上这可以理解为面向fpga编译，这就是并行计算的新时代。

我来了！