Don't understand unbound variables in a lambda calculus expression 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.
 A: 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.


*

*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).  

*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.
