Was sind die neuesten Methoden zur Lösung von Funktionsgleichungen? Angenommen

Question

, dass Sie ein λ-Kalkül Programm finden wollen, T, dass die folgenden Gleichungen erfüllt:

(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)) 

Auf diesem Fall habe ich festgestellt manuell diese Lösung:

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

Gibt es irgendeine Strategie, um solche λ-Kalkül-Gleichungen automatisch zu lösen? Wie ist der Stand der Kunst zu diesem Thema?

Answer 1

Im Allgemeinen ist higher order unification unentscheidbar, so dass Sie nicht auf ein allgemeines Verfahren zur Suche nach Lösungen für diese Art von Gleichungen hoffen können.

Es gab eine Menge Arbeit an der Suche nach Lösungen für solche Probleme, aber ich kenne keine, die die Antwort auf Ihr spezielles Problem gibt. Einige gute Referenzen sind in dieser Antwort zusammengefasst: Higher-order unification

Answer 2

Ich bin nicht sicher über den Stand der Technik, aber William E Byrd Arbeit an relationalen Interpreter (wie this paper) ermöglicht Programm-Synthese dieser Art.

Siehe auch seine PolyConf talk für einige nette Sachen auf der Suche nach Programmbegriffen. Ihre Beispiele scheinen so zu sein, als wären sie ziemlich einfach auszudrücken.