专栏文章

yroeht-epyt 大手子

yywli08
个人记录参与者 1已保存评论 0

文章操作

快速查看文章及其快照的属性，并进行相关操作。

当前评论
0 条
当前快照
1 份
快照标识符
@miohx9oe
此快照首次捕获于
2025/12/02 19:29
3 个月前
此快照最后确认于
2025/12/02 19:29
3 个月前
查看原文
咦惹和特-鄂匹特 入门。
笔记主要来源：B站 无穷类型咖啡

简单类型lambda演算

类型和语境（上下文）

类型论的研究对象是类型，其类似于集合论中的集合。不同的是，类型自由得多 —— 类型由一系列的规则来定义，给出相关的生成元与构造方法，我们可以定义一个类型。
语境在形式上是一个变量-类型对的列表 —— 它给出了一系列变量的定义。

相继式演算

相继式演算的形式如下：
P1 P2 ⋯ PnC(Name)\frac{P_1 \ P_2 \ \dotsb \ P_n}{C} (Name)
其中，P1⋯PnP_1 \dotsb P_n 称为前提，CC称为结论，在末尾可能出现该规则的名称。
前提与结论统称为判断。判断是STLC中命题的形式。
以上的表达式称作一个步骤。步骤是证明和推理的基本过程。

基本的判断

首先，我们引入判断
AtypeA \mathop{\rm type}
表示 AA 是一个类型。同时我们设定基本类型集合 B\mathcal{B} ，定义是：
B={⊤,⊥,Ans}\mathcal{B} = \{\top, \bot, \rm{Ans}\}
对于 B\mathcal{B} 中的类型，我们有判断
⊤type⊥typeAnstype\frac{}{\top \mathop{\rm type}} \quad \frac{}{\bot \mathop{\rm type}} \quad \frac{}{\rm{Ans} \mathop{\rm type}}
可以发现这些判断是无前提的，这类判断又称之为公理。
这些判断保证了基本类型的存在。
同时，我们有判断
Γctx\Gamma \mathop{\rm ctx}
表示 Γ\Gamma 是一个语境。同样的，有公理
∅ctx\frac{}{\mathop{\rm \emptyset} \mathop{\rm ctx}}
即，空语境是存在的。同时，我们有判断
ΓctxAtypeΓ,x:Actx\frac{\Gamma \mathop{\rm ctx} \quad A \mathop{\rm type}}{\Gamma, x : A \mathop{\rm ctx}}
表示，如果 Γ\Gamma 是一个语境，且 AA 是一个类型，那么 Γ,x:A\Gamma, x : A 也是一个语境。

项

项是具有类型的变量。
我们定义判断
x:Ax : A
表示，xx 是一个具有类型 AA 的项。
对于项的判断不能离开语境。引入判断
Γ⊢x:A\Gamma \vdash x : A
意为在语境 Γ\Gamma 中，xx 是一个具有类型 AA 的项。
对于 B\mathcal B 中的类型，我们有以下公理：
Γ⊢tt:⊤\frac{}{\Gamma \vdash \rm {tt} : \top} Γ⊢yes:AnsΓ⊢no:Ans\frac{}{\Gamma \vdash \rm {yes} : \rm Ans} \quad \frac{}{\Gamma \vdash \rm {no} : \rm Ans}
以及还有一个重要的规则：
x:A∈ΓΓ⊢x:A Var\frac{x:A \in \Gamma}{\Gamma \vdash x : A} \ \rm {Var}

实用类型

类型的构造需要规则。
类型的合法性需要形成规则的保证。
引入规则刻画了类型中合法的对象。
消去规则规定了如何定义与该类型相关的函数以及构造相关的证明。
计算规则规定了该类型的计算方法。
唯一性规则表明了该类型对象的唯一性。（可以不需要。）
绝大部分类型 都拥有以上的四（五）条规则。少部分类型可能拥有不完整的规则。

布尔值 B\mathbb B

布尔值类型的规则如下：
  • 形成：布尔值类型是合法的类型。
Btype\frac{}{\mathbb B \mathop{\rm type}}
  • 引入：布尔值类型中只有两个值，分别是 true\rm true 与 false\rm false。
true:Bfalse:B\frac{}{\rm true : \mathbb B} \quad \frac{}{\rm false : \mathbb B}
  • 消去：对于两个具有相同类型的项 ct,cfc_t, c_f，定义项 elimB(b,ct,cf){\rm elim}_{\mathbb B}(b, c_t, c_f)。
b:Bct:Ccf:CelimB(b,ct,cf):B\frac{b : \mathbb B \quad c_t : C \quad c_f : C}{ {\rm elim}_{\mathbb B}(b, c_t, c_f) : \mathbb B }
  • 计算：elimB(b,ct,cf){\rm elim}_{\mathbb B}(b, c_t, c_f) 的计算方法如下：
ct:Ccf:CelimB(true,ct,cf)≡ct:Cct:Ccf:CelimB(false,ct,cf)≡cf:C\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}
可以看出其实是条件表达式。
注意：elimB(∙,∙,∙)\rm elim_{\mathbb B}(\bullet, \bullet, \bullet) 不是一个函数，而是一个项。
  • 唯一性：
b:Bc:B→CelimB(b,c true,c false)≡c b:C\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×BA \times B

类型 AA 和 BB 的积类型 A×BA \times B 是一个值对，其第一个元素是 AA 类型，第二个元素是 BB 类型。可以看做 C++ 中的 pair 类型 注：积类型 A×BA \times B 和 Π\Pi 类型 ∏a:AB(a)\prod_{a:A} B(a) 没有关系。
  • 形成：需要保证 AA 与 BB 都是合法的类型。
AtypeBtypeA×Btype\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A \times B \mathop{\rm type}}
  • 引入：需要保证 a:Aa : A 与 b:Bb : B 是合法的项。其组成的有序对 (a,b)(a, b) 是一个合法的 A×BA \times B 类型的项。
a:Ab:B(a,b):A×B\frac{a : A \quad b : B}{(a, b) : A \times B}
  • 消去：定义项 π1(p)\pi_1(p) 与 π2(p)\pi_2(p) 表示 pp 的第一个元素与第二个元素。π1(p)\pi_1(p) 是 AA 类型的项，π2(p)\pi_2(p) 是 BB 类型的项。
p:A×Bπ1(p):Ap:A×Bπ2(p):B\frac{p : A \times B}{\pi_1(p) : A} \quad \frac{p : A \times B}{\pi_2(p) : B}
  • 计算：π1(p)\pi_1(p) 或 π2(p)\pi_2(p) 的计算方法就是直接返回 pp 的第一个元素或第二个元素。
a:Ab:Bπ1((a,b))≡a:Aa:Ab:Bπ2((a,b))≡b:B\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}
  • 唯一性 ：pp 等价于 (π1(p),π2(p))(\pi_1(p), \pi_2(p))。
p:A×Bp≡(π1(p),π2(p)):A×B\frac{p : A \times B}{p \equiv (\pi_1(p), \pi_2(p)) : A \times B}

函数类型 A→BA \rightarrow B

函数类型 A→BA \rightarrow B 是一个函数，其输入是 AA 类型，输出是 BB 类型。
  • 形成：同积类型，需要保证 AA 与 BB 都是合法的类型。
AtypeBtypeA→Btype\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A \rightarrow B \mathop{\rm type}}
  • 引入（函数抽象）：当且仅当 x:Ax : A 的语境下，表达式 M:BM : B 是合法的，那么表达式 λx.M:A→B\lambda x . M : A \rightarrow B 是合法的。
x:A⊢M:Bλx.M:A→B Lam\frac{x : A \vdash M : B}{\lambda x . M : A \rightarrow B} \ \rm Lam
  • 消去（函数应用）：当且仅当 f:A→Bf : A \rightarrow B 与 a:Aa : A 是合法的项，那么表达式 f af \ a 是一合法的 BB 类型的项。
f:A→Ba:Af a:B App\frac{f : A \rightarrow B \quad a : A}{f \ a : B} \ \rm App
  • 计算 （β\beta 规约）函数 λx.M\lambda x.M 应用于某一项 aa 的结果是： 将表达式 MM 中的所有 xx 替换为 aa。
x:A⊢M:Ba:Aλx.M a≡M[x↦a]:B β\frac{x : A \vdash M : B \quad a : A}{ \lambda x . M \ a \equiv M[x \mapsto a] : B } \ \rm \beta
  • 唯一性（η\eta 规约）：函数 f:A→Bf : A \rightarrow B 等价于函数 λx.f:A→B\lambda x. f : A \rightarrow B。
f:A→Bλx.f a≡f:A→B η\frac{f : A \rightarrow B}{ \lambda x . f \ a \equiv f : A \rightarrow B } \ \rm \eta

余积类型

余积类型 A+BA + B 相当于 C++ 语言中的 union 体。 注：余积类型和 Σ\Sigma 类型 ∑a:AB(a)\sum_{a : A} B(a) 没有关系。
  • 形成：需要保证 AA 与 BB 都是合法的类型。
AtypeBtypeA+Btype\frac{A \mathop{\rm type} \quad B \mathop{\rm type}}{A + B\mathop{\rm type}}
  • 引入：如果存在合法的项 a:Aa : A 或 存在合法的项 b:Bb : B，那么存在合法的项 inl(a):A+Binl(a) : A + B 或 存在合法的项 inr(b):A+Binr(b) : A + B。
a:Ainl(a):A+Bb:Binr(b):A+B\frac{a : A}{inl(a) : A + B} \quad \frac{b : B}{inr(b) : A + B}
  • 消去：对于项 s:A+Bs : A + B，以及项 cl:A→C,cr:B→Cc_l : A \rightarrow C, c_r : B \rightarrow C，定义项 elimA+B(s,cl,cr)elim_{A+B}(s, c_l, c_r)。
s:A+Bcl:A→Ccr:B→CelimA+B(s,cl,cr):C\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}

待续

评论

共 0 条评论，欢迎与作者交流。

正在加载评论...