【读书笔记】formal reasoning about programs 第二章 形式化程序语法 2.1具体语法-爱代码爱编程
CHAPTER 2 Formalizing Program Syntax
2.1 Concrete Syntax 具体语法
程序的定义是从编程语言的定义开始,而编程语言的定义是从它的语法开始,语法涵盖了哪些种类的短语基本上是格式化的。
具体语法决定了哪些字符序列是可以被接受的。
以简单的算术表达式语言为例,下面的字母串是有效的(valid):
3
x
3 + x
y x (3 + x)
以下字符串是无效的(invalid):
1 + + 2
x y z
这不是简单靠对算术的直觉去评判的,这里遵循一种叫作“巴科斯范式(Backus-Naur Form, BNF)”的语法。
巴科斯范式Backus-Naur Form, BNF
以美国人巴科斯(Backus)和丹麦人诺尔(Naur)的名字命名的一种形式化的语法表示方法,用来描述语法的一种形成体系,是一种典型的元语言。
它有一些语法规则:
· 在双引号中的东西代表它本身
· 双引号外的字代表语法
· <必选项> # 尖括号内表示必选项
· [可选项] #方括号内表示可选项
· {0次或多次} #大括号内表示可重复0次至多次的项
· | 代表 or
· ::= 读作定义为
换句话说,我们先假设常数 (Constants)和变量 (Variables)的集合,分别基于自然数 (N)和字符串 (Strings)的集合,然后定义表达式 (Expression),包含了常数、变量、加法和乘法。
加法和乘法是递归指定的语法。巴科斯范式用递归来表达一个或多个符号。
举个例子,我们想表达“单词是有字母组成的”,这是日常语言;
那用数学的语言说就是,单词 = 一个字母或多个字母”;
用巴科斯范式的语法表达就是,单词::=<字母>|<字母><单词>,这个表达式里就有了递归。
再例如,“一个正整数是由一个或多个数字构成的”,寻常的表达式无法表达任意位数字构成的正整数,但通过递归可以完美地诠释出来:
<number> ::= <digit>|<digit><number>
<digit> ::= 0|1|2|3|4|5|6|7|8|9
归纳定义法 Inductive Definitions
归纳定义法是一个非常重要的工具,它解释了如何从一个较小的集合建立更大的集合。上面语法中的递归性质隐含地运用了归纳定义。用更通用的话来解释归纳定义就是,它提供了一系列定义集合的推理规则 (inference rules) ,在形式上,这个集合被定义为“满足所有规则的最小集合”。
每个规则都有前提 (premises)和结论 (conclusion),我们用四条规则来诠释上面的BNF语法,两者是完全等价的。
用于定义表达式 (Expressions)的一个集合Exp:
这个推理规则这样来解读:
如果横线以上的所有事实都是真的,那么横线以下的事实也是真的。可以将这个表达式看作“if P then Q”的逻辑,分子是前提条件P,分母是Q。这条规则隐晦地表达出需要对其中出现的所有的元变量的值都成立(n, e1, e2称为元变量, metavariables)。
刚接触语义学的人往往会对这种定义风格产生消极的情绪,但很快就会发现它是一种非常紧凑的符号,可以用来表达很多概念,也可以把它看作是数学定义的特定领域的编程语言,这么说会比较抽象,但在Coq代码中可以具体体现出来。