$\lambda$-calculus: find $F$ such that $FI = x$ and $FK = y$

lambda-calculustype-theory

I'm learning some $\lambda$-calculus using the following book: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf

I'm having some trouble with exercise 2.12 (iii) on page 15. It asks us to find a $\lambda$-term $F$ such that $FI = x$ but $FK = y$, where $x$, $y$ are (presumably) some arbitrary variables (wheras $I = \lambda x.x$ and $K = \lambda xy.x$).

All my failed tries have one thing in common: I do not know how to deal with the different "arities" of $I$ and $K$. The only difference between $I$ and $K$ is the number of arguments–both terms return their first argument, except $K$ also takes a second one before doing so.

Hence I need to find an $F$ which essentially checks for the number of arguments that its input takes. However, I don't have an idea of how to find such $F$.

Best Answer

Welcome to Math.SE!

You have correctly intuited that we somehow need to end up with two functions of equal "arity"* to solve this problem. However, you don't need (nor can you have) a term that checks for the number of arguments that its input takes.

If you play around with the standard combinators (Example 2.10) for a bit, you'll notice the following:

  • $SIfI \rightarrow_\beta II(fI) \rightarrow_\beta I(fI) \rightarrow_\beta fI$ and
  • $SKfK \rightarrow_\beta KK(fK) \rightarrow_\beta K$

so if you choose the term $f$ to have "arity" 3, the lambda expression $(\lambda e.Sefe)$ will always reduce to something of "arity" 2 when applied to $I$ or $K$. We don't need to check the arity: we can just arrange for it to be a fixed, known quantity. From here on, a clever choice of $f$ will lead us to the solution.

Set $f$ to $(\lambda a. \lambda b. \lambda c. c)$. We have

  • $SIfIyx \rightarrow_\beta(\lambda a. \lambda b. \lambda c. c)Iyx \rightarrow_\beta x$ and
  • $SKfKyx \rightarrow_\beta Kyx \rightarrow_\beta y$

Consequently, the term $\lambda e.Se(\lambda a. \lambda b. \lambda c. c)eyx$ has the desired property (you can simplify it further if you wish).

* The concept of "arity" is of course not precise. Dwelling too much on it would potentially mislead, and at best distract from the relevant considerations. E.g. does it really make sense to say that $I$ has arity 1? After all, one could equally well say that $I$ has arity 3 since it takes 3 arguments in an expression such as $I(\lambda a. \lambda b.a)pq$.

Related Question