Haskell中的两个无限数据结构之间是不是可以进行相等测试？

Posted 2023-03-11

【中文标题】Haskell中的两个无限数据结构之间是不是可以进行相等测试？

【英文标题】：Is equality testing possible between two infinite data structure in Haskell?Haskell中的两个无限数据结构之间是否可以进行相等测试？

【发布时间】：2015-03-30 08:48:29

【问题描述】：

在我正在进行的项目中，某种类型的数据有时可能包含在其中。例如，

data Example = Apple Int
             | Pear Int Example

a = Pear 10 a
b = Pear 10 b

作为一名程序员，我知道a 和b 是相等的，但是当我实际测试它们之间的相等性时，它会无限循环，因为需要评估它们的值以进行比较。

还有其他方法可以在这些数据之间进行相等性测试吗？或者有没有办法避免这些问题？

【问题讨论】：

Relevant SO answer

【参考方案1】：

如果这是您想做的事情，我想谈谈如何真正做到这一点。它比您一开始可能猜到的要难——而且比您一开始可能猜到的要容易！为了好玩，我会让这个问题变得更难一些；我们最终会代表价值观

a = Pear 10 a
b = Pear 10 (Pear 10 b)
c = Apple 10

计算a 和b 是“相等的”——对于精确的相等意义，我们将在下面讨论。这不是可观察共享一定会免费提供给您的东西。

我们将在续集中使用的精确的平等意义是双相似性。通常，双相似性——及其近亲，双模拟——被表示为两个标记图之间的关系。出于我们的目的，您应该在此处描绘图中的节点，其中包含我们数据类型的当前构造函数中的一些数据，以及指向子项的边。因此，对于值Pear 10 (Pear 20 (Apple 30))，我们可能有图Pear 10 -> Pear 20 -> Apple 30；上面的值b 将是循环图

Pear 10 -> Pear 10
   ^         |
    \_______/

可观察到的共享会让你走到这一步，但不会让你明白如何确定这两个图是等价的：

Pear 10 -.            Pear 10 -> Pear 10
   ^      |     ~=       ^         |
    \____/                \_______/

如果您熟悉用于最小化 DFA 的算法，您可能可以在这里停下来；这样的算法很容易适应测试常规语言的相等性，这就是我们接下来要做的。

关键的见解是，上面两个图中的所有三个节点的行为基本相同 - 您可以从左图中的节点开始采取的任何路径在右图中都有一个“相同”的路径。也就是说，假设我们在左右图中的节点之间有一个关系 R 满足这个属性：

if  nl  R nr
and  there is an edge (nl, e, nl') in the graph,
then there is an edge (nr, e, nr') in the graph
and nl' R nr'

我们称 R 为双模拟。最大的关系 R 将被称为双相似性。如果两个图中的“根”节点是双相似的，那么对应的 Haskell 值是相等的！在这一点上，我希望您已经达到了问题似乎比您最初猜测的要难的地步；也许不可能。毕竟，我们应该如何获得最大的此类关系？

一个答案是从完整的关系开始，并删除任何违反上述约束的节点对。继续迭代该过程，直到没有任何变化，然后看看我们还剩下什么。事实证明，你可以证明这个过程实际上产生了 双相似性！我们将在下面以一种非常幼稚的方式实现它；如果你想要更快的速度，你可以在谷歌上搜索高效的双相似性算法。

首先是序言。我们将使用fgl 包来表示我们的图形。

import Control.Monad.Reader
import Data.Graph.Inductive hiding (ap)
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.Map as M
import qualified Data.Set as S

fgl 包为节点的身份定义了一个类型Node。我们将把我们的关系简单地表示为

type Relation = Set (Node, Node)

首先，我们想要一对图的完整关系。当我们这样做时，我们不妨剪掉节点标签不匹配的任何对。 （关于我选择的命名约定的注释：在 fgl 中，每个节点和边都有一个标签——可以是你喜欢的任何类型——和一个身份——必须是 Node 或 Edge 类型。我们的名称将尽可能反映这一点：n 前缀表示节点，e 表示边，i 表示身份，v 表示标签/值。我们将使用 l 和 r 作为后缀对于我们的左手图和右手图。）

labeledPairs :: (Eq n, Graph gr) => gr n e -> gr n e' -> Relation
labeledPairs l r = S.fromList
    [ (nil, nir)
    | (nil, nvl) <- labNodes l
    , (nir, nvr) <- labNodes r
    , nvl == nvr
    ]

现在，下一部分是检查两个节点是否满足我们上面描述的“单步相关性”条件。也就是说，对于其中一个节点的每一条边，我们都在寻找一条与另一条边有相同标签的边，并通向我们当前声称相关的另一个节点。将此搜索音译为 Haskell：

-- assumption: nil and nir are actual nodes in graphs l and r, respectively
ssRelated :: (Ord e, Graph gr) => gr n e -> gr n e -> Relation -> Node -> Node -> Bool
ssRelated l r rel nil nir = rell && relr where
    el = out l nil
    er = out r nil
    mel = M.fromListWith (++) [(evl, [nil]) | (_, nil, evl) <- el]
    mer = M.fromListWith (++) [(evr, [nir]) | (_, nir, evr) <- er]
    rell = and
        [ or [(nil, nir) `S.member` rel | nir <- M.findWithDefault [] evl mer]
        | (_, nil, evl) <- el
        ]
    relr = and
        [ or [(nil, nir) `S.member` rel | nil <- M.findWithDefault [] evr mel]
        | (_, nir, evr) <- er
        ]

我们现在可以编写一个函数来检查每对节点的单步适用性：

prune :: (Ord e, Graph gr) => gr n e -> gr n e -> Relation -> Relation
prune l r rel = S.filter (uncurry (ssRelated l r rel)) rel

如上所述，为了计算双相似度，我们将从完整关系开始，并反复修剪掉不符合条件的节点。

bisimilarity :: (Eq n, Ord e, Graph gr) => gr n e -> gr n e -> Relation
bisimilarity l r
    = fst . head
    . dropWhile (uncurry (/=))
    . ap zip tail
    . iterate (prune l r)
    $ labeledPairs l r

现在我们可以通过在每个图中选择根节点并检查它们的双相似性来检查两个图是否具有相同的无限展开：

-- assumption: the root of the graph is node 0
bisimilar :: (Eq n, Ord e, Graph gr) => gr n e -> gr n e -> Bool
bisimilar l r = (0, 0) `S.member` bisimilarity l r

现在让我们看看它的实际效果！我们将在图形表示的答案中模拟前面的a、b 和c。由于我们的数据类型只有一次可能的递归出现，我们不需要有趣的边缘标签。 mkGraph 函数获取标记节点列表和标记边缘列表，并根据它们构建图形。

data NodeLabel = Apple Int | Pear Int
    deriving (Eq, Ord, Read, Show)
type EdgeLabel = ()

a, b, c :: Gr NodeLabel EdgeLabel
a = mkGraph [(0, Pear 10)] [(0, 0, ())]
b = mkGraph [(0, Pear 10), (1, Pear 10)] [(0, 1, ()), (1, 0, ())]
c = mkGraph [(0, Apple 10)] []

在 ghci 中：

*Main> bisimilar a b
True
*Main> bisimilar a c
False
*Main> bisimilar b c
False
*Main> bisimilar a a
True
*Main> bisimilar b b
True
*Main> bisimilar c c
True

看起来不错！使其快速并将其连接到可观察共享库作为练习留给读者。请记住，虽然这种方法可以处理具有无限展开的图，但以这种方式处理无限图当然可能会遇到麻烦！

【讨论】：

哇，这太棒了。我真的不知道我还能说什么......非常感谢丹尼尔！

【参考方案2】：

一般来说：没有。这种相等性测试减少了停机问题。看到这一点的一种方法是，我们可以将图灵机在某些输入上的执行表示为像这样的无限数据结构。另一种看待它的方式是惰性数据结构可以表示任意挂起的计算。

避免此类问题的唯一真正方法是对您的数据结构设置一些额外的限制，或者检查比相等更受限制的东西。

第一种方法的一个示例是使用某种引用使数据类型中的循环显式化，让您在执行过程中检测到它们。这将完全限制您可以用数据结构表达的内容，但也会让您的相等谓词可靠地检测循环。我认为您可以通过 可观察共享 做到这一点；查看data-reify 以获得执行此操作的包。这种方法应该使检查像您的示例这样非常直接的递归结构变得容易。

对于第二种方法，您可以有一个返回 Maybe Bool 的函数：如果在 X 步中无法确定两个结构是否相等，则返回 Nothing。根据您的数据类型的创建方式，您可能可以确保具有相同前缀的超出特定大小的任何类型几乎总是相等，并且仅依赖于此。

【讨论】：

我会试用 data-reify 包。不久前，我在 SML 中实现了相同的项目，并通过 SML ref 功能解决了这个问题。似乎 data-reify 提供的东西与此非常相似？

@Enzo：是的，没错。这是一个不同的，在大多数情况下，比使用 refs 来明确你的循环更好的选择。