Каковы современные методы решения функциональных уравнений?

Предположим, что вы хотите найти программу λ-calculus, 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)))

Существует ли какая-либо стратегия для решения таких уравнений λ-исчисления автоматически? Каково состояние искусства в этом вопросе?

Ответ 1

В общем, унификация более высокого порядка неразрешима, поэтому вы не можете надеяться на общую процедуру поиска решений этих уравнений.

Проделана значительная работа по поиску решений таких проблем, но я не знаю никого из того, что дает ответ на вашу конкретную проблему. В этом ответе кратко изложены хорошие ссылки: Унификация более высокого порядка

Ответ 2

Я не уверен в современном уровне, но Уильям Э. Бирд работает над реляционными переводчиками (например, этот документ) позволяет синтезировать такие программы.

Также см. его обсуждение PolyConf для некоторых аккуратных вещей при поиске условий программы. Ваши примеры кажутся такими, что их было бы довольно легко выразить таким образом.