Iam a beginner in Lambda Calculus, I have a expression saying


Here y is a free variable and x is a bound variable. My question is what would be the value of the expression (which has free variables).

  • 1
    $\begingroup$ What do you mean by value? Are you talking about the semantic notion of value, that is, are you asking what the mathematical meaning of $\lambda x . x y$ is? Or are you asking about the syntactic notion of value, i.e., what is the normal form, or "final result", of reducing $\lambda x . x y$? $\endgroup$ – Andrej Bauer Dec 23 '13 at 7:15
  • 1
    $\begingroup$ Also, is this supposed to be typed or untyped $\lambda$-calculus? $\endgroup$ – Andrej Bauer Dec 23 '13 at 7:15
  • $\begingroup$ Yes Iam asking about the "final result" of reducing λx.xy. The reason for my question is that while trying to learn about the substitutions in lambda calculus I got struck with resolving free and bound variables concept. $\endgroup$ – prasonscala Dec 23 '13 at 8:42
  • $\begingroup$ Perhaps you're interested in $(\lambda x.x)y = y$? $\endgroup$ – Yuval Filmus Dec 23 '13 at 9:35
  • 1
    $\begingroup$ Did you check out the lambda-calculus tag info? $\endgroup$ – Guy Coder Dec 23 '13 at 17:02

The term $\lambda x . x y$ is in normal form. It does not reduce any further.

In general, to find out these things, you can just type them into a $\lambda$-calculus calculator. One is available in my PL zoo (hmm, it is momentarily under construction):

lambda @ programming languages zoo
Type Ctrl-D to exit or "#help;" for help.
# #constant y ;
y is a constant.
# ^ x . x y ;
    = λ x . x y

The language wants you to declare free variables as constants, which is why we first explain that y is a known constant.

| cite | improve this answer | |
  • $\begingroup$ Why does the system require declaring free variable, rather than finding them on its own? $\endgroup$ – babou Feb 18 '14 at 10:26
  • $\begingroup$ To protect against typos. Feel free to modify the source code. $\endgroup$ – Andrej Bauer Feb 18 '14 at 19:14
  • $\begingroup$ Good reason ... I was just curious. Thanks for the code, but not right now :) $\endgroup$ – babou Feb 19 '14 at 0:49

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.