6

我正在用 Haskell 编写一种小型函数式编程语言，但我找不到 (==) 如何实现的定义，因为这似乎很棘手？

4

4 回答 4

14

Haskell 使用“类型类”的概念。实际的定义是这样的：

class Eq a where
  (==) :: a -> a -> Bool
  -- More functions follow, for more complex concepts of equality (eg NaN)

然后你可以为你自己的类型定义它。例如：

-- Eq can't be automatically derived, because of the function
data Foo = Foo Int (Char -> Bool)

-- So define it here
instance Eq Foo where
  (Foo x _) == (Foo y _) = x == y
于 2009-10-09T21:07:27.683 回答
11

我认为你的问题非常非常有趣。如果您还意味着您想知道您的问题背后的理论根源，那么我认为，我们可以从 Haskell 中抽象出来，并在更一般的算法概念中研究您的问题。至于 Haskell，我认为以下两个事实很重要：

  • 函数是 Haskell 中的一等公民
  • Haskell 是图灵完备的

但我还没有完成讨论（语言的强度在这里究竟如何重要）。

特定情况的可能性，但全面的禁止定理

我认为，从根本上说，计算机科学的两个定理提供了答案。如果我们想从技术细节中抽象出来，我们可以在 lambda 演算（或组合逻辑）中调查您的问题。可以在其中定义平等吗？因此，让我们首先将自己限制在 lambda 演算或组合逻辑领域。

必须注意的是，这两种算法方法都非常简约。它们中没有“预定义”数据类型，没有偶数，也没有布尔值，也没有列表。但是您可以以巧妙的方式模仿所有这些。

因此，即使在 lambda 演算和组合逻辑等极简“函数式语言”中，您也可以模仿所有有意义的数据类型。您可以在模仿您想要的数据类型的巧妙场景中使用 lambda 函数（或组合器）。

现在让我们首先尝试用这些简约的函数式语言来回答您的问题，看看答案是否是特定于 Haskell 的，或者仅仅是一些更一般定理的结果。

  • Böhm 定理提供：对于任何两个先前给定的不同表达式（即停止，并且不冻结计算机），始终可以编写合适的测试函数来正确判断两个给定表达式在语义上是否相同（Csörnyei 2007：132， = 7.2.2)。在大多数实际情况（列表、树、布尔值、数字）中，Böhm 定理提供了始终可以编写合适的特定等式函数。请参阅Tromp 1999中的列表示例：第 2 节。
  • Scott-Curry 不可判定性定理排除了可以编写任何全一般等式函数，对每个可能的场景都有意义（Csörnyei 2007: 140, = Th 7.4.1）。

一个去定理

在你“实现”了一个数据类型之后，你可以为此编写相应的相等函数。对于大多数实际案例（列表、数字、案例分析选择），没有相应的相等函数会缺少的神秘“数据类型”。伯姆定理提供了这个肯定的答案。

你可以编写一个 Church-numeral-equality 函数，它接受两个 Church 数字，并回答它们是否相等。您可以编写另一个lambda-function/combinator 接受两个 (Church)-booleans 并回答它们是否相等。此外，您可以在纯 lambda 演算/CL 中实现列表（一种建议的方法是使用变态的概念），然后，您可以定义一个函数来回答布尔列表的相等性。您可以编写另一个函数来回答 Church 数字列表的相等性。您也可以实现树，然后，您可以编写一个函数来回答树的相等性（在布尔值上，另一个在教堂数字上）。

您可以自动化其中的一些工作，但不是全部。您可以自动派生一些（但不是全部）相等函数。如果您已经拥有用于树和列表的特定映射函数，以及用于布尔值和数字的相等函数，那么您也可以自动为布尔树、布尔列表、数字列表、数字树派生相等函数。

一个不可行的定理

但是没有办法为所有可能的“数据类型”定义一个单一的全自动相等函数。如果您在 lambda 演算中“实现”一个具体的给定数据类型，您通常必须为该场景计划其特定的相等函数。

此外，没有办法定义一个接受两个 lambda 项并回答两个 lambda 项在归约时的行为方式是否相同的 lambda 函数。更重要的是，没有办法定义一个 lambda 函数，它会采用两个 lambda 项的表示（引号）并回答两个原始 lambda 项在减少时是否会表现相同（Csörnyei 2007：141，Conseq 7.4.3)。Scott-Curry 不可判定性定理 (Csörnyei 2007: 140, Th 7.4.1) 提供了这个不可行的答案。

在其他算法方法中

我认为，以上两个答案不仅限于 lambda 演算和组合逻辑。类似的可能性和限制适用于其他一些算法概念。例如，没有递归函数会采用两个一元函数的哥德尔数并决定这些编码函数在扩展上的行为是否相同（Monk 1976：84，= Cor 5.18）。这是赖斯定理(Monk 1976: 84, = Th 5.17) 的结果。我觉得，Rice 定理在形式上听起来与 Scott-Curry 不可判定性定理非常相似，但我还没有考虑过。

非常狭义的全面平等

如果我想编写一个组合逻辑解释器来提供全面的等式测试（仅限于停止、具有范式的术语），那么我会这样实现：

  • 我会将考虑中的两个组合逻辑项简化为它们的正常形式，
  • 并查看它们是否与 terms 相同。

如果是这样，那么它们未简化的原始形式在语义上也一定是等价的。

但这仅适用于严格的限制，尽管此方法适用于几个实际目标。我们可以在数字、列表、树等之间进行操作，并检查我们是否得到了预期的结果。我的 quine（用纯组合逻辑编写）使用了这种受限的相等概念，尽管事实上这种 quine 需要非常复杂的构造（在组合逻辑本身中实现的术语树），但它就足够了。

我还不知道这个受限制的平等概念的限制是什么，但我怀疑，如果与平等的正确定义相比，它是非常受限制的。它使用背后的动机是它是可计算的，不像不受限制的平等的概念。

这些限制也可以从这个受限相等概念仅适用于具有范式的组合子这一事实中看出。举个反例：受限等式概念不能检查I Ω   =   Ω是否，尽管我们很清楚这两个项可以相互转换。

我还必须考虑，这种受限的平等概念的存在如何与 Scott-Curry 不可判定性定理和赖斯定理所声称的负面结果相关联。这两个定理都处理偏函数，但我还不知道这到底有什么关系。

可扩展性

但受限平等概念也有进一步的局限性。它不能处理外延性的概念。例如，它没有注意到S K会以任何方式与K I相关，尽管事实上S K在应用于至少两个参数时与K I行为相同：

后一个例子必须更详细地解释。我们知道S K和K I不等同于项：S K   ≢   K I。但是，如果我们将两者分别应用到任意两个参数X和Y上，我们就会看到相关性：

  • S K X Y   ⊳   K Y ( X Y ) ⊳   Y
  • K I X Y   ⊳   I Y   ⊳   Y

当然Y   ≡   Y，对于任何Y。

当然，我们不能为每个可能的X和Y参数实例“尝试”这种相关性，因为可以有无限多个这样的 CL 项实例被替换到这些元变量中。但我们不必拘泥于这个无穷大的问题。如果我们用（自由）变量扩充我们的对象语言（组合逻辑）：

  • K是一个术语
  • S是一个术语
  • 任何（自由）变量都是一个术语（新行，这是修改！）
  • 如果X和Y都是项，那么 ( X Y ) 也是项
  • 不能以任何其他方式获得条款

并且我们以适当的方式相应地定义归约规则，然后我们可以以“有限”方式陈述相等的扩展定义，而不依赖于具有无限可能实例的元变量。

因此，如果在组合逻辑术语中允许自由变量（对象语言增加了它自己的对象变量），那么可以在某种程度上实现可扩展性。我还没有考虑到这一点。对于上面的例子，我们可以使用一个符号

S K   = 2   K I

(Curry & Feys & Craig 1958: 162, = 5 C 5)，基于可以证明S K x y和K I x y相等的事实（已经不诉诸外延性）。这里，x和y不是方程组中无限多可能的 CL 项实例的元变量，而是对象语言本身的一等公民。因此，这个方程不再是一个方程组，而是一个单一的方程。

至于理论研究，我们可以通过 = 所有 n 个实例的“并集”来表示= 。

或者，可以定义等式，使其归纳定义也考虑外延性。我们添加了另一条处理外延性的推理规则 (Csörnyei 2007: 158)：

  • ...
  • ...
  • 如果E , F是组合子，x是一个（对象）变量，并且x既不包含在E也不包含在F中，那么，从E x =   F x 我们可以推断出E   =   F

不包含的约束很重要，如以下反例所示：K x  ≠  I，尽管是K x x  =  I x。两个（偶然相同的）变量出现的“角色”完全不同。排除此类事件，这就是约束的动机。-

可以通过展示如何证明定理S K x   =   K I x来举例说明这种新推理规则的使用：

  • S K   =   K I被认为是成立的，因为S K x   =   K I x已经被证明成立，见下面的证明：
  • S K x   =   K I x被认为是成立的，因为S K x y   =   K I x y已经被证明成立，见下文：
  • S K x y   =   K I x y无需借助外延即可证明，我们只需要熟悉的转换规则。

这些剩余的推理规则是什么？以下是它们的列表（Csörnyei 2007：157）：

转换公理方案：

  • `` K E F = E '' 是可推导的（K-公理方案）
  • `` S F G H = F H ( G H )'' 是可推导的（S-公理方案）

等式公理方案和推理规则

  • `` E = E '' 是可推导的（反身公理方案）
  • 如果“ E = F ”是可演绎的，那么“ F = E ”也是可演绎的（推理的对称规则）
  • 如果“ E = F ”是可演绎的，并且“ F = G ”也是可演绎的，那么“ E = G ”也是可约的（传递性规则）
  • 如果“ E = F ”是可演绎的，那么“ E G = F G ”也是可演绎的（莱布尼茨规则I）
  • 如果“ E = F ”是可演绎的，那么“ G E = G F ”也是可演绎的（莱布尼茨规则II）

参考

附录

伯姆定理

我还没有清楚地解释 Böhm 定理与以下事实之间的关系：在大多数实际情况下，肯定可以为有意义的数据类型编写合适的相等性测试函数（即使在像纯 lambda 演算或组合逻辑这样的极简函数语言中）。

陈述

  • 设E和F是 lambda 演算的两个不同的封闭项，
  • 并让它们都有正常的形式。

然后，该定理声称，有一种合适的方法可以通过将它们应用于一系列合适的参数来测试相等性。换句话说：存在一个自然数n和一系列封闭的 lambda 项G 1 , G 2 , G 3 ,... G n，因此将它们应用于这一系列参数分别减少为false和true：

  • E G 1 G 2 G 3 ... G n   ⊳   假
  • F G 1 G 2 G 3 ... G n   ⊳   真

其中true和false是两个众所周知的、驯服的、易于管理和区分的 lambda 术语：

  • 真    ≡ λ x y。X
  • 假   ≡ λ x y。是的

应用

如何利用这个定理在纯 lambda 演算中实现实际数据类型？该定理的隐含应用可以通过可以在组合逻辑中定义链表的方式来举例说明（Tromp 1999：第 2 节）。

于 2009-10-10T12:25:29.793 回答
8

(==)是类型类的一部分Eq。每个实例类型都提供一个单独的实现Eq。因此，要找到实现，您通常应该查看定义类型的位置。

于 2009-10-09T21:30:16.110 回答
-3

我闻起来像家庭作业。详细说明为什么你觉得它很棘手。你可以看看 ML 和各种 Lisps 是如何尝试解决这个问题的。您还可以查看其他语言解释器/编译器之一的源代码，其中一些是为了学习而编写的。

于 2009-10-13T04:52:14.393 回答