LISP——关于其过去和未来的笔记——1980，中文翻译

Programming
1

目录

原文链接：https://www-formal.stanford.edu/jmc/lisp20th.pdf

McCarthy 的这篇文章以历史为论据阐述了 LISP 未来发展方向，如声明式编程、用数学证明程序正确性，至今大都仍保持超高逼格。然而就是触之不及的东西才有逼格，这些东西投入使用的难度估计跟量子计算机一个等级的。

概述

LISP 已经存活了 21 年，因为它占据了编程语言领域中的某种局部最优。然而时间的汪洋大海上不乏蜉蝣，漂流 21 年不可避免会沾上藤壶，船只维护却长期以来被我们遗漏。合作的程序库自然有益于 LISP，尤其是在程序库的创建和维护方面。现在，对于纯 LISP 和稍微扩展一些的纯 LISP，可以检查程序正确性，其中论证过程可以丢给计算机检查，但在我们充分利用 LISP 的数学基础之前，还需要更深的理论和语言本身的一些优化。

1999 年注：本文发表在 1980 年在斯坦福大学举行的 Lisp 会议中。由于它几乎完全符合我现在的观点，所以我要求在 1998 年 Lisp 用户会议论文集中重印它。我在 1998 年的会议上发表了同题演讲。

1. 引子

LISP 约莫 21 岁1，作为人类已经成年了（虽说编程语言的预期寿命可能跟人类差得有点多）。事实上，LISP 是现存第二古老的编程语言，仅次于 Fortran。也许我们应该采访一下这位爷爷，问问他长寿的原因是什么。言归正传，LISP 的早期历史已经在 [McC81]2 中进行了介绍，转载自 1977 年 ACM 编程语言历史会议论文集。

因此，本文首先回顾了 LISP 的一些显著特征，分析了这些特征与 LISP 长期存活的关系，顺便提到了 LISP 从未得到计算机公司的支持。LISP 比大多数计算机语言更基于数学理论，大概原因有三：函数式语法，λ 表示法，解释器基于泛应用函数。

我想自动编写 LISP 程序相关、可以用计算机验证的证明，现在这种技术已经可以应用于大部分 LISP 了，所以我也会把这部分技术写在本文中。本文下一部分简要描述了其他（现有或拟定的）理论不够清晰的技术。最后，LISP 有什么可能的改进？以及用更好的东西取代 LISP 前景如何？我会对这两个问题发表一些评论。

2. LISP 的生存

作为一种编程语言，LISP 具有以下思想：

  1. 使用符号表达式而不是数字进行计算。
  2. 在计算机内存中，用链表表示符号表达式和其他信息。
  3. 在纸上、键盘上，或者其他外部媒体中，主要用多层列表表示信息，有时也用 S-表达式。任何类型的数据都可以用单个通用类型表示，这一点很重要。
  4. 少量选择器和构造器，表示为函数，即 car 、 cdr 和 cons 。
  5. 简单函数可以组合形成复杂函数。
  6. 使用条件表达式可以把分支放入函数定义。
  7. 递归使用条件表达式以构建任意可计算函数。
  8. 使用 λ 表达式命名函数3。
  9. 符号可以用属性表存储额外信息。
  10. 用 LISP 数据表示 LISP 程序，从而 LISP 程序本身也可被 LISP 程序操作。这一特色消除了系统程序员和应用程序员之间的分离。每个人都可以“改进” 他的 LISP，其中许多 “改进” 已经发展成为对语言的改进。
  11. 用条件表达式解释布尔连词。
  12. LISP 函数 eval ，既是 LISP 的形式化定义，也是 LISP 语言的解释器。
  13. 用垃圾回收管理内存。
  14. 对声明的最低要求。因此 LISP 语句不仅可以在线4执行，甚至还无需预设。
  15. LISP 语句可以用作在线环境中的命令语言。

当然，上面仅仅提到了 LISP 的 “数学特色”，而没有提到和其它大多数编程语言类似的 “程序特色”。

上述所有特性都存活下来了，可以看出这种组合基本上就是编程语言空间中的局部最优了，毕竟多次取代 LISP 的尝试都没有成功，其中一些是相当确定的无法成功。不妨回顾有代表性的几个，然后分析它们没有成功的原因。

  1. SLIP 在 Fortran 中引入列表处理。它使用双向链表，不允许递归函数和条件表达式。双向链表仅在少数应用中占优，而在其他方面浪费了空间和时间。SLIP 不鼓励在线使用，因为 Fortran 不鼓励。

  2. Formac 是另一种基于 Fortran 的语言，部分 IBM 员工推进了一段时间。它操作 Fortran 风格的代数公式，并且面向批处理。

  3. Formula Algol 致力于语言二义性，即基本运算既可以操作数字，也可以操作公式。最根本的想法是，如果变量 x 没有值，那么涉及 x 的表达式会被视为对公式的运算。可以编写一些程序，但事实证明，二义性不足以作为实质性程序的基础。

  4. POP-2 是（或曾经是）LISP 的竞争对手中比较有趣的一个。它包含 LISP 所拥有的一切，只是语句以类似 Algol 的形式编写，并且内部没有任何列表。因此，POP-2 程序只能生成字符串来表示其它 POP-2 程序。这导致了系统程序员和应用程序程序员之间的鸿沟。相反，在 LISP 中，任何人都可以制作形态各异的宏识别器和扩展器。

  5. Microplanner 是比 LISP 更高级别的通用语言的尝试。“更高级别” 涉及数据（模式匹配）和操控（目标搜索和失败机制）。不幸的是，两者都不够通用，程序员被迫进行非常复杂的构建，甚至需要改用控制功能更复杂的其它语言，比如 CONNIVER。最终许多人又回到了 LISP。

    似乎没有人充分理解模式计算。简单的示例上倒是没什么问题，但在推广时会导致系统过于复杂。我们可以在某些宏扩展系统（如 LISP 机器 [WM78]）的 LISP 中看到这一点。

  6. 我应该提到 Prolog，但我还没有充分理解它，无法发表评论。5

3. 改进

正如其它所有事物，在时间海洋的航行中，名为 “LISP” 的每条船只都沾上了藤壶。只有清洗掉这些藤壶，明确的可标准化语言才有可能实现 —— 这个目标有很大价值，但并不是一朝一夕可完成的。这里给出一些改进方向，有些纯粹是操作上的，有些则具有更多的概念性内容。

  1. 在语言中加入更多的标准功能，并合理化当前版本的标准功能。

    编程语言的设计者经常建议语言规范省略用户可以定义的工具，结果用户通常无法使用彼此的程序，因为每个 LISP 发行版和用户都以不同的方式执行各种常见任务。目前来说，程序员为了避免重写函数会使用本地库，所以不同的本地库就等同于不同的语言。如果有更多的标准功能，LISP 用户之间的兼容性将大大提高。

  2. 特定语法（syntax directed）的输入和输出。

    表示符号信息的记法可以从三个角度进行优化：易于书写、便于阅读、程序操作方便。三个需求都很迫切，然而它们几乎总是严重不相容。LISP 的大部分成功归功于优化第三个。事实证明 LISP 列表和 S-表达式（其中项目的 car 表示其类型）最适合作为编程数据。

    输入输出视为列表或 S-表达式有点不方便，但是输入输出量较小时，用户通常可以忍受。毕竟要是不用的话，那就得编写、读取、打印各种语法不同的程序了。输入和输出程序通常是工作的很大一部分，也是 bug 的主要来源。此外，输入程序通常应该检测并报告输入语法中的错误。

    如果有指定语法输入和输出的标准工具，LISP 会极大改善。几年前，Lynn Quam 实施了一个系统，对输入和输出使用相同的语法描述，但改善不大。可能人们想要不同的输入和输出语法，并且输入语法应该准确报告错误。这个想法是为程序员提供标准工具，以描述外部媒介中的数据和 S-表达式之间的对应关系。例如，程序员应该能够写出类似这样的代码：

    • (\mathrm{PLUS}\ x\ …\ z) → x + ⋯ + z
    • (\mathrm{DIFFERENCE}\ x\ y) → x - y

    顺带一提，我对上面这两个记法不予置评，只是举个例子而已。

  3. 针对特定语法的一般计算。尚不清楚这个功能要添加到 LISP 还是新语言。然而，LISP 现在所具有的函数计算形式和语法特定功能似乎都需要一种语言。

  4. 我们想资助和管理一个中央机构，由它审议标准库，讨论独立于机器的特性，维护一个标准子集，并协调对计算机制造商的压力，要求在其机器上开发和维护足够的 LISP。它不应该变得太强大。6

4. 证明 LISP 程序的正确性

利用 LISP 的理论基础，我们可以证明 LISP 程序的正确性。

如果把 LISP 函数用纯 LISP 的形式写出，不难发现其性质可以通过代数操作和数学归纳来研究。因此我们的目标是建立一门数学计算理论，为程序写出可以被计算机检查的证明 [McC62]。由于 LISP 函数在数学上是函数而非映射，也就是涉及计算，因此标准逻辑技术并不能立即适用，虽然递归归纳（recursion induction）[McC63] 很快作为一种非正式方法可用。[Kle52] 一文的方法可能已经被用来证明程序的性质了，任何了解这些程序的人都应该可以理解其中的联系。

首个适当的形式化方法基于 Cartwright 的论文 [Car77]，这个方法把类似这样的 LISP 函数定义：

\begin{align*} append[u, v] ← {}&\mathbf{if\ null}\ u\ \mathbf{then}\ v \\ &\mathbf{else}\ cons[car\ u, append[cdr\ u, v]] \end{align*}

替换为一阶逻辑的陈述句：

\begin{align*} (∀ u\ v)(append(u, v) ={} &\mathbf{if\ null}\ u\ \mathbf{then}\ v \\ &\mathbf{else}\ cons(car\ u, append(cdr\ u, v))) \end{align*}

无需证明程序对任何列表 u, v 都停机。停机证明与任何其他归纳证明具有完全相同的形式。另见 [CM79]。

Elephant 形式（McCarthy 1981 即将出版）7提供了适用于顺序 LISP 程序的第二种方法。Boyer 和 Moore [BM79] 用不同的形式提供了证明发现以及证明检查，他们的形式要求证明函数都会停机，作为函数定义过程的一部分。

我不认为 LCF（Logic of Computable Functions，可计算函数的逻辑）方法足够，因为 “可计算函数” 太弱了，无法包含所有的程序。

这些方法（非正式使用）已作为斯坦福大学 LISP 课程的一部分成功教授，并将在教科书中进行描述（McCarthy 和 Talcott 1980）8。至于机器检查证明，完全可以使用 Richard Weyhrauch 的 FOL 交互式一阶逻辑证明检查器，但实践中需要证明检查器、解释器和编译器集成一体的 LISP 系统。9 , 10

计算机证明检查的最终目标是给没有数学倾向的人用，以此更快地找到没有 bug 的程序。这需要进一步的技术发展，缩短证明，并改善程序规范的编写方式。

在程序可检查性方面，程序规范的某些部分（例如程序停机）可能只起到语法上的作用。然而，人工智能中使用的程序规范甚至连指定都需要新的想法。我认为最近在非单调推理方面（non-monotonic reasoning）的工作将与此相关，因为人工智能程序需要对它所在的世界下结论。

虽然纯 LISP 和比较简单的 “程序特色” 很容易形式化，但可操作的 LISP 系统，如 Interlisp、Maclisp 和 Lisp Machine LISP [WM78]，它们的许多更高级的功能更难形式化。其中 F-表达式之类的东西需要更多的数学研究，而其它特性依我看仍然不成熟，应该在数学上更加整洁，以便可以轻松证明使用它们的程序的属性，这样也能减少普通 bug。

当前 LISP 系统的以下（包括拟定的扩展）特性需要新的正确性证明方法：

  1. 涉及修改（re-entrant）列表结构的程序。那些不涉及 rplaca 和 rplacd 的程序，例如搜索和打印，比涉及它们的那些程序更方便使用。我有一个适用于有限图的归纳法，但我还不清楚如何处理 rplaca 和类似的函数。有限图归纳法也可用于证明流程图相关程序的性质。11
  2. 关于语法计算的性质，我们目前还没有成体系的方法可以形式化陈述和证明。12
  3. 使用宏扩展的程序。理论上来说可以通过解释器的公理化来证明其正确性，但我不知道任何实际的形式化证明。
  4. 暂时无法证明涉及惰性求值器的程序的正确性。
  5. 原则上，可以用 Dana Scott 的方法构造具有函数式参数的程序，但不同种类的函数式参数只能用描述性和非正式的方式处理。13
  6. 证明检查离实用工具之间还有其它障碍，其中最大的可能是程序规范的描述方式。许多程序都有实用的非完全规范（partial specification）——它们不应该循环或修改不属于它们的内存。一些规范满足代数关系，比方说编译器。然而，有的程序需要与世界交互，它们的规范涉及对世界的假设。一般来说，人工智能程序的规范很难指定；有可能它们的规范本身就涉及默认推理和其他非单调推理。（参见 [McC80]）

5. 谜团和其它事项

  1. Daniel Friedman 和 David Wise 认为， cons 不应该求值其参数，这样我们就可以把某些无限列表视为对象。不必担心正常情况下无限列表会遇到的问题，因为这种情况下，无限列表只有操作（例如打印）所需的部分会被求值。我不清楚无限列表的确切定义域是什么。虽然他们给出的应用示例挺有趣，但实用价值尚不清楚。

  2. 很多人提出了全 λ 演算的实现。这允许更高级别的函数，即函数的函数的函数的……，但允许的操作只有组合和 λ 转换，而没有对符号表达式的一般操作。虽然没有直接提供条件表达式，但可以通过将 \mathbf{true} 写成 (λx\ y.x) ， \mathbf{false} 写成 (λx\ y.y) ，然后把 \mathbf{if}\ p\ \mathbf{then}\ a\ \mathbf{else}\ b 写成 f(a)(b) 来模拟。Scott 的另一个巧妙想法（改进自 Church）是，把自然数 n 用取列表第 n+1 个元素的运算来表示。问题是扩展到 λ 演算是否具有任何实际意义，目前最好的猜测是否定的，尽管 Scott 的符号想法建议改变 LISP 的记法，用 0 表示 car ， 1 表示 cadr ， 2 表示 caddr ，等等。

  3. 如果所有列表在内存中唯一表示，纯 LISP 在概念上会简单得多，这可以使用哈希 cons 来完成。但这样的话普通 LISP 里 rplaca 和类似的函数就没用了。就没有两全其美的方案吗？

  4. 在我看来，LISP 可能会在许多方面被某种语言所取代，这种语言对 LISP 的作用就像 LISP 对机器语言的作用一样。也就是说，它将是一种比 LISP 更高级的语言，就像 LISP 是比机器语言更高级的语言一样，这种语言可以引用自己的程序。（但是，比 LISP 更高的语言可能含有大量用于声明性编程的组件，以至于其文本与程序不对应。如果取代解释器的东西足够聪明，那么用户编写的文本将更像是对目标的描述，或者是对实现目标可用手段的描述，而非程序本身）。14

    LISP 和这种语言之间有一个直接的障碍：无论是抽象语法和还是模式匹配，操作含绑定变量的表达式都太笨拙了。

6. 参考文献

Lisp 首次在 [McC60] 中描述，第一本手册是 [ML+66]，其第一个版本于 1962 年出现。15

[BM79] Robert Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979.
[Car77] Robert S. Cartwright. A practical formal semantic definition and verification system for typed lisp. Phd dissertation, stanford university, 1977.
[CDE+98] M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, and J. Meseguer. Metalevel Computation in Maude. In C. Kirchner and H. Kirchner, editors, 2nd International Workshop on Rewriting Logic and its Applications, WRLA98, volume 15 of Electronic Notes in Theoretical Computer Science, 1998. URL: http://www.elsevier.nl/locate/entcs/volume15.html.
[CM79] Robert Cartwright and John McCarthy. Recursive programs as functions in a first order theory. In Proceedings of the International Conference on Mathematical Studies of Information Processing, Kyoto, Japan, 1979.
[Gro99] The Maude Group. The Maude System, 1999. See http://maude.csl.sri.com/.
[HMST95] F.Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A Variable Typed Logic of Effects. Information and Computation, 119(1):55-90, 1995.
[Kle52] Stephen C. Kleene. Introduction to Metamathematics. Van Nostrand, 1952.
[Mas86] I. A. Mason. The Semantics of Destructive Lisp. PhD thesis, Stanford University, 1986. Also available as CSLI Lecture Notes No. 5, Center for the Study of Language and Information, Stanford University.
[McC60] J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, part 1. Comm. A.C.M., 3:184-195, 1960. （中文翻译）
[McC62] John McCarthy. Checking mathematical proofs by computer. In Proceedings Symposium on Recursive Function Theory (1961). American Mathematical Society, 1962.
[McC63] John McCarthy. A Basis for a Mathematical Theory of Computation16. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33-70. North-Holland, Amsterdam, 1963.
[McC80] John McCarthy. Circumscription A Form of Non-Monotonic Reasoning17. Artificial Intelligence, 13:27-39, 1980. Reprinted in [McC90].
[McC81] John McCarthy. History of lisp. In Richard L. Wexelblat, editor, History of programming languages. Academic Press, 1981. Reprinted from Proceedings of the ACM Conference on the History of Programming Languages, Los Angeles, 1977. （中文翻译）
[McC90] John McCarthy. Formalizing Common Sense: Papers by John McCarthy. Ablex Publishing Corporation, 355 Chestnut Street, Norwood, NJ 07648, 1990.
[McC96] John McCarthy. elephant 200018. Technical report, Stanford Formal Reasoning Group, 1996. Available only as http://www-formal.stanford.edu/jmc/elephant.html.
[ML+66] John McCarthy, Michael Levin, et al. LISP 1.5 Programmers Manual. MIT, 1966.
[Wil97] Wilson97. Cars and their enemies. Commentary, pages 1723, July 1997.
[WM78] Daniel Weinreb and David Moon. Lisp machine manual. Technical report, M.I.T. Artificial Intelligence Laboratory, 1978.

/@steam.stanford.edu:/u/ftp/jmc/lisp20th.tex: begun Mon Feb 1 17:36:27 1999, latexed March 22, 1999 at 5:09 p.m.

脚注

1 译注：此处 “21 岁” 为本文最初发表的时间，即 1980 年，相较于 LISP 出现的时间的差值。

2 译注：既然 [McC81] 是 81 年才出版的文献，这篇 1980 年发表的文章是怎么引用它的呢？难道那个 “81” 指的是 1881 吗？其实是因为 [McC81] 是 1977 年论文的重印版（见 §6），所以本文可以预知 [McC81] 的存在和它的内容。

3 译注：原文为 “naming functions”，真的是命名函数，虽然我也不知道“命” 的 “名” 在哪里。

4 译注：“在线（on-line）” 类似现如今 Common Lisp 的 REPL 或者 Emacs Lisp 的 ielm ，表示交互式执行 LISP 程序，并回显程序执行结果的工具。

5 原文注释：1999 年注：Prolog 的想法类似于 Microplanner 的子集。但是 Prolog 经过了系统的设计，因此幸存下来，而 Microplanner 则没有。 Prolog 的关键永久思想是，逻辑的某个子集（Horn 子句）可以作为进行回溯搜索的程序执行。在我看来，这一发现与 Lisp 背后的想法一样具有永久的重要性。

6 原文注释：1999: 只有标准化发生了。

7 原文注释：1999 年：1981 年的想法已与其他想法（例如关于言语行为（speech act）的想法）相结合，并进行了详细阐述。参见 [McC96]。该论文提到的 Elephant 想法是通过允许直接引用过去来避免数据结构。

8 原文注释：1999 年：那本教科书没有出现，主要是因为作者之间对最合适的证明形式存在分歧。

9 原文注释：1999 年：FOL 在 Lisp 课程中被 Jussi Ketonen 的 EKL 证明器接替。本文设想的集成 LISP 系统尚未实现。

10 原文注释：1999 年：Shankar 在教授该课程时使用了 NQTHM（又名 Boyer-Moore 证明器）。该证明器旨在使用归纳法来证明无缺 Lisp 函数（total function）的性质。使用逻辑的 Eval 函数，以及用 S-表达式表示的函数定义，也可以证明缺漏函数（partial function）的属性。NQTHM 已经发展为 ACL2，它支持 Common Lisp 的大型应用子集，并且几乎完全在该子集中进行编程。[见 http://www.cs.utexas.edu/users/moore/acl2/acl2doc.html]（译注：链接挂了，新的链接是 https://www.cs.utexas.edu/~moore/acl2/）

11 原文注释：1999 年：Ian Mason 的论文 [Mas86] 给出了一些推理一阶逻辑 Lisp 的原则，包括 rplaca 和 rplacd。

12 原文注释：1999 年：也许情况仍然如此。

13 原文注释：1999: Mason 和 Talcott [HMST95] 研制了一套推理类似 Lisp-Scheme-ML 程序的逻辑，这种程序里有函数和可变的数据结构。在可变数据方面，这套逻辑有一个相对完备的公理化原语集。同时，这套逻辑还包含许多用于证明程序属性的归纳原则。

14 原文注释：1999 年：一个例子是 Maude [Gro99、CDE+98、Wil97]，这是一种基于重写逻辑（Rewriting Logic）的语言。在 Maude 中，动作和效果以声明性方式表达，并且使用反射能力，可以在 Maude 中表示、推理、修改和执行 Maude 程序。

15 原文注释：1999: 我在这里感谢 Carolyn Talcott 额外提供的参考资料。

16 原文注释：http://www-formal.stanford.edu/jmc/basis.html

17 原文注释：http://www-formal.stanford.edu/jmc/circumscription.html

18 原文注释：http://www-formal.stanford.edu/jmc/elephant.html

4 个赞
2

所以40多年过去了，谜团还是谜团，并没有什么答案。

作者预言的比lisp更高级的语言，什么文本与程序不对应，用户编写的文本将更像是对目标的描述…而非程序本身，这些感觉是在讲AI，写代码应该是现在AI能做得最好的一件事了

3

过度解读了，实际上这个章节的概念早就被 Haskell 啥的函数式语言实现了

5.1 对应 Haskell 的惰性求值，5.2 有 Cedille， 5.3 的 hashcons ACL2 就在用，5.4 就是声明式编程，比如 Prolog，当然你说是AI也没错，70年代的AI罢了

顺带给译者 @hauka 提个意见，hashcons 是专有名词，不要拆开来翻译

4

这就是皮亚诺数字吧？用函数模拟出自然数后就可以模拟出加减乘除、数组，以及if/true/false等。问题是，按理说，速度应该会非常慢。

5

Church Scott encoding 不止能定义数字，还能定义所有的 inductive datatype

这类编码的意义正是因为只有纯 lambda calculus 就能定义数据类型，不用额外引入基础数据类型，这样的情况才能享受到比如parallel interaction net 的性能优势

6

感谢感谢！