Арифметика с цифрами Чёрча

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

• Каждое число 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))))
  

  (Ну, не слишком весело, так как этот, вероятно, более очевиден.)

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

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

Как вы кодируете 0, 1, 2 как не что иное, как функции? Нам каким-то образом нужно встроить в систему понятие количества. У нас есть только функции, каждая функция может быть применена только к 1 аргументу. Где мы можем увидеть что-либо похожее на количество? Эй, мы можем применить функцию к параметру несколько раз! Очевидно, что в трех повторных вызовах функции есть смысл: 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.. Упражнение: чтобы убедиться, что это правда, быстро научитесь β-редукции и уменьшите (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)), чтобы увеличить 2 на 1.

Теперь, поняв интуицию, лежащую в основе переноса тела в другой вызов функции, как нам реализовать сложение двух чисел? Нам нужна функция, которая, учитывая λ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.

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

Они в значительной степени подводят к ответу, предлагая применить метод подстановки, а затем следует заметить, что эффект сложения представляет собой наложение одного числа на другое. Понятие «композиция» было введено в упражнении 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))))