3622
правки
Изменения
Нет описания правки
'''Аппликативный порядок редуцирования''' {{---}} первым делом редуцирования самый правый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.
Те же примеры (во всех случаях одна редукция будет произведена):
* (λ a . a) ((λ x . x) y) <tex> \Rightarrow </tex> (λ a . a) y
* x (λ a . ((λ x . x) y) ((λ z . z) y)) <tex> \Rightarrow </tex> x (λ a . ((λ x . x) y) y)
Ещё один для разнообразия:
((λ 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)
==Выписать систему уравнений типизации==
