计算机语言上的类型论在很大意义可以看作term model。虽然这么说很奇怪。

++++

经典逻辑本身是静态的，不存在停机问题。它的model也都是集合论下的代数模型。所谓model就是我能用集合论定义一堆数学对象，把这个theory里的每一个term或formula都对应上去，并且保持运算的代数结构。比如命题逻辑到布尔代数就是最典型的例子。

λ就复杂一点。它竟然出现了一个神奇的、可以和经典逻辑model类比的集合论model，就是著名的Scott Model。

1969年前后Scott老师正在撰写一篇论文，他想声称无类型λ的集合论model是没可能实现的，他想了一种argue的方法。但一个月后他发现这个argument做一个小修改，λ的集合论model竟然塔玛的是可以实现的。

任何一个λ项能map到一个Scott domain的集合对象上，不同的λ项如果他们在函数的意义上是一样的，即同样的输入一定有同样的输出，他们对应同一个集合对象。Application运算可以在这个模型上定义并保持一致。

λ不是只有一个model。我见过的，当时看懂了现在全忘了的有趣的model是在Bimbo的组合子书里看到的。每个term能构造一个自然数数列，自然数数列和自然数数列之间可以定义一种类似矩阵和矢量计算的规则，对应application。在这个定义之下，每个项都能map到这样的数列上，保持application运算。

当然最无趣的model，我们一般称之为term model，就是拿λ给λ做model。先筛掉不是normal form的项，剩下的都是λ表达式的直觉意义上的值。每个λ项都跟它的值对应，这样λ上的beta-eta相等性还是保留了的。这种属于trivial model，最没卵用的一种。

但是两个λ项对应的数学函数一样，这两个项一样吗？这等于说冒泡和排序是一回事吗？直觉上不一样对吧。所以我们需要一种能反映出他们的「算法」不同的语义。

于是来了Plotkin的（小步）操作语义和Kahn改良的（大步）操作语义。他们直接以虚机的方式描述一段程序的每一步在干什么，如果没有随机函数的话，如果函数都有确定性的话，那么这种描述虽然看起来不高明，没有把Knuth的组合数学意义上的算法精神提炼出来，但至少，完整操作语义是包含了算法的。

++++

非经典逻辑也有一个常用的模型方法，即Kripke语义。在经典语义里，变量的域是集合。集合是什么东西？它是不可名状的一坨，集合里的元素除了彼此不同之外，看不出这一家人之间有什么关系和内在的组织结构。

Modal Logic是一个大家族。最最保守最最机械化的理解是，Modal Logic的模型在经典逻辑模型里的黑呼呼一坨的集合里构建一点结构和秩序。粗糙的说是有向图，精致一点的可以是偏序（可达）。有了这个图之后，判定一个语句是不是真，要像visitor模式一样跑到每个节点问我手上这句话真不真？Kripke语义只允许使用每个节点和他一步可达的节点上的属性，以及表达式本身包含的属性，来判定这句话真不真。在这个语义里，每个节点叫做possible world，一句话为真需要在all possible worlds里为真。

你觉得这个设计有说服力吗？Quine持续猛烈的抨击Kripke真值定义很多年，原因很简单。集合论是外延理论，比如集合相等的定义取决于满足同一个属性，而possible world是构造的，判定依赖于这个人为和随意构造的结构。

但是Modal Logic能描述的东西远超这个粗鄙模型给人的第一眼简陋印象。它可以表达必然，可能，指称，对话，时序，认识，知识之间的关系，等等等等。这是又一个小身材大能量的强大逻辑武器。

而且，Kripke语义也是直觉逻辑最常用的模型。因为在直觉逻辑里，我们没法象上帝一样知道什么是永真，但是（在偏序结构上）每推演一步，我们就有更多的真。这就像我们的λ计算模型一样，无论是有类型的还是没有类型的，我们每计算一步，就向前一步，也是在一个偏序结构上。

为什么会有柯霍同构呢？为什么集合运算和数字电路同构呢？因为直觉逻辑和λ模型都可以用偏序结构联系起来的。

++++

我们现在重申两个直觉。

一个是形式化语言可以有看起来很没用的term model，比如把λ项按照相等性「合并」到一个值上。

另一个是我们在构造模型时，有选择结构的自由，象Kripke那样。

然后我们会问更加惊人的问题：

第一，我们能不能合并所有类型相同的项，作为该类型下所有项在model里对应的元素。

第二，我们能不能把λ或组合子这种applicative structure，这种带着动态性的结构看作结构？拿动态结构作为all possible world？

这两个问题的答案都是能。所以从这个意义上，类型论是有类型λ作为理论编程语言的model。

++++

martin lof类型论（mltt）带来了在类型里的applicative structure和改变世界的内涵相等性定义。Girard在线性逻辑里带来了动态执行时的资源跟踪。

因为在逻辑里proof checking是一定停机的，对公式作为资源的使用可以用规则限制。这种检查proof的方法，也是类型论语言里类型检查的方法。但是在pl的角度来说，我们说，type checking是把这个term model当作一个简化的抽象程序，在「所有」估值（即执行）路径上跑了一遍（限类型部分，不含语义计算）。

因为线性逻辑里表达了对公式的使用次数限制，我们可以定义什么是量；因为我们有在类型上做计算（applicative structure）的能力，所以我们可以用类型追踪量的变化，因为mltt提供了革命性的内涵相等定义，我们可以用它来书写复杂的类型相等条件。把这些叠加在一起，我们可以这样表达：

这个term model是动态程序的一个动态model（modulo type），type checking时等于所有可能的路径都被跑了一遍，在所有的执行路径上，资源使用符合要求。100%的coverage，100%的term model层面上的程序正确性。这就是martin lof类型论和线性逻辑带给编程语言的强大能力。

++++

通讯和协议是软件工业谈了很多很多年的话题。但是通讯本身就带着「线性性」，比如我们会精确的描述每个包或者每个操作的顺序，只有几次。其实session，state这些词语本身，在线性逻辑的理解下，就在说他们都是线性的。

session type是需要一个表达线性的类型系统精确表达和可以验证的。无论是linear type，它的子结构逻辑变种，还是quantative type。

++++

Philip Wadler在1990年前后就有一片激情四射但文章，Linear types can change the world。在下愚钝，终于窥得一点奥妙。

这个看起来非常有趣的人，给Java和Go两门语言装上泛型的人，在λ大会上撕开衬衫露出超人内衣胸口写着λ大字的人，让爱丁堡的星光更璀璨，也真是学者里令人羡慕的精彩人生。