Ответ 1
Для уменьшения лямбда-выражений вы можете выполнить следующие шаги:
- Полностью заключить в скобки выражение, чтобы избежать ошибок и сделать его более очевидным, когда происходит приложение функции.
- Найти приложение-функцию, то есть найти вхождение шаблона
(λX. e1) e2
, гдеX
может быть любым допустимым идентификатором, аe1
иe2
могут быть любыми допустимыми выражениями. - Примените эту функцию, заменив
(λX. e1) e2
наe1'
, гдеe1'
является результатом замены каждого свободного вхожденияX
вe1
наe2
. - Повторяйте 2 и 3 до тех пор, пока шаблон больше не появится. Обратите внимание, что это может привести к бесконечному циклу для ненормирующих выражений, поэтому вы должны остановиться после 1000 итераций или около того; -)
Итак, для вашего примера мы начинаем с выражения
((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x)))
Здесь подвыражение (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))
соответствует нашей схеме с X = m
, e1 = (λn. (λa. (λb. (m ((n a) b)) b))))
и e2 = (λf. (λx. x))
. Итак, после подстановки получим (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)))
, что делает все наше выражение:
(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x)))
Теперь мы можем применить шаблон ко всему выражению с помощью X = n
, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))
и e2 = (λf. (λx. (f x)))
. Поэтому после подстановки получаем:
(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b))
Теперь ((λf. (λx. (f x))) a)
соответствует нашей схеме и становится (λx. (a x))
, что приводит к:
(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b))
На этот раз мы можем применить шаблон к ((λx. (a x)) b)
, который сводится к (a b)
, что приводит к:
(λa. (λb. ((λf. (λx. x)) (a b)) b))
Теперь примените шаблон к ((λf. (λx. x)) (a b))
, который сводится к (λx. x)
и получит:
(λa. (λb. b))
Теперь все готово.