3622
правки
Изменения
→Кр1
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) <tex> \Rightarrow </tex>
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)
== Ленивый порядок ==
Ленивый порядок редуцирования {{---}} это когда мы якобы заворачиваем терм в коробку, и если делаем редукцию в одном из термов коробки, то она делается во всех. При этом сам порядок редуцирования нормальный.
То есть пример:
(\ f . f f) ((\ x . x) z)
Сначала делаем обычную редукцию нормальным порядком и получаем:
((\ x . x) z) ((\ x . x) z)
А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции:
z z
==Выписать систему уравнений типизации==
