逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」 的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题， 也可以看做计算中的类型。此外，相关的结构可以看做命题的证明或者其相应类型的程序。 更进一步来说，证明的化简与程序的求值对应。

与此相应，本书的名字也有两种含义。它可以看做「编程语言的基础」，也可以看做 「编程的语言基础」。我们用 Agda 证明助理编写的规范（Specification） 同时描述了编程语言以及该语言编写的程序自身。

本书面向本科最后一年的学生、一年级的研究生或博士生。 本书以简单类型 λ-演算（Simply-Typed Lambda Calculus，简称 STLC）作为核心示例， 旨在教授编程语言的操作语义基础。全书以 Agda 文学脚本（Literal Script）的形式写成。 使用证明助理可以让开发过程变得更加具体而清晰易懂，还可以给予学生即时反馈， 帮助学生发现理解有误的地方并及时纠正。

【译注：文学编程（Literal Programming）用带有代码的自然语言文章来进行编程， 此概念由高德纳（Donald Knuth）提出，详情可参考维基百科。】

本书分为两册。第一分册为逻辑基础，发展了所需的形式化工具。第二分册为编程语言基础， 介绍了操作语义的基本方法。

个人评论

从 2013 年开始，我在爱丁堡大学为四年制本科生和研究生教授编程语言的类型和语义的课程。 该课程的早期版本基于 Benjamin Pierce 的著作 TAPL。我的版本则基于 Pierce 的后续教材《软件基础》（英文版 Software Foundations），此书为 Pierce 与他人合著，基于 Coq 编写。正如 Pierce 在 ICFP 的主题演讲 Lambda, The Ultimate TA 中所言，我也相信基于证明助理的课程会对学习有所帮助。

然而有了五年的教学经验后，我发现 Coq 并不是最好的授课载体。 对于学习编程语言理论基础而言，我们花费了太多课程去专门学习证明推导的策略（Tactic）。 每个概念都需要学习两遍：例如，在学过一遍积数据类型（Product Data Type）之后， 我们还要再学一遍与之对应的合取（Conjunction）的引入（Introduction）和消除（Elimination）策略。 Coq 用来生成归纳假设（Induction Hypothesis）的规则有时看起来很玄学。而 notation 构造则允许直观但灵活多变的语法，同一个概念总是有两个名字有时会令人迷惑， 例如，subst N x M 和 N [x := M]。策略的名字时短时长；标准库中的命名约定则非常不一致。 命题即类型作为证明的基础虽然存在，但却被雪藏了。

我发现自己热衷于用 Agda 重构此课程。在 Agda 中，我们不再需要学习策略了： 这里只有依值类型编程，简单纯粹。我们总是通过构造子来引入，通过模式匹配来消除。 归纳不再是谜之独立的概念，它与我们熟悉的递归概念直接对应。混缀语法十分灵活， 但每个概念只需要一个名字，例如代换就是 _[_:=_]。标准库虽不完美，但它的一致性却很合理。 命题即类型作为证明的基础则被骄傲地展示了出来。

不过，此前还没有用 Agda 语言描述的编程语言理论教材。虽然 Stump 的 Verified Functional Programming in Agda 涵盖了相关的范围， 但比起编程语言理论，却更多关注于依值类型编程。

本书最初的目标只是简单地改编《软件基础》，保持同样的内容，而只是将代码从 Coq 翻译成 Agda。但五年的课堂经验很快让我明白，自己有一些关于如何展示这些材料的想法。 有人说除非你不得不写书，否则绝对不要写书。而我很快发现这就是一本我不得不写的书。

我很幸运地得到了我的学生 Wen Kokke 的热情帮助。她引导着我站在 Agda 新手的视角写书，还提供了一些十分易用的工具来生成清晰易读的页面。

这里的大部分内容都是在 2018 年上半年的休假期间写的。

—— Philip Wadler，里约热内卢，2018 年 1 月 - 6 月

习题说明

标有推荐的习题是爱丁堡大学使用本教材的课程中学生需要做的。

标有延伸的习题提供了额外的挑战。很少有学生能全部做完，但至少应该尝试一下。

标有实践的习题供想要更多实践的学生练习。

你可以从 Github 上下载本书并将 “– 请将代码写在此处” 替换为你的习题解答。 此外，你也可能在课程作业中收到需要编辑的文件，其中包含了练习。

你在解题时或许需要导入库函数，也可能需要将 PLFA 设置为 Agda 库，方法可参考 读者指南。

请勿在公共空间发布习题答案。

GitHub 上有一个发布了部分习题答案的非公开代码仓库。如果你想获得访问，请联系 Philip Wadler。