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

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

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

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

В этой статье может быть использована сокращённая λ-нотация для абстракций, $\lambda xy.z\equiv \lambda x.\lambda y.z\equiv \lambda x.(\lambda y.z)$ .

Пары Чёрча

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

\operatorname {pair} \equiv \lambda xy.\lambda f.f\ x\ y

Здесь $f$ выступает в роли функции-продолжения, или функции-обработчика двух величин из пары.

Функции $\operatorname {first}$ и $\operatorname {second}$ , возвращающие соответственно первый и второй элемент пары, а также функция $\operatorname {swap}$ (два варианта, для примера), меняющая местами два элемента пары, определяются как:

\operatorname {first} \equiv \lambda p.p\ (\lambda xy.x)

\operatorname {second} \equiv \lambda p.p\ (\lambda xy.y)

\operatorname {swap} \equiv \lambda p.p\ (\lambda xy.\lambda f.f\ y\ x)

\operatorname {swap} \equiv \lambda p.\lambda f.p\ (\lambda xy.f\ y\ x)

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

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

\top \equiv \lambda a.\lambda b.a

\bot \equiv \lambda a.\lambda b.b

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

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

(\wedge )\equiv \lambda p.\lambda q.p\ q\ \bot

(\vee )\equiv \lambda p.\lambda q.p\ \top \ q

\lnot \equiv \lambda p.p\bot \top =\lambda p.\lambda a.\lambda b.p\ b\ a

(\oplus )\equiv \lambda a.\lambda b.a\ (\lnot \ b)\ b

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

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

.

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

Числа Чёрча

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

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

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

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

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

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

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

(+)\equiv \lambda m.\lambda n.\lambda fx.m\ f\ (n\ f\ x)

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

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

Для умножения замечаем, что $(m\cdot n)$ -кратное повторение функции $f$ это $m$ -кратное повторение $n$ -кратно повторенной функции $f$ , $f^{\circ (m\cdot n)}=(f^{\circ n})^{\circ m}$ :

(\cdot )\equiv \lambda m.\lambda n.\lambda fx.m\ (n\ f)\ x

Возведение в степень $b^{n}$ это умножение на $b$ , повторенное $n$ раз, $b\ (b\ (b\ldots (b\ f)\ldots ))$ :

\operatorname {exp} \equiv \lambda b.\lambda n.\lambda fx.n\ b\ f\ x

Число-предшественник выполняет данную ему функцию на один раз меньше, подменяя её функцией тождества, один только раз, при первом применении:

\operatorname {pred} \equiv \lambda nfx.n\ (\lambda ri.i\ (r\ f))\ (\lambda f.x)\ (\lambda u.u)

Для примера, $\operatorname {pred} 3\ f\ x=(\lambda u.u)\ (f\ (f\ ((\lambda f.x)\ f)))=f\ (f\ x)$ .

Вычитание числа $n$ достигается повторным вычитанием единицы, $n$ раз:

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

Похожим образом могли бы быть определены:

{\begin{aligned}(+)&\equiv \lambda m.\lambda n.n\ \operatorname {succ} \ m\\(\cdot )&\equiv \lambda m.\lambda n.n\ ((+)\ m)\ 0\\\operatorname {exp} &\equiv \ \lambda b.\lambda n.n\ ((\cdot )\ b)\ (\operatorname {succ} \ 0)\end{aligned}}

Аналогично функции $\operatorname {pred}$ определяются и другие функции, как например:

{\begin{aligned}\operatorname {half} &\equiv \lambda nfx.n\ (\lambda rij.i\ (r\ j\ i))\ (\lambda ji.x)\ (\lambda u.u)\ f\\\operatorname {fact} &\equiv \lambda nfx.n\ (\lambda ri.i\ (r\ (\operatorname {succ} \ i)))\ (\lambda i.f)\ 1\ x\end{aligned}}

вычисляющие целочисленное деление на 2, и факториал (выполняющий, к примеру, $\operatorname {fact} 3\ f\ x=1\ (2\ (3\ f))\ x$ ).

Предикаты для чисел Чёрча

Предикат $\operatorname {isZero}$ , возвращающий $\top$ , если его аргумент является числом Чёрча $0$ , и $\bot$ в ином случае, вводится таким образом:

\operatorname {isZero} \equiv \lambda n.n\ (\lambda x.\bot )\ \top

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

(\leqslant )\equiv \lambda m.\lambda n.\operatorname {isZero} \ ((-)\ m\ n)

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

(=)\equiv \lambda m.\lambda n.(\wedge )\ ((\leqslant )\ m\ n)\ ((\leqslant )\ n\ m)

Предикат «меньше» это

(<)\equiv \lambda m.\lambda n.\lnot \ ((\leqslant )\ n\ m)

Числа по Скотту

Для сравнения, кодирование чисел по Скотту определено как^[1]

0\equiv \lambda xy.x

1\equiv \lambda xy.y\ 0

\operatorname {succ} \equiv \lambda u.\lambda xy.y\ u

\operatorname {pred} \equiv \lambda n.n\ 0\ (\lambda u.u)

\operatorname {isZero} \equiv \lambda n.n\ \top \ (\lambda u.\bot )

Кодировка Скотта для каждого алгебраического типа данных напрямую соответствует его определению. Натуральные числа по Пеано — это суммарный тип данных с двумя вариантами, 0 и не-0:

{\text{Nat}}\ :=\ 0\mid S\,\ {\text{Nat}}

.

Соответственно, числo по Скотту это функция, ожидающaя две функции-обработчика, по числу вариантов.

Число по Скотту являет собой уже совершённое сопоставление с образцом, и вызывает соответствующую функцию-обработчик в соответствии с тем, является ли оно нулём или нет. В случае нуля дополнительных данных нет, так что это не функция а просто некая величина $x$ , $0=\lambda xy.x$ . В случае же не-нулевого числа, дополнительным данным явлается его предшествующее число, например $1=\lambda xy.y\ 0$ .

В то время как в кодировке Чёрча $2\ f\ x=f\ (f\ x)$ , в кодировке Скотта $2\ x\ f=f\ 1$ , $1\ x\ f=f\ 0$ , и $0\ x\ f=x$ . Соответственно и функции перевода в другой тип тоже разнятся,

\operatorname {fromChurch} \equiv \lambda sz.\lambda n.n\ s\ z

\operatorname {fromScott} s\ z=\lambda n.n\ z\ (\lambda u.s\ (\operatorname {fromScott} s\ z\ u))

Как видим, определение перевода чисел Скотта рекурсивно, и требует использования оператора неподвижной точки, или соответственного переопределения с использованием само-применения, «вручную»:

\operatorname {fromScott} \equiv \lambda sz.(\lambda g.g\ g)\ (\lambda gn.n\ z\ (\lambda u.s\ (g\ g\ u)))

Сложение определяется через повторение операции $\operatorname {succ}$ , с использованием явной рекурсии:

(+)\ m\ n=m\ n\ (\lambda u.\operatorname {succ} \ ((+)\ u\ n))

(+)\equiv \lambda mn.(\lambda g.g\ g\ m)\ (\lambda gm.m\ n\ (\lambda u.\operatorname {succ} \ (g\ g\ u)))

Так же с использованием явной рекурсии приходится определять и все остальные операции над числами Скотта:

{\begin{aligned}(\cdot )\equiv \ &\lambda mn.n\ 0\ (\lambda v.(\lambda g.g\ g\ m)\ (\lambda gm.m\ 0\ (\lambda u.(+)\ n\ (g\ g\ u))))\\\operatorname {exp} \equiv \ &\lambda mn.n\ 1\ (\lambda v.m\ 0\ (\lambda u.(\lambda g.g\ g\ v)\ (\lambda gv.(\cdot )\ m\ (v\ 1\ (g\ g))))))\end{aligned}}

Зато операция вычитания (и следовательно деления) в целом более проста чем в кодировании Чёрча, благодаря простоте операции $\operatorname {pred}$ для чисел Скотта. Аналогично и предикаты равенства и «меньше чем» гораздо проще (в смысле сложности вычислений):

{\begin{aligned}(-)\equiv \ &(\lambda g.g\ g)\ (\lambda gmn.m\ 0\ (\lambda u.n\ m\ (\lambda v.g\ g\ u\ v)))\\(\leqslant )\equiv \ &(\lambda g.g\ g)\ (\lambda gmn.m\ \top \ (\lambda u.n\ \bot \ (\lambda v.g\ g\ u\ v)))\\(=)\equiv \ &(\lambda g.g\ g)\ (\lambda gmn.m\ (\operatorname {isZero} n)\ (\lambda u.n\ \bot \ (\lambda v.g\ g\ u\ v)))\\(<)\equiv \ &(\lambda g.g\ g)\ (\lambda gmn.m\ (\lnot \ (\operatorname {isZero} n))\ (\lambda u.n\ \bot \ (\lambda v.g\ g\ u\ v)))\end{aligned}}

Списки

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

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

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

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

\operatorname {nil} \equiv \operatorname {pair} \top \ \top \

— пустой список;

\operatorname {isnil} \equiv \operatorname {first} \

— возвращает первый элемент пары, который и означает, является ли список пустым;

\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \bot \,(\operatorname {pair} h\ t)\

— конструирует новый непустой список из первого элемента (головы списка)

h

и хвоста

t

;

\operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)\

— первый элемент пары во втором элементе — голова списка;

\operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)\

— второй элемент пары во втором элементе — хвост списка.

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

\operatorname {length} \ l=\operatorname {if} \ (\operatorname {isnil} l)\ 0\ (\operatorname {succ} \ (\operatorname {length} \ (\operatorname {tail} \ l)))

хотя оно рекурсивно, что недопустимо в лямбда исчислении и требует дальнейшего применения комбинатора неподвижной точки. Возможно и более непосредственное определение, как

\operatorname {length} \equiv (\lambda g.g\ g)\ (\lambda gl.l\ (\lambda xy.x\ 0\ (\operatorname {succ} \ (g\ g\ \ (\operatorname {second} \ y)))))

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

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

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

\operatorname {cons} \equiv \operatorname {pair}

\operatorname {head} \equiv \operatorname {first}

\operatorname {tail} \equiv \operatorname {second}

\operatorname {nil} \equiv \bot

\operatorname {isnil} \equiv \lambda l.l\,(\lambda ht.\lambda z.\operatorname {\bot } )\,\top

Здесь предикат $\operatorname {isnil}$ вызывает функцию-представление списка $l$ с функцией продолжения, в качестве первого аргумента, которая получает два аргумента $h$ и $t$ , голову и хвост списка, в случае если список не пуст; и со значением $\top$ в качестве второго аргумента, которое будет возвращено, если список $l$ пустой. Этот выбор уже произведен, заранее, в момент создания значения $l$ .

Списки по Чёрчу

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

\operatorname {cons} \equiv \lambda h.\lambda t.\lambda cn.c\ h\ (t\ c\ n)

\operatorname {nil} \equiv \lambda cn.n

\operatorname {isnil} \equiv \lambda l.l\ (\lambda hr.\bot )\ \top

\operatorname {head} \equiv \lambda l.l\ (\lambda hr.h)\ \bot

\operatorname {tail} \equiv \lambda l.\lambda cn.l\ (\lambda hrg.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda hr.r)

Здесь используются мнемонические имена переменных $h$ для $head$ (голова списка), $t$ для $tail$ (хвост списка), и $r$ для рекурсивного результата свертки хвоста списка.

Таким образом, $\operatorname {head} \operatorname {nil} \equiv \bot$ и $\operatorname {tail} \operatorname {nil} \equiv \operatorname {nil}$ . Функция $\operatorname {tail}$ определена таким же путём что и функция $\operatorname {pred}$ для чисел Чёрча — передачей комбинирующей функции вперёд по цепочке после её одноразовой замены в самом начале на функцию пропускающую самый первый элемент (и соотвестственно, одноразовой замены данной функции $f$ на функцию тождества в случае чисел Чёрча, для выполнения операции $f$ на один раз меньше).

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

\operatorname {singleton} \equiv \lambda h.\lambda cn.c\ h\ n

\operatorname {length} \equiv \lambda l.l\ (\lambda hr.\operatorname {succ} \ r)\ 0

\operatorname {toChurchNum} \equiv \lambda lfx.l\ (\lambda hr.f\ r)\ x

\operatorname {fold} \equiv \lambda lcx.l\ c\ x

\operatorname {foldEndo} \equiv \lambda lx.l\ (\lambda hr.h\ r)\ x

\operatorname {map} \equiv \lambda fl.\lambda cn.l\ (\lambda h.c\ (f\ h))\ n

\operatorname {filter} \equiv \lambda pl.\lambda cn.l\ (\lambda h.p\ h\ (c\ h)\ (\lambda r.r))\ n

Итак списки Чёрча — это функции свёртки, и операция $\operatorname {fold}$ это тождественная функция ( $\operatorname {foldEndo}$ свёртывает список составленный из эндофункций). Числа же по Чёрчу (как видно и из определения $\operatorname {toChurchNum}$ ) — это свертка справа унарного представления натуральных чисел, то есть списка из неразличимых, неинтересных элементов, длиной равной величине числа. Поэтому $\operatorname {pred}$ соответствует функции $\operatorname {tail}$ , а $\operatorname {succ}$ соответствует $\operatorname {cons}$ , с исключением аргумента $h$ в обоих случаях.

Списки по Скотту

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

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

\operatorname {cons} \equiv \lambda h.\lambda t.\lambda nc.c\ h\ t

\operatorname {nil} \equiv \lambda nc.n

\operatorname {isnil} \equiv \lambda l.l\ \top \ (\lambda ht.\operatorname {\bot } )

\operatorname {head} \equiv \lambda l.l\ \bot \ (\lambda ht.h)

\operatorname {tail} \equiv \lambda l.l\ \operatorname {nil} \ (\lambda ht.t)

Таким образом каждая величина в кодировке Скотта представляет собой результат уже произведённого сопоставления с образцами соответствующего типа данных. Например, величина $cons\ 1\ nil=\lambda nc.c\ 1\ nil$ заключает в себе уже произведённый выбор варианта — получив $n$ и $c$ , она проигнорирует $n$ и вызовет $c$ с соответствующими данными, $1$ и $nil$ .

Как числа по Чёрчу соответствуют спискам по Чёрчу с игнорированием их элементов, так же и для кодировок Скотта.

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

\operatorname {length} \equiv (\lambda g.g\ g)\ (\lambda gl.l\ 0\ (\lambda ht.\operatorname {succ} \ (g\ g\ t)))

\operatorname {toChurchNum} \equiv \lambda lfx.(\lambda g.g\ g\ l)\ (\lambda gl.l\ x\ (\lambda ht.f\ (g\ g\ t)))

\operatorname {map} \equiv \lambda f.(\lambda g.g\ g)\ (\lambda gl.\lambda nc.l\ n\ (\lambda ht.c\ (f\ h)\ (g\ g\ t)))

\operatorname {filter} \equiv \lambda p.(\lambda g.g\ g)\ (\lambda gl.\lambda nc.l\ n\ (\lambda h.p\ h\ (\lambda t.c\ h\ (g\ g\ t))\ (g\ g)))

Примечания

↑ History of Lambda-calculus and Combinatory Logic, 2006, by Felice Cardone and J. Roger Hindley, p. 18, note 38
↑ 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.