Как работи ламбда смятането с израз като: (Ly.Lt.yt)zx?

Не разбирам как да реша този израз на ламбда смятане:

(Lx.yx)((Ly.Lt.yt)zx)

Не разбирам как zx се предава и оценява. Предава ли се на Ly или Lt? Можеш ли да ми помогнеш?

РЕДАКТИРАНЕ: Ето как се опитах да го реша:

(Lx.yx)((Ly.Lt.yt)zx) Първо разглеждам zx като 2 параметъра и прилагам Ly към z:

->(Lx.yx)((Lt.zt)x) След това прилагам Lt към x и получавам:

->(Lx.yx)(zx) Сега прилагам Lx към (zx):

->(y(zx))

Трябва да е правилно, но не разбирам добре какви са ролите в тази ситуация: ((Ly.Lt.yt)zx). Какво да кандидатствате, кога да кандидатствате и как да кандидатствате. Бихте ли ми помогнали?


lambda-calculus
person bog    schedule 15.06.2014    source източник
comment
Проверих вашето решение. Така е правилно.   -  person Dan D.    schedule 15.06.2014
comment
Благодаря ти. Бих искал да ви попитам какво означава (Ly.Lt.yt)? като Lt(Ly(x)) ли е ??   -  person bog    schedule 15.06.2014
comment
Разширява се до (Ly.(Lt.yt)).   -  person Dan D.    schedule 15.06.2014

Отговори (2)


arrow_upward
0
arrow_downward

Винаги намалявате бета възможно най-лявата бета редукция, което правите правилно. Когато прилагате, заменете целия ламбда член с тялото на функцията, с изключение на това, че всички срещания на променливата на функцията трябва да бъдат заменени от аргумента.

Пример:

(Lx.Ly.x)(La.Lb.ab)(La.Lb.ba)
[^left most redex^]
(Ly.(La.Lb.ab))(La.Lb.ba)
[^^^^left most redex^^^^]
(Ly.(La.Lb.ab))

(no more beta redexes, done evaluating)
person R Z    schedule 10.12.2020

arrow_upward
0
arrow_downward

Правилата са:

  • Lx.Ly.M означава (Lx.(Ly.M)).
  • MNP означава ((MN)P).

Така че ((Ly.Lt.yt)zx) е (((Ly.(Lt.yt))z)x). Така първият наличен редекс тук е (Ly.(Lt.yt))z и всичките ви стъпки са правилни. Много добре!

person lemontree    schedule 10.12.2020