# 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$? Dec 23, 2013 at 7:15
• Also, is this supposed to be typed or untyped $\lambda$-calculus? Dec 23, 2013 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. Dec 23, 2013 at 8:42
• Perhaps you're interested in $(\lambda x.x)y = y$? Dec 23, 2013 at 9:35
• Did you check out the lambda-calculus tag info? Dec 23, 2013 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? Feb 18, 2014 at 10:26
• To protect against typos. Feel free to modify the source code. Feb 18, 2014 at 19:14
• Good reason ... I was just curious. Thanks for the code, but not right now :) Feb 19, 2014 at 0:49

You're asking what the value of $$λx·xy$$ as if the expression, itself, were a math problem to somehow be solved. The situation is similar to asking what the value of "4/3" is, as if it were to be treated as the math problem of "divide 4 by 3". However, there's nothing in this that excludes the expression "4/3", itself, from being the final answer to the question, though the kind of thing you have in mind is more akin to answering the question with "1.333⋯". So long as you're able to do reductions like "8/6 = 4/3" or "4/1 = 4", then you're fine just using the fraction notation as a final answer. Similarly, you can go $$λx·(λz·z)xy = λx·xy$$ and then treat the latter as "fully reduced" or go $$λx·yx = y$$.

If you want an answer more like $$1.333⋯$$, thinking of $$λx·(⋯)$$ as analogous to $$(⋯)/x$$ - which indeed it is - then in addition to such rules as $$(yx)/x = y$$ (the η-rule), you'd want ways to crunch other $$(⋯)/x$$'s.

So, make a distinction between terms, like $$a$$ and $$b$$ that contain no $$x$$'s in them, versus terms like $$u$$ and $$v$$ that do contain $$x$$'s in them, but where $$u ≠ x$$ and $$v ≠ x$$. Then, treating $$λx·(⋯)$$ as just a fancy way of writing $$(⋯)/x$$, write the following: $$x/x = I,\quad a/x = Ka,\quad (xx)/x = D,\\ (ax)/x = a,\quad (au)/x = Ba(u/x),\quad (xb)/x = Tb,\quad (vb)/x = C(v/x)b,\\ (ux)/x = W(u/x),\quad (vx)/x = U(v/x),\quad (uv)/x = S(u/x)(v/x).$$ Impose the following as axioms $$Ix = x,\quad Kxy = x,\quad Dx = xx,\\ Bxyz = x(yz),\quad Txy = yx,\quad Cxyz = xzy,\\ Wxy = xyy,\quad Uxy = y(xy),\quad Sxyz = xz(yz),$$ as well as the axiom $$A = (Ax)/x$$ for any λ-term $$A$$. Then you can solve your problem by saying that $$yx/x = Ty$$, or in λ-term notation: $$λx·yx = Ty$$.

Internal consistency of the scheme is ensured, for instance, in that $$(xzy)/z = C((xz)/z)y = Cxy = (Cxyz)/z,$$ with similar results for the other cases. The extra axiom $$A = (Ax)/x$$ makes further reductions possible, such as $$S(Ka)x = (S(Ka)xy)/y = (Kay(xy))/y = (a(xy))/y = Ba((xy)/y) = Bax,\\ S(Ka) = (S(Ka)x)/x = (Bax)/x = Ba,\\ BaI = (BaIx)/x = (a(Ix))/x = (ax)/x = a,\\ BIa = (BIax)/x = (I(ax))/x = (ax)/x = a,\\ B(Bab)cx = Bab(cx) = a(b(cx)),\\ (a(b(cx)))/x = Ba((b(cx))/x) = Ba(Bb((cx)/x))) = Ba(Bbc),\\ B(Bab)c = (B(Bab)cx)/x = (a(b(cx)))/x = Ba(Bbc),\\ S(Ka)(Kb) = (S(Ka)(Kb)x)/x = (Kax(Kbx))/x = (ab)/x = K(ab),\\ SKa = (SKax)/x = (Kx(ax)/x = x/x = I,\\ SK = (SKx)/x = I/x = KI.$$ where neither $$x$$ nor $$y$$ occur in any of the terms $$a$$, $$b$$ and $$c$$.