Don’t understand unbound variables in a lambda calculus expression

lambda-calculus

I'm learning lambda calculus. I came across this lambda expression:

lambda f s e . e f s

When I pass arguments 1 and 2 to the expression, it should return 1 2 but I cannot figure out how is that possible. The way I tried to expand this:

(lambda f s e . e f s) 1 2 -> beta reduction (lambda s e . e 1 s) 2 -> beta reduction (lambda e . e 1 2). I don't know what to do next.

When I passed this expression to some online lambda calculus tool, it said that f and s are unbound and it returns 1 2.

Can someone explain and show how the result is obtained here and what am I doing wrong? How is that possible that f and s are unbound? These variables are before the dot so I thought they're bound, or aren't they? Thanks for any help.

Best Answer

Reading the comments, the reason for your confusion are differing bracketing conventions.
The term $\lambda fse.efs$ is omitting brackets (for easier readability), and there has to be a convention how to re-interpret the invisible brackets back into the term. Depending on where the missing brackets are supposed to be, $\lambda fse.efs$ can be two different terms which will have different reduction behavior. To say it a bit more radically, $\lambda fse.efs$ is not actually a lambda-term - it is just an abbreviation for either $(\lambda f. (\lambda s. (\lambda e. ((ef)s))))$ or $(((\lambda f. (\lambda s. (\lambda e. e)))f)s)$. Which of the two terms is meant by the abbreviation $\lambda fse.efs$ depends on bracketing conventions, more precisely on the convention for precedence of abstraction and application.

  1. The reading you and DanielV assumed - which is the more usual convention - is that $\lambda fse.efs = (\lambda f. (\lambda s. (\lambda e. ((ef)s))))$. In this term, all variables are bound, and $(\lambda f. (\lambda s. (\lambda e. ((ef)s)))) 1 2$ reduces to $\lambda e.e 1 2$.
    This is the bracketing that results if one defines that application as precedence over abstraction: First you form possible applications (here: $ef$, $(ef)s$), and afterwards abstractions (here: $\lambda e$, $\lambda s$, $\lambda f$) which have the applications as subterms (so the scope of the lambda abstractions extends as far right as possible).
  2. The reading the Lambda Calculus interpreter - and likely also your school materials - assume is that $\lambda fse.efs = (((\lambda f. (\lambda s. (\lambda e. e)))f)s)$. In this term, $f$ and $s$ are unbound, and $(((\lambda f. (\lambda s. (\lambda e. e)))f)s) 1 2$ reduces to $1 2$ as shown in the lambda calculator.
    This is the bracketing that results if one defines that abstraction has precedence over application: First you form possible abstractions (here: $\lambda e$, $\lambda s$, $\lambda f$), and afterwards applications (here: $((\lambda f. (\lambda s. (\lambda e. e)))f$, $(((\lambda f. (\lambda s. (\lambda e. e)))f)s)$) which have the abstractions as subterms (so the scope of the lambda abstractions is as narrow as possible).

So which is the "correct" reduction depends on which term $\lambda fse.efs$ is supposed to mean. Both readings are possible, but they are different terms and result in different reductions.
So take another close look at the conventions for omission of brackets (at the very beginning where the syntax of lambda expressions is defined) in the materials you're using. It has to be defined somewhere, otherwise, your material's notation is sloppy. (If they don't explicitly define it, then just assume that what the lambda calculator tells you is the desired reading.) Once you insert all the missing brackets, you'll see how the beta reduction works out.

Related Question