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$ Dec 23, 2013 at 7:15
  • 1
    $\begingroup$ Also, is this supposed to be typed or untyped $\lambda$-calculus? $\endgroup$ Dec 23, 2013 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$ Dec 23, 2013 at 8:42
  • $\begingroup$ Perhaps you're interested in $(\lambda x.x)y = y$? $\endgroup$ Dec 23, 2013 at 9:35
  • 1
    $\begingroup$ Did you check out the lambda-calculus tag info? $\endgroup$
    – Guy Coder
    Dec 23, 2013 at 17:02

1 Answer 1


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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.