Церковная цифра для сложения

Question

Я застрял на следующем шаге. Будет здорово, если кто-нибудь сможет мне помочь:

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)

С скобками все в порядке? Я действительно путаю себя с заменами и круглыми скобками. Есть ли формальная, более простая техника для решения таких проблем?

Answer 1

Попробуйте Яйца аллигатора!

Вот мои шаги, которые я получил с помощью яйца аллигатора:

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))  )))))

Answer 2

Мой совет, из моего собственного ограниченного, но недавнего опыта:

1. Делайте одну вещь за раз: выполняйте альфа-преобразование, уменьшение бета-версии или eta-преобразование. Обратите внимание, на полях страницы вы работаете над тем, что вы сделали, чтобы перейти к следующей строке. Если эти слова вам не знакомы, то что они будут делать - просто посмотрите на Википедия .

Краткое описание этих шагов сокращения:

Альфа просто означает последовательное изменение имен переменных в контексте:

λfx. f (f x) => λgx. g (g x)

Бета просто означает применение лямбды к одному аргументу

(λf x. f x) b => λx. b x

Eta просто «разворачивает» ненужную упакованную функцию, которая не меняет своего значения.

λx.f x => f

Тогда

2. Используйте лоты альфа-преобразования, чтобы изменить имена переменных, чтобы сделать вещи более понятными. Все эти f, это всегда будет сбивать с толку. Вы сделали нечто подобное с " во втором ряду

3. Представь, что ты компьютер! Не прыгайте вперед и не пропускайте шаг при оценке выражения. Просто сделайте следующее (и только одно). Двигайтесь быстрее, только если вы уверены, что двигаетесь медленно.

4. Подумайте о присвоении имен некоторым выражениям и заменяйте их лямбда-выражениями только тогда, когда вам нужно их оценить. Я обычно отмечаю подстановку на полях страницы как by def, так как на самом деле это не шаг сокращения. Что-то вроде:

   add two three 
   (λm n f x. m f (n f x)) two three | by def
   

Итак, следуя приведенным выше правилам, вот мой рабочий пример:

two   = λfx. f (f x)
three = λfx. f (f (f x))
add   = λmnfx. m f (n f x)

0  | add two three 
1  | (λm n f x. m f (n f x)) two three           | by def
2  | (λn f x. two f (n f x)) three               | beta
3  | (λf x. two f (three f x))                   | beta
4  | (λf x. two f ((λfx. f (f (f x))) f x))      | by def
5  | (λf x. two f ((λgy. g (g (g y))) f x))      | alpha
6  | (λf x. two f ((λy. f (f (f y))) x))         | beta
7  | (λf x. two f (f (f (f x))))                 | beta
8  | (λf x. (λfx. f (f x)) f (f (f (f x))))      | by def
9  | (λf x. (λgy. g (g y)) f (f (f (f x))))      | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x))))         | beta
11 | (λf x. (λy. f (f (f (f (f x))))))           | beta

Answer 3

Существует ли формальная, более простая техника для решения таких проблем?

На намного проще написать редуктор и симпатичный принтер для лямбда-терминов, чем делать сокращения вручную. Но PLT Redex может помочь вам сократить расходы; попробуйте определить правила для уменьшения нормального порядка, и все, что вам нужно сделать, это беспокоиться о красивой печати результатов без лишних скобок .

Возможно, вы тоже узнаете намного больше.