6
$\begingroup$

I am familiar with free and bound variables theory , but while learning I somewhere saw this lambda expression

((lambda var ((fn1 var) & (fn2 var))) argument)

From what I have learned it seems to me as var is bounded in both fn1 and fn2. But the reference from where the expression is taken says that both var are free and hence can be substituted by argument while doing β-reduction .

Someone please clear my doubt.

$\endgroup$
9
$\begingroup$

In the usual mathematical notation: $(\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) A$

The two green occurrences of $\color{green}{x}$ in the subterms $f_1 \color{green}{x}$ and $f_2 \color{green}{x}$ are bound in the term $\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))$. The binding occurrence is the blue $\color{blue}{x}$.

When evaluation $(\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) A$ by beta-reduction of the top redex, the result is the substitution of $A$ for the free occurrences of $x$ in the body of the lambda abstraction. If $\&$, $f_1$ and $f_2$ are variables, then the result is simply $$ (\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) A \to_{\beta} (\& (f_1 A) (f_2 A)) $$ If $\&$, $f_1$ and $f_2$ are lambda-terms, then they may contain free occurrences of $x$, which need to be substituted. $$ (\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) A \to_{\beta} (\&[x\leftarrow A] (f_1[x\leftarrow A] A) (f_2[x\leftarrow A] A)) $$

Note that the notion of free or bound variable is really a free or bound occurrence of a variable, in a given term. A variable is often said to be free in a term if it has a free occurrence. For example, in the term $(\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) (g \, \color{magenta}{x})$, the green occurrences of $\color{green}{x}$ are bound, and the magenta occurrence of $\color{magenta}{x}$ is free. In the term $\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))$, the two occurrences of $\color{green}{x}$ are free.

$\endgroup$
  • $\begingroup$ But if x is bounded by λx why are we substituting A with x , this is still unclear to me. As you said if & ,f1 ,f2 are variables then aren't they supposed to be substituted instead of x because they will be so called free variables. $\endgroup$ – Totoro Nov 24 '14 at 12:43
  • 1
    $\begingroup$ @Batman Substituting the argument for the bound variable is the definition of beta reduction. $\endgroup$ – Gilles 'SO- stop being evil' Nov 24 '14 at 12:50
5
$\begingroup$

In a nutshell

There are two issues that justify the statement of your reference:

  • The free or bound character of a variable depends on how much context you are considering, and whether it contains a binding occurrence of the variable

  • A variable may be re-bound within the scope of an existing binding, so that removing that binding does not preclude that some occurrences may still be bound.

More detailed explanation

There are really several issues, some of which do not seem to be emphasized by Gilles'answer, which is very good and need not be duplicated here for the issues it addresses (as I understand it).

Being free or bound is a property of variable occurrences, not of variables themselves. Note that the occurrence that follows the $\lambda$ (in blue in Gilles'examples) is a binding occurrence, and is neither free nor bound.

The other issue is that, for a given occurrence, being free or bound is dependent on the part of the context you are considering.

If you examine the example: $$\color{purple}{(}\lambda \color{blue}{x}. \color{red}{(\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))}\color{purple}{)}A$$ the $\color{blue}{\text{blue}}$ occurrence of $x$ is a binding occurrence. The $\color{green}{\text{green}}$ occurrences of $x$ are bound by this binding occurrence whenever you consider a context that includes the binding occurrence, such as the whole $\lambda$-expression or just the part between the $\color{purple}{\text{purple}}$ parentheses.

But if you consider a smaller context, abstracting away the part containing the binding occurrence, as for example the sub-expression in $\color{red}{\text{red}}$, the $\color{green}{\text{green}}$ (occurrences of the) variable $x$ are free in this subexpression.

So being free or bound is dependent on the occurrence considered and on the context considered.

But it may be said that variable $x$ is free in some (sub-)expression when it constitutes a context where $x$ is never bound. Note that a variable $x$ can be free for some occurrences and bound for others in the same $\lambda$-expression, depending on the scope of binding occurrences.

The confusion you are confronted with comes from the fact that when you do the $\beta$-reduction, applying the function between $\color{purple}{\text{purple}}$ parentheses to the argument $A$, you replace the whole redex by just the part in $\color{red}{\text{red}}$ where the variable $x$ is indeed free, now that the binding occurrence is removed, prior to making the substitution of $x$ for the arguments.

But the situation could be more complex. There could be several binding occurrences of $x$ as in:

$$\color{purple}{(}\lambda \color{blue}{x}. \color{red}{(\& (f_1 \color{green}{x}) (\lambda \color{magenta}{x}.f_2 \color{green}{x}))}\color{purple}{)}A$$

Now both $\color{green}{\text{green}}$ $x$ are bound, but the first is bound by the $\color{blue}{\text{blue}}$ binding occurrence, while the second is bound by the $\color{magenta}{\text{magenta}}$ binding occurrence.

When you do the $\beta$-reduction as before, you remove as before the $\color{blue}{\text{blue}}$ binding occurrence of $x$ and substitute the now free occurrences of $x$ for the argument. But only the first green occurrence is free, while the second is still bound by the $\color{magenta}{\text{magenta}}$ binding occurrence.

That is why your reference insisted that the variable occurrences were (now) free for being substituted by the arguments. There could also be non free occurrences, as in the example I just gave, despite the fact that a binding occurrence of the variable had been removed.

$\endgroup$
  • $\begingroup$ Isn't the scope of λx in (λx.(&(f1x)(f2x)))A is upto far right and f2x comes in it. $\endgroup$ – Totoro Nov 24 '14 at 13:32
  • $\begingroup$ @Batman This is true in the original example. But it is not quite true in the modified version I give as second example. The magenta binding has its own scope, that becomes a "hole" in the scope of the blue binding. So that f2x is protected against substitution of x in the β-reduction, this second x being still bound. That is what explains the statement of your reference, checking that all occurences of x are indeed free and can all be substituted by the argument. They might not all be free. $\endgroup$ – babou Nov 24 '14 at 15:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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