Кодирование Чёрча

Кодирование Чёрча ― способ представления данных, не являющихся функциями и переменными, в лямбда-исчислении, к примеру, натуральных чисел и других констант. Метод назван в честь Алонзо Чёрча, разработавшего лямбда-исчисление.

Термы, которые в других формальных системах обычно являются примитивами, такие как целые числа, булевы значения, пары и списки, с помощью кодирования Чёрча представляются в лямбда-исчислении как функции высшего порядка. В одной из своих формулировок тезис Чёрча — Тьюринга утверждает, что в кодировке Чёрча может быть представлен любой вычислимый оператор (и его операнды). В чистом (бестиповом) лямбда-исчислении единственным примитивным типом данных являются функции, а все остальные сущности конструируются при помощи кодирования Чёрча.

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

Числа Чёрча

Представления натуральных чисел в кодировке Чёрча называются числами Чёрча. Число Чёрча, соответствующее натуральному числу n, определяется как функция от двух параметров $f$ и $x$, применяющая $f$ к $x$ n раз — другими словами, число Чёрча отображает функцию $f$ в её n-кратную композицию:

$f^{\circ n}=\underset{n\text{ раз}}{\underbrace{f\circ f\circ \cdots \circ f}}.$

$0fx$ значит «не применять функцию $f$ к $x$ вообще», $1fx$ значит «применять функцию 1 раз» и т. д.:

Число	Определение нумерала	Лямбда-выражение
0	$0fx=x$	$0=\lambda f.\lambda x.x$
1	$1fx=fx$	$1=\lambda f.\lambda x.fx$
2	$2fx=f(fx)$	$2=\lambda f.\lambda x.f(fx)$
3	$3fx=f(f(fx))$	$3=\lambda f.\lambda x.f(f(fx))$
⋮	⋮	⋮
$n$	$nfx=f^{n}x$	$n=\lambda f.\lambda x.f^{\circ n}x$

Вычисления над числами Чёрча

Арифметические операции над числами можно представить в лямбда-исчислении, как функции над числами Чёрча.

Булеаны Чёрча

Представление булевых значений (Шаблон:Lang-en), то есть «истина» (Шаблон:Lang-en) и «ложь» (Шаблон:Lang-en) в кодировке Чёрча называется булеанами Чёрча. Некоторые языки программирования, такие как Smalltalk и Pico, используют их в качестве модели реализации для булевой арифметики.

Булева логика может рассматриваться как выбор из двух вариантов. Кодировки Чёрча булевых значений являются функциями от двух аргументов:

• true из двух аргументов выбирает первый ― $\mathrm{true}\equiv \lambda a.\lambda b.a$.
• false из двух аргументов выбирает второй ― $\mathrm{false}\equiv \lambda a.\lambda b.b$.

Это определение позволяет использовать предикаты (функции, возвращающие логические значения) как условия в условных выражениях:

$\mathrm{x}\mathrm{-}\text{предикат}\text{ветвь}\mathrm{-}\text{то}\text{ветвь}\mathrm{-}\text{иначе}$

вычисляется как ветвь-то, если х-предикат выдаёт истинное значение, и как ветвь-иначе, если х-предикат выдаёт ложное.

Над true и false могут быть реализованы стандартные логические операторы (AND, OR, NOT, XOR, if).

$\begin{array}{cc}\mathrm{and}& =\lambda p.\lambda q.pqp\\ \mathrm{or}& =\lambda p.\lambda q.ppq\\ \mathrm{not}& =\lambda p.p\mathrm{false}\mathrm{true}=\lambda p.p(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=\lambda p.\lambda a.\lambda b.pba\\ \mathrm{xor}& =\lambda a.\lambda b.a(\mathrm{not}b)b\\ \mathrm{if}& =\lambda p.\lambda a.\lambda b.pab\end{array}$

Несколько примеров:

$\begin{array}{cc}\mathrm{and}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.pqp)\mathrm{true}\mathrm{false}=\mathrm{true}\mathrm{false}\mathrm{true}=(\lambda a.\lambda b.a)\mathrm{false}\mathrm{true}=\mathrm{false}\\ \mathrm{or}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.ppq)\mathrm{true}\mathrm{false}=\mathrm{true}\mathrm{true}\mathrm{false}=(\lambda a.\lambda b.a)\mathrm{true}\mathrm{false}=\mathrm{true}\\ \mathrm{not}\mathrm{true}& =(\lambda p.p\mathrm{false}\mathrm{true})\mathrm{true}=\mathrm{true}\mathrm{false}\mathrm{true}=(\lambda a.\lambda b.a)\mathrm{false}\mathrm{true}=\mathrm{false}\end{array}$

Предикаты

Предикатами называются функции, возвращающие логическое значение.

Одним из базовых предикатов является $\mathrm{IsZero}$, который возвращает $\mathrm{true}$, если его аргумент является числом Чёрча $0$, и $\mathrm{false}$, если его аргумент является любым другим:

$\mathrm{IsZero}=\lambda n.n(\lambda x.\mathrm{false})\mathrm{true}$

Предикат $\mathrm{LEQ}$ проверяет, меньше или равен его первый аргумент второму:

$\mathrm{LEQ}=\lambda m.\lambda n.\mathrm{IsZero}(\mathrm{minus}mn)$,

Из тождества $x=y\equiv (x\le y\wedge y\le x)$ получается предикат проверки на равeнство $\mathrm{EQ}$:

$\mathrm{EQ}=\lambda m.\lambda n.\mathrm{and}(\mathrm{LEQ}mn)(\mathrm{LEQ}nm)$

Пары Чёрча

Представление в кодировке Чёрча пар, то есть наборов из двух элементов, называется парами Чёрча. Пара представляется как функция, которая применяет свой единственный аргумент $f$ к обоим элементам пары $x$ и $y$, получая в результате $fxy$.

Определение в лямбда-исчислении функции $\mathrm{pair}$, возвращающей пару из двух элементов, и функций $\mathrm{first}$ и $\mathrm{second}$, возвращающих соответственно первый и второй элемент пары:

$\begin{array}{cc}\mathrm{pair}& \equiv \lambda x.\lambda y.\lambda z.zxy\\ \mathrm{first}& \equiv \lambda p.p(\lambda x.\lambda y.x)\\ \mathrm{second}& \equiv \lambda p.p(\lambda x.\lambda y.y)\end{array}$

Пример:

$\begin{array}{cc}& \mathrm{first}(\mathrm{pair}ab)\\ =& (\lambda p.p(\lambda x.\lambda y.x))((\lambda x.\lambda y.\lambda z.zxy)ab)\\ =& (\lambda p.p(\lambda x.\lambda y.x))(\lambda z.zab)\\ =& (\lambda z.zab)(\lambda x.\lambda y.x)\\ =& (\lambda x.\lambda y.x)ab=a\end{array}$

Списки Чёрча

(Неизменяемый) список состоит из нескольких элементов. Ниже приводятся основные операции, которые должны быть реализованы для списка:

Функция	Описание
nil	Возвращает пустой список.
isnil	Проверяет, является ли список пустым.
cons	Вставляет переданное значение в начало (возможно пустого) списка.
head	Возвращает первый элемент списка.
tail	Возвращает весь список, кроме первого элемента.

С их помощью, например, можно реализовать функцию вычисления длины списка $\mathrm{length}$:

$\mathrm{length}=\lambda l.\mathrm{if}(\mathrm{isnil}l)0(\mathrm{inc}\mathrm{length}\mathrm{tail}l)$

Ниже даются четыре различных представления списков:

• Через создание каждого элемента списка из двух пар.
• Через создание каждого элемента списка из одной пары.
• Представление списка через функцию свёртки справа.
• Представление списка с использованием кодирования Скотта.

Представление в виде двух пар

Непустой список может быть реализован парой Чёрча;

• Первый элемент содержит первый элемент списка.
• Второй содержит оставшиеся элементы («хвост» списка).

Однако, таким способом не получится выразить пустой список. Для этого мы можем обернуть пару в другую пару:

• Первый элемент — является ли список пустым.
• Второй элемент ― пара из первого элемента списка и хвоста списка.

Используя эту идею, базовые операции со списками можно выразить следующим образом:

Функция	Описание
$\mathrm{nil}\equiv \mathrm{pair}\mathrm{true}\mathrm{true}$	Первый элемент пары true означает пустоту списка.
$\mathrm{isnil}\equiv \mathrm{first}$	Возвращает первый элемент пары, который и означает, является ли список пустым.
$\mathrm{cons}\equiv \lambda h.\lambda t.\mathrm{pair}\mathrm{false}(\mathrm{pair}ht)$	Создаём новый непустой список из первого элемента (головы списка) h и хвоста t.
$\mathrm{head}\equiv \lambda z.\mathrm{first}(\mathrm{second}z)$	Первый элемент пары во втором элементе — голова списка.
$\mathrm{tail}\equiv \lambda z.\mathrm{second}(\mathrm{second}z)$	Второй элемент пары во втором элементе — хвост списка.

В пустом списке доступ ко второму элементу никогда не применяется, поскольку к нему не применимы понятия головы и хвоста списка.

Представление в виде одной пары

В качестве альтернативы, списки можно определить следующим образом ($\mathrm{false}$ соответствует пустому списку, непустые задаются парой головы и хвоста):

$\begin{array}{cc}\mathrm{cons}& \equiv \mathrm{pair}\\ \mathrm{head}& \equiv \mathrm{first}\\ \mathrm{tail}& \equiv \mathrm{second}\\ \mathrm{nil}& \equiv \mathrm{false}\\ \mathrm{isnil}& \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\mathrm{false})\mathrm{true}\end{array}$

где последнее определение — пример более общей функции:

$\mathrm{process-list}\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\text{функция от головы и хвоста})\text{случай пустого списка}$

Представление списка через функцию свёртки справа

В качестве альтернативы кодированию с использованием пар Чёрча список можно закодировать, отождествив его с функцией свёртки справа. Например, список из трёх элементов x, y и z может быть закодирован функцией высшего порядка, которая при применении к комбинатору c и значению n возвращает $cx(cy(czn))$.

$\begin{array}{cc}\mathrm{nil}& \equiv \lambda c.\lambda n.n\\ \mathrm{isnil}& \equiv \lambda l.l(\lambda h.\lambda t.\mathrm{false})\mathrm{true}\\ \mathrm{cons}& \equiv \lambda h.\lambda t.\lambda c.\lambda n.ch(tcn)\\ \mathrm{head}& \equiv \lambda l.l(\lambda h.\lambda t.h)\mathrm{false}\\ \mathrm{tail}& \equiv \lambda l.\lambda c.\lambda n.l(\lambda h.\lambda t.\lambda g.gh(tc))(\lambda t.n)(\lambda h.\lambda t.t)\end{array}$

Представление списка с использованием кодирования Скотта

Ещё одним альтернативным представлением является представление списков через кодирование Скотта, которое использует идею продолжения и может привести к упрощению кода. (см. также Шаблон:Iw). В этом подходе используется факт, что списки можно обрабатывать путём сопоставления с образцом.

См. также

• Система F — пример использования кодирования Чёрча.
• Шаблон:Iw
• Определение порядковых чисел по фон Нейману — способ представления натуральных чисел как множества.

Литература

• Directly Reflective Meta-Programming
• Church numerals and booleans explained. Robert Cartwright Rice University
• Theoretical Foundations For Practical 'Totally Functional Programming' (главы 2.4 и 5)
• Some interactive examples of Church numerals
• Lambda Calculus Live Tutorial: Boolean Algebra