Помогите осилить Church encoding

Такие вещи лучше понимаются на статически-типизированных языках. forall a. (a -> a) -> (a -> a).

Собственно говоря, если n — число, закодированное по Чёрчу, то n f x = f (f (f (f... (f x)...))), где f повторяется n раз. Отсюда: ноль кодируется тождественной функцией, 0 f x = x, а чтобы к n прибавить единичку, нужно добавить одно f.

Почему 0 - тождественная ф-я? Помоги развернуть inc - (+ n 1) в таком сочетании: ((zero inc) 0). В смысле переписывать по шагам, а потом редукция. У меня останетсаги скоро не останется марать.

* бумаги не останется

Непонятно, что есть zero

Кажется, вы не до конца понимаете, что такое математика. Вот вам не пофиг? Сказано, что это — ноль, так оно и есть.

Вот пример: есть на лоре некоторый эталонный тролль. Сопоставим ему число 0. Кроме того, известно, что для каждого тролля на лоре существует другой тролль, в два раза толще того, первого. Вот вам операция «+1».

Здесь все вообще элементарно. Число Черча — это функция, принимающая функцию f и возвращающая функцию y(x) = (f^:N)(x), где за (f^:N) обозначено N последовательных применений f. Соответственно

0 = \f -> [\x->x]
+1 = \n -> [\f -> [\x f((n f) x)]]

Вычислим, например, 0+1

0+1 = \f -> [\x -> f((0 f) x)] = \f -> [\x f ((\x->x) x)] = \f -> [\x->f(x)]

Вычислим 1+1

1+1 = \f -> [\x -> f((1 f) x)] = \f -> [\x f ((\x->f(x) x)] = \f -> [\x->f(f(x))]

((zero inc) 0)

Зачем вы пытаетесь применить 0 к операции «+1» а потом еще и применить это к десятичному числу?

Почему 0 - тождественная ф-я?

Можете хоть так определить натуральные числа:

0 = \f -> [\x->sin x]
+1 = \n -> [\f -> [\x sin ((n f) x)]]

Почему 0 - тождественная ф-я?

Я неверно выразился. Не ноль — тождественная функция, а 0 f — тождественная функция, для любой f. Ну, напиши f (f (... f(x)...)), только f ни одного раза. Будет x.

((zero inc) 0)

В обозначениях со скобочками, получается ((zero inc) 0) = (((lambda (f) (lambda (x) x)) inc) 0) = ((lambda (x) x) 0) = 0.

Я понял, что это ноль. Я не понял, как это работает в любых, примитивнейших комбинациях с другими сущностями. Теперь яснее, но запись такую мне еще надо осилить для беглого понимания. а ((zero inc) 0) работает. Попробуй сам. И вместо нуля другие числа. Miguel ниже написал, я наконец-то понял.

Спасибо вам всем:)

((zero inc) 0) работает

Я знаю, что работает, но это не имеет никакого смысла :)

Ну демонстрация вроде как. Ноль-функция принимает аргументом функцию, выполняет ее 0 раз и в итоге инкрементация не происходит. Я так понял?

Тьфу ты, вы имели в виду самый обычный inc? Тогда все так.

Ага, обычный. Я надеюсь, в сикпе немного таких задач будет - я хочу сберечь свою церебральную девственность для чего-то другого.