Berry在1979年的PhD论文里给出的域论上的对象的stability定义太牛了，是到目前为止最精确的并行计算定义。
----
我们从PCF语言的POR函数来直觉的理解一下。
POR函数有两个参数，如果其中任何一个能估值为true，则POR的值也是true，如果两个都是false，结果也是false，其余情况是⊥，不停机。（据说这是Kleene强三值逻辑里析取的精确定义，但我没去求证）。
这个函数的困难在于，在估值por(x,y)时，无论先估x还是先估y，都可能遇到⊥，以至于即使另一个是true，应该返回true，也估不出来了。
----
首先我们澄清两件事，第一，这不说明POR不是一个可计算函数，第二，这也不说明PCF语言不是图灵完备的，实际上它是。
POR是可计算函数，因为可以用图灵机（或λ）实现一个PCF语言的解释器，在估值POR时，交替估值参数x和y，这样是可以得到和POR函数定义一样的结果的，即可以正确估值。
第二，PCF语言是图灵完备的，POR函数不能直接实现但是可以同样通过实现一个meta circular解释器改变估值规则实现。
----
那么，什么是The Element of Parallelism呢？Berry在Scott Domain上给出了一个stability定义，稳定的函数是保持了单调性的那些。但是我们不必去搞艰涩的论域，可以从我们熟悉的语法对象来了解。
λ演算有一个基本特性是compositionality，即它的估值是完全由subterm决定的，这也是curry化能成立的前提。比如我们说f x y可以把f x当作高阶函数，应用在y上，这几乎是λ理论的根基。
但是por函数不是如此。por x y不能把por x单独拿出来估值，否则做不到我们前面说的交替估值。换句话说我们必须承认x和y之间是「并行」组合，不能拆开的。
如果你足够了解证明论，尤其是子结构逻辑，可以很容易看出来，f(x,y)在所谓顺序执行模型下，x和y是合取的逻辑关系，实际上函数本身从输入到输出是这个合取关系的逆（蕴含）。但是por(x,y)中的x和y不是合取关系，事实上它变成了析取。这里的逗号成了矢列表达式中后件里的逻辑公式之间的关系。
----
我们不深入探讨它对逻辑和计算的代数结构的影响。实际上合取和蕴含是比较「美」的结构部分，析取是比较丑陋的，熟悉自然演绎的都会理解这一点。
我们从另一个角度来类比一下这个x和y的析取关系。如果它是一个显式定义的operator的话，它没有办法被其它关系表达。在计算里如前所述，承认compositionality就没有真并行。在逻辑里，析取在经典逻辑里可以被其它连接符表达，但这是因为经典逻辑默许了后件多公式，实际上已经默许了析取。而直觉逻辑不允许，所以直觉逻辑里析取具有独立性。
一个惊人的类比是这样的：
我们都知道逻辑里有个Cut规则是结构规则。它是可容不可导的，即加入Cut当作规则（公理）使用，它不增加定理（也因此它可以被eliminate），但是它自己本身不可从其它规则出发证明。
假如我们有一个表达并行的算子，例如写成∨，它同样是可容不可导的。因为原来可以实现的函数就是可计算函数全集，加上它没有产生不可计算函数。换句话说它同样可以被elimnate，只是这里的推断不算一个构造性的证明。
Cut意味着什么？搞逻辑的人都清楚，Cut消除得到normal form的代价是证明复杂度是hyper exponential增长的。∨会不会也如此，我没有严格证明，但直觉上的回答是Yes。
这是一个有点可怕的结论。因为它意味着自然界里普遍存在的并行计算，如果按照现行计算机语言理论和对算法的理解，坚持串行计算约等于指数级的浪费算力。
----
逻辑角度。
当把合取和析取理解为数据结构上的product（record）和sum（union）时，这个理解不算错，但是它不能真的overcome串行和并发之间的矛盾。这就像允许在后件里出现A∨¬A，和允许写出⊢A,¬A是不同的。这种「模拟」只能解决有限场景，即所谓「data parallelism」。
Katalin Bimbo的书里有一章在讨论「反向应用」，即把参数应用在函数上。这个在形式化系统里的第一感觉就像是学术无厘头。但是在我们讨论的这个问题上，这个理解爆发出了威力，因为，f x y是把参数一个接一个的应用在f上，还是把x和y「一起」应用在f上，成了串行和并行的分水岭。
承认Arguments are Premisses，是对这种理解更有帮助的。
----
此文逻辑上有误，但是先不改了。简单说一下，f x y和por x y里的x和y都是AND，不是OR，但是两者的区别要找到子结构逻辑看。
f x y或者整个λ theory，都是multiplicative的，代数结构是剩余格，参数之间的关系是fusion，而是是非交换的那种（因为参数不能随意修改顺序）。
但por x y让multiplicative λ语义的基石崩塌了。这个基石我们有四个不同的术语描述他：currying，compositiinality，sequentiality，和Berry的stability定义。
por是additive的，它没有adjoint算子，没有剩余格结构，只剩下格。adjoint算子在逻辑上是蕴含（或逆蕴含），同构函数的。additive合取（&）没这个东西。
以上和gemini battle了几遍，无误。这个重要的理论根基站住了。
