幸福迟了一夜才来。
类型系统是指一种根据所计算出值得种类对词语进行分类从而证明某程序行为不会发生的可行语法手段。
# 无类型系统
# 无类型算术表达式
# 语法
项的集合是最小集合T \mathcal{T} T ,满足:
{ t r u e , f a l s e , 0 } ⊆ T \{true,false,0\}\subseteq \mathcal{T} { t r u e , f a l s e , 0 } ⊆ T 。
如果t 1 ∈ T t_1\in\mathcal{T} t 1 ∈ T ,则{ s u c c t 1 , p r e d t 1 i s z e r o t 1 } ⊆ T \{succ\;t_1,pred\;t_1\;iszero\;t_1\}\subseteq \mathcal{T} { s u c c t 1 , p r e d t 1 i s z e r o t 1 } ⊆ T 。
如果t 1 , t 2 , t 3 ∈ T t_1,t_2,t_3\in\mathcal{T} t 1 , t 2 , t 3 ∈ T ,则i f t 1 t h e n t 2 e l s e t 3 ∈ T if\;t_1\;then\;t_2\;else\;t_3\in\mathcal{T} i f t 1 t h e n t 2 e l s e t 3 ∈ T 。
# 对项的一些归纳定义
常量集合:
C o n s t s ( t r u e ) = { t r u e } ; C o n s t s ( f a l s e ) = { f a l s e } ; C o n s t s ( 0 ) = { 0 } ; C o n s t s ( s u c c t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( p r e d t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( i s z e r o t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( i f t 1 t h e n t 2 e l s e t 3 ) = C o n s t s ( t 1 ) ∪ C o n s t s ( t 2 ) ∪ C o n s t s ( t 3 ) Consts(true)=\{true\};Consts(false)=\{false\};Consts(0)=\{0\};\\
Consts(succ\;t_1)=Consts(t_1);Consts(pred\;t_1)=Consts(t_1);Consts(iszero\;t_1)=Consts(t_1);\\
Consts(if\;t_1\;then\;t_2\;else\;t_3)=Consts(t_1)\cup Consts(t_2)\cup Consts(t_3)
C o n s t s ( t r u e ) = { t r u e } ; C o n s t s ( f a l s e ) = { f a l s e } ; C o n s t s ( 0 ) = { 0 } ; C o n s t s ( s u c c t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( p r e d t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( i s z e r o t 1 ) = C o n s t s ( t 1 ) ; C o n s t s ( i f t 1 t h e n t 2 e l s e t 3 ) = C o n s t s ( t 1 ) ∪ C o n s t s ( t 2 ) ∪ C o n s t s ( t 3 )
项的长度:
s i z e ( t r u e ) = s i z e ( f a l s e ) = s i z e ( 0 ) = 1 ; s i z e ( s u c c t 1 ) = s i z e ( p r e d t 1 ) = s i z e ( i s z e r o t 1 ) = s i z e ( t 1 ) + 1 ; s i z e ( i f t 1 t h e n t 2 e l s e t 3 ) = s i z e ( t 1 ) + s i z e ( t 2 ) + s i z e ( t 3 ) + 1 ; size(true)=size(false)=size(0)=1;\\
size(succ\;t_1)=size(pred\;t_1)=size(iszero\;t_1)=size(t_1)+1;\\
size(if\;t_1\;then\;t_2\;else\;t_3)=size(t_1)+size(t_2)+size(t_3)+1;
s i z e ( t r u e ) = s i z e ( f a l s e ) = s i z e ( 0 ) = 1 ; s i z e ( s u c c t 1 ) = s i z e ( p r e d t 1 ) = s i z e ( i s z e r o t 1 ) = s i z e ( t 1 ) + 1 ; s i z e ( i f t 1 t h e n t 2 e l s e t 3 ) = s i z e ( t 1 ) + s i z e ( t 2 ) + s i z e ( t 3 ) + 1 ;
项的深度:
d e p t h ( t r u e ) = d e p t h ( f a l s e ) = d e p t h ( 0 ) = 1 ; d e p t h ( s u c c t 1 ) = d e p t h ( p r e d t 1 ) = d e p t h ( i s z e r o t 1 ) = d e p t h ( t 1 ) + 1 ; d e p t h ( i f t 1 t h e n t 2 e l s e t 3 ) = m a x ( d e p t h ( t 1 ) , d e p t h ( t 2 ) , d e p t h ( t 3 ) ) + 1 ; depth(true)=depth(false)=depth(0)=1;\\
depth(succ\;t_1)=depth(pred\;t_1)=depth(iszero\;t_1)=depth(t_1)+1;\\
depth(if\;t_1\;then\;t_2\;else\;t_3)=max(depth(t_1),depth(t_2),depth(t_3))+1;
d e p t h ( t r u e ) = d e p t h ( f a l s e ) = d e p t h ( 0 ) = 1 ; d e p t h ( s u c c t 1 ) = d e p t h ( p r e d t 1 ) = d e p t h ( i s z e r o t 1 ) = d e p t h ( t 1 ) + 1 ; d e p t h ( i f t 1 t h e n t 2 e l s e t 3 ) = m a x ( d e p t h ( t 1 ) , d e p t h ( t 2 ) , d e p t h ( t 3 ) ) + 1 ;
有∣ C o n s t s ( t ) ∣ ≤ s i z e ( t ) |Consts(t)|\leq size(t) ∣ C o n s t s ( t ) ∣ ≤ s i z e ( t ) 。
同理,对项上的一个谓词,我们可以对长度或对深度归纳,或结构归纳。
# 求值
语法:
t : : = t r u e ∣ f a l s e ∣ i f t t h e n t e l s e t v : : = t r u e ∣ f a l s e t::=true|false|if\;t\;then\;t\;else\;t\\
v::=true|false
t : : = t r u e ∣ f a l s e ∣ i f t t h e n t e l s e t v : : = t r u e ∣ f a l s e
求值:
i f t r u e t h e n t 2 e l s e t 3 → t 2 ( E − I F T R U E ) i f f a l s e t h e n t 2 e l s e t 3 → t 3 ( E − I F F A L S E ) t 1 → t 1 ′ i f t 1 t h e n t 2 e l s e t 3 → i f t 1 ′ t h e n t 2 e l s e t 3 ( E − I F ) if\;true\;then\;t_2\;else\;t_3\rightarrow t_2(E-IFTRUE)\\
if\;false\;then\;t_2\;else\;t_3\rightarrow t_3(E-IFFALSE)\\
\frac{t_1\rightarrow t_1'}{if\;t_1\;then\;t_2\;else\;t_3\rightarrow if\;t_1'\;then\;t_2\;else\;t_3}(E-IF)
i f t r u e t h e n t 2 e l s e t 3 → t 2 ( E − I F T R U E ) i f f a l s e t h e n t 2 e l s e t 3 → t 3 ( E − I F F A L S E ) i f t 1 t h e n t 2 e l s e t 3 → i f t 1 ′ t h e n t 2 e l s e t 3 t 1 → t 1 ′ ( E − I F )
t → t ′ t\rightarrow t' t → t ′ 表示 “t 一步求值为 t’”,意思是如果 t 是抽象机器在某瞬间的状态,则机器可以做一步计算,并将状态转换为 t’ .
# 无类型算术表达式
语法形式:
t : : = 0 ∣ s u c c t ∣ p r e d t ∣ i s z e r o t ∣ t r u e ∣ f a l s e ∣ i f t t h e n t e l s e t v : : = n v ∣ t r u e ∣ f a l s e n v : : = 0 ∣ s u c c n v t::=0|succ\;t|pred\;t|iszero\;t|true|false|if\;t\;then\;t\;else\;t\\
v::=nv|true|false\\
nv::=0|succ\;nv
t : : = 0 ∣ s u c c t ∣ p r e d t ∣ i s z e r o t ∣ t r u e ∣ f a l s e ∣ i f t t h e n t e l s e t v : : = n v ∣ t r u e ∣ f a l s e n v : : = 0 ∣ s u c c n v
我们常用阿拉伯数字来记s u c c 0 = 1 , s u c c s u c c 0 = 2 , . . . succ\;0=1,succ\;succ\;0=2,... s u c c 0 = 1 , s u c c s u c c 0 = 2 , . . .
求值规则:
i f t r u e t h e n t 2 e l s e t 3 → t 2 ( E − I F T R U E ) i f f a l s e t h e n t 2 e l s e t 3 → t 3 ( E − I F F A L S E ) t 1 → t 1 ′ i f t 1 t h e n t 2 e l s e t 3 → i f t 1 ′ t h e n t 2 e l s e t 3 ( E − I F ) t 1 → t 1 ′ s u c c t 1 → s u c c t 1 ′ ( E − S U C C ) p r e d 0 → 0 ( E − P R E D Z E R O ) p r e d ( s u c c n v 1 ) → n v 1 ( E − P R E D S U C C ) t 1 → t 1 ′ p r e d t 1 → p r e d t 1 ′ ( E − P R E D ) i s z e r o 0 → t r u e ( E − I S Z E R O Z E R O ) i s z e r o ( s u c c n v 1 ) → f a l s e ( E − I S Z E R O S U C C ) t 1 → t 1 ′ i s z e r o t 1 → i s z e r o t 2 ( E − I S Z E R O ) if\;true\;then\;t_2\;else\;t_3\rightarrow t_2\quad(E-IFTRUE)\\
if\;false\;then\;t_2\;else\;t_3\rightarrow t_3\quad(E-IFFALSE)\\
\frac{t_1\rightarrow t_1'}{if\;t_1\;then\;t_2\;else\;t_3\rightarrow if\;t_1'\;then\;t_2\;else\;t_3}\quad(E-IF)\\
\frac{t_1\rightarrow t_1'}{succ\;t_1\rightarrow succ t_1'}\quad(E-SUCC)\\
pred\;0\rightarrow 0\quad(E-PREDZERO)\\
pred(succ\;nv_1)\rightarrow nv_1\quad(E-PREDSUCC)\\
\frac{t_1\rightarrow t_1'}{pred\;t_1\rightarrow pred\;t_1'}\quad(E-PRED)\\
iszero\;0\rightarrow true\quad(E-ISZEROZERO)\\
iszero(succ\;nv_1)\rightarrow false\quad(E-ISZEROSUCC)\\
\frac{t_1\rightarrow t_1'}{iszero\;t_1\rightarrow iszero\;t_2}\quad(E-ISZERO)
i f t r u e t h e n t 2 e l s e t 3 → t 2 ( E − I F T R U E ) i f f a l s e t h e n t 2 e l s e t 3 → t 3 ( E − I F F A L S E ) i f t 1 t h e n t 2 e l s e t 3 → i f t 1 ′ t h e n t 2 e l s e t 3 t 1 → t 1 ′ ( E − I F ) s u c c t 1 → s u c c t 1 ′ t 1 → t 1 ′ ( E − S U C C ) p r e d 0 → 0 ( E − P R E D Z E R O ) p r e d ( s u c c n v 1 ) → n v 1 ( E − P R E D S U C C ) p r e d t 1 → p r e d t 1 ′ t 1 → t 1 ′ ( E − P R E D ) i s z e r o 0 → t r u e ( E − I S Z E R O Z E R O ) i s z e r o ( s u c c n v 1 ) → f a l s e ( E − I S Z E R O S U C C ) i s z e r o t 1 → i s z e r o t 2 t 1 → t 1 ′ ( E − I S Z E R O )
项 t 被称为范式 当且仅当不存在t ′ t' t ′ 使得t → t ′ t\rightarrow t' t → t ′ .
显然,范式就是那些t r u e , f a l s e , 0 , s u c c ( 0 ) , s u c c ( s u c c ( 0 ) ) , . . . true,false,0,succ(0),succ(succ(0)),... t r u e , f a l s e , 0 , s u c c ( 0 ) , s u c c ( s u c c ( 0 ) ) , . . . . 注意,若出现了 pred 一定不是范式,因为总可以用 E-PREDZERO 或 E-PREDSUCC 把它消掉.
我们认为s u c c t r u e succ\;true s u c c t r u e 是一个错误而不是一个值.
定义 ,如果一个封闭项是一个范式但不是一个值,则称该项受阻 。
# 无类型的 lambda 演算
# 基础
lambda 演算用最可能纯的形式表示函数的定义和应用。在 lambda 演算中,每个事物均是一个函数:函数接受的参数是函数,一个函数的结果是另一个函数。
lambda 演算的语法由 3 种项组成。一个变量 x 本身是一个项;一个变量 x 在项t 1 t_1 t 1 中的抽象,记为λ x . t 1 \lambda x.t_1 λ x . t 1 ,是一个项;并且一个项应用到另一个项t 1 t 2 t_1\;t_2 t 1 t 2 也是一个项。用语法描述,项为:
t : : = x ∣ λ x . t ∣ t t t::=x|\lambda x.t|t\;t
t : : = x ∣ λ x . t ∣ t t
我们规定,分析 lambda 演算式子时,从左到右分析,而抽象的顺序是从右到左。即:
t 1 t 2 t 3 = ( t 1 t 2 ) t 3 λ x . λ y . t = λ x . ( λ y . t ) t_1\;t_2\;t_3=(t_1\;t_2)\;t_3\\
\lambda x.\lambda y.t=\lambda x.(\lambda y.t)
t 1 t 2 t 3 = ( t 1 t 2 ) t 3 λ x . λ y . t = λ x . ( λ y . t )
# 抽象语法和具体语法
# 辖域
对变量 x,当它出现在抽象λ x . t \lambda x.t λ x . t 的 t 中时,则认为 x 的出现是囿界 (或称被界定)的。等价地,也可以说λ x \lambda x λ x 是一个绑定器,它的辖域是 t。x 是自由的如果它出现的位置不被任何对 x 的抽象所界定。比如 x 在x y xy x y 和λ y . x y \lambda y.xy λ y . x y 中式自由的,而在( λ x . x ) x (\lambda x.x)x ( λ x . x ) x 中的第一个出现是囿界的,而第二个是自由的。
一个不含自由变量的项称为封闭项 (或称为组合子 )。最简单的组合子就是恒等函数:
i d = λ x . x id=\lambda x.x
i d = λ x . x
规定,抽象总是尽量向右延展的,而应用是从左到右的。譬如:
λ x . x y = λ x . ( x y ) ≠ ( λ x . x ) y ( λ x . x y ) a → a y ( λ x . x ) y a → y a i d x y = ( i d x ) y \lambda x.x\;y=\lambda x.(x\;y)\neq(\lambda x.x)y\\
(\lambda x.x\;y)a\rightarrow a\;y\\
(\lambda x.x)y\;a\rightarrow y\;a\\
idx\;y=(idx)\;y
λ x . x y = λ x . ( x y ) = ( λ x . x ) y ( λ x . x y ) a → a y ( λ x . x ) y a → y a i d x y = ( i d x ) y
# 操作语义
纯形式的 lambda 演算没有内置的常量或原语算子 —— 没有数、算术运算、条件子、记录、循环、序列、I/O 等到。项计算的唯一含义是将函数应用到参数(而参数本身也是函数)。
计算的每一步是重写一个左端部分为抽象的应用,用右端部分代换抽象体中的囿变量。
( λ x . t 12 ) t 2 → [ x ↦ t 2 ] t 12 (\lambda x.t_{12})t_2\rightarrow [x\mapsto t_2]t_{12}
( λ x . t 1 2 ) t 2 → [ x ↦ t 2 ] t 1 2
其中[ x ↦ t 2 ] t 12 [x\mapsto t_2]t_{12} [ x ↦ t 2 ] t 1 2 表示由t 2 t_2 t 2 代换在t 12 t_{12} t 1 2 中所有出现的 x 得到的项。例如:
( λ x . x ) y → y ( λ x . x ( λ x . x ) ) ( u r ) → ( u r ) ( λ x . x ) (\lambda x.x)y\rightarrow y\\
(\lambda x.x(\lambda x.x))(u\;r)\rightarrow(u\;r)(\lambda x.x)
( λ x . x ) y → y ( λ x . x ( λ x . x ) ) ( u r ) → ( u r ) ( λ x . x )
(其中第二个式子实际上是用( u r ) (u\;r) ( u r ) 去代换x ( λ x . x ) x(\lambda x.x) x ( λ x . x ) 中所有自由的 x,即为( u r ) ( λ x . x ) (u\;r)(\lambda x.x) ( u r ) ( λ x . x ) 。)
考虑项:
( λ x . x ) ( ( λ x . x ) ( λ z . ( λ x . x ) z ) ) (\lambda x.x)((\lambda x.x)(\lambda z.(\lambda x.x)z))
( λ x . x ) ( ( λ x . x ) ( λ z . ( λ x . x ) z ) )
记λ x . x = i d \lambda x.x=id λ x . x = i d ,即∀ t , ( λ x . x ) t = i d t → t \forall t,(\lambda x.x)t=idt\rightarrow t ∀ t , ( λ x . x ) t = i d t → t 。即为:
i d ( i d ( λ z . i d z ) ) id(id(\lambda z.idz))
i d ( i d ( λ z . i d z ) )
在全 beta 归约下,任何时刻可以归约任何一个约式。可以选择:
从内到外归约:
i d ( i d ( λ z . i d z ) ) → i d ( i d ( λ z . z ) ) → i d ( λ z . z ) → λ z . z id(id(\lambda z.idz))\\
\rightarrow id(id(\lambda z.z))\\
\rightarrow id(\lambda z.z)\\
\rightarrow \lambda z.z
i d ( i d ( λ z . i d z ) ) → i d ( i d ( λ z . z ) ) → i d ( λ z . z ) → λ z . z
从外到内归约:
i d ( i d ( λ z . i d z ) ) → i d ( λ z . i d z ) → λ z . i d z → λ z . z id(id(\lambda z.idz))\\
\rightarrow id(\lambda z.idz)\\
\rightarrow \lambda z.idz\\
\rightarrow \lambda z.z
i d ( i d ( λ z . i d z ) ) → i d ( λ z . i d z ) → λ z . i d z → λ z . z
我们也可以不允许抽象内部的归约。即λ z . i d z \lambda z.idz λ z . i d z 已经作为一个范式,而不对λ z . \lambda z. λ z . 抽象内部进行归约。当然应该从外到内归约:
i d ( i d ( λ z . i d z ) ) → i d ( λ z . i d z ) → λ z . i d z id(id(\lambda z.idz))\\
\rightarrow id(\lambda z.idz)\\
\rightarrow \lambda z.idz
i d ( i d ( λ z . i d z ) ) → i d ( λ z . i d z ) → λ z . i d z
# lambda 演算中的程序设计
我理解的 lambda 演算实际上还是在描述函数。譬如λ x . x + 1 \lambda x.x+1 λ x . x + 1 ,其中 λ 跟着的是函数参数,“.” 后面跟着函数的内容。然后如果传入一个参数,即作用于 a 时,就会求值得到用 a 去替换函数内容中的自变量 x。
如果想描述的函数有多自变量怎么办?λ ( x , y ) . s \lambda(x,y).s λ ( x , y ) . s 。实际上,我们可以写为λ x . λ y . s \lambda x.\lambda y.s λ x . λ y . s ,这样先传入 y 的值,然后会继续得到一个 lambda 抽象(函数),再求值。譬如:λ ( x , y ) . x + y ( λ x . λ y . x + y ) 3 4 → ( λ x . x + 3 ) 4 → 4 + 3 \lambda(x,y).x+y\\
(\lambda x.\lambda y.x+y)3\;4\\
\rightarrow(\lambda x.x+3)\;4\\
\rightarrow 4+3
λ ( x , y ) . x + y ( λ x . λ y . x + y ) 3 4 → ( λ x . x + 3 ) 4 → 4 + 3
# Church 布尔式
定义:
t r u = λ t . λ f . t f l s = λ t . λ f . f t e s t = λ l . λ m . λ n . l m n tru=\lambda t.\lambda f.t\\
fls=\lambda t.\lambda f.f\\
test=\lambda l.\lambda m.\lambda n.l\;m\;n
t r u = λ t . λ f . t f l s = λ t . λ f . f t e s t = λ l . λ m . λ n . l m n
为什么要定义这些东西?实际上,它用函数来描述了 if 语句:
t e s t t r u v w = ( λ l . λ m . λ n . l m n ) t r u v w → ( λ m . λ n . t r u m n ) v w → ( λ n . t r u v n ) w → t r u v w = ( λ t . λ f . t ) v w → ( λ f . v ) w → v test\;tru\;v\;w\\
=(\lambda l.\lambda m.\lambda n.l\;m\;n)tru\;v\;w\\
\rightarrow(\lambda m.\lambda n.tru\;m\;n)v\;w\\
\rightarrow(\lambda n.tru\;v\;n)w\\
\rightarrow tru\;v\;w\\
=(\lambda t.\lambda f.t)v\;w\\
\rightarrow(\lambda f.v)w\\
\rightarrow v
t e s t t r u v w = ( λ l . λ m . λ n . l m n ) t r u v w → ( λ m . λ n . t r u m n ) v w → ( λ n . t r u v n ) w → t r u v w = ( λ t . λ f . t ) v w → ( λ f . v ) w → v
t e s t f l s v w = ( λ l . λ m . λ n . l m n ) f l s v w → ( λ m . λ n . f l s m n ) v w → ( λ n . f l s v n ) w → f l s v w = ( λ t . λ f . f ) v w → ( λ f . f ) w → w test\;fls\;v\;w\\
=(\lambda l.\lambda m.\lambda n.l\;m\;n)fls\;v\;w\\
\rightarrow(\lambda m.\lambda n.fls\;m\;n)v\;w\\
\rightarrow(\lambda n.fls\;v\;n)w\;\\
\rightarrow fls\;v\;w\\
=(\lambda t.\lambda f.f)v\;w\\
\rightarrow(\lambda f.f)w\\
\rightarrow w
t e s t f l s v w = ( λ l . λ m . λ n . l m n ) f l s v w → ( λ m . λ n . f l s m n ) v w → ( λ n . f l s v n ) w → f l s v w = ( λ t . λ f . f ) v w → ( λ f . f ) w → w
实际上,t r u v w tru\;v\;w t r u v w 可以归约到w w w ,f l s v w fls\;v\;w f l s v w 可以归约到w w w 。我们用 test 可以判断布尔的真假。即
t e s t b v w test\;b\;v\;w t e s t b v w 如果归约到 v 了 b 就为真,否则为假。
我们可以定义逻辑联结词:
a n d = λ b . λ c . b c f l s and=\lambda b.\lambda c.b\;c\;fls
a n d = λ b . λ c . b c f l s
它的作用是:
a n d t r u t r u = ( λ b . λ c . b c f l s ) t r u t r u → ( λ c . t r u c f l s ) t r u → t r u t r u f l s → t r u a n d f l s t r u → f l s and\;tru\;tru\\
=(\lambda b.\lambda c.b\;c\;fls)tru\;tru\\
\rightarrow (\lambda c.tru\;c\;fls)tru\\
\rightarrow tru\;tru\;fls\\
\rightarrow tru\\
and\;fls\;tru\rightarrow fls
a n d t r u t r u = ( λ b . λ c . b c f l s ) t r u t r u → ( λ c . t r u c f l s ) t r u → t r u t r u f l s → t r u a n d f l s t r u → f l s
同理:
o r = λ b . λ c . b t r u c n o t = λ b . b f l s t r u or=\lambda b.\lambda c.b\;tru\;c\\
not=\lambda b.b\;fls\;tru
o r = λ b . λ c . b t r u c n o t = λ b . b f l s t r u
我们能定义值得序对为项:
p a i r = λ f . λ s . λ b . b f s f s t = λ p . p t r u s n d = λ p . p f l s pair=\lambda f.\lambda s.\lambda b.b\;f\;s\\
fst=\lambda p.p\;tru\\
snd=\lambda p.p\;fls
p a i r = λ f . λ s . λ b . b f s f s t = λ p . p t r u s n d = λ p . p f l s
有:
f s t ( p a i r v w ) = f s t ( ( λ f . λ s . λ b . b f s ) v w ) → f s t ( λ b . b v w ) = ( λ p . p t r u ) ( λ b . b v w ) → ( λ b . b v w ) t r u → t r u v w → v fst(pair\;v\;w)\\
=fst((\lambda f.\lambda s.\lambda b.b\;f\;s)v\;w)\\
\rightarrow fst(\lambda b.b\;v\;w)\\
=(\lambda p.p\;tru)\;(\lambda b.b\;v\;w)\\
\rightarrow (\lambda b.b\;v\;w)\;tru\\
\rightarrow tru\;v\;w\\
\rightarrow v
f s t ( p a i r v w ) = f s t ( ( λ f . λ s . λ b . b f s ) v w ) → f s t ( λ b . b v w ) = ( λ p . p t r u ) ( λ b . b v w ) → ( λ b . b v w ) t r u → t r u v w → v
# Church 数值
定义 Church 数值:
c 0 = λ s . λ z . z c 1 = λ s . λ z . s z c 2 = λ s . λ z . s ( s z ) c 3 = λ s . λ z . s ( s ( s z ) ) . . . . . . . c_0=\lambda s.\lambda z.z\\
c_1=\lambda s.\lambda z.s\;z\\
c_2=\lambda s.\lambda z.s\;(s\;z)\\
c_3=\lambda s.\lambda z.s\;(s\;(s\;z))\\
.......
c 0 = λ s . λ z . z c 1 = λ s . λ z . s z c 2 = λ s . λ z . s ( s z ) c 3 = λ s . λ z . s ( s ( s z ) ) . . . . . . .
s u c c = λ n . λ s . λ z . s ( n s z ) s u c c c 3 = ( λ n . λ s . λ z . s ( n s z ) ) c 3 → λ s . λ z . s ( c 3 s z ) = λ s . λ z . s ( [ λ s . λ z . s ( s ( s z ) ) ] s z ) → λ s . λ z . s ( [ λ z . s ( s ( s z ) ) ] z ) → λ s . λ z . s ( s ( s ( s z ) ) ) = c 4 succ=\lambda n.\lambda s.\lambda z.s\;(n\;s\;z)\\
succ\;c_3=(\lambda n.\lambda s.\lambda z.s\;(n\;s\;z))c_3\\
\rightarrow\lambda s.\lambda z.s\;(c_3\;s\;z)\\
=\lambda s.\lambda z.s\;([\lambda s.\lambda z.s(s(s\;z))]s\;z)\\
\rightarrow\lambda s.\lambda z.s([\lambda z.s(s(s\;z))]z)\\
\rightarrow\lambda s.\lambda z.s(s(s(s\;z)))=c_4
s u c c = λ n . λ s . λ z . s ( n s z ) s u c c c 3 = ( λ n . λ s . λ z . s ( n s z ) ) c 3 → λ s . λ z . s ( c 3 s z ) = λ s . λ z . s ( [ λ s . λ z . s ( s ( s z ) ) ] s z ) → λ s . λ z . s ( [ λ z . s ( s ( s z ) ) ] z ) → λ s . λ z . s ( s ( s ( s z ) ) ) = c 4
这里解释下。还记得抽象式中,λ s . λ z . s z \lambda s.\lambda z.s\;z λ s . λ z . s z 中 s 和 z 都表示了函数的内容。我们可以理解 s 为一个 “后继函数”。可以记c n = λ s . λ z . s n z c_n=\lambda s.\lambda z.s^n\;z c n = λ s . λ z . s n z 。求值为c n a b → a n b c_n\;a\;b\rightarrow a^n\;b c n a b → a n b 。
那么后继函数实际上就是用了这个求值,使得s ( c n s z ) → s ( s n z ) = s n + 1 z s\;(c_n\;s\;z)\rightarrow s\;(s^n\;z)=s^{n+1}\;z s ( c n s z ) → s ( s n z ) = s n + 1 z 。
定义加法:
p l u s = λ m . λ n . λ s . λ z . m s ( n s z ) plus=\lambda m.\lambda n.\lambda s.\lambda z.m\;s\;(n\;s\;z)\\
p l u s = λ m . λ n . λ s . λ z . m s ( n s z )
只看函数内容m s ( n s z ) m\;s\;(n\;s\;z) m s ( n s z ) ,因为求值有:
c a s ( c b s z ) → s a ( c b s z ) → s a ( s b z ) = s a + b z c_a\;s\;(c_b\;s\;z)\rightarrow s^a\;(c_b\;s\;z)\rightarrow s^a\;(s^b\;z)=s^{a+b}\;z
c a s ( c b s z ) → s a ( c b s z ) → s a ( s b z ) = s a + b z
所以有p l u s c n c m → c n + m plus\;c_n\;c_m\rightarrow c_{n+m} p l u s c n c m → c n + m 。
定义乘法:
t i m e s = λ m . λ n . m ( p l u s n ) c 0 times=\lambda m.\lambda n.m\;(plus\;n)\;c_0
t i m e s = λ m . λ n . m ( p l u s n ) c 0
只看函数内容m ( p l u s n ) c 0 m\;(plus\;n)\;c_0 m ( p l u s n ) c 0 ,因为有:
c a ( p l u s c b ) c 0 → ( p l u s c b ) a c 0 = p l u s c b ( p l u s c b ( . . . p l u s c b c 0 ) ) ) ) → c a × b c_a\;(plus\;c_b)\;c_0\rightarrow (plus\;c_b)^a\;c_0=plus\;c_b\;(plus\;c_b\;(...\;plus\;c_b\;c_0))))\\
\rightarrow c_{a\times b}
c a ( p l u s c b ) c 0 → ( p l u s c b ) a c 0 = p l u s c b ( p l u s c b ( . . . p l u s c b c 0 ) ) ) ) → c a × b
因为实际上就是把c b c_b c b 往c 0 c_0 c 0 上加了 a 次。
定义判零:
i s z r o = λ m . m ( λ x . f l s ) t r u i s z r o c 0 → c 0 ( λ x . f l s ) t r u iszro=\lambda m.m\;(\lambda x.fls)\;tru\\
iszro\;c_0\rightarrow c_0\;(\lambda x.fls)\;tru\\
i s z r o = λ m . m ( λ x . f l s ) t r u i s z r o c 0 → c 0 ( λ x . f l s ) t r u
\rightarrow(\lambda z.z);tru\
\rightarrow tru\
iszro;c_n\rightarrow c_n;(\lambda x.fls);tru\
=(\lambda s.\lambda z.s^n;z)(\lambda x.fls);tru\
\rightarrow (\lambda z.(\lambda x.fls)^n;z);tru\
\rightarrow (\lambda x.fls)^n tru\
\rightarrow fls\
返回值也是个 C h u r c h 布尔值。 返回值也是个Church布尔值。
返 回 值 也 是 个 C h u r c h 布 尔 值 。
z z = p a i r c 0 c 0 s s = λ p . p a i r ( s n d p ) ( p l u s c 1 ( s n d p ) ) p r d = λ m . f s t ( m s s z z ) zz=pair\;c_0\;c_0\\
ss=\lambda p.pair\;(snd\;p)\;(plus\;c_1\;(snd\;p))\\
prd=\lambda m.fst\;(m\;ss\;zz)
z z = p a i r c 0 c 0 s s = λ p . p a i r ( s n d p ) ( p l u s c 1 ( s n d p ) ) p r d = λ m . f s t ( m s s z z )
为什么它可以实现前趋呢?不难发现,p r d c n → f s t ( s s n z z ) prd\;c_n\rightarrow fst\;(ss^n\;zz) p r d c n → f s t ( s s n z z )
而s s z z ss\;zz s s z z 求值其实等于p a i r c 0 c 1 pair\;c_0\;c_1 p a i r c 0 c 1 。然后s s 2 z z = p a i r c 1 c 2 ss^2\;zz=pair\;c_1\;c_2 s s 2 z z = p a i r c 1 c 2 。因此s s n z z = p a i r c n − 1 c n ss^n\;zz=pair\;c_{n-1}\;c_n s s n z z = p a i r c n − 1 c n 。
所以p r d c n → f s t ( p a i r c n − 1 c n ) → c n − 1 prd\;c_n\rightarrow fst\;(pair\;c_{n-1}\;c_n)\rightarrow c_{n-1} p r d c n → f s t ( p a i r c n − 1 c n ) → c n − 1 。
定义减法:
m i n u s = λ m . λ n . n p r d m m i n u s c a c b → c b p r d c a → p r d b c a → c a − b minus=\lambda m.\lambda n.n\;prd\;m\\
minus\;c_a\;c_b\rightarrow c_b\;prd\;c_a\rightarrow prd^b\;c_a\rightarrow c_{a-b}
m i n u s = λ m . λ n . n p r d m m i n u s c a c b → c b p r d c a → p r d b c a → c a − b
定义判等:
e q u a l = λ m . λ n . i s z r o ( m i n u s m n ) equal=\lambda m.\lambda n.iszro(minus\;m\;n)
e q u a l = λ m . λ n . i s z r o ( m i n u s m n )
# 丰富演算 ——Church 编码和真实值的转换
可以定义抽象,使其可以将 Church 布尔式转化为之前无类型算术表达式中真正的布尔式:
r e a l b o o l = λ b . b t r u e f a l s e r e a l b o o l t r u → t r u e ; r e a l b o o l f l s → f a l s e ; realbool=\lambda b.b\;true\;false\\
realbool\;tru\rightarrow true;\\
realbool fls\rightarrow false;
r e a l b o o l = λ b . b t r u e f a l s e r e a l b o o l t r u → t r u e ; r e a l b o o l f l s → f a l s e ;
同理可以反过来转换:
c h u r c h b o o l = λ b . i f b t h e n t r u e l s e f l s c h u r c h b o o l t r u e → i f t r u e t h e n t r u e l s e f l s → t r u c h u r c h b o o l f a l s e → f l s churchbool=\lambda b.if\;b\;then\;tru\;else\;fls\\
churchbool\;true\rightarrow if\;true\;then\;tru\;else\;fls\rightarrow tru\\
churchbool false\rightarrow fls
c h u r c h b o o l = λ b . i f b t h e n t r u e l s e f l s c h u r c h b o o l t r u e → i f t r u e t h e n t r u e l s e f l s → t r u c h u r c h b o o l f a l s e → f l s
这里的推导,既可以根据 λ 演算的规则,也可以根据无类型算术表达式的推导规则。
同样也可以定义,真正判等:(我们如果带了个真正,就表示求值是个 true 或 false,而不是 Church 编码的布尔式)
r e a l e q = λ m . λ n . r e a l b o o l ( e q u a l m n ) realeq=\lambda m.\lambda n.realbool(equal\;m\;n)
r e a l e q = λ m . λ n . r e a l b o o l ( e q u a l m n )
Church 数值转真正数值:
r e a l n a t = λ m . m ( λ x . s u c c x ) 0 r e a l n a t c 3 → s u c c s u c c s u c c 0 = 3 realnat=\lambda m.m\;(\lambda x.succ\;x)\;0\\
realnat\;c_3\rightarrow succ\;succ\;succ\;0=3
r e a l n a t = λ m . m ( λ x . s u c c x ) 0 r e a l n a t c 3 → s u c c s u c c s u c c 0 = 3
我们不能直接定义r e a l n a t = λ m . m s u c c 0 realnat=\lambda m.m\;succ\;0 r e a l n a t = λ m . m s u c c 0 ,因为s u c c succ s u c c 只是一个标识而本身没有语法意义。因此我们需要把它包装在一个小函数中,而不能直接当作一个函数来用。
# 递归
有些抽象在归约时,仍是他自己。譬如:
o m e g a = ( λ x . x x ) ( λ x . x x ) omega=(\lambda x.x\;x)(\lambda x.x\;x)
o m e g a = ( λ x . x x ) ( λ x . x x )
不动点组合式 :
f i x = λ f . ( λ x . f ( λ y . x x y ) ) ( λ x . f ( λ y . x x y ) ) fix=\lambda f.(\lambda x.f\;(\lambda y.x\;x\;y))(\lambda x.f\;(\lambda y.x\;x\;y))
f i x = λ f . ( λ x . f ( λ y . x x y ) ) ( λ x . f ( λ y . x x y ) )
这有啥用呢?实际上,它可以解决递归问题。用最简单的阶乘函数来考虑下:
g = λ f c t . λ n . i f r e a l e q n c 0 t h e n c 1 e l s e ( t i m e s n ( f c t ( p r d n ) ) ) f a c t o r i a l = f i x g g=\lambda fct.\lambda n.if\;realeq\;n\;c_0\;then\;c_1\;else\;(times\;n\;(fct\;(prd\;n)))\\
factorial=fix\;g
g = λ f c t . λ n . i f r e a l e q n c 0 t h e n c 1 e l s e ( t i m e s n ( f c t ( p r d n ) ) ) f a c t o r i a l = f i x g
先定义g = λ f . < . . . > g=\lambda f.<...> g = λ f . < . . . > ,< . . . > <...> < . . . > 内为函数内容。然后再定义F = f i x g F=fix\;g F = f i x g 。
以一个例子,考虑下f a c t o r i a l c 3 factorial\;c_3 f a c t o r i a l c 3 :
f a c t o r i a l c 3 = f i x g c 3 → h h c 3 ( h : = λ x . g ( λ y . x x y ) ) → g f c t c 3 ( f c t : = λ y . h h y ) → λ n . i f r e a l e q n c 0 t h e n c 1 e l s e ( t i m e s n ( f c t ( p r d n ) ) ) c 3 → i f r e a l e q c 3 c 0 t h e n c 1 e l s e ( t i m e s c 3 ( f c t ( p r d c 3 ) ) ) → ∗ t i m e s c 3 ( f c t ( p r d c 3 ) ) → ∗ t i m e s c 3 f c t c 2 → ∗ t i m e s c 3 ( g f c t c 2 ) → ∗ t i m e s c 3 ( i f r e a l e q c 2 c 0 t h e n c 1 e l s e t i m e s c 2 ( f c t ( p r d c 2 ) ) ) → ∗ t i m e s c 3 ( t i m e s c 2 c 1 ) → ∗ c 6 factorial\;c_3=fix\;g\;c_3\\
\rightarrow h\;h\;c_3\quad (h:=\lambda x.g\;(\lambda y.x\;x\;y))\\
\rightarrow g\;fct\;c_3\quad(fct:=\lambda y.h\;h\;y)\\
\rightarrow \lambda n.if\;realeq\;n\;c_0\;then\;c_1\;else\;(times\;n\;(fct\;(prd\;n)))\;c_3\\
\rightarrow if\;realeq\;c_3\;c_0\;then\;c_1\;else\;(times\;c_3\;(fct\;(prd\;c_3)))\\
\rightarrow^*times\;c_3\;(fct\;(prd\;c_3))\\
\rightarrow^* times\;c_3\;fct\;c_2\\
\rightarrow^* times\;c_3\;(g\;fct\;c_2)\\
\rightarrow^* times\;c_3\;(if\;realeq\;c_2\;c_0\;then\;c_1\;else\;times\;c_2\;(fct(prd\;c_2)))\\
\rightarrow^* times\;c_3\;(times\;c_2\;c_1)\\
\rightarrow^* c_6
f a c t o r i a l c 3 = f i x g c 3 → h h c 3 ( h : = λ x . g ( λ y . x x y ) ) → g f c t c 3 ( f c t : = λ y . h h y ) → λ n . i f r e a l e q n c 0 t h e n c 1 e l s e ( t i m e s n ( f c t ( p r d n ) ) ) c 3 → i f r e a l e q c 3 c 0 t h e n c 1 e l s e ( t i m e s c 3 ( f c t ( p r d c 3 ) ) ) → ∗ t i m e s c 3 ( f c t ( p r d c 3 ) ) → ∗ t i m e s c 3 f c t c 2 → ∗ t i m e s c 3 ( g f c t c 2 ) → ∗ t i m e s c 3 ( i f r e a l e q c 2 c 0 t h e n c 1 e l s e t i m e s c 2 ( f c t ( p r d c 2 ) ) ) → ∗ t i m e s c 3 ( t i m e s c 2 c 1 ) → ∗ c 6
其中关键在于:
f c t c 2 → h h c 2 → g ( λ y . h h y ) c 2 → g f c t c 2 fct\;c_2\rightarrow h\;h\;c_2\rightarrow g\;(\lambda y.h\;h\;y)\;c_2\rightarrow g\;fct\;c_2
f c t c 2 → h h c 2 → g ( λ y . h h y ) c 2 → g f c t c 2
即f c t fct f c t 是自重复的。
# 形式化定义
其实前面已经用半天了,又回来形式化定义下。
定义项的自由变量,记为F V ( t ) FV(t) F V ( t ) ,定义如下:
F V ( x ) = { x } F V ( λ x . t 1 ) = F V ( t 1 ) − { x } F V ( t 1 t 2 ) = F V ( t 1 ) ∪ F V ( t 2 ) FV(x)=\{x\}\\
FV(\lambda x.t_1)=FV(t_1)-\{x\}\\
FV(t_1\;t_2)=FV(t_1)\cup FV(t_2)
F V ( x ) = { x } F V ( λ x . t 1 ) = F V ( t 1 ) − { x } F V ( t 1 t 2 ) = F V ( t 1 ) ∪ F V ( t 2 )
关于代入,首先,我们约定只是囿变量名称不同的项在所有上下文中可交替使用。即可以 “换名”:
λ x . x + y = λ w . w + y \lambda x.x+y=\lambda w.w+y
λ x . x + y = λ w . w + y
对代换的定义为:
[ x ↦ s ] x = s [ x ↦ s ] y = y i f y ≠ x [ x ↦ s ] ( λ y . t 1 ) = λ y . [ x ↦ s ] t 1 i f y ≠ x a n d y ∉ F V ( s ) [ x ↦ s ] ( t 1 t 2 ) = ( [ x ↦ s ] t 1 ) ( [ x ↦ s ] t 2 ) [x\mapsto s]x=s\\
[x\mapsto s]y=y\quad if\;y\neq x\\
[x\mapsto s](\lambda y.t_1)=\lambda y.[x\mapsto s]t_1\quad if\;y\neq x\;and\;y\notin FV(s)\\
[x\mapsto s](t_1\;t_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)
[ x ↦ s ] x = s [ x ↦ s ] y = y i f y = x [ x ↦ s ] ( λ y . t 1 ) = λ y . [ x ↦ s ] t 1 i f y = x a n d y ∈ / F V ( s ) [ x ↦ s ] ( t 1 t 2 ) = ( [ x ↦ s ] t 1 ) ( [ x ↦ s ] t 2 )
其中,第三行可以先把 y 换名换成满足条件的。
lambda 演算语义的定义:
t 1 → t 1 ′ t 1 t 2 → t 1 ′ t 2 t 2 → t 2 ′ v 1 t 2 → v 1 t 2 ′ ( λ x . t 12 ) v 2 → [ x ↦ v 2 ] t 12 \frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\\
\frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\\
(\lambda x.t_{12})\;v_2\rightarrow [x\mapsto v_2]t_{12}
t 1 t 2 → t 1 ′ t 2 t 1 → t 1 ′ v 1 t 2 → v 1 t 2 ′ t 2 → t 2 ′ ( λ x . t 1 2 ) v 2 → [ x ↦ v 2 ] t 1 2
# 项的无名称表示
# 项和上下文
对每个 λ 抽象,我们可以找到对应的 de Bruijn 项,即去掉囿变量,用数字替换:
λ z . ( λ y . y ( λ x . x ) ) ( λ x . z x ) = λ . ( λ . 1 ( λ . 1 ) ) ( λ . 2 1 ) \lambda z.(\lambda y.y\;(\lambda x.x))\;(\lambda x.z\;x)=\lambda.(\lambda.1\;(\lambda.1))(\lambda.2\;1)
λ z . ( λ y . y ( λ x . x ) ) ( λ x . z x ) = λ . ( λ . 1 ( λ . 1 ) ) ( λ . 2 1 )
而书上是从 0 开始标号的。
然后自由变量的话,可以用大于囿变量个数的自然数代换它。
形式化的,定义无名项:
设T \mathcal{T} T 是最小的集簇{ T 0 , T 1 , . . . } \{\mathcal{T_0},\mathcal{T_1},...\} { T 0 , T 1 , . . . } ,使得:
∀ 0 ≤ k < n , k ∈ T n \forall 0\leq k< n,k\in\mathcal{T}_n ∀ 0 ≤ k < n , k ∈ T n 。
如果t 1 ∈ T n , λ . t 1 ∈ T n − 1 t_1\in\mathcal{T}_n,\lambda.t_1\in\mathcal{T}_{n-1} t 1 ∈ T n , λ . t 1 ∈ T n − 1 。
如果t 1 , t 2 ∈ T n t_1,t_2\in\mathcal{T}_n t 1 , t 2 ∈ T n ,那么t 1 t 2 ∈ T n t_1\;t_2\in\mathcal{T}_n t 1 t 2 ∈ T n 。
仔细想一想,可以发现T n \mathcal{T}_n T n 为至多含有 n 个自由变量的项。例如λ . 5 0 ∈ T 6 \lambda .5\;0\in\mathcal{T}_{6} λ . 5 0 ∈ T 6 ,5 为自由变量。
我们可以对所有的 de Bruijn 变量指派一个 de Bruijn 索引(称为一个命名的上下文),例如:
Γ = x ↦ 4 y ↦ 3 z ↦ 2 a ↦ 1 b ↦ 0 \Gamma=x\mapsto 4\\y\mapsto 3\\z\mapsto 2\\
a\mapsto 1\\b\mapsto 0
Γ = x ↦ 4 y ↦ 3 z ↦ 2 a ↦ 1 b ↦ 0
那么a λ x . a = 1 λ . 2 a\;\lambda x.a=1\;\lambda.2 a λ x . a = 1 λ . 2 。注意自由变量的索引需要加上非自由变量的个数。
上面那个指派也可以简写为Γ = x , y , z , a , b \Gamma=x,y,z,a,b Γ = x , y , z , a , b
# 移位和代换
定义移位:
↑ c d ( k ) = { k i f k < c k + d i f k ≥ c ↑ c d ( λ . t 1 ) = λ . ↑ c + 1 d ( t 1 ) ↑ c d ( t 1 t 2 ) = ↑ c d ( t 1 ) ↑ c d ( t 2 ) \uparrow^d_c(k)=\begin{cases}k&if\;k<c\\k+d&if\;k\geq c\end{cases}\\
\uparrow^d_c(\lambda.t_1)=\lambda.\uparrow^d_{c+1}(t_1)\\
\uparrow^d_c(t_1\;t_2)=\uparrow^d_c(t_1)\;\uparrow^d_c(t_2)
↑ c d ( k ) = { k k + d i f k < c i f k ≥ c ↑ c d ( λ . t 1 ) = λ . ↑ c + 1 d ( t 1 ) ↑ c d ( t 1 t 2 ) = ↑ c d ( t 1 ) ↑ c d ( t 2 )
默认从 0 开始移位,例:
↑ 2 ( λ . 0 1 ( λ . 0 1 2 ) ) = λ . ↑ 1 2 0 1 ( λ . 0 1 2 ) = λ . 0 ↑ 1 2 1 ( λ . 0 1 2 ) = λ . 0 3 ( λ . ↑ 2 2 0 1 2 ) = λ . 0 3 ( λ . 0 1 4 ) \uparrow^2(\lambda.0\;1\;(\lambda.0\;1\;2))=\lambda.\uparrow^2_10\;1\;(\lambda.0\;1\;2)\\
=\lambda.0\;\uparrow^2_11\;(\lambda.0\;1\;2)\\
=\lambda.0\;3\;(\lambda.\uparrow^2_2 0\;1\;2)\\
=\lambda.0\;3\;(\lambda.0\;1\;4)
↑ 2 ( λ . 0 1 ( λ . 0 1 2 ) ) = λ . ↑ 1 2 0 1 ( λ . 0 1 2 ) = λ . 0 ↑ 1 2 1 ( λ . 0 1 2 ) = λ . 0 3 ( λ . ↑ 2 2 0 1 2 ) = λ . 0 3 ( λ . 0 1 4 )
定义代换:
[ j ↦ s ] k = { s i f k = j k e l s e [ j ↦ s ] ( λ . t 1 ) = λ . [ j + 1 ↦ ↑ 1 s ] t 1 [ j ↦ s ] ( t 1 t 2 ) = [ j ↦ s ] t 1 [ j ↦ s ] t 2 [j\mapsto s]k=\begin{cases}s&if\;k=j\\k&else\end{cases}\\
[j\mapsto s](\lambda.t_1)=\lambda.[j+1\mapsto \uparrow^1 s]t_1\\
[j\mapsto s](t_1\;t_2)=[j\mapsto s]t_1\;[j\mapsto s]t_2
[ j ↦ s ] k = { s k i f k = j e l s e [ j ↦ s ] ( λ . t 1 ) = λ . [ j + 1 ↦ ↑ 1 s ] t 1 [ j ↦ s ] ( t 1 t 2 ) = [ j ↦ s ] t 1 [ j ↦ s ] t 2
譬如对全局上下文Γ = a , b \Gamma=a,b Γ = a , b ,有
[ b ↦ a ( λ z . a ) ] ( b ( λ x . b ) ) = [ 0 ↦ 1 ( λ . 2 ) ] ( 0 ( λ . 1 ) ) = ( 1 λ . 2 ) [ 0 ↦ 1 ( λ . 2 ) ] ( λ . 1 ) = ( 1 λ . 2 ) λ . [ 0 + 1 ↦ ↑ 0 1 ( 1 λ . 2 ) ] 1 = ( 1 λ . 2 ) λ . [ 1 ↦ ( 2 λ . 3 ) ] 1 = ( 1 λ . 2 ) λ . ( 2 λ . 3 ) = ( a λ z 1 . a ) ( λ z 2 . a λ z 3 . a ) [b\mapsto a\;(\lambda z.a)](b\;(\lambda x.b))=[0\mapsto 1\;(\lambda.2)](0\;(\lambda.1))\\
=(1\;\lambda.2)\;[0\mapsto 1\;(\lambda.2)](\lambda.1)\\
=(1\;\lambda.2)\;\lambda.[0+1\mapsto\uparrow^1_0(1\;\lambda.2)]1\\
=(1\;\lambda.2)\;\lambda.[1\mapsto(2\;\lambda.3)]1\\
=(1\;\lambda.2)\;\lambda.(2\;\lambda.3)\\
=(a\;\lambda z_1.a)\;(\lambda z_2.a\;\lambda z_3.a)
[ b ↦ a ( λ z . a ) ] ( b ( λ x . b ) ) = [ 0 ↦ 1 ( λ . 2 ) ] ( 0 ( λ . 1 ) ) = ( 1 λ . 2 ) [ 0 ↦ 1 ( λ . 2 ) ] ( λ . 1 ) = ( 1 λ . 2 ) λ . [ 0 + 1 ↦ ↑ 0 1 ( 1 λ . 2 ) ] 1 = ( 1 λ . 2 ) λ . [ 1 ↦ ( 2 λ . 3 ) ] 1 = ( 1 λ . 2 ) λ . ( 2 λ . 3 ) = ( a λ z 1 . a ) ( λ z 2 . a λ z 3 . a )
# 求值
t 1 → t 1 ′ t 1 t 2 → t 1 ′ t 2 t 2 → t 2 ′ v 1 t 2 → v 1 t 2 ′ ( λ . t 12 ) v 2 → ↑ 0 − 1 ( [ 0 ↦ ↑ 0 1 v 2 ] t 12 ) \frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\\
\frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\\
(\lambda.t_{12})\;v_2\rightarrow \uparrow^{-1}_0([0\mapsto\uparrow^1_0 v_2]t_{12})
t 1 t 2 → t 1 ′ t 2 t 1 → t 1 ′ v 1 t 2 → v 1 t 2 ′ t 2 → t 2 ′ ( λ . t 1 2 ) v 2 → ↑ 0 − 1 ( [ 0 ↦ ↑ 0 1 v 2 ] t 1 2 )
例如
( λ . 1 0 2 ) ( λ . 0 ) → 0 ( λ . 0 ) 1 (\lambda.1\;0\;2)(\lambda.0)\rightarrow 0\;(\lambda.0)\;1
( λ . 1 0 2 ) ( λ . 0 ) → 0 ( λ . 0 ) 1
而不是1 ( λ . 0 ) 2 1\;(\lambda.0)\;2 1 ( λ . 0 ) 2 ,因为需要对自由变量重新编排。
# 简单类型
# 类型算术表达式
# 类型关系
语法定义:
T : : = B o o l − − − − − − − − − − − − − − t r u e : B o o l f a l s e : B o o l t 1 : B o o l t 2 : T t 3 : T i f t 1 t h e n t 2 e l s e t 3 : T − − − − − − − − − − − − − − T : : = N a t − − − − − − − − − − − − − − 0 : N a t − − − − − − − − − − − − − − t 1 : N a t s u c c t 1 : N a t t 1 : N a t p r e d t 1 : N a t t 1 : N a t i s z r o t 1 : B o o l T::=Bool\\
--------------\\
true:Bool\\
false:Bool\\
\frac{t_1:Bool\quad t_2:T\quad t_3:T}{if\;t_1\;then\;t_2\;else\;t_3:T}\\
--------------\\
T::=Nat\\
--------------\\
0:Nat\\
--------------\\
\frac{t_1:Nat}{succ\;t_1:Nat}\\
\frac{t_1:Nat}{pred\;t_1:Nat}\\
\frac{t_1:Nat}{iszro\;t_1:Bool}\\
T : : = B o o l − − − − − − − − − − − − − − t r u e : B o o l f a l s e : B o o l i f t 1 t h e n t 2 e l s e t 3 : T t 1 : B o o l t 2 : T t 3 : T − − − − − − − − − − − − − − T : : = N a t − − − − − − − − − − − − − − 0 : N a t − − − − − − − − − − − − − − s u c c t 1 : N a t t 1 : N a t p r e d t 1 : N a t t 1 : N a t i s z r o t 1 : B o o l t 1 : N a t
注,T 表示类型。而 if 语句里表示t 2 , t 3 t_2,t_3 t 2 , t 3 和 if 语句最后都是同一类型。(而非必须是 Bool,只是目前我们类型只定义了 Bool)
定义 ,形式地,算术表达式的类型关系是项和类型之间的最小二元关系。如果存在某个 T,使得t : T t:T t : T ,则称项 t 是可类型化 的,或良类型 的。
定理 ,如果一个项是可类型化的,那么它的类型是唯一的。(t 的生成树唯一。)
# 安全性 = 进展 + 保持
# 简单类型的 lambda 演算
定义 ,类型 Bool 上的简单类型集合是由下列语法产生的:
T : : = B o o l ∣ T → T T::=Bool|T\rightarrow T
T : : = B o o l ∣ T → T
类型构造子→ \rightarrow → 是右结合的。可以把它理解为 “函数类型”。譬如B o o l → B o o l Bool\rightarrow Bool B o o l → B o o l 就是一个布尔到布尔的函数类型,可以说λ x . t r u e : B o o l → B o o l \lambda x.true:Bool\rightarrow Bool λ x . t r u e : B o o l → B o o l 。
我们可以对抽象确定参数类型:λ x : T . t \lambda x:T.t λ x : T . t ,其中相当于要求了函数的自变量(参数)x 是 T 类型的。
像上面直接用注释的形式t : T t:T t : T 标出项的类型的语言称为显式类型化语言 。要求类型检查其自己推导类型的称为隐式类型化语言 。显然我们主要讨论前者。
定义抽象类型的推导规则:
x : T 1 ⊢ t 2 : T 2 ⊢ λ x : T 1 : t 2 : T 1 → T 2 \frac{x:T_1\vdash t_2:T_2}{\vdash \lambda x:T_1:t_2:T_1\rightarrow T_2}
⊢ λ x : T 1 : t 2 : T 1 → T 2 x : T 1 ⊢ t 2 : T 2
中文说就是,如果确定参数 x 的类型为T 1 T_1 T 1 可以推导出函数体t 2 t_2 t 2 会返回一个T 2 T_2 T 2 类型的话,那么抽象λ x : T 1 : t 2 \lambda x:T_1:t_2 λ x : T 1 : t 2 也可以被推导出是一个T 1 → T 2 T_1\rightarrow T_2 T 1 → T 2 的函数。
定义 ,一个类型环境(或称类型化的上下文)Γ \Gamma Γ 是一个 变量 + 类型的序列。而逗号表示引入新的变量 + 类型来扩展Γ \Gamma Γ 。
譬如:Γ : { x : N a t } \Gamma:\{x:Nat\} Γ : { x : N a t } ,则有Γ ⊢ i s z r o ( x ) : B o o l \Gamma\vdash iszro(x):Bool Γ ⊢ i s z r o ( x ) : B o o l 。相当于整了个假设大前提。显然∅ ⊢ { t r u e : B o o l } \emptyset\vdash\{true:Bool\} ∅ ⊢ { t r u e : B o o l } ,可以简写省略空集符号。
我们用d o m ( Γ ) dom(\Gamma) d o m ( Γ ) 表示Γ \Gamma Γ 中规定了类型的变量的集合。
抽象的类型规则一般表示为:
Γ , x : T 1 ⊢ t 2 : T 2 Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 ( T − A b s ) \frac{\Gamma,x:T_1\vdash t_2:T_2}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad (T-Abs)
Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 Γ , x : T 1 ⊢ t 2 : T 2 ( T − A b s )
中文说就是,如果Γ ∪ { x : T 1 } \Gamma\cup\{x:T_1\} Γ ∪ { x : T 1 } 下可以推出t 2 : T 2 t_2:T_2 t 2 : T 2 ,那么Γ \Gamma Γ 下就可以推出λ x : T 1 . t 2 : T 1 → T 2 \lambda x:T_1.t_2:T_1\rightarrow T_2 λ x : T 1 . t 2 : T 1 → T 2 。
根据定义,也有:
x : T ∈ Γ Γ ⊢ x : T ( T − V a r ) \frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad(T-Var)
Γ ⊢ x : T x : T ∈ Γ ( T − V a r )
前提x : T ∈ Γ x:T\in\Gamma x : T ∈ Γ 读作 “在Γ \Gamma Γ 中假设 x 的类型为 T”。
定义应用的类型规则:
Γ ⊢ t 1 : T 1 → T 2 Γ ⊢ t 2 : T 1 Γ ⊢ t 1 t 2 : T 2 ( T − A p p ) \frac{\Gamma\vdash t_1:T_1\rightarrow T_2\quad\Gamma\vdash t_2:T_1}{\Gamma\vdash t_1\;t_2:T_2}\quad(T-App)
Γ ⊢ t 1 t 2 : T 2 Γ ⊢ t 1 : T 1 → T 2 Γ ⊢ t 2 : T 1 ( T − A p p )
纯简单类型 lambda 演算的语法定义:t : : = x ∣ λ x : T . t ∣ t t v : : = λ x : T . t T : : = T → T Γ : : = ∅ ∣ Γ , x : T t::=x|\lambda x:T.t|t\;t\\
v::=\lambda x:T.t\\
T::=T\rightarrow T\\
\Gamma::=\emptyset|\Gamma,x:T
t : : = x ∣ λ x : T . t ∣ t t v : : = λ x : T . t T : : = T → T Γ : : = ∅ ∣ Γ , x : T
语义定义:t 1 → t 1 ′ t 1 t 2 → t 1 ′ t 2 ( E − A p p 1 ) t 2 → t 2 ′ v 1 t 2 → v 1 t 2 ′ ( E − A p p 2 ) ( λ x : T 1 . t 1 ) v 2 → [ x ↦ v 2 ] t 1 ( E − A p p A b s ) x : T ∈ Γ Γ ⊢ x : T ( T − V a r ) Γ , x : T 1 ⊢ t 2 : T 2 Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 ( T − A b s ) Γ ⊢ t 1 : T 1 → T 2 Γ ⊢ t 2 : T 1 Γ ⊢ t 1 t 2 : T 2 ( T − A p p ) \frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\quad(E-App_1)\\
\frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\quad(E-App_2)\\
(\lambda x:T_1.t_1)\;v_2\rightarrow [x\mapsto v_2]t_1\quad(E-AppAbs)\\
\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad(T-Var)\\
\frac{\Gamma,x:T_1\vdash t_2:T_2}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad (T-Abs)\\
\frac{\Gamma\vdash t_1:T_1\rightarrow T_2\quad\Gamma\vdash t_2:T_1}{\Gamma\vdash t_1\;t_2:T_2}\quad(T-App)\\
t 1 t 2 → t 1 ′ t 2 t 1 → t 1 ′ ( E − A p p 1 ) v 1 t 2 → v 1 t 2 ′ t 2 → t 2 ′ ( E − A p p 2 ) ( λ x : T 1 . t 1 ) v 2 → [ x ↦ v 2 ] t 1 ( E − A p p A b s ) Γ ⊢ x : T x : T ∈ Γ ( T − V a r ) Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 Γ , x : T 1 ⊢ t 2 : T 2 ( T − A b s ) Γ ⊢ t 1 t 2 : T 2 Γ ⊢ t 1 : T 1 → T 2 Γ ⊢ t 2 : T 1 ( T − A p p )
我们用λ → \lambda_\rightarrow λ → 来表示简单类型的 lambda 演算。
# 类型的性质
定理 ,类型唯一性:在一个给定的类型环境Γ \Gamma Γ 中,一个项 t (F V ( t ) ∈ d o m ( Γ ) FV(t)\in dom(\Gamma) F V ( t ) ∈ d o m ( Γ ) ),至多有一个类型。
定理 [进展]:若 t 是一个封闭的,良类型的项(即存在 T,使得⊢ t : T \vdash t:T ⊢ t : T ),则 t 要么是一个值,要么存在t ′ t' t ′ 使t → t ′ t\rightarrow t' t → t ′ 。
引理 [置换]:如果Γ ⊢ t : T \Gamma\vdash t:T Γ ⊢ t : T ,Δ \Delta Δ 是Γ \Gamma Γ 的一个置换,则Δ ⊢ t : T \Delta\vdash t:T Δ ⊢ t : T 。(感觉是废话,因为集合是无序的)
引理 [弱化]:如果Γ ⊢ t : T \Gamma\vdash t:T Γ ⊢ t : T 且x ∉ d o m ( Γ ) x\notin dom(\Gamma) x ∈ / d o m ( Γ ) ,则Γ , x : S ⊢ t : T \Gamma,x:S\vdash t:T Γ , x : S ⊢ t : T 。(即加了个没用的绑定)
引理 [类型在代换下保持]:如果Γ , x : S ⊢ t : T \Gamma,x:S\vdash t:T Γ , x : S ⊢ t : T 且Γ ⊢ s : S \Gamma\vdash s:S Γ ⊢ s : S ,则Γ ⊢ [ x ↦ s ] t : T \Gamma\vdash[x\mapsto s]t:T Γ ⊢ [ x ↦ s ] t : T 。
定理 [保持]:如果Γ ⊢ t : T \Gamma\vdash t:T Γ ⊢ t : T 且t → t ′ t\rightarrow t' t → t ′ ,则Γ ⊢ t ′ : T \Gamma\vdash t':T Γ ⊢ t ′ : T 。
# Curry-Howard 对应
# 抹除和类型性
可以定义 erase 函数去抹除对项的类型注释:
e r a s e ( x ) = x e r a s e ( λ x : T 1 . t 2 ) = λ x . e r a s e ( t 2 ) e r a s e ( t 1 t 2 ) = e r a s e ( t 1 ) e r a s e ( t 2 ) erase(x)=x\\
erase(\lambda x:T_1.t_2)=\lambda x.erase(t_2)\\
erase(t_1\;t_2)=erase(t_1)\;erase(t_2)
e r a s e ( x ) = x e r a s e ( λ x : T 1 . t 2 ) = λ x . e r a s e ( t 2 ) e r a s e ( t 1 t 2 ) = e r a s e ( t 1 ) e r a s e ( t 2 )
定理 ,若t → t ′ t\rightarrow t' t → t ′ ,则e r a s e ( t ) → e r a s e ( t ′ ) erase(t)\rightarrow erase(t') e r a s e ( t ) → e r a s e ( t ′ ) 。若e r a s e ( t ) → m erase(t)\rightarrow m e r a s e ( t ) → m ,则存在t ′ t' t ′ ,使得t → t ′ , e r a s e ( t ′ ) = m t\rightarrow t',erase(t')=m t → t ′ , e r a s e ( t ′ ) = m 。
定义 ,无类型 lambda 演算中一个项 m,如果存在某个简单类型项 t,类型 T 和上下文Γ \Gamma Γ 使得e r a s e ( t ) = m erase(t)=m e r a s e ( t ) = m 且Γ ⊢ t : T \Gamma\vdash t:T Γ ⊢ t : T ,则 m 在λ → \lambda_\rightarrow λ → 中是可类型化的 。
# 简单扩展
我们用 A 表示基本类型 (String,Float,Nat,Bool 等),用 Unit 表示单位类型 。于是有扩展:T : : = . . . ∣ A ∣ U n i t t : : = . . . ∣ u n i t v : : = . . . ∣ u n i t − − − − − − − − − − − − − − − − Γ ⊢ u n i t : U n i t t 1 ; t 2 = ( λ x : U n i t . t 2 ) t 1 , x ∉ F V ( t 2 ) T::=...|A|Unit\\
t::=...|unit\\
v::=...|unit\\
----------------\\
\Gamma\vdash unit:Unit\\
t_1;t_2=(\lambda x:Unit.t_2)\;t_1,x\notin FV(t_2)
T : : = . . . ∣ A ∣ U n i t t : : = . . . ∣ u n i t v : : = . . . ∣ u n i t − − − − − − − − − − − − − − − − Γ ⊢ u n i t : U n i t t 1 ; t 2 = ( λ x : U n i t . t 2 ) t 1 , x ∈ / F V ( t 2 )
Unit 的作用类似于 C 和 Java 中的 void 类型。
# 序列和通配符
t 1 → t 1 ′ t 1 ; t 2 → t 1 ′ ; t 2 ( E − S e q ) u n i t ; t 2 → t 2 Γ ⊢ t 1 : U n i t Γ ⊢ t 2 : T 2 Γ ⊢ t 1 ; t 2 : T 2 ( T − S e q ) \frac{t_1\rightarrow t_1'}{t_1;t_2\rightarrow t_1';t_2}\quad(E-Seq)\\
unit;t_2\rightarrow t_2\\
\frac{\Gamma\vdash t_1:Unit\quad \Gamma\vdash t_2:T_2}{\Gamma\vdash t_1;t_2:T_2}\quad(T-Seq)
t 1 ; t 2 → t 1 ′ ; t 2 t 1 → t 1 ′ ( E − S e q ) u n i t ; t 2 → t 2 Γ ⊢ t 1 ; t 2 : T 2 Γ ⊢ t 1 : U n i t Γ ⊢ t 2 : T 2 ( T − S e q )
这时候,会发现这个求值规则实际上是符合t 1 ; t 2 = ( λ x : U n i t . t 2 ) t 1 t_1;t_2=(\lambda x:Unit.t_2)\;t_1 t 1 ; t 2 = ( λ x : U n i t . t 2 ) t 1 的定义的。我们可以把序列看作这样一个 λ 抽象的缩写。
定理 ,用λ E \lambda^E λ E 表示带序列的简单类型 lambda 演算,λ I \lambda^I λ I 表示只带 Unit 类型的简单类型 lambda 演算。
设e ∈ λ E → λ I e\in\lambda^E\rightarrow\lambda^I e ∈ λ E → λ I ,e 表示用( λ x : U n i t . t 2 ) t 1 (\lambda x:Unit.t_2)\;t_1 ( λ x : U n i t . t 2 ) t 1 去替换t 1 ; t 2 t_1;t_2 t 1 ; t 2 。于是对λ E \lambda^E λ E 中的每个项,都有:
t → E t ′ t\rightarrow_E t' t → E t ′ 当且仅当e ( t ) → I e ( t ′ ) e(t)\rightarrow_I e(t') e ( t ) → I e ( t ′ ) 。
Γ ⊢ E t : T \Gamma\vdash^E t:T Γ ⊢ E t : T 当且仅当Γ ⊢ I e ( t ) : T \Gamma\vdash^I e(t):T Γ ⊢ I e ( t ) : T 。
其实序列是我们写程序时常用的顺序结构。上述定理说明了序列可以用更基本的类型和求值行为推导出。注意到我们用λ I \lambda^I λ I 去替换序列时,有要求x ∉ F V ( t 2 ) x\notin FV(t_2) x ∈ / F V ( t 2 ) ,所以有时候也会写成( λ _ : U n i t . t 2 ) t 1 (\lambda\_:Unit.t_2)\;t_1 ( λ _ : U n i t . t 2 ) t 1 ,
# 归属
定义 “将类型 T 归属到项 t”:
t : : = . . . ∣ t a s T t::=...|t\;as\;T
t : : = . . . ∣ t a s T
定义对应的求值规则:
v 1 a s T → v 1 ( E − A s c r i b e ) t 1 → t 1 ′ t 1 a s T → t 1 ′ a s T ( E − A s c r i b e 1 ) v_1\;as\;T\rightarrow v_1\quad(E-Ascribe)\\
\frac{t_1\rightarrow t_1'}{t_1\;as\;T\rightarrow t_1'\;as\;T}\quad (E-Ascribe1)\\
v 1 a s T → v 1 ( E − A s c r i b e ) t 1 a s T → t 1 ′ a s T t 1 → t 1 ′ ( E − A s c r i b e 1 )
定义对应的类型规则:
Γ ⊢ t 1 : T Γ ⊢ t 1 a s T : T ( T − A s c r i b e ) \frac{\Gamma\vdash t_1:T}{\Gamma\vdash t_1\;as\;T:T}\quad(T-Ascribe)
Γ ⊢ t 1 a s T : T Γ ⊢ t 1 : T ( T − A s c r i b e )
归属可以用来做 typedef。譬如:
U U a s U n i t → U n i t ; ( λ f : U U . f u n i t ) ( λ x : U n i t . x ) ; UU\;as\;Unit\rightarrow Unit;\\
(\lambda f:UU.f\;unit)(\lambda x:Unit.x);
U U a s U n i t → U n i t ; ( λ f : U U . f u n i t ) ( λ x : U n i t . x ) ;
就可以很容易推导出:( λ f : U U . f u n i t ) ( λ x : U n i t . x ) : U n i t (\lambda f:UU.f\;unit)(\lambda x:Unit.x):Unit ( λ f : U U . f u n i t ) ( λ x : U n i t . x ) : U n i t
# let 绑定
语法定义:
t : : = . . . ∣ l e t x = t i n t t::=...|let\;x=t\; in\;t
t : : = . . . ∣ l e t x = t i n t
求值规则:
l e t x = v 1 i n t 2 → [ x ↦ v 1 ] t 2 ( E − L E T V ) t 1 → t 1 ′ l e t x = t 1 i n t 2 → l e t x = t 1 ′ i n t 2 ( E − L E T ) let\;x=v_1\;in\;t_2\rightarrow [x\mapsto v_1]t_2\quad(E-LETV)\\
\frac{t_1\rightarrow t_1'}{let\;x=t_1\;in\;t_2\rightarrow let\;x=t_1'\;in\;t_2}\quad(E-LET)
l e t x = v 1 i n t 2 → [ x ↦ v 1 ] t 2 ( E − L E T V ) l e t x = t 1 i n t 2 → l e t x = t 1 ′ i n t 2 t 1 → t 1 ′ ( E − L E T )
类型规则:
Γ ⊢ t 1 : T 1 Γ , x : T 1 ⊢ t 2 : T 2 l e t x = t 1 i n t 2 : T 2 ( T − L E T ) \frac{\Gamma\vdash t_1:T_1\quad\Gamma,x:T_1\vdash t_2:T_2}{let\;x=t_1\;in\;t_2:T_2}\quad(T-LET)
l e t x = t 1 i n t 2 : T 2 Γ ⊢ t 1 : T 1 Γ , x : T 1 ⊢ t 2 : T 2 ( T − L E T )
这东西的理解,首先应该把它看成l e t ( x = t 1 ) i n t 2 let\;(x=t_1)\;in\;t_2 l e t ( x = t 1 ) i n t 2 ,意思为在表达式t 2 t_2 t 2 中,绑定x x x 为t 1 t_1 t 1 的求值。譬如l e t x = 3 + 5 i n x − 2 let\;x=3+5\;in\;x-2 l e t x = 3 + 5 i n x − 2 。
也可以用一个 lambda 抽象来等价地表示它:l e t x = t 1 i n t 2 = ( λ x : T 1 . t 2 ) t 1 let\;x=t_1\;in\;t_2=(\lambda x:T_1.t_2)\;t_1 l e t x = t 1 i n t 2 = ( λ x : T 1 . t 2 ) t 1 。
在出现 let 绑定时,类型检查器一定会有一个推导:
. . . Γ ⊢ t 1 : T 1 . . . Γ , x : T 1 ⊢ t 2 : T 2 l e t x = t 1 i n t 2 : T 2 ( T − L E T ) \frac{\frac{...}{\Gamma\vdash t_1:T_1}\quad\frac{...}{\Gamma,x:T_1\vdash t_2:T_2}}{let\;x=t_1\;in\;t_2:T_2}\quad(T-LET)
l e t x = t 1 i n t 2 : T 2 Γ ⊢ t 1 : T 1 . . . Γ , x : T 1 ⊢ t 2 : T 2 . . . ( T − L E T )
这个推导就对应了 lambda 抽象的一个推导:
. . . Γ , x : T 1 ⊢ t 2 : T 2 Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 . . . Γ ⊢ t 1 : T 1 Γ ⊢ ( λ x : T 1 . T 2 ) t 1 : T 2 \frac{\frac{\frac{...}{\Gamma,x:T_1\vdash t_2:T_2}}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad\frac{...}{\Gamma\vdash t_1:T_1}}{\Gamma\vdash(\lambda x:T_1.T_2)\;t_1:T_2}
Γ ⊢ ( λ x : T 1 . T 2 ) t 1 : T 2 Γ ⊢ λ x : T 1 . t 2 : T 1 → T 2 Γ , x : T 1 ⊢ t 2 : T 2 . . . Γ ⊢ t 1 : T 1 . . .
# 序对
语法定义:
t : : = . . . ∣ { t , t } ∣ t . 1 ∣ t . 2 v : : = . . . ∣ { v , v } T : : = T 1 × T 2 t::=...|\{t,t\}|t.1|t.2\\
v::=...|\{v,v\}\\
T::=T_1\times T_2
t : : = . . . ∣ { t , t } ∣ t . 1 ∣ t . 2 v : : = . . . ∣ { v , v } T : : = T 1 × T 2
求值规则:
{ v 1 , v 2 } . 1 → v 1 ( E − P A I R B E T A 1 ) { v 1 , v 2 } . 2 → v 2 ( E − P A I R B E T A 2 ) t 1 → t 1 ′ t 1 . 1 → t 1 ′ . 1 ( E − P R O J 1 ) t 1 → t 1 ′ t 1 . 2 → t 1 ′ . 2 ( E − P R O J 2 ) t 1 → t 1 ′ { t 1 , t 2 } → { t 1 ′ , t 2 } ( E − P A I R 1 ) t 2 → t 2 ′ { v 1 , t 2 } → { v 1 , t 2 ′ } ( E − P A I R 2 ) \{v_1,v_2\}.1\rightarrow v_1\quad(E-PAIRBETA1)\\
\{v_1,v_2\}.2\rightarrow v_2\quad(E-PAIRBETA2)\\
\frac{t_1\rightarrow t_1'}{t_1.1\rightarrow t_1'.1}\quad(E-PROJ1)\\
\frac{t_1\rightarrow t_1'}{t_1.2\rightarrow t_1'.2}\quad(E-PROJ2)\\
\frac{t_1\rightarrow t_1'}{\{t_1,t_2\}\rightarrow\{t_1',t_2\}}\quad(E-PAIR1)\\
\frac{t_2\rightarrow t_2'}{\{v_1,t_2\}\rightarrow\{v_1,t_2'\}}\quad(E-PAIR2)
{ v 1 , v 2 } . 1 → v 1 ( E − P A I R B E T A 1 ) { v 1 , v 2 } . 2 → v 2 ( E − P A I R B E T A 2 ) t 1 . 1 → t 1 ′ . 1 t 1 → t 1 ′ ( E − P R O J 1 ) t 1 . 2 → t 1 ′ . 2 t 1 → t 1 ′ ( E − P R O J 2 ) { t 1 , t 2 } → { t 1 ′ , t 2 } t 1 → t 1 ′ ( E − P A I R 1 ) { v 1 , t 2 } → { v 1 , t 2 ′ } t 2 → t 2 ′ ( E − P A I R 2 )
类型规则:
Γ ⊢ t 1 : T 1 Γ ⊢ t 2 : T 2 Γ ⊢ { t 1 , t 2 } : T 1 × T 2 ( T − P A I R ) Γ ⊢ t 1 : T 1 × T 2 Γ ⊢ t 1 . 1 : T 1 ( T − P R O J 1 ) Γ ⊢ t 1 : T 1 × T 2 Γ ⊢ t 1 . 2 : T 2 ( T − P R O J 2 ) \frac{\Gamma\vdash t_1:T_1\quad \Gamma\vdash t_2:T_2}{\Gamma\vdash\{t_1,t_2\}:T_1\times T_2}\quad(T-PAIR)\\
\frac{\Gamma\vdash t_1:T_1\times T_2}{\Gamma\vdash t_1.1:T_1}\quad(T-PROJ1)\\
\frac{\Gamma\vdash t_1:T_1\times T_2}{\Gamma\vdash t_1.2:T_2}\quad(T-PROJ2)\\
Γ ⊢ { t 1 , t 2 } : T 1 × T 2 Γ ⊢ t 1 : T 1 Γ ⊢ t 2 : T 2 ( T − P A I R ) Γ ⊢ t 1 . 1 : T 1 Γ ⊢ t 1 : T 1 × T 2 ( T − P R O J 1 ) Γ ⊢ t 1 . 2 : T 2 Γ ⊢ t 1 : T 1 × T 2 ( T − P R O J 2 )
这就是平常用的 C++ 里的 pair。用它可以扩展成元组,数组。要注意的是,无论求 1 还是 2,或者代入函数时,都必须把两项都算出值:
( λ x : N a t × N a t . x . 2 ) { p r e d 4 , p r e d 5 } → ( λ x : N a t × N a t . x . 2 ) { 3 , p r e d 5 } → ( λ x : N a t × N a t . x . 2 ) { 3 , 4 } → { 3 , 4 } . 2 → 2 (\lambda x:Nat\times Nat.x.2)\{pred\;4,pred\;5\}\\
\rightarrow(\lambda x:Nat\times Nat.x.2)\{3,pred\;5\}\\
\rightarrow(\lambda x:Nat\times Nat.x.2)\{3,4\}\\
\rightarrow\{3,4\}.2\\
\rightarrow 2
( λ x : N a t × N a t . x . 2 ) { p r e d 4 , p r e d 5 } → ( λ x : N a t × N a t . x . 2 ) { 3 , p r e d 5 } → ( λ x : N a t × N a t . x . 2 ) { 3 , 4 } → { 3 , 4 } . 2 → 2
# 元组
语法定义:
t : : = . . . ∣ { t i , i ∈ 1.. n } ∣ t . i v : : = { v i , i ∈ 1.. n } T : : = { T i , i ∈ 1.. n } t::=...|\{t_i,i\in1..n\}|t.i\\
v::=\{v_i,i\in1..n\}\\
T::=\{T_i,i\in1..n\}
t : : = . . . ∣ { t i , i ∈ 1 . . n } ∣ t . i v : : = { v i , i ∈ 1 . . n } T : : = { T i , i ∈ 1 . . n }
求值规则:
{ v i , i ∈ 1.. n } . j → v j t 1 → t 1 ′ t 1 . i → t 1 ′ . i t j → t j ′ { v i , i ∈ 1.. j − 1 , v j , v i , i ∈ j + 1.. n } → { v i , i ∈ 1.. j − 1 , v j ′ , v i , i ∈ j + 1.. n } \{v_i,i\in1..n\}.j\rightarrow v_j\\
\frac{t_1\rightarrow t_1'}{t_1.i\rightarrow t_1'.i}\\
\frac{t_j\rightarrow t_j'}{\{v_i,i\in1..j-1,v_j,v_i,i\in j+1..n\}\rightarrow\{v_i,i\in1..j-1,v_j',v_i,i\in j+1..n\}}
{ v i , i ∈ 1 . . n } . j → v j t 1 . i → t 1 ′ . i t 1 → t 1 ′ { v i , i ∈ 1 . . j − 1 , v j , v i , i ∈ j + 1 . . n } → { v i , i