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).
5
-
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 BauerDec 23, 2013 at 7:15
-
1$\begingroup$ Also, is this supposed to be typed or untyped $\lambda$-calculus? $\endgroup$– Andrej BauerDec 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$– prasonscalaDec 23, 2013 at 8:42
-
$\begingroup$ Perhaps you're interested in $(\lambda x.x)y = y$? $\endgroup$– Yuval FilmusDec 23, 2013 at 9:35
-
1$\begingroup$ Did you check out the lambda-calculus tag info? $\endgroup$– Guy CoderDec 23, 2013 at 17:02
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
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.
answered Dec 23, 2013 at 16:13
-
$\begingroup$ Why does the system require declaring free variable, rather than finding them on its own? $\endgroup$– babouFeb 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$– babouFeb 19, 2014 at 0:49