Церковные цифры:как закодировать ноль в лямбда-исчислении?

Question

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

как "функция, которая принимает функцию и второе значение и применяет функцию ноль раз к аргументу"ноль?Есть ли другой способ закодировать ноль?Может ли кто-нибудь здесь помочь мне закодировать 0?

Answer 1

«Функция, которая принимает функцию и второе значение и применяет функцию ноль раз к аргументу», конечно, не равна нулю.Это кодирование нуля.Когда вы имеете дело с простым лямбда-исчислением, вам приходится каким-то образом кодировать числа (а также другие примитивные типы), и для каждого из этих типов предъявляются некоторые требования.Например, одно из требований к натуральным числам — уметь прибавлять 1 к заданному числу, а другое — уметь отличать ноль от больших чисел (если вы хотите узнать больше, поищите «Арифметику Пеано»).Популярная кодировка, которую цитировал Дарио, дает вам эти две вещи, а также представляет целое число N функцией, которая что-то делает (закодировано как f аргумент) N раз — это своего рода естественный способ использования натуральных чисел.

Возможны и другие кодировки — например, если вы можете представлять списки, вы можете представить N как список из N элементов.У этих кодировок есть свои плюсы и минусы, но приведенная выше является, безусловно, самой популярной.

Answer 2

Видеть Википедия:

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

Если вы изучаете лямбда-исчисление, вы, вероятно, уже знаете, что λxy.y arg1 *arg2* сократится до arg2, поскольку x заменяется ничем, а остаток (λy.y) является тождественной функцией.

Вы можете написать ноль многими другими способами (т.е.придумать другое соглашение), но есть веские причины для использования λxy.y.Например, вы хотите, чтобы ноль был первым натуральным числом, чтобы если вы примените к нему функцию-преемник, вы получили 1, 2, 3 и т. д.С помощью функции λabc.b(abc) вы получаете λxy.x(y), λxy.x(x(y)), λxy.x(x(x(y))) и т.д., другими словами, вы получаете целая система счисления.

Более того, вы хотите, чтобы ноль был нейтральным элементом по отношению к сложению.С помощью нашей функции-преемника S := λabc.b(abc) мы можем определить н+*м* как н С м, то есть, н раз применение функции-преемника к м.Наш нуль λxy.y удовлетворяет этому, как 0 S м и м S 0 уменьшить до м.