# how to solve this lambda expression with free variable/s

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

(λx.xy)

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

• 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$? – Andrej Bauer Dec 23 '13 at 7:15
• Also, is this supposed to be typed or untyped $\lambda$-calculus? – Andrej Bauer Dec 23 '13 at 7:15
• 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. – prasonscala Dec 23 '13 at 8:42
• Perhaps you're interested in $(\lambda x.x)y = y$? – Yuval Filmus Dec 23 '13 at 9:35
• Did you check out the lambda-calculus tag info? – 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.

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