1
$\begingroup$

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

$\endgroup$
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$ 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

2 Answers 2

2
$\begingroup$

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.

$\endgroup$
3
  • $\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
1
$\begingroup$

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

$\endgroup$

Your Answer

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

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