Moderator: Konzepte der Programmiersprachen
in Exercise 5, where the Y-Operator is applied for obtaining a recursive function application, the expression is reduced as follows in the solution: The "n" in the "f(n+1)" is replaced by the "n+1" argument of the function application.
However, I don't quite understand why we are allowed to do this.
The interpreters that were shown in the lecture would not replace the inner n as they only consider free variables. I would argue that the n is already bound by the inner binding instance and thus is not in the scope of the outer (left) binding instance.
But still it is replaced in the exercise (which makes sense because we want achieve recursion) and the two binding instances seem to refer to the very same bound variables.
So... what are the scopes in lambda calculus, actually? Are there any at all? Does beta reduction make no difference between bound variables and free ones if two binding instances have the same name, and just "stupidly" replaces all occurences of identifiers with the matching name?
Here, the left-most (outer) lambda is not being reduced, it remains untouched.
\beta reduction is being performed in the body of the outer lambda.
like this :
(added square brackets for clarity)
λn.[ (λn.f(n + 1)) (n + 1) ]
= λn.[ f(n+2) ]
Thank you for your response, your brackets made it clearer for me!