haskell - Haskell 中嵌入的无类型 lambda 演算的基数

Question

Haskell 接受以下类型的定义

data Lam = Func (Lam -> Lam)

打算代表 untyped lambda-terms .例如，Church 的 bool 值就是这种类型

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 .当我们查看这些类型的基数(大小)时，这是令人惊讶的。由于上面的 Church bool 值， Lam 的红衣主教至少为 2，因此 Lam -> Lam 中有更多元素比 Lam -> Bool .后者是 Lam的子类型类型，即 Lam 的幂集，并由 Cantor's theorem它已经拥有比 Lam 更多的元素做。 Lam类型怎么存在不违反康托尔定理？
部分答案可能在 domain theory .如果我理解正确， Lam -> Lam 的元素不会是所有集合论函数(根据康托尔定理，它们大于 Lam)，而只是连续函数。如果是，定义这种连续性的拓扑是什么，为什么是 Lam -> Lam 类型的 Haskell 术语连续换吗？

Answer 1

可能解决悖论的最简单方法是观察并非每个(集合论)函数都可以表示为 lambda 项。
每个有效的 lambda 项都可以通过从最多可数集中选择有限数量的语法产生式并最多应用它们多次来获得。因此，所有 lambda 项的集合是可数集合的可数并集，因此它本身是可数的。0 该论点透明地适用于 Haskell 类型:获得类型 Lam 的项的唯一方法是调用构造函数，并且在任何给定的时间点，即使您的程序没有终止，构造函数也可能只被调用了有限次。因此，在整个执行过程中，程序最多可能会遇到无数个不同的 Lam值(value)观。在实践中，鉴于计算机内存是有限的，您的程序实际能够操作的术语数量会少一些。
从集合论上讲，没有什么能阻止你将通过掷硬币无数次获得的位串视为有效函数 ℕ → 𝟐:它满足函数的集合论定义，因为它恰好分配了域的每个元素(位串中的位置)的域(掷硬币的结果)。但是考虑到构造这样一个函数需要做出无限多的任意选择1，它没有对应的 lambda 项。
(更正式地说:在 ZFC 的语言中添加一个符号 f，并且对于每个自然数 n，随机选择 'f(n) = 0' 或 'f(n) = 1' 之一作为公理。如果我们选择一个定义 f 的公理的有限子集，显然与 ZFC 一致，存在满足该有限子集的函数。由 compactness theorem ，与 ZFC 一致，存在满足所有公理的函数 f。)
无需调用复杂的概念，如连续性。以上所有内容仅来自对基数本身的考虑，同时注意 lambda 项(以及 Haskell 中的类型项)的来源。

0 如果您从一组不可数的变量符号开始，这在技术上是错误的。但即便如此，您也可以选择一个可数无限的 lambda 项子集，整个集合中的每个 lambda 项都将是 α 等价的。如果您使用 de Bruijn 索引而不是变量符号，该问题也会消失。
1 当然，假设抛硬币确实是不确定的和独立的。