目录

第 1章 ζ-演算 .....................................................................................................1 

1.1 ζ-演算的起源............................................................................................1 

1.2不带类型的 ζ-演算....................................................................................2 

1.2.1语法 ..............................................................................................3 

1.2.2船-等价 ...........................................................................................4 

1.2.3替换 ..............................................................................................6 

1.2.4 (-归约 ...........................................................................................7 

1.2.5表达能力........................................................................................9 

1.2.6不动点 .........................................................................................12 

1.2.7其他数据类型 ...............................................................................13 

1.2.8邱奇-罗索定理 ..............................................................................14 

1.2.9归约策略......................................................................................15 

1.3简单类型的 ζ-演算..................................................................................16 

1.3.1简单类型的项 ...............................................................................16 

1.3.2归约 ............................................................................................19 

1.3.3正规化 .........................................................................................20 

1.4 F系统 ...................................................................................................21 

1.4.1语法 ............................................................................................21 

1.4.2语义 ............................................................................................22

第 2章 Coq ......................................................................................................24 

2.1基本的函数式编程...................................................................................24 

2.2归约规则 ................................................................................................31 

2.3列表.......................................................................................................33 

2.4规则归纳 ................................................................................................39 

2.5多态列表 ................................................................................................40 

2.6依赖类型 ................................................................................................42 

2.7高阶函数 ................................................................................................43 

2.8柯里-霍华德关联.....................................................................................45 

2.9归纳证明 ................................................................................................47 

2.10常用证明策略........................................................................................50 

2.11证明自动化 ...........................................................................................53 

2.12余归纳类型 ...........................................................................................55 

2.13代码抽取 ..............................................................................................62 

函数式程序设计

第 3章 OCaml .................................................................................................65 

3.1安装和使用 OCaml .................................................................................65 

3.2数据类型与函数 ......................................................................................66 

3.3控制结构 ................................................................................................78 

3.4高阶函数 ................................................................................................82 

3.5记忆.......................................................................................................84 

3.6异常.......................................................................................................85 

3.7排序.......................................................................................................86 

3.8队列.......................................................................................................87 

3.9模块.......................................................................................................90 

3.10函子 .....................................................................................................92 

3.11单子 .....................................................................................................94

第 4章部分习题参考答案 ..................................................................................98 

4.1第 1章练习题.........................................................................................98 

4.2第 2章练习题.........................................................................................99 

4.3第 3章练习题....................................................................................... 106

参考文献 ............................................................................................................ 112

索引................................................................................................................... 113