本书或许是我人生中接触到的第一本严肃编程语言教科书. 那时我还在读SICP, 已经是2019年的事情了. 虽然我当时迫切想要阅读这本书, 但是完全读不明白, 缺乏动机. 或许现在才是学习这本书籍的好时机, 毕竟和那时比起来, 我已经学了点格论和指称语义了. 这也不是我第一次尝试翻译这本书, 不过先前都浅尝辄止了.
对于Christopher Strachey和其工作致敬
我们都希望Christopher能够为本书写下这些引言. 他于1975年5月在58岁时英年早逝, 在其亲人, 同事, 学生以及诸多(学术和非学术的)朋友的生活之中留下了永恒的缺憾. 在他于牛津工作的十年间, 自1971年起他拥有个人讲席, 他所在的领域经历了显著的增长和变化, 很大程度上这要归功于他个人的许多原创性想法和他对于别人工作的影响. 出于对于他的工作的认可, 英国计算机协会于1972年授予他成为首批杰出会士之一. {译注: 首批实际上只有两个人, 另外一个是Dijkstra.}
然而, Strachey自己的发表是不多的, 尽管这并不总是他的问题.
不论如何, 就我个人而言, Strachey他自己能否写出令人满意的开篇文字也是值得怀疑的. 他的讲课风格时而简洁明快, 时而杂乱无章; 有时晦涩难懂, 有时妙趣横生; 既令人愉悦, 又令人抓狂; 带着讽刺意味, 而且始终高度即兴, 但 (对于那些愿意倾听的人们而言) 一直具有强烈的启发性. 他所能做的, 并且的确在一些场合是这么做的, 是产生一些更短的碎片, 这些碎片极其清晰, 提出了什么是基本的想法和重要的问题, 因为他的独特经历赋予了他特殊的洞察力.
前一章末的讨论已经指出若要使得我们对于演算的语义理论的搜索成功, 那么我们必须找到方法来限制我们所能够考虑的函数类. 否则的话, 函数就会太多, 以至于我们无法找到任何带有同构函数空间的非平凡空间.
逻辑学家的通常解法是压根不与函数打交道, 转而与函数的表示打交道. 简而言之, 他们取Gödel配数. 他们通常处理整数上的函数, 在这种情况下Gödel配数的运算将可用有限长度算法表达的函数 (其构成了一个可数集) 映射为整数. 当他们想要考虑一个以另外一个函数作为一个参数的函数时, 那么他们可以形式化地给提供的Gödel配数.
这种方法在牵涉可判定性的论证中的使用是令人满意的. 这些论证通常具有以下形式: 设你声明你有一个可以判定停机问题的函数; 那么我们可以找到另外一个函数使得不能成立.
我们不使用算法的Gödel配数, 转而采取另外一种方法, 其更关心函数 (或者说映射) 本身. 让我们试着通过检视我们的问题的另一方面 (多不动点问题) 来汲取一点灵感. 考虑递归定义:
f = λx. if x = 0 then 1
else if x = 1 then f(3)
else f(x-2)λf.λx. if x = 0 then 1
else if x = 1 then f(3)
else f(x-2)答案在于其他的解都包含任意的信息 (即的值), 这是我们不希望实现所决定的.