Церковная цифра для дополнения
Я застреваю в следующем шаге. Будет замечательно, если кто-то может выручить меня:
2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)
Мои шаги:
(λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)
Действительно ли круглая скобка прекрасна? Я действительно смущаю меня на заменах и круглой скобке. Существует ли формальная, более легкая техника для рассмотрения таких проблем?
2 ответа
Попробуйте Яйца аллигатора!
Вот мои шаги, которые я получил с помощью Alligator Eggs:
ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> (λn f x. (λf x.f(f(f x))) f (n f x)) (λf x.f(f x))
-> (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x))
-> (λf x. (λx.f(f(f x))) ((λf x.f(f x)) f x))
-> (λf x. f(f(f(λf x.f(f x)) f x)))))
-> (λf x. f(f(f (λx.f(f x)) x)))))
-> (λf x. f(f(f (f(f x)) )))))
Есть ли формальный, более простой способ решения таких проблем?
Намного проще написать редуктор и симпатичный принтер для лямбда-терминов, чем выполнять редукцию вручную. Но PLT Redex может дать вам преимущество при сокращении; попробуйте определить правила редукции в нормальном порядке, и тогда все, что вам нужно сделать, это позаботиться о красивом выводе результатов без лишних скобок .
Вы, вероятно, тоже узнаете намного больше.