Revision | 软件科学基础
Abstract. 软件科学基础的复习笔记。
课程网站是 https://xiongyingfei.github.io/SF/2024/,参考资料是 Software Fundations 的 Vol. 1 和 Vol. 2。
- Polymorphism and High-Order Functions
- The Curry-Howard Correspondence, Inductively Defined Propositions
- Simple Imperative Programs
- Automation
- Hoare Logic
- Small-Step Operational Semantics
- Simply Typed Lambda Calculus
- Typing Mutable References
- Subtyping
Polymorphism and High-Order Functions
多态和隐式参数声明
如下两种方法可以定义多态的列表:
1 | Inductive list (X : Type) : Type := |
将 (X : Type)
直接写在 type constructor 相当于是要求在每一个 data constructor 前面都加上 (X : Type)
。
用如下的方法可以将 X
声明为 nil 的隐式参数:
1 | Arguments nil {X} |
这样一来在推不出来 nil 类型的时候和强行给 nil 传参的时候会报错:
1 | Fail Definition mynil := nil. |
但是可以通过手动标注类型或者使用 @
来临时禁用隐式参数:
1 | Definition mynil : list nat := nil. |
这里有一个很重要的东西是,X
不一定要是一个 Type
,还可以是 nat,比如说下面这个东西定义了固定长度的列表。此时的 list n
称为一个 dependent type,它是 nat
和 nat -> Type
的 generalised sum type 的一个元素。
1 | Inductive list : nat -> Type := |
回忆我们在学 Agda 的 Internal Verification 的时候[1],有如下的定义:
1 | data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where |
用这个东西来解释的话,就是 list n = ( n , list ) ∈ Σ nat list
Lambda Calculus, Church Numeral
一个 Lambda 表达式的语法如下:
只有下面两种推导规则:
- Alpha Renaming 将变量改名。
可以改成 实际上改名规则有点复杂,这里不写。 - Beta Reduction 函数调用。
可以写出 Bool 类值的 Lambda 表达式(Church Boolean)
这里两个参数的意思是你要将构造子作为参数传进来。同时下面的函数的功能是求两个 Church Boolean 的与:
这里
和 作为参数传给了 ,当 为 true 时返回 ,否则将返回 。
可以写出自然数的 Church Numerals。
在 Coq 中我们可以翻译成如下的代码:
1 | Definition cnat := forall X : Type, (X -> X) -> X -> X. |
接下来我们来定义各种运算。
1 | Definition plus (n m : cnat) : cnat := |
定义指数运算稍微有一点棘手,这里你需要注意到传给 Church Numeral 的类型不一定非要是 X
。
1 | Definition exp (n m : cnat) : cnat := |
下面的 Y Combinator 用于在 Lambda Calculus 中实现递归
简单计算一下发现
The Curry-Howard Correspondence, Inductively Defined Propositions
指的是命题对应类型,证明对应值的同构关系。具体地有下表:
Logic side | Programming side |
---|---|
universal quantification | generalised product type |
existential quantification | generalised sum type |
implication | function type |
conjunction | product type |
disjunction | sum type |
true formula | unit type |
false formula | bottom type |
在 Coq 中,对于一个定理
1 | Theorem name : content. |
这里 Theorem
实际上是 Definition
的一个别名,content
是这里的 name
的类型,Proof 和 Qed 之间的东西实际上是在构造这个类型的一个值,这个值称为该定理的一个 Proof Object。
因为 Coq 里面的证明风格很命令式,所以这里你可能不能直观地感受到这个 Curry Howard Correspondence。而在 Agda 里面这个则更明显一点。
Coq 中,诸逻辑用语的定义实际上如下:
1 | Inductive and (P Q : Prop) : Prop := |
我们以 or
和 exists
为例简单说一下这个东西怎么解析。
- 我们之前已经提到了直接在 type constructor 后面加的
(P Q : Prop)
意思是每一个 data constructor 都需要带上这两个参数。 - 那么这里的
or_introl
这个 data constructor 实际上意思是,传入两个类型P, Q
(命题 ),并传入一个P
类型的值(命题 的证明)就可以得到一个or P Q
类型的值( 的证明)。or_intror
同理。
对于 exists
,这里面有一个 forall 可能不是很好理解,但是
- 我们之前提到了
ex_intros : forall x : A, P x -> ex P
这个写法等价于ex_intros (x : A) : P x -> ex P
。 - 那么这里的
ex_intros
读入一个A -> Prop
函数P
(一个谓词 ),一个A
类型的x
(论域中的一个具体值 ),一个P x
类型的值(命题 的一个证明),就可以得到一个exists x, P x
类型的值( 的证明)
这一段话不一定对
forall
的本质是什么?
从上面的表格当中我们看到 forall 在 Programming Side 对应的是 generalised producted type。下面我们来解释一下 generalised producted type 是什么东西。对于人类来说 sum type 和 product type 都是理解的,前者是可以具有成分类型中任何一种,后者是一个 tuple。
我们还是考虑第一节中提到的 generalised sigma type,也就是 exists。在 Agda 下的代码为
1 | data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where |
sum type 即表示任意一个单独的 a , b
都是 Σ A B
的一个值(
而 product 的意思是,这里你必须给出一个大小为
那么由于集合中元素都是互异的,这里你想要在程序中写出这个 tuple 一个可操作的方法是写一个单射
你发现我们这里怎么也没法用正常的映射写法精确的描述这个函数的类型,所以我在 mapsto 后面加上了红色的类型。这个函数在类型论里面叫做 Dependent Function Type,就是直接定义成这样子的,跳过了中间经过 tuple 的思考。
这就表明 forall 修饰的命题的 Proof Object 应当形如
1 | fun x : A => ... (* which should have type `B x` *) |
于是根据 Functional Extensionality Axiom 可以知道下面两个定义等价:
1 | constructor (x : A) : something |
于是,常见的 Tactics 本质上是:
- split. 本质上是增加一个
conj
,并将要传入的两个参数作为两个 Goal。 - destruct. 本质上是添加一个
match
来匹配所有的构造子。 - apply. 声称结果必然是某一个函数的输出,转而寻找一个输入使得输出具有该类型。
一些常见的结论的本质是:
- ex_falso 一个空的 match 的返回值可以被推导出任何类型。
可以用 Inductive
定义一系列命题。下面定义的东西是一个经典的命题:
1 | Inductive ev : nat-> Prop := |
不妨自行用上面的 Curry Howard Correspondence 来解释这两个 data constructor 是什么意思,这里不赘述。
现在我们考虑定义结构归纳法的命题,并写出其 Proof Object。这里本质上是你的 Proof Object 中可以有递归函数(fix
)。
对于 Inductive Type 的递归,作为例子我们考虑下面的Peano 自然数递归,其应当具有类型:
1 | Definition nat_ind_type : Type := |
这个 ind_type 生成的方法是,对于每一个 data constructor,都给定从参数上谓词
显然下面的东西是一个具有该类型的值:
1 | Definition nat_ind : nat_ind_type := |
因此我们证明了整数的结构归纳法是对的。
对于 inductively defined propositions,如果直接套用上面的归纳类型定义方式,这里 P
的类型就应当类似于
1 | P : IndProp -> Prop |
这是一个关于证明(注意 P
的输入是一个 IndProp
类型的值,即一个证明)的谓词。但实际上你根本不用在乎证明满足什么性质,只要证出来就好了,所以 inductive propositions 的归纳类型是用下面的方法单独定义的。
对于 inductive propositions 的结构归纳法,我们是希望辅助推导这样的结论:
1 | forall P : Arg -> Prop, (* 1 *) |
不妨假设 IndProp 有几个构造子
1 | Inductive IndProp : Arg -> Prop := |
这里的 Arg1
是某个类型,SomeF
是某个 Arg1 -> Arg
的函数,那么你需要在 (* 1 *)
和 (* 2 *)
之间加上:
1 | forall arg1 : Arg1, IndProp (SomeF1 arg1) -> P (SomeF1 arg1) -> P (SomeF2 arg1) |
言下之意就是,在 (* 2 *)
中你希望证明的这个蕴含关系的前提的证明是由 arg1
这些参数用某种方式组合(SomeF2
),用 Constructor1
这个构造子构造出来的,并且 IndProp -> P
在子结构上也成立(IndProp (SomeF1 arg1)
),那么 P
必须要在 SomeF2
这种组合上面成立。
以 ev
为例,其定义为
1 | Inductive ev : nat -> Prop := |
于是 ev_ind
希望辅助推导 forall n : nat, ev n -> P n
,其类型应当是:
1 | forall P : nat -> Prop, |
观察 ev
的两个构造子的形状,可以发现在 (* insert something *)
的部分插入合适的东西之后应该得到:
1 | forall P : nat -> Prop, |
另一个比较有意思的东西是 eq_ind
。考虑 eq
的定义
1 | Inductive eq (X : Type) (n : X) : X -> Prop := |
按照上面的推法应该写出
1 | Definition eq_ind_type : Type := |
这给出了 rewrite
的本质:rewrite n m
时,把除了 P
的表达式。
接下来是经典的三个问题。
什么时候我们会输入命题,输出命题?
考虑一些作用到
Prop
上的 type constructor。比如说or
就是读入两个命题,生成一个命题。什么时候我们会输入证明,输出证明?
考虑经典的 data contructor
ev_SS
,就是输入了ev n
的证明然后输出了ev (S (S n))
的证明。什么时候我们会输入命题,输出证明?
考虑那几个将命题作为显式参数输入的命题逻辑公式,比如
1
2Definition and_comm (P Q : Prop) : (P /\ Q) -> (Q /\ P)
:= (* omitted. *).
注意 coq 屏蔽了输入一个证明,输出一个命题。Informally 这是因为我们得到的结论不应当随着证明的方法变化而变化。
Simple Imperative Programs
我们定义了一个简单的命令式语言 IMP。这个语言没有很严格的类型系统,包含以下要素:
- 自然数和布尔值,算数和逻辑运算。
- 变量(英文大写字母),赋值(
Assign
),包含一个内存池(用一个 Total Map 表出,称为状态)。 - 基本的程序结构:顺序执行(
Seq
),条件(If
),循环(While
)
为了节约篇幅我们这里并不写出这种语言的 BNF,你可以根据下面的语义定义自动补全一下。
考虑如何建模语义。一个直观的想法是建模成函数,比如说定义:
1 | Fixpoint aeval (a : aexp) : nat := |
或者建模成关系,比如定义
1 | Inductive aevalR : aexp -> nat -> Prop := |
表示一个 aexp 求值之后得到 st =[ prog ]=> st'
表示对状态 st
执行程序 prog
之后得到 st'
。抽象地,有如下几条推导规则:
Automation
除了各种 exxx 之外可以采用如下的方式来智能化地证明:
1 | Ltac find_rwd := |
这里 ?P
可以匹配某一个谓词,?E
可以匹配某个式子,在你加的分支足够多的时候是可以匹配上唯一的前提的。|-
匹配要证明的式子,=>
后面是执行的操作。
Hoare Logic
Hoare Logic 用 Hoare 三元组来描述程序的性质,
Hoare Logic 的规则如下
注意 Asgn 的写法是在前提中置换,所以说下面这个 Hoare triple 是不合法的:
反例是
注意在 If 当中
在模型论的观点下研究 Hoare Logic 的语义,考虑用上文定义的 IMP,将几条规则证明成定理。
在 Coq 当中定义 Hoare triple
1 | Definition Assertion := state -> Prop |
那么可以用 IMP 用关系建模的语义来定义合法的 Hoare triple:
1 | Definition valid_hoare_triple (P : Assertion) (c : com) (Q : Assertion) : Prop := |
然后容易验证所有的 Hoare Logic 规则都成立。
此外可以证明死循环可以推出任何后条件。这称为 Hoare Logic 的部分正确性,即允许写错误的代码,如果写了死循环那么可以推出任何条件。
如果在语言中加入下面的语句,也可以写出对应的 Hoare 规则:
if b then c
相当于if b then c else skip
,不需要额外的规则。repeat c until b
相当于c; while !b do c
,不需要额外的规则。assume b
这句话的意思是在
为真的时候assume b
等价于skip
,其余时候程序会卡在这一句不能往后执行(stuck),行为上相当于while true
,能够推出任何后条件。其 Hoare 规则为assert b
当 不成立时,程序崩溃(crash / error),在一个 error 的状态上不能得到任何结论。其 Hoare 规则为
现在可以通过霍尔规则,用称为 Decorated Program 的风格推导大段程序的正确性。
比如要推导
1 | {{ X <= 3 }} |
其 Decorated Program 如下:
1 | {{ X <= 3 }} |
将 Hoare 规则改成 Decorated Program,有
1 | // Skip |
一个困难的点是,如何获得 while 的循环不变式
Definition(最弱前条件).
记为
Definition(最强后条件).
记为
sp 和 wp 都可以递归地计算,但是式子略微复杂,所以我不想写。wp 有一个很精妙的构造(注意前条件是一个 Assertion
,即 state -> Prop
):
还有一个我上课想到的不一定正确的 sp 的构造(imformally 可以证明是对的)
可以证明一个重要的 Hoare triple
也就是说最弱前条件是循环不变式。
现在我们将 Hoare Logic 看作一个形式系统,验证其
- Soundness,在 IMP 模型下,Hoare Logic 是正确的。(这里前面已经证明了)
- Completeness,所有在 IMP 模型下的 valide hoare triple 都可以被 Hoare 规则推出。
唯一的难点是 Seq 和 While 的证明。这里我们均可以用 wp 作为中间条件。比如说对于 While,你可以先证明
这里用到了重要的 Hoare triple
可以证明 Hoare Logic 是不可判定的。因为停机问题可以规约到 Hoare triple 的判定:
Small-Step Operational Semantics
小步法语义,简而言之就是对于程序的 AST,每次选择中序遍历的第一个叶子进行 evaluate。语义建模成关系,称为
意为程序
重复执行
1 | Inductive cstep : (com * state) -> (com * state) -> Prop := |
这里我们省略了 -->a
和 -->b
之类的东西,这两个东西意思是对一个 nat 表达式或者一个 bool 表达式单步展开。
在此基础上定义任意多步执行的关系
有
在小步法语义中我们主要关注三个性质:
- determinstic
。 - strong progress
。 - normal form
。可以证明 。 - normalizing
上面三个性质是好的,我们总是希望我们的编程语言有上面的性质。但是一般的语言总是存在卡住的项,比如说你在 if 的判断条件里面加入了不是 Bool 的东西。因此我们引入 Type system 来防止这一点。
定义
表示在类型系统下
然后可以定义一系列推导规则,这个不是很重要。仅以 if 为例,我们定义
之后我们可以将 strong progress 改为 progress:
并且有一个新的性质是 preservation:
Simply Typed Lambda Calculus
我们定义 STLC 表达式的语法:
可以用小步法定义 STLC 的语义。注意现在的 STLC 是一种纯函数式语言,所以在小步法定义的时候不会带上一个
上面涉及到了
这是因为
这里并不涉及 Alpha Renaming,因为在 Coq 里面太难实现。因此需要注意,这样的一条规则和上面的语法是不相容的:
如果加上你就可以得到
而在原来的系统里面,这东西按照 Functional Extensionality,行为上相当于
到现在为止你的表达式还是可以随便乱写的,因此需要加上类型系统。
表示在上下文
可以证明 STLC 有如下性质:
Progress
Weakening
这里前件蕴含着
Substitution preserves typing
Preservation
Unique Type
这个性质重要度实际上不高,因为后面引入子类之后就失效了。但是在这里还是可以说明表达式到 Type 有函数关系。
此外可以向语言中添加 nat,let … in …,Pairs,Unit,Sums,Lists,Fix,Records 等成分。
这里直接将 fix 的行为定义出来的原因是 fix 的类型是无穷阶的递归类型,在 STLC 中无法写出。
经典的操作是用 fix 写递归:
1 | fact = \self : Nat -> Nat, |
在小步法求值的过程中,我们顺次展开 fix 和带入 n,以求 3 的阶乘为例
1 | fix fact 3 |
在 Coq 中写
1 | Notation " x <- e1 ;; e2" := (match e1 with |
回忆在 Haskell 里面
1 | e1 >>= (\x -> e2) = do x <- e1 |
其中在 Maybe Monad 里面有
1 | return :: a -> m a |
和上面的定义是极其类似的。
那么以 Pair 的类型检查为例,可以像下面这样写:
1 | Fixpoint type_check (Gamma : context) (t : tm) : option ty := |
Typing Mutable References
为了编码指针和引用,我们增加一些项:
注意引入指针之后 STLC 不再是纯函数式语言,所以在描述小步法的时候要带上内存池
注意你不一定能推导出内存池中每一位的类型,比如对于
你无法知道 loc
,所以类型检查时我们不需要试图知道地址的类型。只需要定义
但是在求值过程中会产生 loc
,因此为了证明 Progress 和 Preservation 你不得不知道每一位是什么类型。所以说这里我们只能弱化 Progress 和 Preservation,只证明你能推出
于是我们可以推到 loc 的类型:
注意 well-typed 的
对于任意的
然后 preservation 和 progress 的定义在 Coq 下面是
1 | Theorem preservation : forall ST t t' T st st', |
第 6 行的谓词 extends 判定
有了引用之后我们无需 fix 也可以编写递归。方法是把函数存到内存里面去。下面的东西将一个阶乘函数存在了内存池的末尾,并返回
在 evaluate 这个语句的时候,首先调用
有了引用、Record、let in 之后我们可以模拟封装,注意对象内部的变量只能用成员函数访问。对于这个类
1 | class counter { |
可以这样模拟:
1 | let newcounter = \_ : Unit, |
那么下面的代码(写在 ...
后面即可)
1 | let c1 = newcounter unit in |
返回值是
需要注意 let x = A in B
相当于
行为上,会首先彻底展开
如果不写第一个 \_: Unit
,就会导致 let c = ref 0 in ...
在最开始被展开,此时 c = ref 0
将被彻底展开(开一个新内存 l
),然后下面的所有 c
将被换成 loc l
,变成单例模式,返回
如果在此基础上不写第二个 \_: Unit
,展开完第一段代码第 (c := succ (!c); !c)
被彻底展开,变成常数 i
只是调用这个常数,因此返回
Subtyping
Liskov 替换原则 如果在任意使用 T 类型的值的场合都可以传入 S 类型的任意值,那么 S 是 T 的子类。
有两个注意点。对于两个函数类型
这里子部分与整体子类关系相反,称为逆变式(contravariance),对应为了提供容器而存在的类型(输入类型);而子部分与整体关系相同,称为协变式(convariance),对应为了提供值而存在的类型(输出类型)。
对于引用
是输入类型:a := b
。 是输出类型:!a
。
因此引用的子类推导关系是
增加
注意这里所有的推导都是充分的。即使子类是一个偏序关系,你也没有很好的办法证明两个类是不可比的。
- 1.https://zhenjiang888.github.io/FP/2023/slides/ch20_internal.pdf,Page 11. ↩