Кодирование Чёрча (Tk;njkfguny C~jcg)

В математике кодирование Чёрча означает представление (или процедуру представления) данных и операторов в процедуре лямбда-исчисления. Необходимость процедуры вызвана тем, что в чистом лямбда-исчислении среди термов присутствуют только переменные и отсутствуют константы. Для того, чтобы получить объекты, ведущие себя таким же образом как и числа, применяется кодирование Чёрча. Сама процедура названа в честь Алонзо Чёрча, разработавшего лямбда-исчисление и впервые применившего этот метод кодирования данных. По аналогии с числами, кодирование Чёрча может быть применено и для представления объектов других типов, ведущих себя как константы.

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

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

Нумералы Чёрча

Нумералы Чёрча являются представлениями натуральных чисел в кодировании Чёрча. Функция высшего порядка, которая представляет натуральное число n, является функцией, которая отображает любую функцию $f$ в её n-кратную композицию. Проще говоря, «значение» нумерала эквивалентно тому, сколько раз функция инкапсулирует свой аргумент.

f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}.\,

Все нумералы Чёрча являются функциями с двумя параметрами. Нумералы Чёрча '0' , '1' , '2' , …, определены в лямбда-исчислении следующим образом:

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

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

Нумерал Чёрча 3 представляет процесс троекратного применения любой используемой функции f. Эта функция последовательно применяется сначала к переданному ей параметру, а затем — к полученному в результате её предыдущего применения результату.

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

Арифметические операции над числами могут быть представлены функциями над нумералами Чёрча. Эти функции могут быть определены в лямбда-исчислении или реализованы в большинстве функциональных языков программирования (см. Преобразование лямбда-выражений в функции).

Кодирование логических значений

Булеаны Чёрча — это результат кодирования Чёрча применённого к представлению логических значений true и false. Некоторые языки программирования используют их в качестве модели реализации для булевой арифметики. Примерами таких языков являются Smalltalk и Pico.

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

true выбирает первый параметр.
false выбирает второй параметр.

Эти два определения известны как булеаны Чёрча:

{\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}

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

Функция, возвращающая логическое значение, которое затем применяется к двум параметрам, возвращает либо первый, либо второй параметр:

\operatorname {predicate} \ x\ \operatorname {then-clause} \ \operatorname {else-clause}

разрешается как then-clause если предикат x разрешается как истина, и как else-clause если предикат x разрешается как ложь.

Поскольку true и false соответствуют выбору первого или второго параметра этой функции, этот формализм может быть использован для реализации стандартных логических операторов. Обратите внимание, что существуют две версии реализации оператора not, в зависимости от выбранной стратегии разрешения выражения.

{\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\ {\scriptstyle {\text{(Это - корректная версия реализации для аппликативного порядка вычислений.)}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ {\scriptstyle {\text{(Это - корректная версия реализации для нормального порядка вычислений.)}}}\\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}

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

{\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}

Предикаты

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

Наиболее фундаментальным предикатом является $\operatorname {IsZero}$ , который возвращает $\operatorname {true}$ (истину), если его аргумент является нумералом Чёрча $0$ , и $\operatorname {false}$ (ложь), если его аргумент является любым другим нумералом Чёрча:

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

Этот предикат проверяет, является ли его первый аргумент меньшим или равным, по сравнению со вторым:

\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)

,

В связи с идентичностью,

x=y\equiv (x\leq y\land y\leq x)

проверка на равeнство может быть реализована следующим способом:

\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)

Пары Чёрча

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

{\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}

Пример:

{\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}

Кодирование списков

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

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

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

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

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

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

First содержит первый элемент списка.
Second содержит оставшиеся элементы ('хвост' списка).

Однако, таким способом не получится выразить пустой список, потому что у нас не определено представление пустого значения (null). Чтобы представить его и получить возможность кодировать пустые списки, пара может быть обёрнута в другую пару.

First — null (пустой список).
Second.First содержит первый элемент списка.
Second.Second содержит хвост списка.

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

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

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

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

В качестве альтернативы, списки можно определить следующим образом:^[2]

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

где последнее определение — это специальный случай более общей функции:

\operatorname {process-list} \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause}

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

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

{\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda t.\lambda g.g\ h\ (t\ c))\ (\lambda t.n)\ (\lambda h.\lambda t.t)\end{aligned}}

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

Ещё одним альтернативным представлением является представление списков через кодирование Скотта, которое использует идею продолжения и может привести к упрощению кода^[3]. (см. также кодирование Могенсена — Скотта). В этом подходе мы используем тот факт, что списки можно обрабатывать путём сопоставления с образцом.

См. также

Система F в части использования и реализации в ней нумералов Чёрча при типизированных вычислениях
Кодирование Могенсена-Скотта^[англ.]
Определение порядковых чисел по фон Нейману — ещё один способ представления натуральных чисел. В этом случае они определяются через множества.

Примечания

↑ Pierce, Benjamin C.^[англ.]. Types and Programming Languages^[англ.]. — MIT Press, 2002. — С. 500. — ISBN 978-0-262-16209-8.
↑ Tromp, John. 14. Binary Lambda Calculus and Combinatory Logic // Randomness And Complexity, From Leibniz To Chaitin (англ.) / Calude, Cristian S.. — World Scientific, 2007. — P. 237—262. — ISBN 978-981-4474-39-9.
As PDF: Tromp, John Binary Lambda Calculus and Combinatory Logic (неопр.) (PDF) (14 мая 2014). Дата обращения: 24 ноября 2017. Архивировано 1 июня 2018 года.
↑ Jansen, Jan Martin. Programming in the λ-Calculus: From Church to Scott and Back (англ.) // LNCS^[англ.] : journal. — 2013. — Vol. 8106. — P. 168—180. — doi:10.1007/978-3-642-40355-2_12.

Литература

Directly Reﬂective Meta-Programming
Church numerals and booleans explained. Robert Cartwright Rice University
Theoretical Foundations For Practical 'Totally Functional Programming' (Главы 2 и 5). Всё про кодирование Чёрча и другие схожие методы кодирования.
Some interactive examples of Church numerals
Lambda Calculus Live Tutorial: Boolean Algebra

[1] Pierce, Benjamin C.^[англ.]. Types and Programming Languages^[англ.]. — MIT Press, 2002. — С. 500. — ISBN 978-0-262-16209-8.

[2] Tromp, John. 14. Binary Lambda Calculus and Combinatory Logic // Randomness And Complexity, From Leibniz To Chaitin (англ.) / Calude, Cristian S.. — World Scientific, 2007. — P. 237—262. — ISBN 978-981-4474-39-9.
As PDF: Tromp, John Binary Lambda Calculus and Combinatory Logic (неопр.) (PDF) (14 мая 2014). Дата обращения: 24 ноября 2017. Архивировано 1 июня 2018 года.

[3] Jansen, Jan Martin. Programming in the λ-Calculus: From Church to Scott and Back (англ.) // LNCS^[англ.] : journal. — 2013. — Vol. 8106. — P. 168—180. — doi:10.1007/978-3-642-40355-2_12.

[1]

[2]

[3]