求解函数方程的最新方法是啥？

Posted 2023-05-08

【中文标题】求解函数方程的最新方法是啥？

【英文标题】：What are the state-of-art methods for solving functional equations?求解函数方程的最新方法是什么？

【发布时间】：2015-12-17 16:17:21

【问题描述】：

假设您想找到一个满足以下等式的 λ 微积分程序 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)))

是否有任何策略可以自动求解此类 λ 微积分方程？该主题的最新技术水平如何？

【问题讨论】：

你在这里使用什么平等概念？

Computational equality*。请阅读a = b，因为a beta 简化为b，是强范式。

虽然我觉得你的问题很有趣，但我认为这不适合 Stack Overflow。如果你问的是算法，你应该问 [computer science.SE]。就目前而言，您的问题似乎与编程无关，而是与算法设计有关，而且范围太广，无法在 SO 上回答（对您的问题的明确答案是一本书/几本书）。

不知道在哪里发帖，欢迎推荐书籍。

【参考方案1】：

我不确定最先进的技术，但 William E Byrd 在关系解释器（例如 this paper）方面的工作允许进行这种程序合成。

另请参阅他的PolyConf talk，了解有关搜索程序术语的一些简洁内容。您的示例似乎很容易以这种方式表达。

【参考方案2】：

一般来说，higher order unification 是不可判定的，所以你不能指望一个通用的过程来找到这类方程的解。

在寻找此类问题的解决方案方面已经做了大量工作，但我不知道有什么可以为您的特定问题提供答案。这个答案总结了一些很好的参考资料：Higher-order unification