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} (&[xleftarrow A] (f_1[xleftarrow A] A) (f_2[xleftarrow 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
