.
形式化入门:从 BNF 到类型安全
-
Glomzzz
-
2026-10-10
-
About
. 形式化入门:从 BNF 到类型安全
- Glomzzz
- 2026-10-10
- About
用布尔值与自然数算术语言,从抽象语法、小步操作语义一路证明到类型安全与算法可靠性.
在程序语言理论中,形式化是把语言的结构、运行规则与类型规则写成精确定义, 再对这些定义证明性质的方法. 这组文章用一门只有布尔值和自然数的小语言,从零演示这项工作: 怎样定义语法,怎样定义“运行”,怎样定义“类型”, 最后怎样证明“通过类型检查的程序不会受阻”.
不少程序语言爱好者都想过设计一门自己中意的语言. 你可能熟悉代数数据类型、所有权、代数作用,也能在项目里熟练使用它们; 真到动手设计时,脑袋里却常常只剩一堆零散的偏好: “我想要这个特性”“我不喜欢那种写法”. 这不说明你没理解这些概念. 会用一个概念,与决定它在新语言中怎样工作,是两项不同的任务: 设计时还要说明它解决什么问题、在什么条件下可用、与其他特性相遇时会发生什么.
偏好可以是设计的起点,却不能代替对语义及特性之间关系的说明. 形式化不替我们判断什么是好设计, 它让设计中的假设、约束与推论变得明确, 使我们能追问它们是否一致、是否成立、是否达到了预期目标.
研究程序语言时,问题往往很朴素:这段程序会算出什么结果, 会不会在运行时崩溃,编译器说它“没有类型错误”到底能不能信. 这些问题都能用自然语言提出来; 若要对所有程序给出可核对的保证, 就必须先规定程序的结构、运行规则,以及“类型错误”和“出错”各指什么. 下文用形式化完成这项工作,并用自然语言解释每个定义与证明.
路线:自然语言与元语言、语法、小步操作语义、规则归纳与确定性、 正规形式与受阻、类型判断、类型安全、检查算法与测试,各篇附带练习. .
自然语言写程序语言规格时的常见歧义,以及对象语言与元语言的分层.
这些约定适用于
形式化入门:从 BNF 到类型安全
的文章与独立条目. 阅读这组文章只需具备中学的“集合”概念,外加愿意逐行核对的耐心;用到的每个概念都会先定义再使用. 文中的定义、定理、引理、推论、例、附注、注记都可以单独打开. 环境名统一用英文,嵌入标题按“环境名 → 编号 → 标题”排列,例如 “Theorem 2.1. 进展”;正文引用只显示条目标题,省略局部编号. 证明以 “Proof.” 起头,覆盖全部情形(对称或重复的论证会合并说明),以 ∎ 结尾.初次阅读可以先跳过证明,看命题说了什么. “附注”补充容易忽略的前提与常见误解;“注记”把概念与哲学、逻辑史上的相关讨论联系起来,区分原著概括、教学类比与工程应用(中文概括仅作意译,不充当逐字引文),跳过注记不影响主线推理. 各个主题末尾附有带提示与解答的练习;标为“扩展”的题目会明确改动哪些规则,其结论只适用于改动后的系统,不直接用于
一步规约
与
类型与类型判断
规定的原语言. Rust 代码用来展示这套规则怎样实现为程序(这门语言的规则恰好能直接写成递归函数,一般规则未必如此);代码旁附有解释,不熟悉 Rust 也能读懂. 网页中公式优先转为 MathML 呈现,无法直接转换的退回内联 SVG;推导规则和推导树的辅助文本分别给出规则名、前提与结论. 术语译名以香蕉空间的条目为准, 尚未收录的术语参考
总结
所列的中文译文: reduction 称“规约”,inference rule 称“推导规则”, normal form 称“正规形式”,rule induction 称“规则归纳法”, context 称“语境”,type soundness 称“类型健全性”,term 称“词项”. “项”是“词项”的简称,“子项”“闭项”等复合词保留; “推导”指规则实例构成的有限证明树,注意与“推导规则”区分. 完整对照见
术语对照
. 日常交流里,无论是汉语还是英语,自然语言都足够好用. 说话的人和听话的人共享大量背景,含糊的地方可以靠语境补上,补错了再问一句. 写程序语言的规格时,我们仍会用到这些背景,却不能把关键设计留给读者自行补全: 读者可能是其他国家的程序语言研究者,也可能是十年后的自己; 把规格变成实现时,还要交代机器应当执行哪些步骤. 下面几个例子展示这项任务中需要澄清的问题(自然语言在日常交流里即使含糊也依然有意义).
“咬死了猎人的狗”可以读成“(咬死了猎人)的狗”,指一条狗; 也可以读成“咬死了(猎人的狗)”,指一件事. 两种读法用的字完全相同,差别只在怎样分组. 程序里同样的情况随处可见:
人读到这些句子时,常会根据语境和常识选择一种结构,但未必选得一样. 实现解析器时,不能指望程序替我们猜出想要的分组, 必须另行规定文法、优先级或其他消歧办法.
一份规格写道:“
再如“
不完整规格中的类型检查问题
按一套明确的类型规则回答前三个问题; 求值顺序的影响见
求值策略、规约策略与合流性
. 规格的作者心里多半有答案,只是觉得“显然”而没写下来; 然而不同的人眼里“显然”的东西往往不同. C 语言标准用英文写成,几十年来关于某些条款到底允许什么的争论一直没停, 后来还出现了专门把它的含义精确化的研究项目(例如 Cerberus).
“所有测试都没通过”可以理解为“每个测试都失败了”, 也可以理解为“至少有一个测试失败,未能全部通过”. 两种读法的差别在于“所有”和否定词哪个管着哪个. 把量词的作用范围明确写出来: 前者是“对每个 , 都没通过”,后者是“不成立:(对每个 , 都通过)”. 写出来之后,两句话的结构就不再混淆了. 讲程序语言的性质时,这类句子到处都是. “每个程序都有某个类型”和“存在一个类型,使得每个程序都有这个类型”, 量词顺序一换,意思就完全不同.
下面是 Berry 悖论的一个汉语版本. 考虑这个短语:“不能用少于二十个字来定义的最小正整数”. 先固定一套包含这些字的有限字符表,以字符数计长, 并假定每个有效描述至多定义一个正整数. 少于二十个字的字符串只有有限多个,所以它们至多定义有限多个正整数; 这些短字符串未能定义的正整数中必有最小者,记为 . 若上面这个十八字短语也是同一描述语言中的有效描述, 并且这里的“定义”仍能无条件地适用于包含它自身的全部描述,它又恰好定义了 . 于是 既能又不能用少于二十个字定义,矛盾. 计数本身没有要求先把这个短语排除. 需要检查的是:描述语言与判定“哪个表达式定义哪个数”的语义条件有没有固定, 以及这个语义概念能否在同一层次无限制地涵盖自身. 把描述语言与谈论其语义的元语言分开,可以避免这种混用(当然,自指本身未必都会引起矛盾). 本文把这个教训落实为
对象语言与元语言
的区分: 不把外部描述自动算作内部表达式.练习 1.4 用固定命名表演示这一点. 前面四个例子讲的是说清楚有多难. 还有一个问题更根本:我们想要的结论是关于所有程序的. “这门语言里,通过类型检查的程序都不会在运行时出错”, 这句话谈论的是无穷多个程序. 无穷多个程序没法逐一试验;要得到普遍保证,就需要覆盖它们的论证. 无论用什么语言写,若没有说明分类是否穷尽、每一步依据什么, 读者都很难判断是否漏了情形. “其余情形类似”“显然成立”这些话,写的人常常真心相信, 但这恰恰是错误最容易藏身的地方. 本文采用明确的抽象语法、归纳定义和推导规则, 使结构、适用条件与论证义务能够分别接受检查. 在结构上,本文直接研究已经分好组的语法树,把从字符串到树的解析留在模型之外(对应
结构歧义
;这并不保证任意文法都能唯一解析). 在适用条件上,用对规则封闭的最小关系定义运行与类型,推不出的判断在这个关系中就不成立,不额外靠常识补规则(对应
不完整的规格
;这种定义仍可能留下受阻状态,是否符合设计目标还要另行检查). 在量词范围上,约定符号的读法,写明量词管到哪里,不靠语气猜范围(对应
量词的范围
). 在层次上,区分对象语言中的项和元语言中关于项的判断,不把外部描述自动算作内部表达式(对应
Berry 悖论
;这并不要求所有形式系统都禁止谈论自身). 在论证义务上,证明要说明怎样覆盖全部情形、怎样使用定义和已有结论;本文先给纸面证明,若要让机器核对,还须把定义与证明编码到明确的逻辑系统中. 性质来自具体的设计选择,换上形式记号本身不会自动带来它们,例如: 本文这门语言是否有唯一后继,要由
确定性
另外证明. 形式化让歧义、选择和假设更容易定位, 本身不保证唯一解析、唯一后继,也不保证所有读者自动理解一致. 形式化同样离不开自然语言的配合. 下文仍用自然语言说明定义与证明; 出现分歧时,先核对约定、规则及其应用,必要时修改模型或说明. 我们的目标是证明这套规则下的性质,无意为一切语言建立唯一标准.
接下来要用“树”描述程序的结构,先把相关术语说清楚.
这里约定的树是由节点和连接节点的边组成的有限结构,有唯一的根. 除根以外,每个节点恰有一个父节点; 从根沿父子方向走到任意节点的路径唯一,不会绕回原处. 每个节点可以带一个符号作为标签. 一条边连接父节点与它的子节点(也称“孩子”). 同一父节点的孩子有顺序,因此这是有序树; 例如
词项的集合
中条件、 分支、 分支的位置不能互换. 没有孩子的节点称为叶子;至少有一个孩子的节点称为内部节点. 根也可能是叶子,只有一个节点的树就是如此. 从某个节点沿父子方向走一步或多步能到达的节点,称为它的后代. 以某节点为根,连同它的所有后代和连接它们的边,构成一棵子树. 整棵树也算以原根为根的子树;排除它自己时,称为真子树. 例如表示 的树有三个节点: 根标着 ,它的孩子标着 ,后者的孩子标着 . 前两个是内部节点, 是叶子;以 为根的子树表示 . 这里“子节点”指单个节点,“子树”指从那个节点开始的整块结构. Exercise 1.1. 分组与执行顺序的区分 “先乘除,后加减”把
可以分别补上“先完整求出左操作数,再求右操作数,最后相加”与相反顺序的规定. 分组解决哪个运算包着哪个运算,执行顺序解决哪件事先发生; 一条优先级约定不能替代后一条规定. Exercise 1.2. 把量词的范围写出来 若把“所有提交的程序都没有接受”理解为“每个提交的程序都遭拒绝”, 那么它为假:甲、乙已经接受. 若理解为“至少有一个提交的程序未获接受”,那么它为真:丙遭拒绝. 第一种说法的否定是“至少有一个提交的程序得到接受”; 第二种说法的否定是“每个提交的程序都得到接受”. 它们的否定也不同,因此原句不能靠读者自行猜范围. 这里约定每次提交最终只有“接受”或“拒绝”两种结果. Exercise 1.3. 补全一份除法规格 一种规定是:两边都必须是非负整数,且除数 必须大于 ; 返回唯一的非负整数 ,满足 . 不满足输入条件时明确报错,不自动把字符串转成整数. 于是
Exercise 1.4. 谈论一个名字,不等于增加一个名字 按命名表, 确实是无法命名的最小正整数, 但这个长短语不在命名表里,不属于这门语言的名字. 我们能在解释规格的自然语言里描述 ,不意味着那门小语言也能命名它. 如果正式把这个短语加进命名表,必须规定它在新语言中表示哪个数, 原先关于“最小无法命名的数”的结论也须重新检查. 这个练习展示的是:外部描述不会自动成为内部名字. 至于 Berry 悖论本身,还涉及能否在同一语言中无限制地使用涵盖自身的可定义性概念, 不能简单归结为忘了重新统计. Exercise 1.5. 找出“其余显然”的缺口 取 为“”. 前一百个正整数都满足它, 却不满足. 因此“检查了一百次”只能支持这一百个具体实例,不能独自推出普遍结论. 要证明所有正整数都满足某个性质,还要给出覆盖所有情况的推理方法; “剩下的显然同理”若没有说明相同的前提和推理步骤, 就只是把待证结论复述了一遍,算不上补完证明. 先解决
Berry 悖论
.
对象语言是作为研究对象的语言,元语言是用来谈论对象语言的语言. 例如,
词项的集合
、
一步规约
与
类型与类型判断
规定的布尔值与自然数语言是对象语言; 用来写这些定义和证明的自然语言与数学符号属于元语言. 用 Rust 实现这门小语言时,Rust 也充当元语言,见
Rust 也是元语言
. 例如“ 是值”是元语言里的一句话,它在谈论对象语言里的 . 对象语言自己说不出这句话,它里面根本没有“值”这个词. 反过来,元语言里的“所有”“如果……那么”,也不属于对象语言. 在这门小语言里,外部关于项的描述不会自动成为内部表达式, 因此可以避开前面例子中的层次混用. 这不等于只要分层,就排除了所有逻辑问题.
1.2
自然语言写规格的局限
1.2.1
弊端一:一句话有多种结构
1 + 2 * 3
1 + 2 * 3
既可按 分组,也可按 分组;
if a then if b then x else y
if a then if b then x else y
里的
else
else
既可挂在内层
if
if
上,也可挂在外层
if
if
上.
1.2.2
弊端二:没说到的情形
if
if
的条件必须是布尔值,两个分支的类型相同.” 这句话读起来没什么问题,却留下几处悬而未决的情形: 条件恒为真、 分支永远不执行时,是否还要检查 分支; “类型相同”指字面上完全一致,还是允许自动转换; 检查器拒绝某个程序时,能否指出它具体违反了哪一条.f() + g()
f() + g()
先算两边再相加”: 当
f
f
和
g
g
都会打印字符时,这句话没有规定哪一边先执行、先打印.
1.2.3
弊端三:全称与否定的范围
1.2.4
弊端四:自指问题
1.2.5
弊端五:“显然”没法检查
1.2.6
形式化带来了什么
E ::= E + E | 0
E ::= E + E | 0
下,字符串
0 + 0 + 0
0 + 0 + 0
仍可有两棵解析树;
1.2.7
练习:自然语言弊端
Exercises (5)
2 + 3 * 4
2 + 3 * 4
的分组以及
f() + g()
f() + g()
的调用顺序; 设两个函数都会打印一个字符,给出两份分组相同、打印顺序不同的完整顺序规定.Solution
2 + 3 * 4
2 + 3 * 4
规定为
2 + (3 * 4)
2 + (3 * 4)
,结果是 , 但没有规定
f() + g()
f() + g()
先调用谁. 设
f
f
打印
F
F
后返回 ,
g
g
打印
G
G
后返回 : 先左后右打印
FG
FG
,先右后左打印
GF
GF
,两者的数值结果都为 .Hint
区分“每一个都遭拒绝”和“至少一个未获接受”, 不要只在原句里换一个近义词.Solution
a / b
a / b
返回它们的商”漏掉的情况; 自行设计一个整数除法操作,完整规定输入范围和错误处理, 并写出三个输入及其预期结果. 答案可以有不同设计,但不能把异常情形留空.Hint
至少说明可接受的输入、非整除时的结果、除数为零的处理; 再给能区分不同规定的例子.Solution
7 / 2
7 / 2
返回 ,
7 / 0
7 / 0
报错,
7 / "2"
7 / "2"
也报错. 第一例排除了“保留小数商”的规定, 后两例分别排除了“零除返回某个普通数”和“字符串自动转换”的规定. 这只是一个可选设计,关键是不能只写“返回商”却把这些决定留给实现者.Hint
先检查规定的命名表里有没有那个短语,再看是否偷偷扩充了语言. 参照
Berry 悖论
.Solution
Hint
构造一个只对前一百个正整数成立的性质, 就能检查有限验证到底证明了什么.Solution
1.3
两个层次的语言
定义算术语言的值与一步规约关系,区分基本规约规则与结构规则.
用规则归纳法证明一步规约的确定性,并证明 Rust 求值函数与规约规则一致.
区分作为合法终点的值与作为运行时错误的受阻项,并定义多步规约关系.
通过典范形式引理、进展定理与保型定理,证明算术语言的良类型词项求值不会受阻.
将语法导向的类型规则实现为 Rust 类型推理函数,并证明它相对类型规则可靠且完备.
把进展、保型与确定性写成基于样本的测试断言,并讨论测试与形式证明的边界.
Backlinks
Backlinks
Built with Typsite.