什么是最先进的求解函数方程的方法？

Question

假设您想要找到T满足以下等式的λ演算程序:

(T (? f x . x))            = (? a t . a)
(T (? f x . (f x)))        = (? a t . (t a))
(T (? f x . (f (f x))))    = (? a b t . (t a b))
(T (? f x . (f (f (f x)))) = (? a b c t . (t a b c))

在这种情况下,我手动找到了这个解决方案:

T = (? t . (t (? b c d . (b (? e . (c e d)))) (? b . b) (? b . b)))

有没有自动解决这种λ演算方程的策略？这个主题的现状是什么？

Answer 1

我不确定最先进的技术,但William E Byrd关于关系翻译的工作(如本文)允许这种程序合成.

另外,请参阅他的PolyConf演讲,了解一些搜索程序术语的好东西.您的示例似乎很容易以这种方式表达.

Answer 2

一般来说，高阶统一是不可判定的，因此您不能指望找到此类方程的解的通用过程。

在寻找此类问题的解决方案方面已经进行了大量工作，但我不知道有任何工作可以为您的特定问题提供答案。这个答案总结了一些很好的参考：高阶统一