関数式を解くための最先端の方法は何ですか？

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

通常、higher order unificationは決定不可能なので、これらの種類の方程式の解を見つける一般的な手順は期待できません。

このような問題の解決策を見つけるには相当の作業がありましたが、私はあなたの特定の問題に対する答えを与えるものは何もわかりません。いくつかの良い参照は、この答えに要約されています：Higher-order unification

Answer 2

私は芸術の状態についてはよく分からないんだけど、（例えばthis paperなど）リレーショナル通訳のウィリアム・E・バードの作品は、この種のプログラムの合成を可能にします。

また、彼のPolyConf talkを参照して、番組の用語を検索する際のいくつかのすてきなことを見てください。あなたの例は、そのように表現するのがかなり容易であるように思えます。