Haskell中的两个无限数据结构之间是否可以进行平等测试？ [英] Is equality testing possible between two infinite data structure in Haskell?

问题描述

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

 数据示例= Apple Int 
 | Pear Int示例
 
a =梨10 a 
b =梨10 b 
  

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

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

解决方案

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

避免像这样的问题的唯一方法是对您的设置一些额外的限制数据结构或检查比平等更有限的东西。

第一种方法的一个例子是使数据类型的循环显式引用某种类型，让您在进行时检测它们。这将限制你可以用你的数据结构来表达的东西，但也可以让你的等式谓词稳健地检测周期。我认为你可以通过可观察的分享来做到这一点;请查看 data-reify ，以获取相应的包。这种方法应该检查一个非常直接的递归结构，就像你的例子easy。

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

In a project I'm working on, data of a certain type may sometimes contain themselves in it. For example,

data Example = Apple Int
             | Pear Int Example

a = Pear 10 a
b = Pear 10 b

As a programmer I know that a and b are equal, but when I actually test equality between them it would infinite loop because their values need to be evaluated for comparison.

Is there any other way to do equality testing between data like these? Or is there a way to avoid problems like these?

解决方案

In general: no. This sort of equality testing reduces to the halting problem. One way to see this is that we could express the execution of a Turing machine on some input as an infinite data structure like this. Another way of looking at it is that lazy data structures can represent arbitrary suspended computations.

The only real way to avoid problems like this is to either set some additional limitations on your data structure or check for something more limited than equality.

An example of the first approach would be to make cycles in your data type explicit with references of some sort, letting you detect them as you go along. This will limit exactly what you can express with your data structure but will also let your equality predicate detect cycles robustly. I think you could do this with observable sharing; take a look at data-reify for a package that does this. This approach should make checking a very directly recursive structure like your example easy.

For the second approach, you could have a function that returns a Maybe Bool: if it can't figure out whether the two structures are equal or not in X steps, it returns Nothing. Depending on how your data types are created, you could probably ensure that any types beyond a certain size with the same prefix are almost always equal and just rely on that.

这篇关于Haskell中的两个无限数据结构之间是否可以进行平等测试？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！