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

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

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

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

Числа Чёрча

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

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

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

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

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

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

Операция сложения, благодаря тождеству ${\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}$, может быть определена как:

${\displaystyle (+)\equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}$.

Добавление единицы ${\displaystyle \operatorname {succ} \equiv (+1)}$ посредством ${\displaystyle \beta }$-редукции выводится из сложения:

${\displaystyle \operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}$.

Умножение вводится следующим образом:

${\displaystyle (\cdot )\equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}$.

Операция возведения в степень ${\displaystyle b^{n}}$ благодаря определению чисел Чёрча формулируется лаконично:

${\displaystyle \operatorname {exp} \equiv \lambda b.\lambda n.n\ b}$.

Более сложное выражение требуется для вычитания единицы ${\displaystyle \operatorname {pred} }$:

${\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$.

Разность двух чисел строится из вычитания единицы:

${\displaystyle (-)\equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m}$.

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

Булеаны Чёрча — представления булевых значений, то есть «истины» (${\displaystyle \top }$) и «лжи» (${\displaystyle \bot }$) как выбора первого и второго аргумента соответственно:

${\displaystyle \top \equiv \lambda a.\lambda b.a}$, ${\displaystyle \bot \equiv \lambda a.\lambda b.b}$.

Некоторые языки программирования, такие как Smalltalk и Pico^[англ.], используют их в качестве модели реализации для булевой арифметики.

Такое определение позволяет использовать предикаты (функции, возвращающие логические значения) как условия в условных выражениях. Над ${\displaystyle \top }$ и ${\displaystyle \bot }$ могут быть реализованы стандартные логические операторы (конъюнкция, дизъюнкция, отрицание, исключающее «или»:

${\displaystyle (\wedge )\equiv \lambda p.\lambda q.p\ q\ p}$,

${\displaystyle (\vee )\equiv \lambda p.\lambda q.p\ p\ q}$,

${\displaystyle \lnot \equiv \lambda p.p\bot \top =\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.\lambda a.\lambda b.p\ b\ a}$,

${\displaystyle (\oplus )\equiv \lambda a.\lambda b.a\ (\lnot \ b)\ b}$.

Реализация тернарной условной операции:

${\displaystyle \operatorname {if} \equiv \lambda p.\lambda a.\lambda b.p\ a\ b}$.

Предикаты — функции, возвращающие логическое значение — реализуются естественным образом, например, предикат ${\displaystyle (=0)}$, возвращающий ${\displaystyle \top }$, если его аргумент является числом Чёрча ${\displaystyle 0}$, и ${\displaystyle \bot }$ в ином случае, вводится таким образом:

${\displaystyle (=0)\equiv \lambda n.n\ (\lambda x.\bot )\ \top }$,

предикат ${\displaystyle (\leqslant )}$ над числами Чёрча, который проверяет, меньше или равен его первый аргумент второму:

${\displaystyle (\leqslant )=\lambda m.\lambda n.(=0)((-)m\ n)}$.

Из тождества ${\displaystyle x=y\equiv (x\leqslant y\land y\leqslant x)}$ получается предикат проверки на равенство ${\displaystyle (=)}$:

${\displaystyle (=)\equiv \lambda m.\lambda n.(\wedge )((\leqslant )\ m\ n)\ ((\leqslant )\ n\ m)}$

Пары Чёрча

См. также: cons

Пары Чёрча — соглашение о кодировании упорядоченных пар, то есть наборов из двух элементов: пара представляется как функция, которая применяет свой единственный аргумент ${\displaystyle f}$ к обоим элементам пары ${\displaystyle x}$ и ${\displaystyle y}$, получая в результате ${\displaystyle f\ x\ y}$. Функция образующая пару из аргументов: ${\displaystyle \operatorname {pair} \equiv \lambda x.\lambda y.\lambda z.z\ x\ y}$. Функции ${\displaystyle \operatorname {first} }$ и ${\displaystyle \operatorname {second} }$, возвращающие соответственно первый и второй элемент пары:

${\displaystyle \operatorname {first} \equiv \lambda p.p\ (\lambda x.\lambda y.x)}$,

${\displaystyle \operatorname {second} \equiv \lambda p.p\ (\lambda x.\lambda y.y)}$.

Списки

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

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

При представлении в виде двух пар первый элемент содержит первый элемент списка, а второй — все остальные элементы, «хвост» списка. Поскольку таким способом не может быть выражен пустой список, то используется дополнительная обёртка — первый элемент указывает, является ли список пустым, а второй элемент содержит пару из первого элемента списка и хвоста списка.

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

${\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \top \top }$ — пустой список;

${\displaystyle \operatorname {isnil} \equiv \operatorname {first} }$ — возвращает первый элемент пары, который и означает, является ли список пустым;

${\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \bot \,(\operatorname {pair} h\ t)}$ — конструирует новый непустой список из первого элемента (головы списка) ${\displaystyle h}$ и хвоста ${\displaystyle t}$;

${\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}$ — первый элемент пары во втором элементе — голова списка;

${\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}$ — второй элемент пары во втором элементе — хвост списка.

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

${\displaystyle \operatorname {length} =\lambda l.\operatorname {if} \ (\operatorname {isnil} l)\ 0\ ((+1)\operatorname {length} \operatorname {tail} l)}$.

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

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

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

${\displaystyle \operatorname {cons} \equiv \operatorname {pair} }$,

${\displaystyle \operatorname {head} \equiv \operatorname {first} }$,

${\displaystyle \operatorname {tail} \equiv \operatorname {second} }$,

${\displaystyle \operatorname {nil} \equiv \bot }$,

${\displaystyle \operatorname {isnil} \equiv \lambda l.l\,(\lambda h.\lambda t.\lambda d.\operatorname {\bot } )\,\top }$.

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

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

${\displaystyle \operatorname {nil} \equiv \lambda c.\lambda n.n}$,

${\displaystyle \operatorname {isnil} \equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {\bot } )\top }$,

${\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)}$,

${\displaystyle \operatorname {head} \equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {\bot } }$,

${\displaystyle \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)}$.

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

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

Примечания

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.

Литература

• 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