# 系统F

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

Curry-Howard同构下，系统F对应于二阶逻辑

## 逻辑和谓词

TRUE := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x}$
FALSE := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}$

AND := ${\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))y)FALSE}$
OR := ${\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))TRUE)y}$
NOT := ${\displaystyle \lambda x^{Boolean}.((x(Boolean))FALSE)TRUE}$

IFTHENELSE := ${\displaystyle \Lambda \alpha .\lambda x^{Boolean}\lambda y^{\alpha }\lambda z^{\alpha }.((x(\alpha ))y)z}$

ISZERO := λ n. nx. FALSE) TRUE

## 系统F结构

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$

${\displaystyle S}$ 自身出现类型${\displaystyle K_{i}}$ 中的一个内的时候递归就出现了。如果你有${\displaystyle m}$ 个这种构造子，你可以定义${\displaystyle S}$ 为：

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

${\displaystyle {\mathit {zero}}:\mathrm {N} }$
${\displaystyle {\mathit {succ}}:\mathrm {N} \to \mathrm {N} }$

0 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}$
1 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}$
2 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}$
3 := ${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))}$