yroeht-epyt 大手子
ywli08
·
·
个人记录
咦惹和特-鄂匹特 入门。
笔记主要来源：B站 无穷类型咖啡
简单类型lambda演算
类型和语境（上下文）
类型论的研究对象是类型，其类似于集合论中的集合。不同的是，类型自由得多 —— 类型由一系列的规则来定义，给出相关的生成元与构造方法，我们可以定义一个类型。
语境在形式上是一个变量-类型对的列表 —— 它给出了一系列变量的定义。
相继式演算
相继式演算的形式如下：
\frac{P_1 \ P_2 \ \dotsb \ P_n}{C} (Name)
其中，P_1 \dotsb P_n 称为前提，C称为结论，在末尾可能出现该规则的名称。
前提与结论统称为判断。判断是STLC中命题的形式。
以上的表达式称作一个步骤。步骤是证明和推理的基本过程。
基本的判断
首先，我们引入判断
A \mathop{\rm type}
表示 A 是一个类型。同时我们设定基本类型集合 \mathcal{B} ，定义是：
\mathcal{B} = \{\top, \bot, \rm{Ans}\}
对于 \mathcal{B} 中的类型，我们有判断
\frac{}{\top \mathop{\rm type}} \quad \frac{}{\bot \mathop{\rm type}} \quad \frac{}{\rm{Ans} \mathop{\rm type}}
可以发现这些判断是无前提的，这类判断又称之为公理。
这些判断保证了基本类型的存在。
同时，我们有判断
\Gamma \mathop{\rm ctx}
表示 \Gamma 是一个语境。同样的，有公理
\frac{}{\mathop{\rm \emptyset} \mathop{\rm ctx}}
即，空语境是存在的。同时，我们有判断
\frac{\Gamma \mathop{\rm ctx} \quad A \mathop{\rm type}}{\Gamma, x : A \mathop{\rm ctx}}
表示，如果 \Gamma 是一个语境，且 A 是一个类型，那么 \Gamma, x : A 也是一个语境。
项
项是具有类型的变量。
我们定义判断
x : A
表示，x 是一个具有类型 A 的项。
对于项的判断不能离开语境。引入判断
\Gamma \vdash x : A
意为在语境 \Gamma 中，x 是一个具有类型 A 的项。
对于 \mathcal B 中的类型，我们有以下公理：
\frac{}{\Gamma \vdash \rm {tt} : \top}
\frac{}{\Gamma \vdash \rm {yes} : \rm Ans} \quad \frac{}{\Gamma \vdash \rm {no} : \rm Ans}
以及还有一个重要的规则：
\frac{x:A \in \Gamma}{\Gamma \vdash x : A} \ \rm {Var}
实用类型
类型的构造需要规则。
类型的合法性需要形成规则的保证。
引入规则刻画了类型中合法的对象。
消去规则规定了如何定义与该类型相关的函数以及构造相关的证明。
计算规则规定了该类型的计算方法。
唯一性规则表明了该类型对象的唯一性。（可以不需要。）
绝大部分类型 都拥有以上的四（五）条规则。少部分类型可能拥有不完整的规则。
布尔值 \mathbb B
布尔值类型的规则如下：
\frac{}{\mathbb B \mathop{\rm type}}
- 引入：布尔值类型中只有两个值，分别是 \rm true 与 \rm false。
\frac{}{\rm true : \mathbb B} \quad \frac{}{\rm false : \mathbb B}
- 消去：对于两个具有相同类型的项 c_t, c_f，定义项 {\rm elim}_{\mathbb B}(b, c_t, c_f)。
\frac{b : \mathbb B \quad c_t : C \quad c_f : C}{
{\rm elim}_{\mathbb B}(b, c_t, c_f) : \mathbb B
}
- 计算：{\rm elim}_{\mathbb B}(b, c_t, c_f) 的计算方法如下：
\frac{c_t : C \quad c_f : C}{{\rm elim}_{\mathbb B}({\rm true}, c_t, c_f) \equiv c_t : C} \quad \frac{c_t : C \quad c_f : C}{{\rm elim}_{\mathbb B}({\rm false}, c_t, c_f) \equiv c_f : C}
可以看出其实是条件表达式。
注意：\rm elim_{\mathbb B}(\bullet, \bullet, \bullet) 不是一个函数，而是一个项。
\frac{b : \mathbb B \quad c : \mathbb B \rightarrow C}{
{\rm elim}_{\mathbb B}(b, c \ {\rm true}, c \ {\rm false}) \equiv c \ b : C
}
积类型 A \times B
类型 A 和 B 的积类型 A \times B 是一个值对，其第一个元素是 A 类型，第二个元素是 B 类型。可以看做 C++ 中的 pair 类型
注：积类型 A \times B 和 \Pi 类型 \prod_{a:A} B(a) 没有关系。
\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A \times B \mathop{\rm type}}
- 引入：需要保证 a : A 与 b : B 是合法的项。其组成的有序对 (a, b) 是一个合法的 A \times B 类型的项。
\frac{a : A \quad b : B}{(a, b) : A \times B}
- 消去：定义项 \pi_1(p) 与 \pi_2(p) 表示 p 的第一个元素与第二个元素。\pi_1(p) 是 A 类型的项，\pi_2(p) 是 B 类型的项。
\frac{p : A \times B}{\pi_1(p) : A} \quad \frac{p : A \times B}{\pi_2(p) : B}
- 计算：\pi_1(p) 或 \pi_2(p) 的计算方法就是直接返回 p 的第一个元素或第二个元素。
\frac{a : A \quad b : B}{\pi_1((a, b)) \equiv a : A} \quad \frac{a : A \quad b : B}{\pi_2((a, b)) \equiv b : B}
- 唯一性 ：p 等价于 (\pi_1(p), \pi_2(p))。
\frac{p : A \times B}{p \equiv (\pi_1(p), \pi_2(p)) : A \times B}
函数类型 A \rightarrow B
函数类型 A \rightarrow B 是一个函数，其输入是 A 类型，输出是 B 类型。
- 形成：同积类型，需要保证 A 与 B 都是合法的类型。
\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A \rightarrow B \mathop{\rm type}}
- 引入（函数抽象）：当且仅当 x : A 的语境下，表达式 M : B 是合法的，那么表达式 \lambda x . M : A \rightarrow B 是合法的。
\frac{x : A \vdash M : B}{\lambda x . M : A \rightarrow B} \ \rm Lam
- 消去（函数应用）：当且仅当 f : A \rightarrow B 与 a : A 是合法的项，那么表达式 f \ a 是一合法的 B 类型的项。
\frac{f : A \rightarrow B \quad a : A}{f \ a : B} \ \rm App
- 计算 （\beta 规约）函数 \lambda x.M 应用于某一项 a 的结果是： 将表达式 M 中的所有 x 替换为 a。
\frac{x : A \vdash M : B \quad a : A}{
\lambda x . M \ a \equiv M[x \mapsto a] : B
} \ \rm \beta
- 唯一性（\eta 规约）：函数 f : A \rightarrow B 等价于函数 \lambda x. f : A \rightarrow B。
\frac{f : A \rightarrow B}{
\lambda x . f \ a \equiv f : A \rightarrow B
} \ \rm \eta
余积类型
余积类型 A + B 相当于 C++ 语言中的 union 体。
注：余积类型和 \Sigma 类型 \sum_{a : A} B(a) 没有关系。
\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A + B\mathop{\rm type}}
- 引入：如果存在合法的项 a : A 或 存在合法的项 b : B，那么存在合法的项 inl(a) : A + B 或 存在合法的项 inr(b) : A + B。
\frac{a : A}{inl(a) : A + B} \quad \frac{b : B}{inr(b) : A + B}
- 消去：对于项 s : A + B，以及项 c_l : A \rightarrow C, c_r : B \rightarrow C，定义项 elim_{A+B}(s, c_l, c_r)。
\frac{s : A + B \quad c_l : A \rightarrow C \quad c_r : B \rightarrow C}{elim_{A+B}(s, c_l, c_r) : C}
待续