Арифметика с церковными числами

Я работаю через SICP, а проблема 2.6 поставила меня в нечто затруднительное. В обращении с числами Церкви понятие кодирования нуля и 1 как произвольных функций, которые удовлетворяют определенным аксиомам, кажется, имеет смысл. Кроме того, получение прямой формулировки отдельных чисел с использованием определения нуля, и функция add-1 имеет смысл. Я не понимаю, как может быть создан оператор плюс.

До сих пор я это имел.

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

Просматривая запись wikipedia для lambda calculus, я обнаружил, что определение плюса было PLUS: = λmnfx.m f (n f x). Используя это определение, я смог сформулировать следующую процедуру.

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

То, что я не понимаю, заключается в том, как эта процедура может быть получена напрямую, используя только информацию, предоставленную ранее полученными процедурами. Может ли кто-нибудь ответить на это в какой-то строгой доказательной форме? Интуитивно я думаю, что я понимаю, что происходит, но как однажды сказал Ричард Фейнман: "Если я не смогу его построить, я не могу этого понять..."

Ответ 1

Это на самом деле довольно просто. Это, вероятно, будет рассматриваться как пламя, но параны затрудняют его восприятие - лучший способ увидеть, что происходит, - либо представить, что вы на валютном языке, либо просто используете тот факт, что Scheme имеет функции с несколькими аргументами и обнимайте это... Вот объяснение, которое использует lambdas и несколько аргументов, где удобно:

Каждое число N кодируется как

(lambda (f x) ...apply (f (f (f ... (f x)))) N times...)

Это означает, что кодирование N фактически
```
(lambda (f x) (f^N x))
```
где f^N - функциональное возведение в степень.
Более простой способ сказать это (при условии каррирования): число N кодируется как
```
(lambda (f) f^N)
```
так что N фактически является функцией "поднять до степени N"
Теперь сделайте свое выражение (смотрите здесь lambda):
```
((m f) ((n f) x))
```
поскольку n - это кодирование числа, это возведение в степень, так что это фактически:
```
((m f) (f^n x))
```
и то же самое для m:
```
(f^m (f^n x))
```
а остальное должно быть очевидно... У вас есть m приложения f, примененные к n приложениям f, примененным к x.
Наконец, оставим немного удовольствия - здесь еще один способ определить plus:
```
(define plus (lambda (m) (lambda (n) ((m add1) n))))
```
(Ну, не слишком весело, так как это, вероятно, более очевидно.)

Ответ 2

Ответ Eli технически корректен, но поскольку в тот момент, когда этот вопрос задан, процедура #apply не была введена, я не думаю, что авторы намеревались, чтобы ученик знал об этом или о таких понятиях, как currying чтобы иметь возможность ответить на этот вопрос.

Они в значительной степени направляют один на ответ, предлагая применить метод подстановки, а затем оттуда следует заметить, что эффект добавления - это состав одного числа на другой. Композиция представляет собой концепцию, введенную в упражнение 1.42; и что все, что требуется, чтобы понять, как аддитивная процедура может работать в этой системе.

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`.
;
; one   : (λ (f) (λ (x) (f x)))
; two   : (λ (f) (λ (x) (f (f x))))
; three : (λ (f) (λ (x) (f (f (f x)))))
;
; Thus one may surmise from this that an additive procedure in this system would
; work by composing one number onto the other.
;
; From exercise 1.42 you should already have a procedure called #compose.
;
; With a little trial and error (or just plain be able to see it) you get the
; following solution.

(define (adder n m)
  (λ (f)
    (let ((nf (n f))
          (mf (m f)))
      (compose nf mf))))

Ответ 3

^{(убедитесь, что вы понимаете функции более высокого порядка).} В Церковь Алонсо нетипизированное лямбда-исчисление функция является единственным примитивным типом данных. Нет чисел, булевых элементов, списков или чего-либо еще, только функции. Функции могут иметь только один аргумент, но функции могут принимать и/или возвращать функции - не значения этих функций, а сами функции. Поэтому для представления чисел, булевых элементов, списков и других типов данных вы должны придумать умный способ анонимных функций для их поддержки. Цифры церкви - это способ представить натуральные числа. Три наиболее примитивные конструкции в нетипизированном лямбда-исчислении:

λx.x, функция идентификации, принимает некоторую функцию и сразу же возвращает ее.
λx.x x, самоприменение.
λf.λx.f x, приложение функции, принимает функцию и аргумент и применяет функцию к аргументу.

Как вы кодируете 0, 1, 2 как ничего, кроме функций? Нам как-то нужно построить понятие количества в системе. У нас есть только функции, каждая функция может применяться только к одному аргументу. Где мы можем увидеть что-то похожее на количество? Эй, мы можем применить функцию к параметру несколько раз! Очевидно, что существует смысл количества в трех повторных вызовах функции: f (f (f x)). Поэтому позвольте закодировать его в исчислении лямбда:

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

И так далее. Но как вы идете от 0 до 1, или от 1 до 2? Как бы вы могли написать функцию, которая, учитывая число, вернет число, увеличивающееся на 1? Мы видим шаблон в элементарных цифрах, что термин всегда начинается с λf.λx. и после того, как у вас есть конечное повторное применение f, поэтому нам нужно как-то попасть в тело λf.λx. и обернуть его в другой f. Как вы меняете тело абстракции без сокращения? Ну, вы можете применить функцию, обернуть тело в функцию, а затем обернуть новое тело в старую абстракцию лямбда. Но вы не хотите изменять аргументы, поэтому вы применяете абстракции к значениям одного и того же имени: ((λf.λx.f x) f) x → f x, но ((λf.λx.f x) a) b) → a b, что нам не нужно.

Вот почему add1 есть λn.λf.λx.f ((n f) x): вы применяете n к f, а затем x, чтобы уменьшить выражение в теле, затем примените f к этому телу, а затем снова отрисуйте его с помощью λf.λx.. Упражнение: тоже убедитесь, что это правда, быстро изучите β-reduction и уменьшите (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)), чтобы увеличить 2 на 1.

Теперь, понимая интуицию за обертыванием тела в другой вызов функции, как мы реализуем добавление 2 чисел? Нам нужна функция, которая при условии λf.λx.f (f x) (2) и λf.λx.f (f (f x)) (3) вернет λf.λx.f (f (f (f (f x)))) (5). Посмотрите 2. Что делать, если вы можете заменить его x на тело 3, то есть f (f (f x))? Чтобы получить тело из 3, это очевидно, просто примените его к f, а затем x. Теперь примените 2 к f, но затем примените его к телу 3, а не к x. Затем снова заверните его в λf.λx.: λa.λb.λf.λx.a f (b f x).

Заключение: Чтобы добавить 2 числа a и b вместе, оба из которых представлены в виде числовых символов, вы хотите заменить x на a телом b, так что f (f x) + f (f (f x))= f (f (f (f (f x)))). Чтобы это произошло, примените a к f, а затем к b f x.