That being said, it can sometimes be useful to do such renamings for easier readability. Therefore it is unproblematic not to rename them during the application. So the x's bound by the inner abstraction and the x at the end of the term are indeed different variables belonging to different abstractions. So the only x that will be substituted by N is the last one, hence (λx.(λf.λx.fx)((λf.λx.fx)x))N will reduce to (λf.λx.fx)((λf.λx.fx)N) - the x's bound in the subterms (λf.λx.fx) remain unchanged. The only free occurrence of x in that term is the very last one the other two xes in the two subterms (λf.λx.fx) are bound by their respective λx's. the term obtained by substituting every free (!) occurence of x in (λf.λx.fx)((λf.λx.fx)x) by N (substitution only operates on free variables by definition). You can try this out: If you apply λx.(λf.λx.fx)((λf.λx.fx)x) to some term N, then according to the definition of beta reduction, this term will reduce to (λf.λx.fx)((λf.λx.fx)x), i.e. This is simply due to the way the evaluation of lambda terms works: If there is a new abstraction over the same variable, then the old abstraction further out will ultimately lose its effect in the subterm with the new abstraction, and the variables bound by the inner abstraction will effectively be different variables than the ones only bound by the outer abstraction. The two uses of x are indeed different variables, but this is already encoded in the term: In general, a new abstraction in a subterm will "overwrite" the binding of further outmost abstractions. "Capturing" bound variables doesn't hurt that much: In λx.(λf.λx.fx)((λf.λx.fx)x) Capture avoidance is to avoid capturing free variables.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |