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

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

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

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

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

Числа Чёрча

Число Чёрча, соответствующее натуральному числу $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=\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$

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

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

Операция сложения, отображая тождество $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)

Для примера, $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

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

\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\ (succ\ i)))\ (\lambda i.f)\ 1\ x

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

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

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

0=\lambda xy.x

1=\lambda xy.y\ 0

succ=\lambda u.\lambda xy.y\ u

pred=\lambda n.n\ 0\ (\lambda u.u)

isZero=\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$ . Соответственно и функции перевода в другой тип тоже разнятся,

fromChurch\ =\lambda sz.\lambda n.n\ s\ z

fromScott\ =\lambda sz.\lambda n.n\ z\ (\lambda u.s\ (fromScott\ s\ z\ u))

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

fromScott\ =\lambda sz.(\lambda g.g\ g)\ (\lambda gn.n\ z\ (\lambda u.s\ (g\ g\ u)))

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

Булеаны Чёрча — представления булевых значений, то есть «истины» ( $\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

.

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

(=0)\equiv \lambda n.n\ (\lambda x.\bot )\ \top

,

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

(\leqslant )=\lambda m.\lambda n.(=0)((-)m\ n)

.

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

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

Пары Чёрча

Пары Чёрча — соглашение о кодировании упорядоченных пар, то есть наборов (кортежей) из двух элементов. Пара величин $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)

Списки

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

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

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

Базовые операции со списками в этой схеме кодирования можно выразить следующим образом^[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} =\lambda l.\operatorname {if} \ (\operatorname {isnil} l)\ 0\ (succ\ (\operatorname {length} \ (\operatorname {tail} \ l)))

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

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

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

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

В качестве альтернативы списки можно определить следующим образом ( $\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.\operatorname {\bot } )\ \top

\operatorname {head} \equiv \lambda l.l\ (\lambda hr.h)\operatorname {\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}$ для чисел Чёрча - передачей комбинирующей функции вперёд по цепочке после её одноразовой замены в самом начале на функцию пропускающую самый первый элемент (и соотвестственно, одноразовой замены функции $\operatorname {succ}$ на функцию тождества в случае чисел Чёрча, для выполнения операции $\operatorname {succ}$ на один раз меньше).

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

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

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

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

Вообще числа по Чёрчу это свертка справа унарного представления натуральных чисел, т.е. списка из неразличимых, неинтересных элементов, длиной равной величине числа. Поэтому $\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$ .

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

Примечания

↑ 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.

Литература

Directly Reﬂective 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

[1] History of Lambda-calculus and Combinatory Logic, 2006, by Felice Cardone and J. Roger Hindley, p. 18, note 38

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

[3] 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 года.

[4] 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]

[4]

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

Содержание

Числа Чёрча

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

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

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

Пары Чёрча

Списки

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

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

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

Списки по Могенсену — Скотту

Примечания

Литература

Навигация

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

Числа Чёрча

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

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

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

Пары Чёрча

Списки

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

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

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

Списки по Могенсену — Скотту

Примечания

Литература

Навигация

Поиск