Числа Чёрча¶

Числа Чёрча — это способ представления неотрицательных целых чисел в лямбда-исчислении, основанный на идее функциональной итерации. В этой системе каждое натуральное число \( n \) кодируется как функция высшего порядка, которая принимает два аргумента: функцию \( f \) и значение \( x \), и применяет \( f \) к \( x \) ровно \( n \) раз. Числа Чёрча названы в честь американского математика и логика Алонзо Чёрча, который ввёл их в 1930-х годах при разработке лямбда-исчисления — формальной системы для описания вычислимых функций.

¶Определение

В лямбда-исчислении числа Чёрча определяются следующим образом:

• Ноль (\( \overline{0} \)): \( \lambda f. \lambda x. x \) — функция, которая не применяет \( f \) к \( x \), а возвращает \( x \) без изменений.
• Единица (\( \overline{1} \)): \( \lambda f. \lambda x. f x \) — применяет \( f \) к \( x \) один раз.
• Два (\( \overline{2} \)): \( \lambda f. \lambda x. f (f x) \) — применяет \( f \) к \( x \) дважды.
• В общем виде, число \( n \) представляется как: \( \lambda f. \lambda x. f^n x \), где \( f^n x \) означает \( n \)-кратное применение \( f \) к \( x \).

Таким образом, каждое число Чёрча — это функция двух аргументов, которая возвращает результат многократного применения первого аргумента ко второму. Эта конструкция отражает интуитивное понимание натурального числа как количества повторений некоторого действия.

¶История

Концепция чисел Чёрча возникла в рамках лямбда-исчисления, которое было предложено Алонзо Чёрчем в 1932 году как часть его работы по основаниям математики. Чёрч стремился создать формальную систему, способную выразить все вычислимые функции, и в 1936 году он доказал, что лямбда-исчисление является полным по Тьюрингу, то есть может моделировать любые алгоритмические процессы. Числа Чёрча стали одним из ключевых примеров кодирования данных в этой системе, демонстрируя, как числа могут быть представлены исключительно через функции, без использования встроенных числовых типов.

В 1940-х годах лямбда-исчисление и числа Чёрча были положены в основу функционального программирования, особенно после того, как Стивен Коул Клини, ученик Чёрча, разработал теорию рекурсивных функций. Впоследствии числа Чёрча нашли применение в языках программирования, основанных на лямбда-исчислении, таких как Scheme, Haskell и ML, а также в теоретической информатике для изучения типов и вычислений.

¶Арифметические операции

Над числами Чёрча можно определить стандартные арифметические операции, используя только лямбда-выражения. Эти операции являются функциями высшего порядка, которые манипулируют числами как функциями.

¶Сложение

Сложение двух чисел Чёрча \( m \) и \( n \) определяется как функция, которая применяет \( f \) к \( x \) сначала \( m \) раз, затем \( n \) раз. Формально: \[ \text{ADD} = \lambda m. \lambda n. \lambda f. \lambda x. m f (n f x) \] Здесь \( m f (n f x) \) означает: сначала применить \( f \) к \( x \) \( n \) раз (с помощью \( n f x \)), а затем к результату применить \( f \) ещё \( m \) раз (с помощью \( m f \)). Таким образом, общее количество применений \( f \) равно \( m + n \).

¶Умножение

Умножение чисел \( m \) и \( n \) определяется как композиция функций: число \( m \) применяется к функции \( n f \), то есть \( m \) раз повторяется \( n \)-кратное применение \( f \). Формально: \[ \text{MUL} = \lambda m. \lambda n. \lambda f. m (n f) \] Здесь \( m (n f) \) означает, что функция \( n f \) (которая применяет \( f \) \( n \) раз) применяется \( m \) раз, что в итоге даёт \( m \times n \) применений \( f \) к аргументу.

¶Возведение в степень

Возведение в степень \( m^n \) определяется как применение \( n \) к \( m \): \[ \text{POW} = \lambda m. \lambda n. n m \] Это выражение работает, потому что число \( n \) как функция принимает аргумент \( m \) и применяет его \( n \) раз к некоторому значению. В результате получается число, соответствующее \( m^n \).

¶Вычитание и предшественник

Вычитание и нахождение предшественника (числа на единицу меньше) сложнее реализовать в лямбда-исчислении, так как они требуют обращения к предыдущему состоянию. Один из стандартных способов — использование пары (упорядоченной пары) для хранения предыдущего значения. Функция предшественника \( \text{PRED} \) может быть определена, например, как: \[ \text{PRED} = \lambda n. \lambda f. \lambda x. n (\lambda g. \lambda h. h (g f)) (\lambda u. x) (\lambda u. u) \] Это выражение использует технику, при которой число \( n \) применяется к функции, которая строит последовательность, и затем извлекается предыдущий элемент. Однако на практике вычитание часто реализуется через пары Чёрча или другие комбинаторы.

¶Связь с другими кодировками

Числа Чёрча — не единственный способ представления натуральных чисел в лямбда-исчислении. Существуют альтернативные кодировки, такие как:

• Числа Скотта — представление, основанное на рекурсивных определениях, где каждое число является функцией, принимающей два аргумента: один для нуля, другой для преемника. Числа Скотта более естественно работают с рекурсией и сопоставлением с образцом.
• Числа Гёделя — кодирование чисел через простые числа, используемое в теории рекурсивных функций, но не в лямбда-исчислении напрямую.
• Числа Чёрча являются наиболее простыми и интуитивными, но их недостаток — сложность реализации вычитания и преемника, что делает их менее удобными для практического программирования.

¶Применение в информатике

Числа Чёрча имеют теоретическое и практическое значение в информатике:

• Теория типов: числа Чёрча используются для демонстрации того, как типы данных могут быть закодированы через функции, что лежит в основе полиморфизма и систем типов, таких как система F.
• Функциональное программирование: в языках, поддерживающих функции высшего порядка, таких как Haskell, можно реализовать числа Чёрча как демонстрацию выразительности лямбда-исчисления. Например, в Haskell число Чёрча можно определить как тип data Church = Church (forall a. (a -> a) -> a -> a).
• Теория вычислимости: числа Чёрча являются частью доказательства эквивалентности лямбда-исчисления и машин Тьюринга, что подтверждает тезис Чёрча-Тьюринга о том, что любая вычислимая функция может быть выражена в этих системах.
• Образование: числа Чёрча часто используются в учебных курсах по теории вычислений и функциональному программированию для иллюстрации концепций функций высшего порядка и кодирования данных.

¶Интересные факты

• Числа Чёрча можно использовать для представления не только натуральных чисел, но и других математических объектов, таких как булевы значения (истина и ложь) и списки, через аналогичные функциональные кодировки.
• В лямбда-исчислении все числа Чёрча являются функциями, поэтому их можно применять друг к другу, что приводит к неожиданным результатам, например, \( \overline{2} \, \overline{3} \) даёт число, соответствующее \( 3^2 = 9 \), а не \( 2^3 \).
• Алонзо Чёрч ввёл эти числа в контексте доказательства неразрешимости проблемы остановки, показав, что в лямбда-исчислении нельзя создать функцию, которая бы определяла, эквивалентны ли два выражения.

¶Источники

• Чёрч, Алонзо. «A set of postulates for the foundation of logic». Annals of Mathematics, 1932.
• Чёрч, Алонзо. «An unsolvable problem of elementary number theory». American Journal of Mathematics, 1936.
• Барендрегт, Хенк. «The Lambda Calculus: Its Syntax and Semantics». North-Holland, 1984.
• Пирс, Бенджамин. «Types and Programming Languages». MIT Press, 2002.