北京
一本讲编程语言理论的书，通篇用证明助手Agda写成。它的目录从自然数、归纳法、关系、等价一路排到lambda演算、双向类型推断、指称语义，最后落在无类型lambda演算的合流性上。这不是一本教你写代码的书，而是一本让你把"程序为什么正确"写成机器可检验证明的书。
全书分成三个部分。第一部分是逻辑基础，从自然数出发，依次处理归纳证明、关系的归纳定义、等价与等式推理、同构与嵌入、联结词、否定（含直觉主义与经典逻辑）、量词、可判定性，以及列表与高阶函数。第二部分转向编程语言基础，从lambda演算入门，讲进展与保持这两条性质，再进入内在类型的de Bruijn表示、简单类型lambda演算的更多构造、双模拟、双向类型推断，以及无类型lambda演算的完全规范化与合流性。第三部分是指称语义，讨论无类型lambda演算的指称语义、其组合性、归约相对指称语义的可靠性、指称语义相对操作语义的充分性，以及指称相等蕴含上下文等价。附录单独处理无类型lambda演算中的替换。
支持者会说，这条路子把"证明"从纸面搬进了机器。每一条定理都要通过Agda的类型检查器，写错一个步骤就编译不过。对学习者而言，这意味着不能靠"看起来对"蒙混过关，进展与保持这类性质必须一步步构造出来。书里的de Bruijn表示、双向类型推断这些主题，本身就是类型理论课程里绕不开的硬骨头，用证明助手重做一遍，理解深度和抄一遍定义完全不同。
反对的声音同样成立。Agda不是主流工业语言，学习者要先跨过工具链这道门槛，才能开始碰编程语言理论本身。对只想理解语义学直觉的读者，机器检验的严格性可能变成额外负担——证明写不出来，卡住的是Agda的语法和类型系统，而不是理论概念。把课程时间花在跟证明助手搏斗上，值不值，取决于教学目标到底是培养能形式化验证的人，还是培养能读懂语义学论文的人。
我的判断是，这本书的定位从一开始就不是普及读物。它面向的是愿意把定理写成代码的人。判断依据在它的使用记录里：2022年，卢布尔雅那大学的Andrej Bauer、圣迭戈大学的Michael Shulman、阿尔贝特-路德维希大学的Peter Thiemann、爱丁堡大学的Philip Wadler都用它开过课。2021年有明尼苏达大学的Favonia、滑铁卢大学的Prabhakar Ragde、麦克马斯特大学的Jacques Carette；2020年的名单更长，包括得克萨斯大学的William Cook、帕多瓦大学的Maria Emilia Maietti与Ingo Blechschmidt、威斯康星大学拉克罗斯分校的John Maraist、印第安纳大学的Jeremy Siek、都灵大学的Ugo de'Liguoro。再往前，2019年有伯明翰大学的Dan Ghica、滑铁卢大学的Prabhakar Ragde、爱丁堡大学的Philip Wadler，以及里约热内卢天主教大学的Philip Wadler；2018年有佛蒙特大学的David Darais、爱丁堡大学的Philip Wadler、谷歌西雅图的John Leo。一门课连续多年被不同国家的高校采用，说明它撑得住课堂教学的检验。
这本书还衍生出了改写版本。PLFArend把书中所有代码片段用Arend重写，PLFaLean则用Lean 4实现了书中的证明，覆盖v22.08版本的第二、三部分。同一套理论内容能在多个证明助手上落地，本身就说明这些材料的组织方式不依赖某一个工具的怪癖。
书是开源的，仓库放在GitHub上，作者明确欢迎关于组织方式、增删材料、解释不清之处、好习题、错误与笔误的意见，并鼓励提交pull request。习题答案另有一个私有仓库，需要联系作者获取访问权限。对想认真啃形式化语义的人来说，这份材料的分量不在页数，而在每一行都要过类型检查器。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
