目录
- 概述
- 1. 引子
- 2. 言语行为与抽象施为句
- 3. 引用过去的情况
- 4. Elephant 2000 程序的结构
- 5. 程序示例
- 6. 抽象对象
- 7. 实现方式
- 8. Elephant 2000 程序的规范制定与验证
- 9. 意向性的层次
- 10. 何为直截了当
- 11. 与人工智能的关联
- 12. 应用领域
- 13. Algol 48 和 Algol 50
- 14. 作为数理逻辑句子的 Elephant 程序
- 15. 笔记
- 16. 致谢
- 17. 参考文献
本文描述了一种名叫 Elephant 2000 的编程语言，它几乎就是 LISP 的反面：
-
LISP 用一种数据结构（S-表达式）描述所有数据，而 Elephant 里一种数据结构也没有。
-
LISP 可以说是 “列表处理” 所自然产生的编程语言；Elephant 2000 则充满了 “人造” 感。
-
LISP 基于一种简洁的数学理论——λ 演算。而 Elephant 基于所谓 “言语行为”（speech act），类似于我们人类所说的自然语言，当然比数学要复杂得多。
-
LISP 开枝散叶，衍生出各种方言。而 Elephant 就连相关讨论都很难找到，我找到的唯一一篇是 http://lambda-the-ultimate.org/node/3180。
-
LISP 诞生的直接目的是处理列表（因为它的名字就来源于 LISt Processor）。LISP 也确实做到了，因为程序本身就是列表，对程序操作的需求促使程序员研发处理列表的工具。Elephant 诞生的直接目的是 “像说话一样编程”，为此需要记住程序产生的所有数据 —— 举个火车站检票口的例子，判断某位旅客能否上站台，我们可以写：
如果这位旅客买了票，并且没有退票，那么开闸放行。
会有人这么说话？“退票” 应该是一个动作，这个动作发生后 “买了票” 的状态就会消失。然而 “买了票” 这个状态一旦出现就不可能消失了，因为 Elephant 不会忘记。“忘记” 凭什么不算人类的能力呢？
这篇文章的标题并没有按照原文翻译。因为原文标题是《基于言语行为的编程语言》（ A Programming Language Based on Speech Acts ），我认为 “言语行为” 这种玄之又玄的玩意儿不该出现在标题里 —— McCarthy 自己都花了一章才解释清楚什么是 “言语行为”（speech act），出现在标题里没人看得懂。所以我换了个可能不太严谨，但是至少能看得懂的标题。
另外，这篇文章里关于飞机的例子我全给换成火车了。因为美国飞机是远距离交通工具，国内这个领域用火车更多。而且我喜欢火车。看到 “火车” 这两个字我就想到两米远处轮轨相撞声、百米开外清脆电笛声，铁道两旁杂草约没过脚踝，我就站在那里，清风吹过脸颊。从头皮至脚底，每一寸皮肤、每一寸肌肉逐步放松，思绪风般飘散。
咳咳，跑题了，总之接下来是这篇论文的翻译：
我想我所说，我说我所想。
大象绝对可信，100% 的可信！
并且，
大象不会忘却！
概述
Elephant1 2000 是一种尚未实现的编程语言，旨在编写和校验与人类交互的程序（比如翻译），也可以和其它组织的程序相交互（比如交换电子数据）。
- 交互的输入和输出使用一种 I-O 语言（I-O language），其中的语句是有意义的言语行为（speech act），可以分为问题（question）、回答（answer）、建议（offer）、接受（acceptance）、声明2、请求（request）、许可（permission）以及承诺（promise）八种。
- 可以定义程序的缺漏正确性（partial correctness）3，表现为正规的言语行为。“回答” 应该真实可信（truthful）、直截了当（responsive）。“承诺” 应该记下来。
- Elephant 程序不需要数据结构，因为可以直接使用 “过去”。因此我们可以写 “如果某位客户买了张火车票，并且没有退票，那么他预定了这趟火车。”
- Elephant 程序本身可以描述为数理逻辑的句子（sentence），后者的外延属性直接遵从前者的表示，而不需要涉及编程理论和 Hoare 逻辑之类的东西。
- 和外部世界交互的非平凡 Elephant 程序既拥有 输入输出规范（input-output specification） ，也拥有 功能说明书（accomplishment specification） ，后者描述了程序在外部世界中会完成（accomplish）的行为。用哲学黑话讲，它们分别是 行事行为（illocutionary act） 和 取效行为（perlocutionary act）4的泛化。
- 业务程序承担自己拥有的义务（obligation），以此交换得到其它实体承担的义务，进而满足主人的要求。义务交换方式可以算是 Elephant 程序的要求之一，但是这个也可以用数理逻辑的句子表示。
- 人类的言语行为需要智能（intelligence）。Elephant 2000 位于人工智能的边界线上，但是这篇文章主要聚焦于不涉及 AI 的用法。
1. 引子
这篇文章受到了一场演讲的刺激，那场演讲的名字是 “新世纪编程语言”（Programming languages of the year 2000），我觉得野心还是太小了。
“编程语言需要更像自然语言” 这句话已经听了很久了，但是到底是哪些特性至今还没有搞清楚，而且过去 20 年也没提出什么重要概念。不过很明显，光是表面的自然语言语法并没有太大作用；比如 COBOL 就不算什么重要进步。
这篇文章提取了自然语言的一些特性，用于编程语言。这篇文章还提出了几种描述说明书的方法，这样就更容易确保说明书写得正确了。作为上述特征的载体，我们提出编程语言 Elephant 2000。有些特性还没有良定义，所以没有写进程序示例。
-
与人类和其它程序交流时，Elephant 程序会使用所谓 “Elephant I-O 语言” 的句子。这些句子一部分由 Elephant 语言定义，另一部分则由程序自己隐式定义。因此 Elephant 输入输出包含 —— 当然 I-O 语言也会区分—— 请求、问题、建议、接受建议、许可、回答问题 以及其它关于事实的断言（assertion）。上述行为是输入输出共有的，输出除此之外还包括承诺和 自我承诺（commitment） 。
-
Elephant 程序的正确性部分来自输入输出的含义。给定一个 Elephant 程序，我们应该能问它有没有完成请求，有没有真实可信、直截了当地回答问题，有没有受到什么建议，有没有完成指定自我承诺，有没有权限做它想要做的事。上述正确性条件中有些是内在的（intrinsic），因为它们由程序文本定义。要想用数理逻辑的句子表达这些内在条件，我们需要形式化地描述 “完成自我承诺”（以及其它动作）是什么意思。不需要完全对应人类行为或者社会风俗；只要对程序正确性有用，就算跟人类行为仅仅比较像也没关系。这些正确性条件和现有编程语言有点像，但是前者是语义上的，而后者是语法上的。
比方说，如果程序 “承诺” 要给某人做什么事，与 Searle (1969) 的想法相反，程序无需相信履行该承诺会对那个人有好处。实际上很多做出承诺的程序根本没相信过任何事。我们希望只要有程序文本，就能自动生成描述内在正确性的数理逻辑句子。因此，若程序把特定的一些输出用来回答问题，那么就可以从该程序的文本中推断出几个数理逻辑句子，进而断言（assert）答案真实可信。
-
Elephant 程序无需数据结构，因为程序可以直接使用过去的事件和状态。 Elephant 解释器会维护事件历史的列表，而编译器则会在目标语言中构建所需的各类数据结构，记录必要信息，从而使得编译后的程序能按照源程序指定的方式运行。但是要是完全省去数据结构的话，好像就不太方便了。
-
Elephant 程序本身就是数理逻辑的句子（或者说是逻辑句子的语法糖）。这个句子，再加上程序作用领域的理论，推导出了程序的外延正确性性质。因此不需要什么 “程序逻辑”（logic of programs）。任何语法糖都应该能通过逐语句的转换反转回来，也就是还原原本的逻辑形式。
-
Elephant 程序执行的请求、许可还有承诺这些行为，在哲学界和语言学界叫做 言语行为 。其核心观点在于，有时 “说话” 并不是陈述，而是行为。一个典型例子就是承诺：作出承诺就会产生履行承诺的 义务 ，因此 “承诺” 并不单纯表达行事意图。出于研究目的，我们暂时忽略 义务 所涉及的哲学复杂性，仅关注程序是否履行了承诺，而无需纠结于程序是否 “有义务” 履行。
用传统哲学术语讲，Elephant 程序的一部分输出是 “施为句”（performative sentences, 简称 performative）。其实，Elephant 2000 设计出来就是为了让程序使用施为句。然而，随着相关理念的发展，我们发现有必要偏离 J. L. Austin (1962) 和 John Searle (1969) 所探讨的言语行为概念。用 Daniel Dennett (1971) 的视角思考言语行为，会得出不同于传统的见解。现在我们使用 “抽象施为句”（abstract performatives）这一术语，囊括了一些纯粹内部行为（例如自我承诺）。这些行为虽然没必要输出，但是程序的正确性依赖于它们的履行。为了让程序使用言语行为，需要从这个视角观察，使用更加具体的方式，而这一过程往往会为言语行为所引发的哲学问题带来新的解读。
需要注意的是，大多数情况下不需要用 “诚实”（honest）、“听话”（obedient）或 “可信”（faithful）等术语评价程序的道德，当然这篇论文也不会用。不过要是这些概念比较有用，那么我们可以找到它们的对应的抽象含义，然后融入研究。目前的哲学探索已经产生了对我们研究目标有价值的理念，有一部分是因为程序与别人的程序交互时，必须执行类似言语行为的操作；而这些程序中需要验证的输入输出规范和功能说明书，往往与 Austin 所说的 “言语行为的顺利实施”（happy performance of the speech acts）相对应。
(McCarthy 1979a) 一文探讨了在何种条件下，可以将信念（belief）、欲望（desire）、意图（intention）及其他心理属性赋予给计算机程序。研究发现，有些程序说明书的恰当表述需要借助这些心理属性的归属，而另一些则无需如此。
赋予程序直接使用 “过去” 的能力，还可能使程序的修改更为简便 —— 因为程序可直接引用过往事件（例如输入与输出），而非通过数据结构间接指代（如果要用数据结构，那就要研究、理解数据结构的设计）。因为直接指代过去是自然语言的典型特征，所以我们认为这一特性在编程语言中同样会有实用价值。
-
言语行为理论区分了所谓 行事行为 和 取效行为 —— 前者如告知某人某事，后者如使某人信服某事。这一区分同样可以应用于言语输入输出。例如，输入层面存在 “听到” 与 “获知” 的差异，类似于输出层面上 “告知” 与 “说服” 的差异。
供人类执行的流程通常会明确指定取效行为。例如，教导主任可能会告诉教师：“周三让你的学生来考试。” 然而要在程序中纳入取效行为，程序必须拥有用于完成目标的丰富资源，以至于可以直接在程序里描述目标，而非能实现该目标的具体操作。因此，取效行为更可能出现在具有意向性的程序里 —— 例如具备信念、且达到一定人工智能水平的程序。
虽然取效行为是不能纳入程序了，但给程序写点输入输出规范和功能说明书还是值得的。它们分别对应行事行为和取效行为。例如，列车调度程序可根据输入输出之间的关系制定，这便是输入输出规范，其验证仅涉及编程语言的语义。但我们的最终目标是明确并验证该程序能够防止列车相撞，这属于功能说明书。要证明程序符合功能说明书，必须对以下几方面做出假设：世界的客观情况、世界向程序提供的信息、程序行为产生的影响，以及程序自身的相关事实。与言语行为顺利实施所对应的内在规格说明不同，这些规格说明属于外在规格说明。
编写同一个程序的输入输出规范和功能说明书，并建立二者间的关联，往往具有重要价值。这是因为假如如此，那么给定一个符合指定输入输出规范的程序，我们总是可以借助关于世界的公理化理论，严谨证明它符合指定的功能说明书。二者对物理世界事实的依赖可能会让部分人感到不安。隔壁应用数学领域同样需要证明物理世界的形式化理论，和这些证明的问题相比，为这类公理化理论提供合理性证明不算多大的问题。我们始终将生命托付于列车设计中所运用的物理理论，不也没事？
-
Elephant 最显然的应用场景是业务处理程序，以及以更通用的方式访问数据库的程序 —— 这类访问方式不仅限于响应查询和执行更新操作。对于与其他组织的程序进行业务通信的程序而言，抽象施为句同样具有重要意义。 McCarthy (1982) 提出了一种 “通用商业通信语言”（Common Business Communication Language）。
本文属于探索性研究，我们目前尚无法断言，2000 年所有前沿编程语言都会纳入 “抽象施为句” 这一概念。我们期望，使用施为句的程序将更易于编写、理解、调试、修改，且最重要的是，更易于验证。而制定一套请求、承诺等行为的标准词汇表，将对此大有裨益。
2. 言语行为与抽象施为句
哲学家和语言学家大多从自然主义的角度研究言语行为，也就是说，他们关注的是 “人类会执行哪些类型的言语行为”。即便他们打算从抽象角度分析，依我看分析结果也还是过于贴近人类行为。而我们的思路是：在交互场景中，哪些类型的言语行为是有用的？交互的本质源于不同主体具有不同的目标、知识和能力，某个主体要实现自身目标，就必须与其他主体进行交互。所需交互的本质，决定了需要用到的言语行为类型。很多关于 “需要哪些言语行为” 的结论，与主体是人类还是机器无关。
通常，只要程序拥有少量几种言语行为，就能顺利运行，即便这些言语行为不具备 Searle (1969) 等哲学家赋予人类言语行为的所有属性。
以下是我们计划为程序提供的几类言语行为：
-
断言（Assertions）：断言的正确性条件之一是 “可信（truthful）”。当然，要证明断言真的可信，就需要基于程序作用领域的公理。还有一个相对宽松的正确性条件，“诚实（sincere）”，这就需要一套关于程序信念的理论。如果证明陈述是否可信（或者诚实）难度过大，程序员可以选择不纳入这些正确性条件，让用户凭借直觉来判断。
-
问题（Questions）：用户可以向程序提问，程序也可以向用户提问。
-
回答（Answers to questions）：回答本质上是断言，需要诚实且可信，同时还必须直截了当。如果问题需要回答 “是 / 否”，那么 “直截了当”的界定会比较简单。但即便如此，也可能会遇到一些复杂情况，比如 Grice 在其论文集 (Grice 1989) 中讨论的那些问题。对于某些问题，恰当的回答可能是 “不知道啊”。还可能有些问题本身就有错误的假设（而回答者知道这一点），这时从字面上直接回答就可能不合适。
（接下来一段有两个版本。HTML 版本是这样的：
假如小王问小明的电话号码是什么，如果回答 “小明的电话号码，就是他妻子的丈夫的电话号码”，这种回答就不算直截了当。如果想要直截了当的回答，我们可以要求回答必须是一串数字，而非求值成一串数字的表达式。这样的范围有可能太小了，毕竟有些情况下回答 “小明的电话号就是他妻子的电话号” 也算是直截了当。另一种方法在 §10 中描述，这一整节都在讲 “何为直截了当”。
在 PDF 版本中，这段不一样，见括号外的下一段。）
假设有人问张三的电话号码，如果回答 “张三的电话号码，就是他妻子的丈夫的电话号码”，这种回答就是不算直截了当。说明书需要表达这样的要求：直截了当的回答必须是一串数字，而不能只是求值为一串数字的表达式。
Elephant 程序的断言和提问，会涉及一些用户与程序共用的谓词符号和函数符号。这些符号共同构成了程序的 I-O 语言，并可以通过一阶逻辑工具进行组合。如果有需要，也可以为其配备自然语言前端。程序的 I-O 语言会在该程序的手册中说明。不过，有一些谓词和函数是所有 Elephant 2000 程序通用的，还有很多符号与日常语言中的词汇非常接近，用户无需专门学习就能使用。
-
自我承诺与承诺（Commitments and promises）： 简单承诺 包含两部分：一是内部的 “自我承诺”（即承诺做某事，也就是让某个语句为真），二是对外输出的 “存在该自我承诺” 的断言。程序正确性的要求这类断言的真实性。
但 Austin（1962）指出，说出承诺这一行为本身，会在公共层面产生一种义务。这一点对计算机程序也很重要，因为程序做出的承诺可能会让运行该程序的机构承担某种义务（甚至是法律义务）。在某些情况下，规范只需关注 “兑现自我承诺” 即可；但在另一些情况下，规范必须考虑承诺的公共属性。
自我承诺是 抽象施为句 的一种，当然还有其他类型的抽象施为句。它之所以 “抽象”，是因为其内容不依赖于表达方式，甚至完全不需要对外表达。
我们还提议用抽象的方式处理外部义务。比如，可以引入 “1 类义务” 和“2 类义务” 的概念。我们可以这样规定：购票程序在完成一次购票时，会产生 1 类义务，同时会让运行该程序的机构承担 2 类义务。至于 1 类义务和 2 类义务具体是什么（比如它们涉及哪些法律要求、与其他考量冲突时该如何处理、未履行义务会有什么后果），则需要由制度（比如法律）来定义。这类义务是通过社会、商业或法律途径确立的，而非由哲学家或心理学家发现的。
3. 引用过去的情况
类似 Algol 的编程语言通过变量、数组和其他数据结构来引用过去的情况，而 Elephant 2000 程序可以直接引用过去的情况。从某个角度来看，两者差异不算特别大 —— 因为 Elephant 程序也可以被视为拥有虚拟的 “历史列表”（或称为“日志”）。程序执行时会产生 “虚拟副作用”：将该行为记录到历史列表中。说历史列表是 “虚拟” 的，是因为编译后的程序可能不会真的采用这种形式，可能会使用传统的数组，并且不会记录那些确定不会被引用的信息。不过，我们提议提供的 “引用过去情况” 的方式，在语义上更接近人类在自然语言中引用过去的方式，而不只是通过索引变量访问列表。
我们将 “过去” 视为一段历史 —— 它是一个关于时间的函数，记录了已经发生的事件和状态。引用过去的情况，本质上就是调用这个历史函数。以下是一些例子：
- 最简单的历史函数应用，是获取某个参数在特定时间的值，比如 “1991 年 1 月 5 日某个人的账户余额”。但实际中，引用过去的情况很少这么简单。
- 其次，我们可能会关注某个事件发生的时间，比如 “某个人的出生日期”。
- 稍复杂一些的情况，是获取某个事件首次或末次发生的时间，或者某个参数首次或末次达到某个值的时间，比如 “某个人最近一次银行账户透支的时间”。
- 更一般地，我们可能会关注某个命题为真的 “唯一时间”“首次时间” 或“末次时间”。
- 再进一步，我们可能会关注以时间为值的 “全局历史函数”，比如 “平均时间”。
- 某个人是否预定了某趟火车，取决于他是否已经买过票，以及后续有没有退票。
- 对于支持子程序的编程语言，其解释器可以不用显式提及栈结构。比如，程序可以这样表述：“子程序返回时，会回到 ‘调用入口语句’ 的下一条语句；同时，返回时变量的值需与子程序调用前保持一致。” 目前还不确定“不显式提及栈结构” 好不好用，但这种方式可能有一个优势：与指定显式数据结构相比，编译器在选择 “如何存储必要信息” 时会更灵活。
- 计算小时工一周的工资，需要先统计他的工作时间段长度，再将每个时间段的长度乘以该时间段对应的时薪（比如夜班时薪更高），最后将所有结果相加。这个例子在本体论（ontological）层面比之前的例子更复杂，因为它需要将 “时间段集合” 作为对象来处理，而不只是处理单个时间点。
为了让 Elephant 语言能实现上述功能，我们将设计一套表达 “历史函数” 的方式，既要足够通用以减少对数据结构的依赖，又要确保在计算上可行。
4. Elephant 2000 程序的结构
我们将通过 “解释器” 来描述 Elephant 2000 的简化版本。编译后的程序需保持相同的输入输出行为，但目标程序会使用常规数据结构，而非直接引用过去的情况。
我们假设程序每次仅接收一个输入，这一功能由运行时系统实现。同时，不符合要求格式的输入会被自动拒绝，因此 Elephant 程序本身无需处理这类输入。
程序在每次收到输入后都会做出响应，从这个角度看，它可以被视为一个 “刺激—— 响应” 机器。但在决定如何响应时，程序可以查看之前所有的输入和响应记录（即完整的历史记录）。此外，程序还可能会引用一个永久性数据库。
5. 程序示例
5.1. 示例一
以下是一个火车购票程序，附带了符号说明。其中，粗体标识符是 Elephant 语言内置的；斜体标识符则是该特定程序自定义的。
\mathbf{accept.request} ：Elephant 语言内置的动作，表示 “执行其后代码所描述的操作”。
\mathbf{answer.query} ：Elephant 语言内置的动作，表示 “回答其后代码所描述的查询”。
admit(psgr, trn) ：该程序自定义的动作，意为 “允许乘客 psgr 坐上 trn 次火车”。它有两种可能的解释：(1) 告知检票员放行该乘客（行事行为）；(2) 使得乘客登上火车（取效行为）。
\mathbf{commitment} ：Elephant 语言内置的函数，接收 “未来动作” 作为参数，生成一个抽象对象，我们把这种对象叫做 “自我承诺”。
内部动作 \mathbf{make} 、 \mathbf{cancel} ，以及谓词 \mathbf{exists} ，均作用于自我承诺。其中， \mathbf{make} 、 \mathbf{exists} 、 \mathbf{cancel} 是 Elephant 语言的内置成分，其含义和公理定义不依赖于具体的抽象对象（无论这些对象是用于创建、验证还是销毁）。需要注意的是，兑现自我承诺所涉及的 “可信度” 这一概念，不一定适用于其他抽象实体。
程序 1（购票）：
在 Elephant 2000 中，运算默认是右结合的，因此上述语句等价于：
程序 2（查询车票）：
程序 3（退票）：
程序 4（发车时检票并放行）：
（注：符号 “$∧$” 表示 “并且”）
程序 5（定义 “火车满员”）：
（译注：card 表示获取集合元素的数量， capacity\ trn 表示 “火车 $trn$” 的载客量）
即便对于这个简单的预订程序，区分 “输入输出规范” 和 “功能说明书” 也很有必要 —— 这一区分体现在对 admit(psgr, trn) 的解释上。若将其解释为 “下达检票通过指令”，则属于行事行为；若解释为 “确保乘客真的上了火车”，则属于取效行为。该程序的输入输出规范是：“下达的检票通过指令数量，不得超过该车次的载客容量”。而 “列车实际能容纳的乘客数不超过其容量”，则是一个外部事实（不属于程序本身的规范）。
5.2. 示例二
类似的逻辑也适用于简易列车调度程序。
该程序的功能包括：接收列车进站请求、感知列车位置、发布指令（如 “2 道发车”“降弓运行”“信号机调成绿色”）。其输入输出规范仅与 “感知信息”“输入”“输出” 相关，例如：“只要没有感知到前一列车已经完全驶离站台，就不得允许下一列车进站”。验证这类规范，只需依赖程序本身的事实即可。
该程序的功能说明书则要求：“列车需抵达站台，且在保证安全的前提下尽可能高效”。验证这类规范，不仅需要依赖程序本身的事实，还需要假设 “程序的感知信息准确”“司机能按指令行动”。
（原文注：英文中 “perceive” 一词存在歧义。《韦伯斯特大学词典》将其定义为“意识到”，这意味着如果 “感知到列车已驶离站台”，则列车确实已驶离站台。但我问了几个同事，大多数人认为 “感知到某件事” 不代表 “这件事实际发生”。因此，为明确含义，我们会在该词前添加副词修饰，如 “准确感知”“可能感知”。）
列车调度领域的专家可以验证：若该程序符合输入输出规范，则它也会符合功能说明书。“输入输出规范” 和 “功能说明书” 的概念，适用于所有与外部世界交互的程序（不仅限于 Elephant 程序）。但我们认为，对于 Elephant 程序而言，二者的编写和验证会更简单。
6. 抽象对象
以购票系统为例：“什么是车票？” 这个问题本身不够恰当。更合适的问法或许是：“为了设计 Elephant 购票程序，我们应该如何定义车票？” 但即便如此，也显得过于绝对。真正关键的问题是：“我们需要让程序对 ‘车票’ 执行哪些操作？” 答案是 “越少越好”—— 只需定义足够的内容，让程序能实现 “购票、退票、查询车票、检票” 即可。定义过多内容，不仅会不必要地限制程序的实现方式，还会增加程序修改所需的知识成本。
那么，我们到底需要定义什么呢？（译注：原文到此结束，没有后续。）
7. 实现方式
我们计划为 Elephant 2000 设计两种实现方式：解释型和编译型。
7.1 解释型实现
解释型实现仅依赖一种简单的数据结构 —— “事件历史列表”。输入必然会作为事件存入该列表；从原理上讲，这是解释型实现的唯一核心需求。但将程序执行的动作（包括外部动作和内部动作）也存入历史列表，能帮助解释器避免重复某些计算。
解释器会实时接收输入，并根据规则判断每个输入的处理方式。目前设想的 Elephant 2000 版本，仅支持特定类型的请求（如创建预订、取消预订），并假设这些请求按一定顺序到达。输入的同步处理，以及不符合程序语句格式的输入的拒绝，均由程序外部的运行时系统完成。每次处理输入时，解释器会显式地将“事件模式” 与 “历史事件列表” 进行匹配。类似 Prolog 的简单匹配机制可能就足以满足这一需求。
因此，解释型实现的运行速度可能较慢，但对于许多场景（如小型购票系统、简单查询程序）而言，其性能已经足够。
7.2 编译型实现
Elephant 2000 编译器会将程序翻译成常规编程语言（如 Common Lisp 或 C）。目标程序会包含数据结构，程序通过引用这些结构来决定 “如何处理输入”，并根据执行的动作更新结构内容。在完整的编译过程中，目标程序不会包含显式的“历史列表”—— 历史信息会被封装在数据结构中。
8. Elephant 2000 程序的规范制定与验证
由于 Elephant 2000 程序本质上是 “逻辑语句的语法糖版本”，其属性可由以下三部分共同推导得出：表示程序本身的逻辑语句；Elephant 2000 的内置公理；程序数据领域的理论（若有）。从这一点来看，Elephant 与后文将介绍的 Algol 48、Algol 50 有相似之处。
（未完待续）（译注：原文如此）
9. 意向性的层次
我们讨论言语行为相关的哲学研究，主要有两个目的：第一，探索计算机语言对言语行为的应用，能从哲学家的大量研究中借鉴哪些内容；第二，从 “计算机如何执行言语行为” 的角度，为哲学问题提供新的视角。这两个目的紧密相关，因此我们会将它们结合讨论，具体观点如下：
-
哲学家将言语行为视为 “待研究的自然现象”，但他们不倾向于从人类学或语言学角度分析，而是聚焦于 “言语行为能实现什么功能”，以此挖掘其本质特征。这种研究思路，比人类学或语言学研究更贴近计算机科学和人工智能领域的需求。
-
我对言语行为的看法是：在 常识信息场景 中，言语行为是必要的 ——人们通过交互实现目标，就处于这类场景中。该场景的核心特征，与 “参与者是人类” 这一事实无关。无论是火星人还是机器人，即使知识和目标与人类不同，都需要言语行为，且其中许多类型会与人类的言语行为具有相似特征。
-
本文的核心观点是：在设计 “与人交互” 或 “与其他程序交互” 的计算机系统时，言语行为具有重要价值。
-
但并非哲学家赋予言语行为的所有特征，都对我们的设计有用。具体需要哪些特征，取决于设计目标。
-
除了人类社会中常见的言语行为，我们还可以根据需求 “发明” 新的言语行为。实际上人类社会中就经常会发明言语行为，比如本文讨论的购票系统就是一个例子。
-
某一特定类型的言语行为，可视为 (McCarthy 1979a) 中所说的 “近似理论” 中的实体。因此精确定义（如 “精确界定购票是什么”）往往是徒劳的。相反，我们会使用非单调公理 (McCarthy 1986) 来部分描述它们的特征。
-
将言语行为视为 “程序语句的执行事件”，这一视角或许对哲学家也有启发。
-
有些施为句不产生外部输出，因此不属于严格意义上的言语行为，但它们同样有用。最典型的例子就是自我承诺：程序创建一个自我承诺后，其正确性就要求 “兑现该自我承诺”。
-
我们与哲学家共同关注的一个核心问题是：“要成功执行某类言语行为，必须满足哪些条件？”
-
本文在一定程度上涉及 John Searle（1984）与人工智能界的争论 ——“计算机是否真的能拥有信念和知识”。根据我对 Searle 观点的理解，其逻辑延伸会得出 “计算机无法真正做出承诺” 的结论。但我们的观点是： Elephant 2000 程序能像人类一样，真正执行某些类型的言语行为。 Elephant 2000 程序的言语行为与人类言语行为的差异，类似于不同人类之间言语行为的差异。我们预计，在很长一段时间内，编程界关注的言语行为类型，会比 Searle 讨论的类型更有限。但人类在特定制度场景下的言语行为，同样具有局限性。例如，“提供车票” 这一行为，通常不涉及“认为这张票对接收方有益” 的主观判断。
目前尚不清楚这一观点差异会对编程实践产生哪些实际影响。
-
对于非 Elephant 编写的程序，我们也可以 “将其视为 Elephant 程序”来分析 —— 只需将其输入视为提问或请求，输出视为承诺或断言即可。这与 Newell (1982) 提出的 “逻辑层次”，或我 (1979a) 提出的 “为机器赋予心理属性” 的思路类似。
-
Austin 和 Searle 将言语行为分为 行事行为 和 取效行为 。例如，“命令某人做某事” 是行事行为，而 “让某人实际做了某事” 是取效行为。同一句话可能同时涉及两种行为，但取效行为的成功不仅取决于说话者的表述，还取决于其对听话者产生的影响。哲学家承认，要精确区分这两类行为存在困难，但对于 Elephant 而言，区分并不复杂：
- 行事行为的正确性仅与程序状态、输入以及输出有关；
- 取效行为的正确性还需依赖现实世界中的事件。
例如，购票程序的规范，可基于其执行的行事行为（即输入和输出）来制定；而列车调度程序的正确性，则本质上属于取效行为范畴 —— 因为要完整定义其正确性，必须包含 “防止列车相撞” 这一现实结果。
在这一背景下，我们可以突破哲学术语的限制，将 “取效行为” 的概念同时应用于输入和输出：
- 输入层面取效行为的正确性，不仅依赖于输入，而且输入还会反映现实世界的事实（如列车的位置）。
列车调度程序的正确性，不仅依赖于 “输入准确”“司机遵守指令”“火车运行物理规律” 等假设，还依赖于程序本身的逻辑。
10. 何为直截了当
证明回答直截了当（而非仅要求真实可信），会涉及意向性和/或元数学相关的问题。
例如，在派对上我问某人：“那边那人是谁？” 他回答：“是小李”—— 这通常会被认为是直截了当的回答。但如果我问：“小李是谁？” 他回答：“是那边那人”——这也通常被认为是直截了当的。这一例子说明，“直截了当” 的通用定义非常复杂，因此我们会先聚焦于一些特殊场景来分析。
要 “表述并证明回答（或其他陈述）直截了当”，所需的逻辑工具，比 “证明回答真实可信” 所需的工具复杂得多。研究发现，(McCarthy 1979b) 中提出的逻辑工具，恰好适用于解决这一问题 —— 该工具使用不同符号来区分 “对象” 和“对象的概念”。
“直截了当的回答” 的定义是：提问者在收到回答后，能够 知道 问题的答案。例如，假如小王问小明的电话号码是什么，如果回答 “小明的电话号码，就是他妻子的丈夫的电话号码”，这种回答就不算直截了当 —— 因为这个回答无法让小王知道小明的电话号码。借助 (McCarthy 1979b) 的工具，我们可以这样定义“知晓电话号码”：
其中，函数 Concept1 将 “电话号码” 映射为 “该号码的标准概念”—— 持有这一概念的人，能够根据它拨出电话号码。 Concept1 的取值范围，需要通过公理进行适当定义。
11. 与人工智能的关联
要充分利用言语行为，需要达到人类水平的智能。人工智能领域虽已取得进展，且基于这些进展形成了实用的专家系统技术，但 “人类水平的智能” 仍遥不可及。因此，关键在于分析 “言语行为的各类应用场景”，并判断每个场景需要多少智能。
本文的一个核心主张是：许多言语行为的应用，并不需要人类的大部分智力能力。我们进一步希望，Elephant 2000 能允许设计者根据具体系统的需求，灵活选用“可行水平的人工智能技术”。同时，还需注意确保程序对 “与其交互的其他程序”的智能要求不会过高。
（未完待续）（译注：原文如此）
12. 应用领域
办公室工作中，有很大一部分涉及 “与外部人员或机构的沟通”—— 这些外部主体的流程不受同一机构的管控。要让计算机充分提升办公效率，就必须将这类沟通流程计算机化。而 “假设所有通信进程是作为一个整体设计的” 分布式处理方法，无法实现这一目标。
这类沟通的计算机化，在以下场景中最容易实现：沟通内容完全标准化，且其中一方有权力规定沟通格式。例如，20 世纪 50 年代，美国国税局（IRS）规定了“工资和扣除项报告” 的磁带格式，要求相关机构按该格式提交数据。
电子数据交换（EDI）的早期应用，主要集中在 “大型制造商与其供应商” 之间—— 制造商有权规定数据交换的格式。这种模式在 “供应商仅服务这一家制造商”的场景下效果最佳。
下一步的发展，体现在 X12 等标准的出现 —— 它们为固定类型的商业文档（如发票）定义了标准电子格式。X12 格式通常包含固定的 “字段”，可在其中填入数字（如数量、价格）或标签（如人名、地名、物品名）。
(McCarthy 1982) 提出了 “通用商业通信语言”（Common Business Communication Language, CBCL）的构想，旨在为商业信息交互提供一套专用语言。该语言的信息可以包含各种实体的复杂描述，例如价格公式、交货计划、付款计划、设备配置以及合同条款等。该论文设想，企业可以发布电子目录和广告，这些内容能让企业自动被列为某些商品的供应商。寻找商品的优惠价格和合适交货条件的程序，或许能自动与代表卖方的程序进行协商，甚至在自身权限范围内自动下达采购订单。不过，(McCarthy 1982) 并未讨论使用 CBCL 的具体程序。
执行外部通信的程序需要具备几个功能，这些功能与使用言语行为的能力大致对应。它们需要能够提问、回答问题、作出自我承诺以及达成协议。它们还需要能够传达这样的保证：自己所达成的协议会得到所属机构的遵守。要做到这一点，最好借助某种权限体系，从下达采购订单的程序，到决定采购何种物品的程序，再到机构的人类层级体系，逐级向上延伸。
由于这些程序运行起来后就基本没人来维护了，所以必须对它们进行仔细的验证。 Elephant 2000 的特性在这方面很重要，因为它所提供的言语行为形式都有明确的含义。这些程序还需要经常修改，修改者往往不是编写者，而且应尽可能让非程序员也能完成修改。
随着人们拥有更多家用电脑，并越来越多地用它们与企业开展业务，事务处理程序将变得更加重要，而且使用这些程序的人也将不仅仅是运营这些程序的机构的员工。这也会对程序的可验证性和可修改性提出要求。
现有的预订程序存在很多局限性，而使用 Elephant 2000 的特性有助于纠正这些局限性。通常，这些程序甚至不会输出具有长期意义的字符串，只会输出用于更新显示的内容。其他机构的程序很难利用这些显示更新内容，因为为了让显示更美观而对输出进行的修改，可能会使其他程序无法解读这些内容。结果就是，当需要改签火车票时，站务往往需要重新输入乘客姓名，因为无法从显示车票信息的屏幕上获取该姓名。Elephant 的言语行为比字符串更高级，因为言语行为的高层级内容具有独立于应用程序的含义。
13. Algol 48 和 Algol 50
本节是下一节的铺垫。
我们引入 “编程语言” Algol 48 和 Algol 50，以便在更简单的环境中说明 Elephant 2000 将要用到的一些理念。这些理念包括在编程语言中明确使用时间，以及用逻辑语句来表示程序。前者能够直接表达语言的操作语义，后者则无需借助专门的程序理论就能证明程序的属性。程序的属性可以从程序本身以及领域公理中推导出来。
我们使用这些名称，是因为这些语言涵盖了 Algol 60 的部分内容，但只使用了一种数学形式 —— 老式的递归方程 —— 这种形式甚至在编程语言发展之前就已经存在了。我觉得，如果数学家意识到 “编程语言需要不同于机器语言”，他们可能在 20 世纪 50 年代就会创造出这样的编程语言。Algol 48 是 Algol 50 的初步版本，就像 Algol 58 是 Algol 60 的初步版本一样。
来看下面这段 Algol 60 代码片段：
这个程序通过将变量 p 初始化为 0 ，然后不断往其中加 m ，总共 n 次，来计算乘积 mn 。Algol 60 程序的正确性可以表述为：如果程序从 start 处开始执行，最终会到达 done 处，并且此时变量 p 的值等于 mn。不同的程序验证形式体系会以各种方式表述这一断言，而且往往不是完全形式化的。通常，在 loop 标签处添加不变式断言 p = m(n-i) ，我们可以证明该程序的缺漏正确性。注意到变量 i 初始值为 n ，从而可以总会递减到 0 ，这就证明了该程序总会停机。不同的程序验证形式体系会以不同方式呈现这一证明过程。
13.1 Algol 48
在 Algol 48 中，我们将这个算法写成三个时间函数的老式递归方程组，即 p(t) 、 i(t) 和 pc(t) ，其中前两个对应程序中的变量， pc(t) 表示 “程序计数器” 的变化情况。在 1948 年，唯一不常见的想法就是明确使用程序计数器和条件表达式。具体如下：
Algol 48 程序的正确性可以用下面这个数理逻辑的句子来表示：
（译注：这里表示 “蕴含” 的逻辑连词使用了箭头，这是原文 HTML 版本中使用的。但是原文的 PDF 版里使用了 “包含子集”（$⊃$）。）
这个句子可以从表示程序的语句，再加上算术公理，以及数学归纳法公理模式推导出来。不需要专门的程序理论。最简单的证明方法是，在等式 p(t) = m(n-i(t)) 中对 n 使用数学归纳法。
Algol 48 程序的组织方式与 Algol 60 程序有很大不同。也就是说，变量的变化是按变量来分类的，而不是按时间顺序。
13.2 Algol 50
通过具体化变量，Algol 50 允许以这样一种方式编写程序：可以将上面那段 Algol 60 代码视为 Algol 50 程序的语法糖版本。要获取变量 var 的值，我们不写成 var(t) ，而是写成 value(var, ξ(t)) ，其中 ξ 是状态向量，也就是说包含所有变量的值。在上面的程序中，我们会有 value(p, ξ(t)) 、 value(i, ξ(t)) 和 value(pc, ξ(t)) 。
Algol 60 程序中的变量，对应于在上面 Algol 50 的版本中关于时间的函数，而在具有具体化变量的 Algol 50 版本中，则成为不同的常量符号。它们的区别通过 “唯一名称”（unique names）公理表示：
$$i ≠ p ∧ i ≠ pc ∧ p ≠ pc$$
在表述程序时，我们使用 (McCarthy 1963) 和 (McCarthy 和 Painter 1967)中的赋值函数 a(var, value, ξ) 和取值函数 c(var, ξ) 。 a(var, value, ξ) 表示：如果当前状态是 ξ ，给变量 var 赋值为 value 后新的状态为 ξ' ，那么 a(var, value, ξ) 就是这个 ξ' 。 c(var, ξ) 是状态 ξ 下变量 var 的值。
如这些论文中所描述的，函数 a 和 c 满足以下公理：
用下面的函数定义可以简化程序表述。需要注意，这些东西只是函数定义，不是特殊的构造。
对于现在这个程序，我们可以把 start+2 缩写成 loop ，进而我们的程序可以写成：
在 Algol 50 中，条件表达式各子句的结果与 Algol 60 程序的语句一一对应。因此，可以将 Algol 60 程序视为相应 Algol 50 程序的缩写。Algol 60 程序的（操作）语义由表示相应 Algol 50 程序的语句，以及描述数据的公理（现在这种情况下是自然数的皮亚诺公理），这二者共同给出。如果不是因为在 Algol 50 中需要明确使用语句编号，那么从 Algol 60 到 Algol 50 的转换完全可以是局部的（local），即逐语句进行。
如果要把程序片段组合成更大的片段，我们需要首先拼接程序片段的语句，然后在需要的地方添加标签，以实现从一个片段到另一个片段的跳转，最后添加语句确保程序计数器不会重叠。
这个通过累加实现乘法的 Algol 50 程序的正确性可以表示为：
注意我们把所有初始状态都放进了全称量词（$∀$）里。正确性公式的最后一部分表明，这段程序只会改变 p 、 i 和 pc ，而不会改变其它变量。
我们还没有深入研究 Algol 50 的理念，以验证是否能方便地用同样的风格表示 Algol 60 的所有内容，但目前看来没有明显的根本性困难。在处理递归过程时，可以引入栈，但更简洁的方式是不使用栈，而是明确说明，返回后会开始执行相应过程调用后面的那条语句，并且变量会恢复到调用时的值。这需要具备解析过去情况的能力，这也是 Elephant 2000 所需要的。
我们主张使用扩展的 Algol 50 来表达类 Algol 编程语言的操作语义，也就是描述程序执行时发生的事件序列。不过，我们目前的应用只是在更简单的环境中说明 Elephant 需要的一些特性。特别是，要正确处理带有副作用的函数过程调用，需要一个在表达式求值期间能保持值的状态。
Nissim Francez 和 Amir Pnueli（见参考文献）曾将明确的时间用于类似的目的。遗憾的是，他们后来改用了时态逻辑（temporal logic）。虽然某些类型的时态逻辑是可判定的，但时态逻辑太弱，无法表达程序的许多重要属性。
14. 作为数理逻辑句子的 Elephant 程序
本节是本文中最具试探性的部分。目前，我们有两种将 Elephant 程序写成逻辑语句的方法。
第一种方法类似于 Algol 50，基于更新程序状态和世界状态。当然，更新世界状态的函数只有一部分是可以得知的。因此会出现未知函数，而我们对世界的了解将通过对这些函数施加公理来表达。
第二种方法用事件来表达程序，以及我们此时对世界的了解。事件发生的时间由公理确定。我们描述我们断言会发生的事件，并依靠限定（circumscription）来将事件的发生限制在从给定公理中推导出来的范围内。我们先从 Algol 50 式的方法开始。
14.1. 第一种方法
与 Algol 50 一样，在第一种方法中，我们在程序运行时使用状态向量 ξ(t) 来表示程序的状态。程序由 ξ(t + 1) 的公式来表示。由于程序与世界交互，我们还有一个计算机外部世界的状态向量 world(t) 。因为我们无法完全了解世界，所以不能期望用一个公式来表达 world(t+1) ，但证明功能说明书需要基于关于确定 world(t) 如何变化的函数的假设。
我们有：
注意，可能和你预期不同，在两个方程的右边，我们写的是 ξ 和 world ，而不是 ξ(t) 和 world(t) 。这使我们可以让 ξ(t + 1) 和 world(t+1) 依赖于整个过去，而不仅仅是现在。（这也允许方程表达对未来的依赖，尽管这样的方程只有在满足相当严格的条件时才不会出现矛盾。）
我们已经用这种形式编写了部分购票程序，但还不够清晰，暂时无法纳入本文。
14.2. 第二种方法
第二种方法使用单独的函数和谓词，将时间作为参数。在这方面，它类似于 Algol 48。
（译注： \mathbf{holds} 表示 “某时刻某命题成立”， \mathbf{arises} 表示 “某时刻发生了某事件”， \mathbf{outputs} 表示 “某时刻程序输出了指定内容”。）
注意 admit 的参数里有变量 ?seat 。我们可以假设 admit 实际上有很多参数，其中一些有默认值。当遇到 admit(…) 表达式时，要明确哪些参数由该表达式赋值，哪些使用默认值。现在我们根据变量名区分，也可以像 Common Lisp 那样根据实际的命名参数区分。现在这种情况下，从可用座位中分配一个是编译器的事。
这里再给几个示例。
逻辑句子 2（查询车票）：
（译注：这里 \mathbf{confirm} 的意思是 “许可某项操作”， \mathbf{deny} 的意思是 “拒绝” 指定输入）
逻辑句子 3（退票）：
（译注：这里 \mathbf{revoke} 的意思是 “某一时刻某件事无效”）
逻辑句子 4（Elephant 的记忆力）：
不难发现其中 ∃ t' (t' < t ∧ \mathbf{arises}(t, \mathbf{commitment}\ x)) 等价于 \mathbf{exists}(t, \mathbf{commitment}\ x) 。这个逻辑句子的意思就是：如果过去某时刻出现了关于 x 的自我承诺，那么到现在为止它都不是无效的。
逻辑句子 5（检票）：
断言某些输出会发生以及某些命题成立，并不能确定其他输出不会发生。因此上面给出的程序需要通过 “限定” 某些谓词来补充，这些谓词就是 \mathbf{arises}, \mathbf{outputs} 和 \mathbf{revoke}。
15. 笔记
要证明程序会兑现其自我承诺，似乎只需将自我承诺表述为 “确保某个语句为真”，例如 “开闸放乘客进站”。在这种情况下，证明程序会兑现其自我承诺，就是证明 “表达自我承诺的数理逻辑句子可以从表达程序的语句中推导出来”。现在的问题是确定允许哪些类型的语句来表达各种自我承诺。如果自我承诺要对外表达，那么它们必须属于 I-O 语言。
自我承诺有点像规范和说明书，但前者是动态的，也就是说，自我承诺是在程序运行过程中产生的。询问程序在特定状态下有哪些自我承诺是有意义的。实际上，有些程序应该能够回答关于自我承诺的问题。
Elephant 解释器只需将输入与以输入为前提的程序语句进行匹配。然后，它会输出结果、执行操作并断言该语句的其他结论。不需要考虑限定，因为可以把限定看成 “断言只有程序语句中指定的事件才会发生”。这种情况与逻辑编程类似。但是限定 会被 用于证明程序符合其规范，例如兑现其自我承诺。
有一个相关的定理有待精确表述和证明。要使该定理可证明，可能需要对形式体系进行一些修改。
许多人类言语行为都与不断变化的社会制度相关。例如，在决斗习俗盛行的社会中，挑战决斗不仅仅是一种提议，它会使挑战者、被挑战者和社会群体承担特定的义务。决斗的废止，部分是通过有意改变这些制度实现的。计算机程序之间的言语行为交换，往往需要设计新的制度来规定言语行为的效果。例如，商业承诺所产生的外部义务类型，部分由许多州颁布的《统一商法典》来规定。做出自我承诺的程序，其规范必须以某种方式与《统一商法典》之类的法律相对应。一方面，要能够证明（在特定假设下）程序会按照法律要求行事；另一方面，商业言语行为的效果必须定义得足够明确，以便程序能够跟踪自己所承担的义务和他人对自己承担的义务。最简单的情况是跟踪言语行为对应收账款和应付账款的影响。
或许我们需要三个层次的规范：内部规范、输入输出规范和功能说明书。内部规范可能涉及计算某个量，而与是否有输出无关。
程序各部分之间的一些通信也可以有效地视为言语行为。
我们可能需要考虑联合言语行为，例如达成协议。在某些情况下，协议可以被视为提议及其接受。但是，我们可能知道双方达成了协议，却不知道最终是谁提议、谁接受。
似乎 (Searle 和 Vanderveken 1985) 在区分言语行为的成功执行和无缺陷执行方面，比 (Searle 1969) 有所改进。目前还不清楚这些区分是否会在计算机言语行为中发挥作用。或许该书提出的行事行为逻辑，将有助于编写规范和证明程序符合规范。
撰写本文始于一个简单的想法：程序可以做出自我承诺，以及证明程序会兑现这些自我承诺。后来，考虑具有更复杂正确性条件的言语行为变得有趣起来。然而，我们期望在 Elephant 2000 及类似语言的初始应用中，简单的情况将是最有用的。
Dorschel (1989) 提出了指令性言语行为（如命令、承诺和宣告）“顺利” 执行的某些条件。事实证明，我们需要其中一些条件，而不需要另一些。我的意思是，当有人验证 Elephant 程序时，他会希望证明 Dorschel 提出的某些条件得到了满足，而另一些则没有。
例如，Dorschel 提出，承诺的兑现必须以 “做出承诺” 为 “兑现行为” 的原因。 Elephant 程序员在验证其程序时，无需证明承诺会因为被做出而得到兑现。只要证明承诺会得到兑现就足够了。另一方面，Dorschel 提出，命令只有在说话者有权发出命令的情况下才是恰当的。我们当然会需要这一点 —— 特别是对于采购订单，它既包含命令成分，也包含承诺成分。
这些考虑表明，我们有权从哲学家提出的概念中进行挑选。
脚注
1 译注：自然界的大象记忆力超群，所以常用 “大象” 表示 “记得所有事情”。
2 译注：原文为 “declination”，我觉得是 “declaration” 打错字了，因为全文都没再出现 “declination”。
3 译注：“缺漏正确性” 指程序总是会返回正确的值，但是不保证程序真的会返回。“无缺正确性（total correctness）” 指要求第二点的正确性。
4 译注：翻译参考 百度百科。“行事行为” 是表达说话者的意图的行为，它是在说某些话时所实施的行为。“取效行为” 是通过某些话所实施的行为，或讲某些话所导致的行为，它是话语所产生的后果或所引起的变化，也是通过讲某些话所完成的行为。