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

Question

Haskell 接受以下类型的定义

data Lam = Func (Lam -> Lam)

它旨在表示无类型的 lambda-terms。例如，Church 的布尔值就是这种类型

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 布尔值， 的基数Lam至少为 2，因此Lam -> Lam中的元素比 中的元素多Lam -> Bool。后者是 的子类型的类型Lam，即 的幂集Lam，并且根据康托定理，它已经比 具有更多的元素Lam。类型如何存在Lam不违反康托尔定理？

部分答案可能在于领域理论。如果我理解正确的话， 的元素将不会全部是集合论函数（比康托定理Lam -> Lam更大），而只是连续函数。Lam如果是这样，定义这种连续性的拓扑是什么，为什么 Haskell 类型项Lam -> Lam对于它来说是连续的？

Answer 1

解决这个悖论的最简单方法可能是观察到并非每个（集合论）函数都可以表示为 lambda 项。

\n

每个有效的 lambda 项都可以通过从最多可数集合中选择有限数量的语法产生式并最多应用它们有限次来获得。因此，所有 lambda 项的集合是可数集合的可数并集，因此它本身是可数的。⁰ 该参数透明地适用于 Haskell 类型：获取类型项的唯一方法Lam是调用构造函数，并且在任何给定时间点，即使您的程序没有\xe2\x80\x99t 终止，构造函数也可能已仅调用有限次数。因此，在整个执行过程中，程序最多可能会遇到无数个不同的Lam值。在实践中，考虑到计算机内存是有限的，您的程序实际上能够操作的术语数量会少一些。

\n

从集合理论上来说，没有什么可以阻止您将通过抛掷硬币可数无限次而获得的位串视为有效函数 \xe2\x84\x95 \xe2\x86\x92 ：它满足 a 的集合理论定义函数，因为它将共域的一个元素（抛硬币的结果）精确地分配给域的每个元素（位串中的位置）。但考虑到构建这样一个函数需要做出无限数量的任意选择¹，它没有相应的 lambda 项。

\n

（更正式地说：在 ZFC 的语言中添加一个符号f ，对于每个自然数n，随机选择 \xe2\x80\x98 f ( n ) = 0\xe2\x80\x99 或 \xe2\x80\x98 之一f ( n ) = 1\xe2\x80\x99 作为公理。如果我们选择定义f的公理的有限子集，则满足该有限子集的函数的存在显然与 ZFC 一致。由紧性定理，它是一致的与 ZFC 函数fZFC 表明存在满足所有公理的

\n

无需调用连续性等复杂概念。以上所有内容都只是出于对基数本身的考虑，同时关注 lambda 项（以及 Haskell 中的类型项）的来源。

\n\n

⁰如果您从一组不可数的变量符号开始，这在技术上是错误的。但即便如此，您也可以选择 lambda 项的可数无限子集，整个集合中的每个 lambda 项都将与 \xce\xb1 等价。如果您使用 de Bru\xc4\xb3n 索引而不是变量符号，该问题也会消失。

\n

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

\n

Answer 2

如果我理解正确的话， 的元素将不会全部是集合论函数（比康托定理Lam -> Lam更大），而只是连续函数。Lam

是的，这是对这个明显悖论的常见答案。

更一般地说，类型就是类型，有其逻辑理论（类型论），而集合就是集合（与集合论一样工作）。

人们倾向于将类型解释为集合，即在集合内构造 lambda 演算模型。

我建议你阅读雷诺兹的里程碑式论文“多态性不是设定理论”。这表明你有像系统 F 中那样的“forall”类型，并且你以“明显”的方式将函数解释为集合，你会得到一个矛盾，通过你提出的类似论点（大致是康托尔的论点）。事实上，雷诺兹构建了T ~= (T -> Bool) -> Bool.

雷诺兹确实建议，其中一种选择是将函数类型解释为集合上函数的“子集”，例如您提到的连续函数。

如果是这样，定义这种连续性的拓扑是什么

斯科特拓扑。

为什么 Haskell 的类型项Lam -> Lam对于它来说是连续的？

粗略地说，因为所有基本操作（lambda 抽象、应用程序等）都是连续的，所以您得到的连续运算符的组合也必须是连续的。

请注意，定义 Haskell 的正确形式语义是一项艰巨的任务。即使只关注相对简单得多的系统F，模型也已经相当复杂。

您可以从简单类型的 lambda 演算开始，了解它们的分类模型：笛卡尔封闭类别 (CCC)。例如，斯科特连续函数范畴是 CCC 的一个特例。CCC 通用结构让您明白，在拥有基本结构（本质上是柯里化和其他一些东西）之后，您可以使用它来创建完整模型，解释任何（类型化）lambda 项。

Answer 3

我不相信用斯科特连续性的概念来解决这个问题有什么好处。Haskell 不具备这些数学论证所需的形式语义。开玩笑地说，这是否意味着Haskell 被破坏了，或者更确切地说，理论家们一直在过度思考，这存在着一场哲学争论。我不知道。

\n

一些问题表明康托尔的论点在这里不成立：

\n

\n

• 可以说，Lam实际上只有基数 1，因为您无法真正区分两个值。您唯一可以做的x :: Lam就是将包含的函数应用于另一个函数y :: Lam以获得...另一个z :: Lam. 当然，所有这些可能有不同的代码和运行时等，但它们都是等价的，因为你永远不会得到任何具有明显不同的 WHNF 或类似内容的 Haskell 值。
  这并不能完全解决讨论，因为您可以轻松添加另一个构造函数并做出类似的参数，但它不会那么简单。

  \n
\n

• Haskell 函数实际上不是函数，特别是它们不是完整的。我还可以写一个 \xe2\x80\x9cisomorphism\xe2\x80\x9d

  \n

  f :: Bool -> Maybe Bool\nf False = Just True\nf True = Just False\n\nf\' :: Maybe Bool -> Bool\nf\' (Just False) = True\nf\' (Just True) = False\nf\' Nothing = f\' Nothing\n

  \n

  祝你好运找到一个x以f (f\' x)不等于 终止的值x。（当然它根本不会终止x = Nothing但现在祝你好运解决停止问题......）

  \n
\n

\n