形式语义04 Types

\newcommand\norm[1]{\left\lVert#1\right\rVert} \newcommand\abs[1]{\left\lvert#1\right\rvert}

Types

首先要说明什么是Type

Types可以看成是对数据的分类、一种约定，即我们用一个界来描述一类数据构成的集合，用不同的界区分不同的数据种类。对于untyped的语言，我们则可以看成是只有唯一一种包罗万象的type

类型实际上有很多作用，可以进行针对性的优化、可以提供部分代码的信息、可以作为接口分离各模块的逻辑、可以保证程序的正确执行…..

如果写过Coq的话，还会知道类型可以与逻辑系统中的元素建立对应关系，从而可以利用类型推导工具来进行定理的证明（虽然我感觉这是绕了一个大弯，毕竟类型系统本来就应该看成一类特殊的逻辑系统），也就是Curry-Howard morphism

这一节讲的就是在$\lambda$-calculus中引入type

Errors

分为trapped errors和untrapped errors

trapped意思是就是出现使得程序停止的错误（除0）

untrapped意思是程序虽然继续运行，但是状态被破坏了（回想注入攻击）

forbidden-error则指的是一个untrapped errors的超集

Safe & Well-behaved

我们称一个程序是safe的，当且仅当它执行过程中不会出现untrapped error。如果一个语言的所有合法程序都是safe的，那么我们就称这个语言是safe的

我们称一个程序是well-behave的，当且仅当它在执行过程中不会出现forbidden-errors。

于是就可以定义type safe了。如果一个语言经过了type system检查的程序都是safe的，那么我们称这个语言就是type safe的

实践中通常不明确定义forbidden-errors、well-behave以及safe，一般混着来，不过不影响理解

Annotations

把变量 $x$ 的类型为 $\tau$ 记作 $x:\tau$

把”以类型 $\tau_1$ 作为输入、$\tau_2$ 作为输出”的函数 $f$ 的类型记作 $f:\tau_1\rightarrow \tau_2$

有些变量的类型由环境决定，例如表达式 $f\;1$，在 $f:\text{int}\rightarrow\text{int}$ 和 $f:\text{int}\rightarrow\text{double}$ 两种情况下的类型就不一样，因此需要引入环境的概念，用函数 $\Gamma:\text{Types}^\text{var}$ 表示，意思是给free variable分配类型，也可以理解成假设

在Simply Typed $\lambda$-calculus里，类型仅由基本类型以及通过函数对基本类型进行复合两种方法得到。很显然类型的数量是可数的

以及若干推导规则：

1. $\Gamma,x:\tau_1\vdash e:\tau_2\Rightarrow \Gamma,x_1:\tau_1\vdash \lambda x.e:\tau_1\rightarrow\tau_2$，意思是函数的类型由参数类型和返回值类型确定。

2. $\Gamma,x:\tau\vdash x:\tau $，意思是在相同环境下，同名变量有相同类型

3. $\Gamma,e_1:\tau_1\rightarrow\tau_2,e_2:\tau_1\vdash e_1\;e_2:\tau_2$，意思是给一个函数传入参数就可以得到返回值的类型

可以发现，一个类型系统类似一个逻辑系统，我们有若干公理（变量类型）、推导规则，并且我们希望所有的命题都可以通过推理得到，也都有相应的语义含义

Soundness & Completeness

也有叫Consistency的

如果一段代码能给所有表达式标上类型：即每个表达式的类型都可以在类型系统中推导得到，那么就称类型系统accept了这段代码

我们称类型系统sound，当且仅当所有通过的代码都不会出错

我们称类型系统complete，当且仅当所有不会出错的代码都能通过检查

很快就能反应过来对于递归可枚举的图灵完备的语言而言，这个问题是不可判定的。因此通常的做法是牺牲completeness追求soundness，意思是也许你的做法是对的，但我们建议用其它可以通过检查的方法来写；并且所有通过的代码都必须是安全的

在Simply Typed $\lambda$-calculus中，不出错就意味着：

如果 $\vdash M:\tau$ 并且 $M\overset *\rightarrow M’$，那么就有 $\vdash M’:\tau$

并且要么 $M’$ 是一个value，要么 $M’$ 可以继续规约。这里value通常就定义为normal form

上面两条分别对应了下面的两个定理

一个证明上述type system不complete的例子如下：

$(\lambda x.(x\; (\lambda y.y))(x\;3))(\lambda z.z)$

关键就在于对于同一个 $x$，它既作用于 $(\lambda y.y)$，又作用于 $3$，因此我们不能推导得到 $x$ 的类型，因此也就无法通过类型系统的检查

但是稍微规约一下就可以得到 $(\lambda y.y)\;3=3$，最终是可以停止并得到值的，意思是这段代码不会出错

Progress TH

如果 $\vdash e:\tau$，那么要么 $e$ 是value，要么存在 $e\rightarrow e’$

证明这个只需要对推导次数进行归纳就可以了

引理1：如果一个拥有 $\tau_1\rightarrow\tau_2$ 类型的表达式 $e$ 是value，那么它一定是 $\lambda x.E$ 的形式

引理1的证明：观察类型推导的规则就可以发现，能够给出 $\tau_1\rightarrow\tau_2$ 类型的规则只有一条。反证即可说明

Progress的证明：

base case 是很简单的，这里就不写了

设当推导次数 $n=k$ 时命题成立，分类讨论第 $k+1$ 次推导时表达式 $e$ 的结构：

1. 常量，此时 $e$ 是value，符合；

2. $e=x$，此时环境为空，不可能有 $\vdash x:\tau$

3. $e=\lambda x.E$，此时 $e$ 是value，符合；

4. $e=e_1\;e_2$，分类讨论 $e_1,e_2$
5. $e_1$ 不是value，那么由归纳假设，存在 $e_1’$ 使得 $e_1\rightarrow e_1’$，符合；
6. $e_1$ 是value，$e_2$ 不是value，那么同理存在 $e_2\rightarrow e_2’$，符合；
7. $e_1,e_2$ 都是value，根据引理有 $e_1=\lambda x.E$，于是有 $e_1\;e_2\rightarrow E[e_2/x]$，符合；

由数学归纳法得命题对任意自然数次的推理成立

关键在于为什么需要引理，以及何时使用引理

Preservation TH

意思是如果 $\vdash e:\tau$ 且 $e\rightarrow e’$，那么有 $\vdash e’:\tau$

引理2：若 $\Gamma,x:\sigma\vdash E:\tau$，且 $\Gamma\vdash e:\sigma$，那么 $\Gamma\vdash E[e/x]:\tau$

证明比较简单，只需要对 $e$ 推导归纳再分类讨论就好了

仍然对推理次数进行归纳，同样省去base case

对 $e$ 的结构分类讨论：

1. $e$ 是常量，那么不存在 $e’$；

2. $e=x$，那么不存在 $e’$

3. $e=\lambda x.E$，那么不存在 $e’$

4. $e=e_1\;e_2$，那么就有 $\vdash e_1\;e_2:\tau$，并且 $\vdash e_1:\sigma\rightarrow \tau,e_2:\sigma$
5. 存在 $e_1\rightarrow e_1’$，那么就有 $e\rightarrow e_1’\;e_2$。根据归纳假设有 $\vdash e_1’:\sigma\rightarrow\tau$，又根据类型推导规则有 $\vdash e_1’\;e_2:\tau$，归纳步骤成立；
6. 存在 $e_2\rightarrow e_2’$，那么就有 $e\rightarrow e_1\;e_2’$。根据归纳假设有 $\vdash e_2’:\sigma$，再根据类型推导规则有 $\vdash e_1\;e_2’:\tau$
7. $e_1,e_2$ 都是normal form，那么根据引理1有 $e_1=\lambda x.E$ 的形式，于是 $e=e_1\;e_2=\lambda x.E\; e_2$。此时显然有 $e\rightarrow E[e_2/x]$，根据引理2有 $\vdash E[e_2/x]:\tau$

于是就证完了