1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ You beta reduced it correctly and it can't be reduced further and there are no free variables in the expression. $\endgroup$ – DanielV May 9 at 18:24
  • $\begingroup$ In our school materials and on this page jacksongl.github.io/files/demo/lambda/index.htm#firstPage this (lambda f s e. e f s) 1 2 is evaluated as 1 2 $\endgroup$ – T.Poe May 9 at 19:05
  • $\begingroup$ Try typing in (lambda f s e . (e f s)) 1 2 $\endgroup$ – DanielV May 9 at 21:20
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ When you write $(\lambda f. (\lambda s. (\lambda e. e) f)s)$, do you mean $(\lambda f. (\lambda s. (\lambda e. ((e f) s))))$? I can't think what rule would produce the former bracketing. $\endgroup$ – Tanner Swett May 9 at 20:51
  • $\begingroup$ Yeah, usually $\lambda abc.xyz$ is read as $\lambda a.(\lambda b.(\lambda c.((xy)z)))$ $\endgroup$ – DanielV May 9 at 21:04
  • $\begingroup$ The document referenced in the comments (homepage.cs.uiowa.edu/~slonnegr/plf/Book/Chapter5.pdf page 142) uses the same convention, I think the program is just wrong. $\endgroup$ – DanielV May 9 at 21:09
  • $\begingroup$ @Tanner Swett Yes, of course, thank you. I fixed it. $\endgroup$ – lemontree May 9 at 21:56
  • $\begingroup$ @DanielV It's really just conventions, I remember to have seen both. I don't think the lambda calculator (or the book) can be called wrong about it, just careless for not precisely defining what they mean by their syntax. $\endgroup$ – lemontree May 9 at 22:00

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.