这一贴说另一个极其重要的概念，逻辑的一致性「不限于」表达计算的停机。

++++

如果逻辑的一致性「限于」表达计算的停机，这就是眼下类型论和计算机语言理论的主流。但是我们可以说说不那么主流，或者说还在发展阶段的看法。

Jean Yves Girard曾经有一篇非常风趣和大胆的论文：

一种新构造逻辑：经典逻辑。

Girard这样使用语言，因为他是Girard，而不是哪个学校的在读博士，编辑们大气也不敢出一声只能放行。按照Zach的说法，整个逻辑学界都接受了Girard的语言风格，没有第二个人有此待遇。大体上Girard之于逻辑证明论的地位相当于维特根斯坦之于语言哲学。

++++

从何种意义上说我们能声称经典逻辑是一种构造逻辑？我们需要修改对于构造性的定义。

构造性要求「合流」特性，confluence，也称Church Rosser定理。简单的说就是一个函数只能有一个值，不能有两个。

经典逻辑不是这样的，它允许有两个，一个不对还可以逃出去找第二个，这就是反证法，排中率，皮尔斯，call/cc，try-catch-finally。

要声称经典逻辑是构造的需要这样诡辩：构造性指的不是绝对合流，而是具有一种策略，无论你怎样怎样，我都能这般这般，达到目的。这叫做winning strategy。这也是逻辑学和计算机语言领域里有一个糟糕的名词。它还自称是博弈语义，game semantics，但实际上跟game theory一毛钱关系都没有。

实际上sigma-delta的极限定义就是这样定义的。芬兰逻辑学家Jaako Hintikka最早注意到这种定义方式是根植在经典逻辑里的。他也是最早给出经典逻辑的博弈语义一词的人。所以如果这算是用词不当的话，这个锅是Hintikka的。

++++

λ在「目标语言」层面是一个顺序计算模型。如果要让它支持call/cc要在「元语言」层面动手脚。我其实有点诧异计算机语言理论的教材里不指出这一点，仿佛各种往λ上糊出来的特性都是在可计算函数里「挑选」和「小修小补」，这也包括整个类型论。实际上不是的。

在保留λ的顺序计算模型的前提下，逻辑一致性在表达停机。但是如果象Girard那样拓展构造性的概念，甚至推广到进程演算领域，这时候一致性证明仍然是需要的，它意味着针对任何输入，都可以达成目标，包括在引入线性逻辑下资源满足需求（资源不足可以拒绝服务）。

在嵌入式里象freertos的任务，在while里循环到永远是perfectly OK的事情。现代计算机语言理论里也是不能拒绝把Y组合子捞回来的。

为什么要把Y组合子捞回来？我在PLT群里问过这个问题。大部分刻板的教科书答案我都没记住，千里冰封给了一个哲学味很重的答案：

一个不一致的逻辑系统是没用的，一个不一致的计算机语言仍然可以做很多事情。

我想这大概是PLT教授给学生们的说法吧。但我现在知道怎么完全在形式化层面理解这个问题了，无需借助哲学，或直觉。