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

Question

在我正在研究的项目中,某种类型的数据有时可能包含在其中.例如,

data Example = Apple Int
             | Pear Int Example

a = Pear 10 a
b = Pear 10 b

作为程序员,我知道a并且b是相同的,但是当我实际测试它们之间的相等时,它将无限循环,因为它们的值需要进行评估以进行比较.

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

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

看起来不错!快速将它连接到一个可观察共享的库是留给读者的练习.请记住,虽然这种方法可以处理具有无限展开的图形,但是当然可能无法以这种方式处理无限图形!

Answer 2

一般来说:没有.这种平等测试减少了停顿问题.一种看待这种情况的方法是,我们可以将某些输入上的图灵机的执行表达为像这样的无限数据结构.查看它的另一种方式是惰性数据结构可以表示任意暂停的计算.

避免这种问题的唯一真正方法是对数据结构设置一些额外的限制,或者检查比平等更有限的东西.

第一种方法的一个示例是使用某种类型的引用显式显示数据类型中的循环,让您在进行时检测它们.这将完全限制您可以用数据结构表达的内容,但也会让您的等式谓词检测循环.我认为你可以用可观察的分享来做到这一点; 看一下这样做的包的data-reify.这种方法应该使得检查一个非常直接的递归结构,就像您的示例一样简单.

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