Сокращение Лямбда-исчисления
Все,
Ниже лямбда-выражение, которое я нахожу трудным уменьшить, т.е. Я не могу понять, как пойти об этой проблеме.
(λm λn λa λb. m (n b) b) (λ f x. x) (λ f x. f x)
Это - то, что я попробовал, но я застреваю:
Рассмотрение вышеупомянутого выражения как: (λm. E) M приравнивается к
E = (λn λa λb. m (n b) b)
M = (λf x. x) (λ f x. f x)
=> (λn λa λb. (λ f x. x) (λ f x. f x) (n b) b)
Рассмотрение вышеупомянутого выражения как (λn. E) M приравнивается к
E = (λa λb. (λ f x. x) (λ f x. f x) (n b) b)
M =??
.. и я потерян!!
Кто-либо может помочь мне понять, что, для КАКОГО-ЛИБО выражения лямбда-исчисления, каковы должны быть шаги для выполнения сокращения?
2 ответа
Для сокращения лямбда-выражений можно выполнить следующие шаги:
- Полностью заключите выражение в круглые скобки, чтобы избежать ошибок и сделать более очевидным, где происходит применение функции.
- Найдите применение функции, т.е. найдите вхождение паттерна
(λ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))
Теперь все.
В чем вы ошибаетесь, так это в том, что на первом этапе у вас не может быть
M = (λf x. x)(λ f x. f x)
, потому что исходное выражение не включает это выражение приложения. Чтобы прояснить это, вы можете заключить неявные круглые скобки, следуя правилу, что приложение является левоассоциативным (используя [и] для новых скобок и вставляя некоторые пропущенные символы "."):
[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x)
Отсюда найдите выражение вида (λv.E) M где-то внутри и уменьшите его, заменив v на M в E . Будьте осторожны, это действительно приложение функции к M: это не так, если у вас есть что-то вроде
N (λv.E) M , с тех пор N применяется к функции и M как два аргумента.
Если вы все еще застряли, попробуйте поставить скобки и для каждой лямбды - в основном новый "(" после каждого "." И соответствующий ")", который идет как можно правее, но все еще соответствует новый "(". В качестве примера я сделал здесь один (используя [и], чтобы выделить их):
( (λm . λn . λa . [λb . m (n a b) b]) (λ f x. x) ) (λ f x. f x)