Какова нормальная форма этого лямбда-исчисления и есть ли свободные переменные? - PullRequest
0 голосов
/ 17 марта 2020

Я пытаюсь выучить лямбда-исчисление, но мне трудно это делать. Так что, если кто-нибудь немного объяснит, я был бы очень признателен!

(λj.λx.f(j x)) (λy.f y)

1 Ответ

1 голос
/ 17 марта 2020

Есть одна свободная переменная, f. j, x и y связаны абстракцией.

Существует два способа достижения нормальной формы. Либо выполните два бета-сокращения

(λj.λx.f(j x)) (λy.f y) == (λx.f(<b>(λy.f y)</b> x))  <i>apply (λj.λx.f(j x)) to (λy.f y) </i>
                        == (λx.f(<b>f x</b>))        <i> apply (λy.f y) to x</i>

, либо выполните eta-сокращение с последующим бета-уменьшением.

(λj.λx.f(j x)) (λy.f y) == (λj.λx.f(j x)) <b>f</b>  <i> replace (λy.f y) with f</i> 
                        == (λx.f(<b>f</b> x))       <i> apply (λj.λx.f(j x)) to f</i> 
...