[Solved]: Free and bound variables

Problem Detail: 

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.

Asked By : Totoro

Answered By : Gilles

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/33465

 Ask a Question

 Download Related Notes/Documents