如何比较两个等价函数，如（λx.2* x）==（λx.x+ x）？ [英] How to compare two functions for equivalence, as in (λx.2*x) == (λx.x+x)?

问题描述

有没有办法比较两个函数的平等？例如，（λx.2* x）==（λx.x+ x）应该返回true，因为那些显然是等价的。

Is there a way to compare two functions for equality? For example, (λx.2*x) == (λx.x+x) should return true, because those are obviously equivalent.

推荐答案

一般来说，一般函数相等是不可判定的，所以你必须选择一个子集您可能会考虑这些部分解决方案中的一些：

It's pretty well-known that general function equality is undecidable in general, so you'll have to pick a subset of the problem that you're interested in. You might consider some of these partial solutions:

• Presburger算术是一阶逻辑+算术的可判定片段。


• universe 包为有限域的总函数提供函数等式测试。


• 你可以检查你的函数在一堆作为未经测试的输入的平等的证据;请查看 QuickCheck 。


• SMT解决方案尽力而为，有时会回应don不知道而不是等于或不等于。在Hackage上有几个绑定到SMT解算器;我没有足够的经验来建议最好的一个，但Thomas M. DuBuisson建议 sbv 。


• 有一个有趣的研究小组的功能平等和其他事情的决策;本研究的基础知识在博客文章看似不可能的功能程序中有所描述。 （注意紧凑是一个非常强大和非常微妙的条件！这不是大多数Haskell函数满足的）


• 如果你知道你的函数是线性的，你可以找到一个基础的源空间;


• 您可以尝试定义自己的表达式语言，证明该语言的等价性是可判定的，然后在Haskell中嵌入该语言。这是最灵活，但也是最困难的进步方式。

• Presburger arithmetic is a decidable fragment of first-order logic + arithmetic.
• The universe package offers function equality tests for total functions with finite domain.
• You can check that your functions are equal on a whole bunch of inputs and treat that as evidence for equality on the untested inputs; check out QuickCheck.
• SMT solvers make a best effort, sometimes responding "don't know" instead of "equal" or "not equal". There are several bindings to SMT solvers on Hackage; I don't have enough experience to suggest a best one, but Thomas M. DuBuisson suggests sbv.
• There's a fun line of research on deciding function equality and other things on compact functions; the basics of this research is described in the blog post Seemingly impossible functional programs. (Note that compactness is a very strong and very subtle condition! It's not one that most Haskell functions satisfy.)
• If you know your functions are linear, you can find a basis for the source space; then every function has a unique matrix representation.
• You could attempt to define your own expression language, prove that equivalence is decidable for this language, and then embed that language in Haskell. This is the most flexible but also the most difficult way to make progress.

这篇关于如何比较两个等价函数，如（λx.2* x）==（λx.x+ x）？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！