4

Let's say I have a lambda expression like this:

$$(\lambda a . (ab))(c)$$

It reduces to

$$cb$$

But let's say I have a nested function

$$(\lambda a . (\lambda x.(ax)))(b)$$

Does this reduce to

$$\lambda x.(bx)$$

or to

$$\lambda x.(ax)$$

In other words, does the lambda calculus use lexical scoping?

Also, if lexical scoping is used, what happens if the bound variable uses the same name within and without the function body? In other words, how does this get reduced?

$$(\lambda x.(x\lambda x.x))a$$

Does it reduce to

$$a\lambda x.x$$

or

$$a\lambda a.a$$

azani
  • 623
  • 1
    Everything Thomas Andrews said in his answer is correct, but if you really want to see the formal way to do it, you should look at the first chapter of the giant Henk Barendregt book. Lambda-terms are defined not as strings but as equivalence classes of "pre-terms" that are equivalent under $\alpha$-conversion, and substitution is carefully defined to avoid free variable capture. – MJD Jan 11 '15 at 03:56
  • It looks like there are at least two Barendregt books that seem like they may be applicable. Could you disambiguate? – azani Jan 11 '15 at 04:09
  • 1
    The Lambda Calculus, Its Syntax and Semantics – MJD Jan 11 '15 at 04:15

2 Answers2

5

Everything works as it should if this were about a pure functional programming language. Yes, it is lexical scoping.

$(\lambda x.(x\lambda x.x))a = a\lambda x.x$.

Basically, $\lambda x.x = \lambda y.y$. You are defining operations as you would expect in a programming language. So you do have to be careful about cases like $\lambda x.(x\lambda x.x)$.

So $\lambda a . (\lambda x.(ax))$ is an operation which, given applied to $b$, returns $\lambda x.(bx)$.

The worst case is something like this:

$$(\lambda a.\lambda x.(ax))x$$

A naive approach would yield $\lambda x.(xx)$. The rigorous definition to deal with this is a bit nightmarish. The Wikipedia page for $\lambda$-calculus has this fairly opaque language:

The freshness condition (requiring that y is not in the free variables of r) is crucial in order to ensure that substitution does not change the meaning of functions. ... In general, failure to meet the freshness condition can be remedied by alpha-renaming with a suitable fresh variable.

Basically, we have to be careful when apply $\lambda x.E$ to an expression with a free $x$ variable in it.

Thomas Andrews
  • 177,126
  • So only free variables are substituted? So how does that interact with the rule that "If two variables have the same name, they are the same thing." Or is that just a simplification and it only applies to free variables, not bound variables. – azani Jan 11 '15 at 03:24
  • 2
    Exactly. It really is the only reasonable way to do it. In particular. It's particular difficult, however, if you do: $$(\lambda a.\lambda x.ax)x$$ Now what do you do? It should not be $\lambda x.xx$. You have to be very careful there, and I've forgotten what the "right" think to do, but that should come out as $\lambda y.xy$, for some new variable $y$. – Thomas Andrews Jan 11 '15 at 03:27
  • It's probably best just to reference the Wikipedia page for a more thorough breakdown. But everything has to work "as expected." – Thomas Andrews Jan 11 '15 at 03:36
  • You keep saying "as expected" and "as it should". What do you mean by that? – azani Jan 11 '15 at 03:39
  • From an intuitive functional programming point of view. @azani It is actually painful to make it all rigorous, and even the wikipedia page resorts to the language: "In general, failure to meet the freshness condition can be remedied by alpha-renaming with a suitable fresh variable," to describe situations like my comment about $(\lambda a.\lambda x.(ax))x$ not being $\lambda x.(xx)$. – Thomas Andrews Jan 11 '15 at 03:41
  • There is an area similar (basically equivalent) to $\lambda$-calculus that I learned first, which always made it clearer for me, combinatory logic. Perhaps that is where my intuition about it comes from.... – Thomas Andrews Jan 11 '15 at 03:47
  • The way I understand the above (please correct me if I am wrong) would be to add a small modification. Instead of using the same names for free and bound variables, use a special unique name for all bound variable. (Say, capital letter) So $$(\lambda A.\lambda X.AX)x$$ is easily reduced to $$\lambda X.Xx$$ I realize this is technically stepping outside the lambda calculus, but it seems to highlight that bound variables are treated differently than free variables. – azani Jan 11 '15 at 03:56
  • Except that it would reduce to $\lambda X. xX$. But yes. – Thomas Andrews Jan 11 '15 at 04:00
  • In combinatory logic, you can create a combinator that is "like" $\lambda x.E$ for some expression $E$, but which actually removes the $x$ completely, avoiding the confusion between bound and unbound, which is a bit of a nightmare in $\lambda$-calculus. – Thomas Andrews Jan 11 '15 at 04:02
  • And that isn't stepping outside the calculus - a rigorous definition would have to do something like this, when transforming $(\lambda x.E_1)E_2$, you'd have to first transform $E_1$ so that none of the $\lambda$s inside use any free variables in $E_2$. – Thomas Andrews Jan 11 '15 at 04:06
2

The rule is simply that the lambda variable is a "bound" variable not to be confused with any "free" variables, and its scope is the function definition. Any variables outside the function with the same name are distinct.

An easy way to see what is going on is to replace the bound variables with de-Bruign indices, replacing from the innermost lambda outwards. For your example

  • (λx.(x (λx.x))) a

First rename the bound variables to indices:

  • (λx.(x (λ\1.\1))) a
  • (λ\2.(\2 (λ\1.\1))) a

Then evaluate by $\beta$-substitution:

  • [(\2 λ\1.\1) : \2=a]
  • a (λ\1.\1)

Notice that the de-Bruign substitution only uses local information, it only looks at what's inside the function.

Toby Kelsey
  • 31