今天非常胡扯的得到了一个非常严谨的结论。

值就是最大并发形式。这也包括证明论上的normal form，λ上的normal form，SK上的normal form，以及经典逻辑和逻辑电路里的CNF/DNF。

----

在逻辑上被认为最重要的连接符，implication，实际上绝大多数都可以被看作cut扔掉。最后剩下的是「算法包含的最少的和必要的」顺序性，它类似并发计算里的Join。实际上Concurrency指的是这种Join。

在证明论的意义上，这是multiplicative conjunction和它的residuated operation（implication），表达了顺序性，一个顺序不可交换的过程，否则算法含义保不住了。

----

人类写的程序是一个proof，我们需要cut规则，它带来组合性，能编码尽可能大的空间。

它的等价变换是，先normalize，然后就只剩下heuristic算法逆向编码，再引入cut和类似cut的「可容不可导」规则（这些规则就是哥德尔不完备里的无法证实无法证伪规则）。

如果不考虑参数的概率分布的话，是可以找出统计上最优的解的。但这是理论上的。实际上没那么多计算资源可用。

但是拼资源人是根本拼不过AI的。[二哈]