Уменьшение лямбда-исчисления

Question

Все,

Ниже приводится лямбда-выражение, которое мне трудно сократить, т. Е. Я не могу понять, как решить эту проблему.

(λm λn λa λb. M(nab) b) (λ f x. x) (λ f x. fx)

Это то, что я пытался, но я застрял:

Рассматривая приведенное выше выражение как: (λm.E) M равно
E = (λn λa λb. M (nab) b)
M = (λf x. X) (λf x. Fx)

=> (λnλa λb. (λ f x. x) (λ f x. fx) (nab) b)

С учетом приведенного выше выражения, когда (λn. E) M равно
E = (λa λb.(λ f x. x) (λ f x. fx) (nab) b)
M = ??

.. и я заблудился !!

Может кто-нибудь помочь мне понять, что для ЛЮБОГО выражения лямбда-исчисления, какие должны быть шаги для выполнения сокращения?

Answer 1

Вы можете выполнить следующие шаги, чтобы уменьшить лямбда-выражения:

1. Полностью заключите в скобки выражение, чтобы избежать ошибок и сделать более очевидным, где происходит применение функции.
2. Найти приложение-функцию, то есть найти вхождение шаблона (λX. e1) e2, где X может быть любым допустимым идентификатором, а e1 и e2 могут быть любыми допустимыми выражениями.
3. Примените функцию, заменив (λx. e1) e2 на e1', где e1' - результат замены каждого свободного вхождения x в e1 на e2.
4. Повторяйте 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))

Теперь мы закончили.

Answer 2

Если вы ошибаетесь, на первом шаге вы не можете получить

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)