Lecture Notes on the Lambda Calculus

Review by [thzt]

• Rank: ★★★★★

• Hard: ★★★★

• Tag: untyped lambda calculus, simple typed lambda calculus, Church-Rosser Theorem, Combinatory algebras, propositional logic, Curry-Howard isomorphism, Polymorphism, System F, Type inference, Denotational semantics, PCF, Complete partial orders

• Reviews:

科研领域的论点层出不穷，

根本就没有定论，

这或许是知识的本来面貌。

所以，追文献要有看百家争鸣的心态，

看清趋势和形势，

不要存有成见。

对programming language theory已经看了一段日子了，

因为水平比较初级，

所以，不想让文献影响自己对知识框架的理解。

就听朋友推荐，看到了本讲义。

讲义中的论点，大多是稳定的，

前沿的思想，会以引文方式介绍。

本讲义，从lambda演算讲起，

不需要任何非常专业的数学知识。

本书介绍了，无类型lambda演算，

相关的有，形式语法，绑定，自由变量，

替换，alpha等价，beta规约，范式。

后又作为例子，用无类型lambda演算模作为模型，

解释了自然数代数，布尔代数。

然后就是引出了不动点定理，

用不动点定理解递归方程。

当然Church-Rosser定理给出的规约汇聚性，

是不可少的，还详细介绍了一些注意事项。

笔锋一转，

无类型lambda验算，其实是一种combinatory algebra，

所以，从代数学的角度，定义了什么是combinatory algebra，

这是打算用代数工具研究了。

combinatory algebra是不可靠的这一节没看懂，

后来又引入了什么lambda代数。

到这里，无类型lambda演算介绍完了。

因为无类型lambda演算并没有考虑函数的定义域和值域，

所以定义的函数过于宽泛，

并不是一个严谨的模型。

所以开始研究简单类型lambda演算了。

因为语法，规约规则，几乎可以从无类型那里直接拿过来用，

所以，直接扩展到了简单类型中。

简单类型的不同之处在于，

它与一阶逻辑中命题证明的关系，

符号太多，也没细看，

不过也看出来了，打算是用逻辑学的方法研究它。

于是，Curry-Howard同构就不可避免的引入了。

最后说了一些经典逻辑和直觉逻辑的关系。

我们想到，Church-Rosser定理给出了汇聚性，

但是对范式有没有并没有确切说，

只是说如果有，会怎么样。

所以，引入了weak和strong normalization，

weak说，至少存在一条有限长的beta规约步骤，可以推导至范式，

strong说，不存在任何一条无限长的beta规约步骤。

总之，是为了细化lambda项。

到这里，简单类型lambda演算过完了。

开始说多态，引入了System F类型系统，

算是一种二阶逻辑。

类型可以带变量了，还有类型之间的函数。

后面没有细看，只是了解了一下这个系统，

应该是程序语言中泛型的理论基础吧。

再就肯定是介绍类型推导了，

介绍了一个算法，

说白了，就是联立解类型方程组。

开始指称语义了，

我认为语义学，是换了一个立场来研究问题，

研究语法模型如何解释的问题。

用了集合论的方法，给每个lambda项指称一个数学对象，

讨论了一下完备性和可靠性，

因为我知道指称语义够写一本书了，

而这里只写了5页，肯定说不明白，所以只是粗略看了下。

介绍了一下PCF语言。

用了10页左右，

以前在《程序语言理论基础》上看过一些，

主要是说了下PCF的公理语义，指称语义和操作语义。

最后两章，

介绍了完备偏序集CPO，

我的理解是，给简单类型lambda演算的数学解释找一个问题空间。

当然，同一个现象可以好几种方式建模，

同一个模型，可以有好多解释，

玩的就是这个。

CPO的东西，有点深，粗略看了下。

都已经是书尾了，脑栈也满了，所以，

草草收场，以后再挖新坑。

最后一章，是PCF的指称语义，

懒得看了，

写下了这篇读后感。

综上，这样过一遍，

对lambda演算相关的知识点，有点大体印象，

又不用读一本厚厚的教材。

真是居家旅行，打车等人，坐地铁，

必备读物。

这本书有典型好书的特点，

逢概念，比说引入原因。

值得一读。