Are there any techniques for solving functional equations for unknown functions in lambda calculus?

Suppose I have the identity function defined extensionally as such:

$I x = x$

(that is, by writing down an equation for the expected behaviour of that function) and now I want to solve it for $I$ by doing some algebraical transformation to get the intensional formula for that function:

$I = \lambda x.x$

that tells how exactly does the function do what was expected (that is, how to implement it in lambda calculus).

Of course the identity function is used just as an example. I'm interested in more general methods of solving such equations. In particular, I would like to find a function $B$ that satisfies the following requirement:

$B\;f\;(\lambda x.M) = (\lambda x.f M)$

that is, "injects" the given function $f$ into the given lambda function $(\lambda x.M)$ before its "body" $M$ (which is some arbitrary lambda expression), possibly by taking it apart and constructing a new one, so that it became a parameter the function $f$ is applied to.


This is a known problem, known as Higher Order Unification.

Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used extensively in, among other things, typechecking of dependently-typed programs with metavariables or pattern matching. This fragment is where unification variables are applied only to distinct bound program variables.

This paper provides a great tutorial of how higher order unification works, and walks through a (relatively) simple implementation of it.

Unfortunately, it doesn't look like your function falls into this pattern fragment. That said, what I'm looking seeing is pretty similar to function composition. Does the following function satisfy your property?

$B = \lambda f\ g\ x\ \ldotp f\ (g\ x) $

We have:

  • $B\ f\ (\lambda x . M)$
  • $= B\ f\ (\lambda y . [y/x]M)$ by $\alpha$-equivalence
  • $ = \lambda x . f\ ((\lambda y. [y/x]M) x) $
  • $= \lambda x . f\ ([x/y][y/x]M)$
  • $= \lambda x . f\ M$
  • 1
    $\begingroup$ Yup, seems like it :) The funny thing is, I almost got that solution, but from some reason I thought that calling $(\lambda x.M)$ on something would "execute it", messing up the expression :q What I missed is that we can substitute the variable with another variable bound outside. $\endgroup$ Nov 9 '17 at 7:31
  • 1
    $\begingroup$ Thanks for the link to the paper too, I'll check it out, and I'll accept your answer in a couple of days to give other people a chance too. $\endgroup$ Nov 9 '17 at 7:32
  • 3
    $\begingroup$ Is this higher order unification? The question seems to be about the untyped lambda calculus rather than the simply typed lambda calculus. $\endgroup$ Nov 9 '17 at 9:07

I think I have a partial answer, regarding the equation with the identity function:

$I x = x$

We want to solve it by finding the formula for $I$, which will be of the form $(\lambda p.M)$ with some yet unknown expression $M$ as its body. Let's substitute it for $I$ in the original equation:

$(\lambda p.M)\; x = x$

then apply the function to $x$ on the left hand side:

$M[p/x] = x$

But what do we have here? :> This equation is the formula for the expression $M$ we're looking for, after substituting every occurrence of $p$ in it with $x$, and it says that it should look like the right hand side afterwards :) In other words, the function we were looking for is:

$I = (\lambda x.x)$

which of course is the right answer :)

Let's try the same approach to find the formula for the $\omega$ combinator. We want it to work in such a way that, when applied to itself, will produce itself applied to itself:

$\omega\;\omega = \omega\;\omega$

Now let's find the formula for $\omega$ which is of the form $(\lambda x.M)$ for some yet unknown expression $M$. Substituting this into the equation we get:

$(\lambda x.M)\;\omega = \omega\;\omega$

Applying it to the parameter on the left hand side gives the formula for $M$:

$M [x/\omega] = \omega\;\omega$

This says that after substituting every occurrence of $x$ in $M$ with $\omega$ it produced $\omega\;\omega$, so we can deduce that the original expression $M$ before substitution should have been $x\;x$, so the function we were looking for should look like this:

$\omega = (\lambda x.x\;x)$

which is indeed the case :)

I have a feeling, though, that it might get so easy just because the right hand side was already in the form we're looking for.

  • $\begingroup$ Is there an algorithmic way of going from $M [x/\omega] = \omega\;\omega$ to $\omega = (\lambda x.x\;x)$ though? $\endgroup$ Nov 9 '17 at 12:17
  • $\begingroup$ In these two simple cases – yes, there is: simply reverse the substitution. But as I said, these cases might work by pure "luck": that the right hand side is already in the required form. When I tried it with some more complex examples, it didn't work. That's what I'm looking for, though: for an algorithmic way. $\endgroup$ Nov 9 '17 at 12:52
  • 1
    $\begingroup$ Note that $\omega\omega=\omega\omega$ is satisfied by any choice of $\omega$, in a trivial way. An algorithm to solve that equation for $\omega$ can output any term. $\endgroup$
    – chi
    Nov 9 '17 at 15:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.