What are the state-of-art methods for solving functional equations?

Question

Suppose that you want to find a λ-calculus program, T, that satisfies the following equations:

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

On this case, I've manually found this solution:

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

Is there any strategy for solving such λ-calculus equations automatically? What is the state of art on that subject?

Abduction

What notion of equality are you using here? – Squireen

Computational equality*. Please read a = b as a beta reduces to b, in strong normal form. – Abduction

While I find your question interesting I do not think this is a good fit for Stack Overflow. If you are asking about algorithms you should ask on [computer science.SE]. As it stands your question doesn't seem about programming but about algorithm design and it's too broad to be answered on SO (a definite answer to your question would be a book/sets of books). – Bogosian

I didn't know where to post, book suggestions are really welcome. – Abduction

Answer 1

In general, higher order unification is undecidable, so you can't hope for a general procedure for finding solutions to these kinds of equations.

There has been a significant amount of work on finding solutions to such problems, but I don't know of any that gives the answer to your particular problem. Some good references are summarized in this answer: Higher-order unification

Crosslet

Answer 2

I'm not sure about state of the art, but William E Byrd's work on relational interpreters (such as this paper) allows program synthesis of this kind.

Also see his PolyConf talk for some neat stuff on searching for program terms. Your examples seem like they would be fairly easy to express in that way.

Holleran