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$
3
  • 1
    $\begingroup$ You beta reduced it correctly and it can't be reduced further and there are no free variables in the expression. $\endgroup$ Commented May 9, 2019 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$ Commented May 9, 2019 at 19:05
  • $\begingroup$ Try typing in (lambda f s e . (e f s)) 1 2 $\endgroup$ Commented May 9, 2019 at 21:20

1 Answer 1

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$
6
  • 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$ Commented May 9, 2019 at 20:51
  • $\begingroup$ Yeah, usually $\lambda abc.xyz$ is read as $\lambda a.(\lambda b.(\lambda c.((xy)z)))$ $\endgroup$ Commented May 9, 2019 at 21:04
  • 1
    $\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$ Commented May 9, 2019 at 21:09
  • $\begingroup$ @Tanner Swett Yes, of course, thank you. I fixed it. $\endgroup$ Commented May 9, 2019 at 21:56
  • 1
    $\begingroup$ Well on the one hand, the help section of the program says that the disambiguation or parens is unpredictable, on the other hand, they do cite the book as documentation, and the default behavior of the program is nonstandard for no good reason, and for a teaching program no less. So I still will affirm "wrong" even if it others have more forgiving standards. $\endgroup$ Commented May 9, 2019 at 22:10

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.