嵌入Haskell的无类型Lambda演算基数为何不违反康托尔定理

问题背景 #

Haskell允许定义如下递归类型：

data Lam = Func (Lam -> Lam)

该类型用于表示无类型lambda项，例如丘奇布尔值就可以用该类型实现：

trueChurch :: Lam
trueChurch = Func (\x -> Func (\y -> x))

falseChurch :: Lam
falseChurch = Func (\x -> Func (\y -> y))

构造器Func :: (Lam -> Lam) -> Lam存在对应的逆函数：

lamUnfold :: Lam -> (Lam -> Lam)
lamUnfold (Func f) = f

这两个函数看起来构成了Lam -> Lam和Lam之间的类型同构，这和集合论中的康托尔定理产生了表面冲突：如果Lam是普通集合，且基数至少为2，那么Lam到Lam的所有函数的集合基数应该远大于Lam本身的基数。 #

详细解答 #

1. 不违反康托尔定理的核心原因 #

康托尔定理的适用前提是集合到集合的所有函数，但Haskell的函数类型a -> b并不包含集合论层面的所有可能函数，仅包含满足特定约束的连续函数，属于全函数集合的一个真子集，因此康托尔定理的结论不能直接套用在这个子集上。

2. 对应的连续性定义与拓扑结构 #

这里的连续性是Scott拓扑下的连续性，相关内容属于论域理论的研究范畴：

• 首先Haskell类型的指称都是带底元的完全偏序集（CPO），偏序关系⊑的含义是：x ⊑ y当且仅当x的定义程度不高于y，或者说x是y的一个逼近。
• 一个函数f :: A -> B是Scott连续的，需要同时满足两个条件：
  • 单调性：如果x ⊑ y，那么f x ⊑ f y
  • 保最小上界：对于任意有向集S ⊆ A，f(⊔S) = ⊔{ f(x) | x ∈ S }，其中⊔表示集合的最小上界
    Lam类型的指称实际上就是Dana Scott构造的无类型lambda演算模型，这是一个满足D ≅ [D → D]的CPO，其中[D → D]表示D到D的所有Scott连续函数的集合，这个集合的基数和D本身的基数相等，因此二者的同构完全成立。

3. 为什么所有Haskell可定义的Lam -> Lam函数都是Scott连续的 #

本质原因是Haskell的计算遵循有限性原则：任何可终止的计算，都只能依赖输入的有限部分信息。
也就是说，函数输出的任意有限部分的定义，都只需要输入的某一部分有限的定义，不可能需要遍历输入的无限结构才能给出输出的有限部分，这个性质正好和Scott连续的定义等价。因此所有Haskell中可以写出的函数天然都是Scott连续的，不存在非连续的可定义函数。 #

内容的提问来源于stack exchange，提问作者V. Semeria