如何比较两个函数的等价性，如 (λ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 求解器会尽最大努力，有时会回答不知道"而不是相等"或不相等".在 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屋！