SICP. Хроники мозга. Вырезка #0

[skiminok]

"Если представление пар как процедур было для Вас еще недостаточно сумасшедшим, то заметьте, что в языке, который способен манипулировать процедурами, мы можем обойтись и без чисел (по крайней мере, пока речь идет о неотрицательных числах), определив 0 и операцию прибавления 1 так:

(define zero (lambda (f) (lambda (x) x)))

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

Такое представление известно как числа Чёрча, по имени его изобретателя, Алонсо Чёрча, того самого логика, который придумал лямбда-исчисление."

Comments

[sofigenr.livejournal.com]

а если несложно, немного детальней с пояснениями?)

[skiminog.livejournal.com]

Грубо:
если у тебя есть формальная теория, в которой определено понятие вычислимой функции (бестиповой и безымянной), то с её помощью можно определить натуральный ряд следующим образом:

0 ≡ функция от 1 параметра f, которая возвращает функцию от 1 параметра x, которая возвращает его же (x) ≡ функция от 1 параметра-функции (f), которая возвращает тождественную функцию

операция "+1", примененная n раз (но n есть число в рамках нашей формальной теории, то есть тоже функция), есть:
функция от 1 параметра f, которая возвращает функцию от 1 параметра x (пока всё то же самое), которая возвращает результат применения функции f к результату применения функции n(f) к x
≡
функция от 1 параметра f, которая возвращает функцию от 1 параметра x, которая возвращает f( (n(f))(x) ).

В более простых терминах:
0 ≡ f ↦ (x ↦ x)
1 ≡ f ↦ ( x ↦ f( (0(f))(x) ) ) ≡ f ↦ ( x ↦ f( (x↦x)(x) ) ≡ f ↦ (x ↦ f(x))
2 ≡ f ↦ ( x ↦ f( (1(f))(x) ) ) ≡ ... ≡ f ↦ (x ↦ f(f(x)))
...

/* Если тебя смущают эти цепочки функций, возвращающих функции, прочитай про каррирование и убери его, получишь функции нескольких аргументов, в меньшем количестве. Если оно тут получится, конечно, я не пробовал. */

SICP дальше задаёт вопрос, как в такой формальной теории определить операцию "+" не через последовательное применение add-1? Попробуй =)

[skiminog.livejournal.com]

Уточнение на всякий случай:
> функция от 1 параметра-функции (f), которая возвращает тождественную функцию
"которая" = конечно же, 0, а не f