_rqy's Blog

一只猫猫,想成为天才少女数学家!

0%

类型论学习笔记 (0) 入门科普

大概从这篇 Blog 开始会写一系列学习笔记,以 Type Theory 为中心写一些学习时的问题和得到的解答,也可能会作为半科普or入门读物。术语的中文翻译基本上都是从 Software-Foundation 那里看来的。

在此感谢 千里冰封 耐心解答我的问题。

作为第 0 篇 Blog,这里是科普文章。求 dalao 轻喷。


类型论和集合论类似,是一类公理体系。其研究对象是term) 以及它们的类型type)。

为了理解什么是类型论,我们造一个没有用的玩具语言。

简单的例子

文字叙述

这种语言只有 Bool{\bf Bool}Int{\bf Int} 两种类型,而项可以由数字、True{\rm True}False{\rm False}if b then u else v{\rm if}\ b\ {\rm then}\ u \ {\rm else}\ v 以及加减来表示(当然补充上乘除也可以,为了方便这里只使用加减)。

我们有一些推导规则:

  1. 任何一个整数属于 Int{\bf Int} 类型;
  2. True{\rm True}False{\rm False} 属于 Bool{\bf Bool} 类型;
  3. 如果 aa, bb 都属于 Int{\bf Int} 类型,那么 a+ba+b 属于 Int{\bf Int} 类型,aba-b 属于 Int{\bf Int} 类型。
  4. 如果 bb 属于 Bool{\bf Bool} 类型,而 u,vu,v 都属于 TT 类型(注意 TT 是不固定的),那么 if b then u else v{\rm if}\ b\ {\rm then}\ u\ {\rm else}\ v 属于 TT 类型。

比如,1414 属于 Int{\bf Int}99 属于 Int{\bf Int},因此 14+914+9 属于 Int{\bf Int},这是由第 3 条规则推导而出的。

注意到这个语言中会有“不合法”的项,比如 if 13 then 5 else 4{\rm if}\ 13\ {\rm then}\ 5\ {\rm else}\ 4,显然它类型不正确。我们称所有具有某种类型的项为 良类型 的(well-typed)。

这个语言没有什么用处,但是可以让我们认识到类型论中的一些记法。

形式化叙述

以文字来叙述规则在系统更复杂的时候很容易出问题,所以以形式化的语言来叙述是有必要的。

a:Ta:T 表示项 aa 属于类型 TTa:T\vdash a:T 表示“我们可以推断出 a:Ta:T”的事实。\vdash 叫做十字转门(turnstile,翻译好像是直译),之后我们会在它左边添加“上下文”,但是现在它左边总是空的。

我们可以把推导规则写成下面的形式:

v is a numberv:Int(NUM)True:Bool(TRUE)False:Bool(FALSE)\cfrac{v{\rm\ is\ a\ number}}{\vdash v:{\bf Int}}{\rm\tiny(NUM)} \qquad\cfrac{}{\vdash {\rm True}:{\bf Bool}}{\rm\tiny(TRUE)} \qquad\cfrac{}{\vdash {\rm False}:{\bf Bool}}{\rm\tiny(FALSE)} a:Intb:Inta+b:Int(PLUS)a:Intb:Intab:Int(MINUS)b:Boolu:Tv:T(if b then u else v):T(IF)\cfrac{\vdash a:{\bf Int}\quad\vdash b:{\bf Int}}{\vdash a+b:{\bf Int}}{\rm\tiny(PLUS)} \qquad\cfrac{\vdash a:{\bf Int}\quad\vdash b:{\bf Int}}{\vdash a-b:{\bf Int}}{\rm\tiny(MINUS)} \quad\cfrac{\vdash b:{\bf Bool}\quad\vdash u:T\quad\vdash v:T}{\vdash ({\rm if}\ b\ {\rm then}\ u\ {\rm else}\ v):T}{\rm\tiny(IF)}

这里我们用一条横线表示从上至下的推导,横线上方会有若干个前提条件(也可能没有,比如这里的 (TRUE) 规则),而横线下方会有一个结论。横线右边的标记表示这条规则的名字。这样就表示一条推导规则inference rule)。

这样写的好处在于,我们可以通过一条一条横线叠加来证明一条结论。比如我们要证明 (if True then (14+5) else 3):Int({\rm if\ True\ then}\ (14+5)\ {\rm else}\ 3):{\bf Int},就可以这样写:

True:Bool(TRUE)14 is a number14:Int(NUM)5 is a number5:Int(NUM)(14+5):Int(PLUS)3 is a number3:Int(NUM)(if True then (14+5) else 3):Int(IF)\cfrac{ \cfrac{}{\vdash {\rm True}:{\bf Bool}}{\rm\tiny(TRUE)} \quad\cfrac{ \cfrac{14{\rm\ is\ a\ number}}{\vdash 14:{\bf Int}}{\rm\tiny(NUM)} \quad\cfrac{5{\rm\ is\ a\ number}}{\vdash 5:{\bf Int}}{\rm\tiny(NUM)} }{\vdash (14+5):{\bf Int}}{\rm\tiny(PLUS)} \quad\cfrac{3{\rm\ is\ a\ number}}{\vdash 3:{\bf Int}}{\rm\tiny(NUM)} }{\vdash ({\rm if\ True\ then}\ (14+5)\ {\rm else}\ 3):{\bf Int}}{\rm\tiny(IF)}

当然这样逐字的写出证明来很无聊也很麻烦。

归约

项的归约reduction)是一系列规则,用来描述一个项如何“化简”。比如这里我们可以定义一些规则:

if True then u else vu(IF_TRUE)if False then u else vv(IF_FALSE)n1+n2the number (n1+n2)(PLUS_NUM)n1n2the number (n1n2)(MINUS_NUM)\begin{aligned} {\rm if\ True\ then}\ u\ {\rm else}\ v&\twoheadrightarrow u&{\rm\tiny(IF\_TRUE)}\\ {\rm if\ False\ then}\ u\ {\rm else}\ v&\twoheadrightarrow v&{\rm\tiny(IF\_FALSE)}\\ n_1+n_2&\twoheadrightarrow {\rm the\ number }\ (n_1+n_2)&{\rm\tiny(PLUS\_NUM)}\\ n_1-n_2&\twoheadrightarrow {\rm the\ number }\ (n_1-n_2)&{\rm\tiny(MINUS\_NUM)}\\ \end{aligned}

(其中 n1,n2n_1,n_2 是两个整数)

实际上我们可以对一个项的任何子项做这样的归约,读者可以自行思考具体定义(无非就是 aaa\twoheadrightarrow a'a+ba+ba+b\twoheadrightarrow a'+b 这种规则)。

如果两个项 a,ba,b 可以归约到同一个项,那么记它们两个相等,记做 a=ba=b。为了与此区分,两个项完全相同,即句法等价syntactically equivalent),也就是不需要归约地相同时记做 aba\equiv b

这里没有给出归约的严谨定义,具体可以去看相关书籍。

需要注意的是,一个项归约之后是另一个项,当 a 规约为 b 的时候不能直接b:T\vdash b:T 推出 a:T\vdash a:T 或者反过来。但是在我们的玩具语言中,可以证明若 a\vdash aT;abT;a\twoheadrightarrow b,则 b:T\vdash b:T。反过来是可以的,因为 if-else 里面的 u 和 v 必须是同一个类型,而归约之后可能丢掉其中一个。

这并不是公理,而是从 reduction rule 和 inference rule 得到的。

上下文

注意这个语言是很无趣的,因为一个 well-typed 的项总可以归约到一个数或者 True 或者 False。

但是当我们在语言中添加“变量”的时候,它就不同了。比如我们可以写 if b then False else True{\rm if}\ b\ {\rm then\ False\ else\ True},可以发现这其实就是 not b{\rm not}\ b。因此我们补充语言的定义:一个项也可以包含变量variable)。

但是这样问题来了:我们没有任何方式判定一个变量应当是什么类型。

那么我们就可以有一个上下文的概念:我们钦定一个(或一些)变量的类型,把它写在 \vdash 左侧。这些钦定的条件叫做上下文环境context),一般用 Γ,Δ\Gamma,\Delta 这些大写希腊字母表示,它实际上是一系列变量的类型限制,比如 Γ::=x:Int,b:Bool\Gamma::=x:{\bf Int},b:{\bf Bool} 这样。当然既然类型都可以钦定了,我们也自然地想到可以钦定一些不确定的类型,比如 x:A,y:Bx:A,y:B 这样。

于是记 Γa:T\Gamma\vdash a:T 表示“在 Γ\Gamma 这个上下文下,aa 的类型是 TT”。比如我们可以自然的认为应该有

b:Bool(if b then False else True):Boolb:{\bf Bool}\vdash({\rm if}\ b\ {\rm then\ False\ else\ True}):{\bf Bool}

这样的话类型推导规则需要修改如下:

(x:A)ΓΓx:A(VAR)v is a numberΓv:Int(NUM)ΓTrue:Bool(TRUE)ΓFalse:Bool(FALSE)\cfrac{(x:A)\in \Gamma}{\Gamma\vdash x:A}{\rm\tiny(VAR)} \qquad\cfrac{v{\rm\ is\ a\ number}}{\Gamma\vdash v:{\bf Int}}{\rm\tiny(NUM)} \qquad\cfrac{}{\Gamma\vdash {\rm True}:{\bf Bool}}{\rm\tiny(TRUE)} \qquad\cfrac{}{\Gamma\vdash {\rm False}:{\bf Bool}}{\rm\tiny(FALSE)} Γa:IntΓb:IntΓa+b:Int(PLUS)Γa:IntΓb:IntΓab:Int(MINUS)Γb:BoolΓu:TΓv:TΓ(if b then u else v):T(IF)\cfrac{\Gamma\vdash a:{\bf Int}\quad\Gamma\vdash b:{\bf Int}}{\Gamma\vdash a+b:{\bf Int}}{\rm\tiny(PLUS)} \qquad\cfrac{\Gamma\vdash a:{\bf Int}\quad\Gamma\vdash b:{\bf Int}}{\Gamma\vdash a-b:{\bf Int}}{\rm\tiny(MINUS)} \quad\cfrac{\Gamma\vdash b:{\bf Bool}\quad\Gamma\vdash u:T\quad\Gamma\vdash v:T}{\Gamma\vdash ({\rm if}\ b\ {\rm then}\ u\ {\rm else}\ v):T}{\rm\tiny(IF)}

简单的说,我们要求前提条件和推导出的结论中的上下文都是相同的(以后我们会遇到不同的情况),并且加了一条规则:当我们钦定 x:Ax:A 的时候我们就可以得到 x:Ax:A。这样我们就可以推导出

b:Bool,u:Int(if b then (u+13) else 7):Intb:Bool,u:T(if b then u else u):T{b:{\bf Bool}, u:{\bf Int}\vdash ({\rm if}\ b\ {\rm then}\ (u+13)\ {\rm else}\ 7):{\bf Int}}\\ {b:{\bf Bool}, u:T\vdash ({\rm if}\ b\ {\rm then}\ u\ {\rm else}\ u):T}

这些trivial的事实。

λ\lambda 演算及 λ\lambda_\to 类型系统

λ\lambda 演算是许多类型论的基础。我们先叙述其定义,再叙述其归约规则,之后给出其上的一个类型系统,即λ\lambda_\to 系统。

定义

λ\lambda 演算中一个项的定义为 t::=xt1t2λx.tt::= x \mid t_1 t_2\mid\lambda x.t。也就是说,每个项或者是一个变量,或者是两个项拼起来,或者是形如 λx.t\lambda x.t 的形式,其中 xx 是一个变量而 tt 是另一个项。当然是可以加括号的。 t1t2t_1t_2 这种形式称为**应用**(*application*)。想象 t1t_1 表示一个函数而 t2t_2 表示函数参数,那么 t1t2t_1t_2 就表示函数应用。这东西是左结合的,也就是说当我们写下 t1t2t3tnt_1t_2t_3\dots t_n的时候,我们实际上在说 (((t1t2)t3))tn((\dots(t_1t_2)t_3)\dots)t_nλx.t\lambda x.t 称为**抽象**(*abstraction*)。直观的说,它表示一个函数,当传入一个参数 NN 的时候,得到的是 t[x:=N]t[x:=N](这个记号大概是说是把 tt 里面的 xx 都换成 NN)。这东西优先级比 application 高,也就是说 λx.t1t2\lambda x. t_1t_2 表示 λx.(t1t2)\lambda x. (t_1t_2) 而不是 (λx.t1)t2(\lambda x.t_1)t_2

比方说,λx.λy.x\lambda x.\lambda y. x(表示 λx.(λy.x)\lambda x.(\lambda y.x)),表示“传入一个参数 x0x_0 之后返回一个函数 f=λy.x0f=\lambda y. x_0,这个函数 ff 传入任何一个参数都会返回 x0x_0”,也就是说(λx.λy.x)x0y0=x0(\lambda x.\lambda y.x)x_0y_0=x_0

我们以后不区分这种说法和“传入两个参数 x0,y0x_0,y_0 之后会返回 x0x_0”的说法(这称为柯里化 curry (反义词是 uncurry ))。

当然这只是直观的意义,具体的意义要以归约规则决定。

自由的/绑定了的变量

在介绍归约规则之前,我们先来看自由变量free variable)和绑定了的变量bounded variable)的概念。

一个项里的某个变量 xx 称为自由的当且仅当它没有匹配上某个抽象。比如说 y(λx.x)y (\lambda x. x) 这个项里 yy 是 free 的而 xx 是 bounded 的。同一个名字的变量也可以既有自由的也有约束的,比如 x(λx.x){\color{red}x}(\lambda x. {\color{green}x}) 里红色的 xx 是 free 的而绿色的 xx 是 bounded 的。注意 λ\lambda 后面那个位置不算 xx 出现了,它在这里只是一个记号。

具体地说,单个一个 xx 的项中 xx 是 free 的;t1t2t_1t_2 不会改变其中每个变量是否 free;λx.t\lambda x. t 则会把 tt 中所有的 xx 都 bound 起来,不会影响其他变量。

做一个类比,自由变量就是全局变量而绑定了的变量就是局部变量。

之前我们说 M[x:=N]M[x:=N] 是说把 MM 里的 xx 都换成 NN,现在我们可以表达它的大致准确的意思:我们把所有自由出现的 xx 都替换成 NN,比如 (y(λx.x)x)[x:=(zw)](y(\lambda x. x)x)[x:=(zw)] 就是 y(λx.x)(zw)y(\lambda x.x)(zw)

对于一个 λx.M\lambda x. M,我们可以把 MM 中所有的 free 的 xx 一起改个名字。比如说 λx.xy\lambda x. xy 可以改成 λa.ay\lambda a.ay。这就是接下来要说的 α\alpha-conversion。

α\alpha-conversion

如上所述,我们可以给局部变量改一个名字,比如 λx.xy\lambda x.xy 改成 λa.ay\lambda a.ay,或者 λx.(λx.x)\lambda x.(\lambda x. x) 变成λy.(λx.x)\lambda y.(\lambda x.x)(因为里面的 xx 不是 free 的,所以不需要改)。但是也不是随便改,比如我们不能把 λx.xy\lambda x.xy 改成 λy.yy\lambda y.yy

所以说我们的要求大概是:在 λx.M\lambda x.M 中,如果 MM 中所有 yy 都是 bounded 的(或者根本不出现),那么我们可以把它变成 λy.(M[x:=y])\lambda y. (M[x:=y])。这样的转化叫做 α\alpha-conversion。一般我们认为通过 α\alpha-conversion 能够互相转化的项也是相同的(句法等价的,即 \equiv,而不是可以归约到相同项意义下的相等)。

α\alpha-conversion 的必要性在于,我们在计算 M[x:=N]M[x:=N] 的时候有时候需要对 MM 中别的变量进行更名,比如 (λy.xy)[x:=(yz)](\lambda y. xy)[x:=(yz)] 应该变成 (λa.(yz)a)(\lambda a.(yz)a) 而不能变成 (λy.(yz)y)(\lambda y. (yz)y)。后者会使得本应该 free 出现的 y 被错误地 bound 掉了。

另外还有一个称为 η\eta-conversion 的东西, 大概是说 xx 不在 MM 中 free 出现的时候, λx.MxM\lambda x. Mx\equiv M。这条一般来说是不必要的,但是加上一般也不会出问题。

归约规则

归约规则称为 β\beta-reduction,它也很简单:(λx.M)NM[x:=N](\lambda x.M)N\twoheadrightarrow M[x:=N]。有时候也会记作 β\twoheadrightarrow_\beta

简单的说,就是一个函数应用。等下,这个规则怎么这么简单

这种东西是有一大堆(看上去显然的)性质的,比如如果 MM 能分别归约到 N1N_1N2N_2,那么后两者也一定能归约到完全相同的项。

类似的,如果两个项 M,NM,N 可以归约到完全相同的项,那么就称它们是相等的,记做 M=NM=N 或者 M=βNM=_\beta N

λ\lambda_\to 系统

定义

这是一个很简单但是性质却不是那么简单的类型系统,不同于前面那个仅仅只能用来举例子的玩具语言,有什么性质几乎是一目了然的并且证明也很 trivial。

类型也很简单:一个类型定义为 T::=AT1T2T::=A\mid T_1\to T_2,也就是说一个类型要么是一个 primal 的名字,要么是 T1T2T_1\to T_2 的形式。

ABA\to B 的类型称为**箭头类型**(*arrow type*),直观上表示 AABB 的函数。这个是右结合的,也就是说 ABCA\to B\to C 表示 A(BC)A\to(B\to C)

推导规则

推导规则其实很简单:单独变量的类型是需要钦定的;若 M:AB,N:AM:A\to B,N:A(MN):B(MN):B(也就是函数应用)。λx.M\lambda x.M 的推导则是这样的:如果我们额外钦定 x:Ax:A 的时候 M:BM:B ,那么就可以得到 (λx.M):(AB)(\lambda x. M):(A\to B)

(x:A)ΓΓx:A(VAR)ΓM:(AB)ΓN:AΓ(MN):B(APP)Γ,x:AM:BΓ(λx.M):(AB)(ABS)\cfrac{(x:A)\in\Gamma}{\Gamma\vdash x:A}{\rm\tiny(VAR)} \qquad\cfrac{\Gamma\vdash M:(A\to B)\quad\Gamma\vdash N:A}{\Gamma\vdash (MN):B}{\rm\tiny(APP)} \qquad\cfrac{\Gamma,x:A\vdash M:B}{\Gamma\vdash (\lambda x.M):(A\to B)}{\rm\tiny(ABS)}

(ABS) 规则中 Γ,x:A\Gamma, x:A 是指扩充上下文,补充 x:Ax:A,如果 Γ\Gamma 中本来就有 x:Cx:C 那么就把那个东西去掉(意会一下,里面的局部变量屏蔽了外面的局部变量)。

三条 Inference Rule 就可以得到一个有用的类型系统还是很优美的。比如我们可以这样推导:

x:A,y:Bx:Ax:A(λy.x):(BA)(λx.λy.x):(ABA)\cfrac{\cfrac{x:A,y:B\vdash x:A}{x:A\vdash(\lambda y.x):(B\to A)}}{\vdash (\lambda x.\lambda y.x):(A\to B\to A)}

这两步都使用了 (ABS) 规则。一种简便的写法是不写 Context 和 \vdash 符号,在对某个变量进行抽象的时候把它划掉。比如

{x:A}2{y:B}1x:A(λy.x):(BA)1(λx.λy.x):(ABA)2\cfrac{\cfrac{\cfrac{\{x:A\}^2\quad\{y:B\}^1}{x:A}}{(\lambda y.x):(B\to A)}\small1}{(\lambda x.\lambda y.x):(A\to B\to A)}\small2

由于没法打删除线,请自行想象把花括号改成删除线(

就是说推导到 1 那一步的时候把 y:By:B 划掉(因为这一步之后它就不在上下文里了),2 那一步的时候把 x:Ax:A 划掉。

一些性质

λ\lambda_\to 系统中有一些性质(定理),比如:
  1. ΓM:A\Gamma\vdash M:A,那么 MM 中的自由变量都在 Γ\Gamma 里出现,特别的,如果 M:A\vdash M:A,那么 MM 中不含自由变量;
  2. 如果 ΓM:A,ΓΓ1\Gamma \vdash M:A, \Gamma\subseteq\Gamma_1,则 Γ1M:A\Gamma_1\vdash M:A
  3. ΓM:A,MβM\Gamma\vdash M:A,M\twoheadrightarrow_\beta M',则 ΓM:A\Gamma\vdash M':A (反过来不成立,如 (λy.λx.x)(yy)(\lambda y.\lambda x.x)(yy) 没有类型);
  4. ΓM:A,ΓM:A,M=βM\Gamma\vdash M:A,\Gamma\vdash M':A',M=_\beta M',则 AAA\equiv A'

当然还有好多,这里不再赘述。

柯里-霍华德同构

柯里-霍华德同构Curry-Howard Isomorphism)建立了类型系统和形式逻辑系统之间的对应(类型即命题,程序即证明)。

λ\lambda_\to 类型系统就对应于命题逻辑。考虑每个类型 AA 对应一个命题(也用 AA 表示),ABA\to B 的类型对应 “AA 蕴含 BB” 这个命题。一个项对应命题的一个证明。

这样的话,由于 AA 蕴含 BB 等价于“只要有一个 AA 的证明,就可以构造一个 BB 的证明”,所以这和“给出一个 AA 类型的项,应用这个函数就可以得到一个 BB 类型的项”是等价的。

举个例子,命题逻辑一种仅使用蕴含来表示的公理系统中某两条公理分别是:

A(BA);(A(BC))((AB)(AC))A\to (B\to A);\\ (A\to(B\to C))\to((A\to B)\to(A\to C))

对应到类型上,就可以用如下的项给出:

λx.λy.xλx.λy.λz.xz(yz)\lambda x.\lambda y.x\\ \lambda x.\lambda y.\lambda z.xz(yz)

分离规则

ABAB\cfrac{\vdash A\to B\quad\vdash A}{\vdash B}

也正是 application。

上下文也可以对应起来:类型系统中一个上下文 Γ\Gamma,对应到逻辑系统中就是说 Γ\Gamma 中所有类型作为前提条件。(ABS) 规则也对应了 ABA\vdash BAB\vdash A\to B 的定理。

当我们之后扩展类型系统的时候,就可以用它来对应更复杂的逻辑系统,如高阶命题逻辑、谓词逻辑等。

这里还有一个小问题:命题逻辑中 ¬A\lnot A 应该对应什么?

λ\lambda_\to 中,我们可以扩展类型系统,添加 \bot 类型。它表示“空类型”,即不存在这种类型的项,对应逻辑上的永假命题。并且可以加一条规则:Γx:Γx:A\cfrac{\Gamma\vdash x:\bot}{\Gamma\vdash x:A}。简单的说,如果我们得到了一个空类型的值,就可以得到任意类型的值。对应到逻辑上就是说,如果我们得到了矛盾那就可以导出任何结论。

那么就可以定义 ¬A=A\lnot A=A\to\bot

这样又出现了新的问题:我们不能得到这样的项:¬(¬A)A\lnot(\lnot A)\to A。没有这样的项,就不能进行反证(反证法本质就是证明原命题的否定是假,从而证明原命题为真)。于是添加 \bot 之后 λ\lambda_\to 事实上对应直觉主义逻辑,或者称为构造主义逻辑,因为我们本质上只能构造一个证明,而不能通过排中律(A¬AA\lor\lnot A)、二次互反律(¬(¬A)A\lnot(\lnot A)\to A)来做证明,除非我们把这种类型的项一直放在 Context 里(即,设定为公理)。

总结

这一篇 Blog 大致写了类型系统是什么样子,提供一个入门。但是很多东西是没有完全严格定义的,如果有想了解的可以自己去查资料、找书看。我是看的 Lambda Calculi with Types, Henk Barendregt 入门。

简要解释了 Curry-Howard 同构,它将类型系统与逻辑系统联系起来从而使得形式化验证(即借助计算机来证明定理,可以避免证明错误、并且某些情况下可以通过自动化的步骤来证明一些过程简化证明)成为可能,因为它把寻找一个证明转化成了写一个给定类型的程序。

之后的博客大概会先介绍 Dependent Type、 Lambda Cube 之类的数学基础,然后随着我尝试自己实现一种 DT 的语言来写这之间遇到的问题及解决方案的笔记。