Кодирование Чёрча ― способ представления любых данных при помощи лямбда-выражений, например, натуральных чисел и данных других типов. Метод назван в честь Алонзо Чёрча, разработавшего лямбда-исчисление.
Поскольку в чистом (бестиповом) лямбда-исчислении, в отличие от многих формальных систем (где выделены в качестве термов, например, целые числа, булевы значения, пары), единственным примитивным типом являются сами лямбда-выражения, все виды данных необходимо конструировать с использованием только лямбда-выражений. Кодирование подразумевает соглашение о том, как представлять те или иные типы данных; например, числа Чёрча — способ кодирования натуральных чисел, булеаны Чёрча — соглашение о кодировании логических значений, пары Чёрча — кодирование упорядоченных пар элементов. Есть несколько способов закодировать списки.
Кодирование Чёрча отображает любые данные как операции над ними, используя только лишь функции, представляя функции через лямбда термы-абстракции.
Кодирование Чёрча редко используется в практических языках программирования из-за его неэффективности, но при этом демонстрирует, что любые вычисления могут быть сведены исключительно к функциям, а другие примитивные типы данных не обязательны.
В этой статье иногда используется сокращённая λ-нотация для абстракций, , а также стандартные комбинаторы и .
Пары Чёрча
Пары Чёрча — соглашение о кодировании упорядоченных пар, то есть наборов (кортежей) из двух элементов. Пара величин и представляется функцией, которая ожидает как свой единственный аргумент некую функцию , и применяет её к обоим элементам пары, и :
Здесь выступает в роли функции-продолжения, или функции-обработчика двух величин из пары.
Функции и , возвращающие соответственно первый и второй элемент пары, а также функция (два варианта, для примера), меняющая местами два элемента пары, определяются как:
Булеаны Чёрча Булеаны Чёрча — представления булевых значений, то есть «истины» () и «лжи» () как выбора первого и второго аргумента соответственно:
Некоторые языки программирования, такие как Smalltalk и , используют их в качестве модели реализации для булевой арифметики.
Такое определение позволяет использовать предикаты (функции, возвращающие логические значения) как условия в условных выражениях. Над и могут быть реализованы стандартные логические операторы (конъюнкция, дизъюнкция, отрицание, исключающее «или»:
Реализация тернарной условной операции:
Предикаты — функции, возвращающие логическое значение — реализуются естественным образом, как функции возвращающие Булеаны как результат.
Числа Чёрча Число Чёрча, соответствующее натуральному числу , определяется как функция от двух параметров и , последовательно применяющая раз функцию начиная с — другими словами, число Чёрча отображает функцию в её -кратную само-композицию:
значит «не применять функцию к вообще», значит «применять функцию 1 раз», значит «применять функцию по цепочке 2 раза», и так далее:
Число Определение нумерала Лямбда-выражение ⋮ ⋮ ⋮
Вычисления над числами Чёрча Арифметические операции над числами можно выразить в лямбда-исчислении как функции над числами Чёрча.
Операция сложения, отображая тождество , то есть , определяется как:
Добавление единицы выводится из сложения посредством -редукции, полагая :
Действительно, выполнить что-то на один раз больше значит выполнить это ещё один раз. Таково последующее число после любого данного числа. В частности, и -эквивалентны.
И наоборот, беря эту операцию за основу вместе с нулём, как в аксиомах Пеано, можно вывести операцию сложения из неё, повторяя её данное число раз, получая эквивалентное определение
Для умножения замечаем, что -кратное повторение функции это -кратное повторение -кратно повторенной функции , :
Возведение в степень это умножение на , повторенное раз, ; а тетрация это повторное возведение в степень, :
Число-предшественник создаётся данным числом через подмену самого первого применения данной ему функции функцией тождества , используя для всех оставшихся применений:
Например, . Здесь используется парадигма передачи состояния с помощью добавочного аргумента. В ламбда исчислении отсутствует изменяемость данных, так что нельзя ничего изменить, но можно подменить.
Вычитание числа достигается повторным вычитанием единицы, раз:
Подобным образом могли бы быть определены также и
Здесь это -тая стрелка Кнута.Dan Doel (https://math.stackexchange.com/users/590896/dan-doel), Tetration of Church numerals?, URL (version: 2026-02-27): https://math.stackexchange.com/q/4601054
Аналогично функции , в парадигме передачи состояния с помощью добавочных аргументов определяются и другие функции, как например , вычисляющая целочисленное деление на 2, или факториал, , а также и более эффективная версия вычитания,
Примеры вычисления: ; ; .
Деление определяется аналогично вычитанию,
Применение обеспечивает вычитание на , создавая цикл действий, повторно испускающих после шагов.
Вместо можно также использовать .
Предикаты для чисел Чёрча Предикат , возвращающий , если его аргумент является числом Чёрча , и в ином случае, вводится таким образом:
Предикат над числами Чёрча, который проверяет, меньше или равен его первый аргумент второму:
Из тождества получается предикат проверки на равенство :
Предикат «меньше» это
Числа по Скотту Для сравнения, кодирование чисел по Скотту определено какHistory of Lambda-calculus and Combinatory Logic, 2006, by Felice Cardone and J. Roger Hindley, p. 18, note 38
Кодировка Скотта для каждого алгебраического типа данных напрямую соответствует его определению. Натуральные числа по Пеано — это суммарный тип данных с двумя вариантами, 0 и не-0:
Соответственно, числo по Скотту — это функция, ожидающaя две функции-обработчика, по числу вариантов.
Число по Скотту являет собой уже совершённое сопоставление с образцом, и вызывает соответствующую функцию-обработчик в соответствии с тем, является ли оно нулём или нет. В случае нуля дополнительных данных нет, так что это не функция а просто некая величина , . В случае же не-нулевого числа, дополнительным данным явлается его предшествующее число, например .
В то время как в кодировке Чёрча , в кодировке Скотта , , и . Соответственно и функции перевода в другой тип тоже разнятся,
Как видим, определение перевода чисел Скотта рекурсивно, и требует использования оператора неподвижной точки, или соответственного переопределения с использованием само-применения, «вручную»:
Сложение определяется через повторение операции , с использованием явной рекурсии:
Так же с использованием явной рекурсии приходится определять и все остальные операции над числами Скотта:
Зато операция вычитания (и следовательно деления) в целом более проста чем в кодировании Чёрча, благодаря простоте операции для чисел Скотта. Аналогично и предикаты равенства и «меньше чем» гораздо проще (в смысле сложности вычислений):
Списки Неизменяемые списки из упорядоченных элементов можно кодировать несколькими способами: используя по две пары на каждый узел списка; с одной парой на каждый узел списка; кодированием Чёрча - через функцию свёртки справа; и кодированием Скотта, как aлгебраический тип данных.
Две пары на узел При представлении в виде пары первый элемент содержит первый элемент списка, а второй — «хвост» списка, содержащий все остальные элементы. Поскольку таким способом не может быть выражен пустой список, то используется дополнительная обёртка — первый элемент указывает, является ли список пустым, а второй элемент содержит пару из первого элемента списка и хвоста списка.
Базовые операции со списками в этой схеме кодирования можно выразить следующим образом:
— пустой список; — возвращает первый элемент пары, который и означает, является ли список пустым; — конструирует новый непустой список из первого элемента (головы списка) и хвоста ; — первый элемент пары во втором элементе — голова списка; — второй элемент пары во втором элементе — хвост списка.
Используя эти функции можно определить остальные необходимые операции для списков, например, определение длины можно записать как:
хотя оно рекурсивно, что недопустимо в лямбда исчислении и требует дальнейшего применения комбинатора неподвижной точки. Возможно и более непосредственное определение, как
В пустом списке доступ ко второму элементу никогда не применяется, поскольку к нему не применимы понятия головы и хвоста списка.
Одна пара на узел В качестве альтернативы списки можно определить следующим образом ( здесь соответствует пустому списку, непустые задаются парой головы и хвоста)As PDF: :
Здесь предикат вызывает функцию-представление списка с функцией продолжения, в качестве первого аргумента, которая получает два аргумента и , голову и хвост списка, в случае если список не пуст; и со значением в качестве второго аргумента, которое будет возвращено, если список пустой. Этот выбор уже произведен в момент создания значения .
Обобщенный образец обработки таких списков это . Соответственно, лучше определять
для большей надежности.
Списки по Чёрчу В качестве альтернативы кодированию с использованием пар, кодировка Чёрча отождествляет список с функцией которая осуществляет его свёртку справа. Например, список из трёх элементов , и представляется функцией , которая ожидает комбинирующую функцию и значение , и возвращает значение свёртки :
Здесь используются мнемонические имена переменных для (голова списка), для (хвост списка), и для рекурсивного результата свертки хвоста списка.
Таким образом, и . Функция определена таким же путём что и функция для чисел Чёрча — передачей комбинирующей функции вперёд по цепочке после её одноразовой замены в самом начале на функцию пропускающую самый первый элемент (соотвестственно одноразовой замене данной функции на функцию тождества в случае чисел Чёрча, для выполнения операции на один раз меньше).
Легко определяются добавочные функции, как например:
Итак списки Чёрча — это функции свёртки, и операция это тождественная функция ( свёртывает список составленный из эндофункций). Числа же по Чёрчу (как видно и из определения ) — это свертка справа унарного представления натуральных чисел, то есть списка из неразличимых, неинтересных элементов, длиной равной величине числа. Поэтому соответствует функции , а соответствует , с исключением аргумента в обоих случаях.
Списки по Скотту Ещё одним альтернативным представлением является представление списков через , которое использует идеи продолжения и сопоставления с образцом, и может привести к упрощению программного кода, а может и к усложнению.
Списки — это суммарный тип данных с двумя вариантами. В соответствии с общими принципами кодировки Скотта, каждый список представлен функцией которая ожидает два аргумента, две функции-получателя соответствующие этим двум вариантам: одна для варианта пустого списка и другая для непустого. Функция для непустого варианта получит головной элемент и хвост, а для пустого никаких данных нет, так что это не функция а просто величина:
Таким образом каждая величина в кодировке Скотта представляет собой результат уже произведённого сопоставления с образцами соответствующего типа данных. Например, величина заключает в себе уже произведённый выбор варианта — получив и , она проигнорирует и вызовет с соответствующими данными, и .
Как числа по Чёрчу соответствуют спискам по Чёрчу с игнорированием их элементов, так же и для кодировок Скотта.
В отличие от кодирования Чёрча, которое, будучи сверткой, уже содержит в себе рекурсию для рекурсивных типов, кодирование Скотта игнорирует рекурсивность и представляет любые типы с одинаковым подходом, просто отображая их внешнюю структуру. Поэтому в отличие от списков Чёрча где мы передаём списку новую функцию свёртки и всю работу выполняет он сам, рекурсивные функции для списков Скотта проходится кодировать с явной рекурсией:
Примечания
Литература Directly Reflective Meta-Programming Church numerals and booleans explained. Robert Cartwright Rice University