背景呢还是背景呢
这学期学了一门Type System and Programming Language,感觉是一门很有意思的课。虽然讲的是编程语言,但是很多思想其实工作的时候可能也会用的到。记得老师有一节课说:『你们现在不学习(PL),以后就不会学了。这是你们多数人唯一的机会了』。这门课有个本科生版本的Principles of Programming Languages,多了些写代码的作业,少了点证明,可惜Fall不开。教材是老师自己写的Practical Foundations for Programming Languages,这里只写下我自己的理解,有错了欢迎讨论。
Judgement 和 Inference Rule
一个Judgement就是一组断言,比如说( au~type),就是说( au)是一个类型。再比如(n~nat) 就是说(n)是一个自然数。从这里看其实就是一个断言。
当我们有多个Judgement的时候,我们可以推导出其余的Judgement。比如说:(a=3)并且(b=5),那么在某些条件下面(就是多一些别的规则)我们可以推出来(a+b=8)。用正式的语言写出来就是
在PL里面,可以用这种规则来定义一个类型的规则。比如
就是说,如果(a)是一个自然数,而且(b)也是一个自然数,那么(a+b)就是一个自然数。这个就是Inference Rule。
我们如下定义所有的自然数
这里我们首先有(0mathrel{ riangleq} z)。然后如果(n)是一个自然数,那么(succ(n))也是一个自然数。这样其实就是说(1mathrel{ riangleq} mathtt{succ}(0)),(n+1mathrel{ riangleq} mathtt{succ}(n))。
书上的另外一个例子是定义一棵树
就是说,如果我们有两个树,那么着两个子树可以组成另一个树。
其实这种定义的方法,在BNF里面也可以看到,比如
Exp := num | Exp + Exp
就是说一个表达式可以是一个数字也可以是两个表达式的和。
Rule Induction
如果我们要证明某个类型有某种属性,那么我们该怎么证明呢?这里就是用归纳法。
首先让我们会想下数学归纳法。数学归纳法是定义在自然数上的
- 首先证明最简单的情况是对的
- 然后假设当(n=i)的时候也是对的
- 最后证明当(n=i+1)的时候也是对的
通常(n=i+1)是定义在(n=i)上面的。
不过如果说我们有(a_{i+1} = f(a_i , a_{i-1}))那么我们再第二步还需要假设(a_{i-1})也是对的。现在让我们假设(fmathrel{ riangleq} mathtt{node}),然后我们要证明类型(tree)满足某个属性(P),那么和数学归纳法类似,我们需要
- 证明(P(empty)),即(P)在空树上成立(类似(n=0)时,成立)
- 假设当(a_1~tree)且(a_2~tree)时,(P(a_1)) 且(P(a_2))
- 证明(P(node(a_1, a_2)))
这就是Rule Induction。其实感觉上就是数学归纳在树形结构上的推广。
最后我们证明如下一个定理来加深一下理解下:
如果(succ(s)~nat),那么(s~nat)。
这条定理叫做inversion lemma。乍一看显然,其实还是需要证明的:
- 当(e=zero)时,因为(e)不能被写成(succ(s))的形式,所以定理成立。(初始情况)
- 假设(s)满足这条定理,当(e=succ(s))时,我们需要证明,如果(e~nat)那么(s~nat)。因为(s)满足这条定理,并且(e=succ(s)~nat),那么我们有(s~nat)。那么(e)满足这条定理。
证明完毕。