2024-12-30-类型论

类型论初学

简述：类型论是一种形式理论，被视为编程语言中类型系统的数学表述。

特点：

- 基于lambda 演算
- 使用规则定义类型
- 不需要穷举无穷大集合中的所有元素
- 命题也视为类型

函数类型对应内射态

积类型对应积

对应映射集 和 Descartes 积

类型论的范畴语义

模型：范畴 （范畴语义）

类型论为范畴的内语言

| 集合论 | 类型论 | 范畴论 | 逻辑学 | | :———————————————–: | :———————————————————-: | :———————————————–: | :———————————————————-: | | 集合 | 类型 | 对象 | 命题 | | 单点集 | 单位类型 | 终对象 | 永真命题 | | 空集 | 空类型 | 始对象 | 永假命题 | | 元素 | 实例 | 从终对象出发的态射 | 证明 |

举例类型论：简单类型λ演算 ( 记作 λ→ 或者 STλC)

函数类型

任何 λ→都是函数类型上扩充的

1
2

A,B::=V∣A→B
M,N,u,v::= V∣(M N)∣(λV. M)

其中：A,B 符号标识类型论中的类型

M，N，u，v这四个符号都表示类型论中的值(λ 表达式)

V标识变量或类型变量

符号u代表一个表达式的意思满足三个条件：

• u∈V
• u形如 v1 v2 其中 v1 v2是类型u的表达式
• u 形如 λx. v, 其中 x∈V, 而 v 是类似 u 的表达式.

对 A,B 等表示类型的符号的描述也类似.