3622
правки
Изменения
м
→Нормальный порядок редукции
==Нормальный порядок редукции==
(λ a . y (y (y (λ b . a))) y) (x (x (x (λ c d . d) y)) x)
[http://softoption.us/content/node/46 Здесь] про стратегии редуцирования с примерами и определениями.
'''Нормальный порядок редуцирования''' {{---}} самым первым делом раскрывается самый левый самый внешний редекс.
Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y
Более показательные и содержательные примеры (во всех случаях одна редукция будет произведена):
* (λ a . a) ((λ x . x) y) <tex> \Rightarrow </tex> (λ x . x) y
* x (λ a . ((λ x . x) y) ((λ z . z) y)) <tex> \Rightarrow </tex> x (λ a . y ((λ z . z) y))
==Аппликативный порядок редукции==
