title: What are the state-of-art methods for solving functional equations?
body: <p>Suppose that you want to find a λ-calculus program, <code>T</code>, that satisfies the following equations:</p>
  
  <pre><code>(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))
  </code></pre>
  
  <p>On this case, I've manually found this solution:</p>
  
  <pre><code>T = (λ t . (t (λ b c d . (b (λ e . (c e d)))) (λ b . b) (λ b . b)))
  </code></pre>
  
  <p>Is there any strategy for solving such λ-calculus equations automatically? What is the state of art on that subject?</p>