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

Question

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

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

(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 is - это кодировка числа, это возведение в степень, так что это на самом деле:

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

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

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

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

Answer 3

Ответ Илии технически верен, но поскольку этот вопрос задается #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))))