嵌入在Haskell中的非类型化λ演算的基数

Question

data Lam = Func (Lam -> Lam)

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

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

部分答案可能来自领域理论。如果我理解正确的话，lam->lam的元素并不全是集合论函数（根据康托定理，这些函数比lam大），而只是连续函数。如果是，定义这种连续性的拓扑是什么？为什么LAM->LAM类型的Haskell术语对它是连续的？

Answer 1

也许解决这个悖论的最简单的方法是观察并不是每一个（集合论的）函数都可以表示为一个λ项。

每一个有效的lambda项都可以通过从一个至多可数的集合中选择有限数量的语法产生物，并将它们至多有限地应用多次而得到。因此，所有lambda项的集合是可数集的可数并集，因此它本身是可数的。⁰参数透明地应用于Haskell类型：获得lam类型项的唯一方法是调用构造函数，在任何给定的时间点，即使程序没有终止，构造函数也只能被调用有限次。因此，在整个执行过程中，程序最多可能遇到无限多个不同的LAM值。在实践中，考虑到计算机内存有限，你的程序实际上能够操纵的项数会少一点。

集合--理论上，没有什么能阻止你把通过抛硬币无数次获得的比特串视为一个有效的函数→它满足了函数的集合理论定义，因为它给域的每一个元素（比特串中的位置）指定了共域的一个元素（抛硬币的结果）。但是假定构造这样一个函数需要做出无限多的任意选择¹，它就没有相应的λ项。

没有必要调用像连续性这样复杂的概念。上面所有的内容都是基于基数本身的考虑，同时注意lambda术语（以及Haskell中的类型术语）来自哪里。

⁰如果从变量的不可数符号集开始，从技术上讲，这是错误的。但即使这样，你也可以选择一个可数的无限个λ项子集，在这个子集上，每个λ项都是α-等价的。如果使用de bru n索引而不是变量符号，这个问题也会消失。

¹当然，假设掷硬币确实是不确定和独立的。