类型论与coq (5-3)

介绍完这个之后我们再来稍微介绍一下所谓的∑-Type，其实这个Type就是笛卡尔积的推广

Def 3. 给定一个类型A：U，和一个类型族B：A → U，我们考虑函数

∑ B(x)：U，

x：A

注意到当B是一个常类型族即将所有的α：A都映到同一个类，此时

∑ B：U≡(A × B)，

x：A

并且我们有，对于给定的α：A，b：B(α)那么

(α，b)：∑ 。

(x：A)B(x)

这里有个非常有意思的值得一提的点是在集合论中我们假设A × B中的元素都是形如(α，b)的，而在类型论中则不然，我们更多的是通过假设定义在

∑ B(x)

x：A

的函数只需要给出在所有形如(α，b)处的值，那么这个函数就是良定的，通过这一点我们就可以证明所有

∑ B(x)

x：A

的元素都是形如(α，b)的了

在这里我们希望多提一点的是，如果我们给定了一个函数

g：∏ B(x) → C，

x：A

那么我们可以递归的定义一个函数f：(∑B(x)) → C，并且f满足

x：A

f((α，b))：≡g(α)(b)

首先我们先定义投影函数如下

pr₁：(∑B(x)) → A

x：A

＜br＞pr₁((α，b))：≡α

以及

pr₂： ∏ B(pr₁(p))

p：∑x：A B(x)

我们希望归纳的定义p₂，那现在考虑一个类型族C：(∑B(x)) → U假设我们已经有了函数 x：A

g：∏ ∏ C((α，b))

α：A b∈B(α)

那么我们就可定义

f： ∏ → C(p)

p：∑x：A B(x)

为

f((α，b))：≡g(α)(b)

于是我们现在可以令C(p)：≡ B(pr₁(p))，于是我们就可以定义我们的

pr₂： ∏ B(pr₁(p))了，

p：∑x：A B(x)

pr₂((α，b))：≡b

我们现在可以把我们上面做的递归和归纳的东西打包成两个函数

rec∑x：A B(x)：∏(Πx：A B)(x) → C) ↓

C：U

→ (Σx：A B(x)) → C

写成表达式就是

recΣx：A B(x)： ∏ (Πα：AΠb：B(α)C((α，b))) → ∏ C(p)

C：(Σx：A B(x)) → U

p：Σx：A B(x)

写成表达式就是

indΣx：A B(x)(C，g，(α，b))：≡g(α)(b)

当然，很明显的看到当递归其实就是归纳在C是常数的特例

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。