跳转至

类型系统

学习资料

是什么

类型系统，可以看做是附着在语言语法之上的一套符号证明系统。 给表达式确定类型的过程，相当于对程序应该具备的属性做形式证明， 因此，数理逻辑是我们的朋友。

λ演算

λ演算实际上只是一套“符号推导系

  • 定义某些合法的符号
  • 定义一些符号推导规则
  • 这种推导过程称之为演算

Peano系统

有序三元组 (M, F, e) 其中 M 是一个集合，F 是 M 到 M 的映射，e 是首元素

其满足以下五个要求

  • e 属于 M
  • M 在 F 下封闭
  • e 不在 F 值域中
  • F 是单射
  • M 在以下规则中具有唯一性，即如果 A 是 M 的子集且满足在 F 上封闭，则 A = M

理解

如果认为 M 是自然数集(包含0)，e 为 0，F 为 ++ 操作，就很容易理解了 至少这是符合要求的一组三元组 (N, ++, 0)

lambda 演算

三种合法的语法 term

  • 变量 x
  • lambda x. t1 在 t1 中抽象出 x
  • t1t2 将 t1 应用于 t2

alpha 变换

函数参数可以重命名

beta 规约

可以用参数值替换函数参数

组合子逻辑(CL)

组合子逻辑和 lambda 演算很像，但是它是多参数无变量绑定的函数

合法的 CL term

  • 所有变量、常量、组合子 I K S
  • 如果 X Y 是合法的，那么 XY 也是合法的

变换规则

在 CL 中变换规则称为 weak reduction

  • IX -> X
  • KXY -> X
  • SXYZ -> XZ(YZ)

等价性

CL 和 lambda 演算是等价的

也都有不动点 Yx = x(Yx)

命题逻辑

形式系统

公理

  • a -> (b -> a)
  • (a -> (b -> r)) -> ((a -> b) -> (a -> r))
  • (¬a -> ¬b) -> (b -> a)

推导规则

  • a,a->b/b

自然演义系统

语法

  • 可数个命题符号 p1, p2, …
  • 5个联接词符号 ¬, \/, /\, ->, <->
  • 2个辅助符号 (, )

合法的公式 BNF

  • a ::= p | (¬a) | (a1 \/ a2) | (a1 /\ a2) | (a1 -> a2) | (a1 \<-> a2)

等价性

两种系统是等价的

证明(略)

谓词逻辑

一阶谓词逻辑，只是比命题逻辑多添加了一些公理或推导规则 然而，这样的举动，却会让形式系统截然不同

需要更多的理解和练习，略

简单类型化 lambda 演算

无类型 lambda 演算的类型化版本，是众多类型化 lambda 演算中最简单的一个 它只包含一个类型构造器（type constructor） -> ，即，接受两个类型 T1, T2 作为参数，返回一个函数类型 T1 -> T2

合法 term BNF

  • t ::= x | lambda x.t | t t

即 变量、抽象或应用

值

值（value）是一个和语义相关的概念，有三种常用的方法为项指定语义

  • 操作语义：抽象机器上的操作，有慢慢规约的小步语义和按照表达式和语句解释的大步语义
  • 指称语义：更关注从一种到另一种的转换
  • 公理语义（不懂，略）

用操作语义表示：

值和语义相关，首先，我们人为指定项的一个子集，将其中的元素称为值。 值可能是项被求值的最终结果，但也不全是，因为对某些项的求值过程可能不会终止。

如项定义如下：\~t ::= true | false | if t then t else t\~ 可以定义值：\~v ::= true | false\~

类型

一个类型上下文（也称类型环境），是一个变量和类型之间绑定关系的集合。