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

Question

Я работаю через SICP, а problem 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))))) 

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

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

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

Answer 1

Это на самом деле довольно просто. Это, вероятно, будет рассматриваться как пламя, но параны затрудняют его восприятие - лучший способ увидеть, что происходит, - либо представить, что вы на валютном языке, либо просто используете тот факт, что 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)))) 
  

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

Answer 2

Ответ Эли технически корректен, но поскольку в момент, когда задан этот вопрос, не была введена процедура #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)))) 

Answer 3

^{(Убедитесь, что вы понимаете higher-order functions).} В Alonzo Churchuntyped lambda calculus функция является единственным примитивным типом данных. Нет чисел, булевых элементов, списков или чего-либо еще, только функции. Функции могут иметь только один аргумент, но функции могут принимать и/или возвращать функции - не значения этих функций, а сами функции. Поэтому для представления чисел, булевых элементов, списков и других типов данных вы должны придумать умный способ анонимных функций для их поддержки. Church numerals - способ представлять natural numbers. Три наиболее примитивные конструкции в нетипизированного лямбда-исчисления являются:

1. λx.x, identity function, принимает некоторую функцию и немедленно возвращает его.
2. λx.x x, само приложение.
3. λ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 вместе, оба из которых представлены в виде Чёрча, вы хотите заменить в ax с телом b, так что f (f x) + f (f (f x)) = f (f (f (f (f x)))). Чтобы это произошло, примените a к f, затем к b f x.