Scope in Lambda Calculus

Moderator: Konzepte der Programmiersprachen

topracer
Mausschubser
Mausschubser
Beiträge: 53
Registriert: 10. Jan 2014 19:14

Scope in Lambda Calculus

Beitrag von topracer » 3. Mär 2019 19:56

Hello,

in Exercise 5, where the Y-Operator is applied for obtaining a recursive function application, the expression is reduced as follows in the solution:
Y-Operator_lambdas.png
Y-Operator_lambdas.png (8.41 KiB) 111 mal betrachtet
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?


Best regards,
Frederic

aditya_oak
Neuling
Neuling
Beiträge: 3
Registriert: 8. Okt 2018 11:24

Re: Scope in Lambda Calculus

Beitrag von aditya_oak » 3. Mär 2019 22:19

Hello,

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) ]
= λn.f(n+2)

Regards,
Aditya

topracer
Mausschubser
Mausschubser
Beiträge: 53
Registriert: 10. Jan 2014 19:14

Re: Scope in Lambda Calculus

Beitrag von topracer » 4. Mär 2019 19:19

Ohh... Of course the function application is inside the scope of the leftmost binding, so the substitution is done in the scope of the inner binding instance. Then it makes sense... I mistakenly assumed that the function to which the argument is applied was the whole left side of it.
Thank you for your response, your brackets made it clearer for me!

Antworten

Zurück zu „Konzepte der Programmiersprachen“