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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle \lnot \equiv \lambda p.p\bot \top =\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 n}$, определяется как функция от двух параметров ${\displaystyle f}$ и ${\displaystyle x}$, последовательно применяющая ${\displaystyle n}$ раз функцию ${\displaystyle f}$ начиная с ${\displaystyle x}$ — другими словами, число Чёрча отображает функцию ${\displaystyle f}$ в её ${\displaystyle n}$-кратную само-композицию:

${\displaystyle n:f\mapsto f^{\circ n}}$

${\displaystyle f^{\circ n}(x)=(\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ раз}}})\,(x)=\underbrace {f(f(\ldots (f} _{n{\text{ раз}}}\,(x))\ldots ))}$

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

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

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

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

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

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

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

Действительно, выполнить что-то на один раз больше значит выполнить это ещё один раз. Таково последующее число после любого данного числа. В частности, ${\displaystyle \operatorname {succ} 0}$ и ${\displaystyle 1}$ ${\displaystyle \beta }$-эквивалентны.

И наоборот, беря эту операцию за основу вместе с нулём, как в аксиомах Пеано, можно вывести операцию сложения из неё, повторяя её данное число раз, получая эквивалентное определение

${\displaystyle (+)\equiv \lambda mn.n\ \operatorname {succ} \ m\,}$

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

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

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

${\displaystyle {\begin{aligned}\operatorname {exp} &\equiv \lambda bn.\lambda fx.n\ b\ f\ x\\\operatorname {tet} &\equiv \lambda bn.n\ (\lambda rb.r\ b\ b)\ 0\ b\end{aligned}}}$

Значит для чисел Чёрча "энная степень" это просто ${\displaystyle I}$, т.е. само число, а "энная тетрация" это ${\displaystyle \lambda n.n\ W\ 0}$, где ${\displaystyle W}$ это стандартный комбинатор удвоения аргумента, ${\displaystyle Wxy=x\ y\ y}$.

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

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

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

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

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

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

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

Аналогично функции ${\displaystyle \operatorname {pred} }$ определяются и другие функции, как например ${\displaystyle \operatorname {half} }$, вычисляющая целочисленное деление на 2, или факториал, ${\displaystyle \operatorname {fact} }$, а также и более эффективная версия вычитания,

${\displaystyle {\begin{aligned}\operatorname {half} &\equiv \lambda nfx.n\ (\lambda rij.i\ (r\ j\ i))\ (\lambda ji.x)\ I\ f\\\operatorname {fact} &\equiv \lambda nfx.n\ (\lambda ra.a\ (r\ (\operatorname {succ} \ a)))\ (\lambda a.f)\ 1\ x\end{aligned}}}$

${\displaystyle {\begin{aligned}(-)\equiv \lambda mnfx.m\ &(\lambda rq.q\ r)\ (\lambda q.x)\\(n\ &(\lambda qr.r\ q)\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}}$

Примеры вычисления: ${\displaystyle \operatorname {half} \ 5\ f\ x=I\ (f\ (I\ (f\ (I\ x))))}$ ; ${\displaystyle \operatorname {fact} \ 3\ f\ x=1\ (2\ (3\ (K\ f\ 4)))\ x}$ ; ${\displaystyle \operatorname {(-)} \ 6\ 3\ f\ x=f\ (2\ f\ x)}$.

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

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

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

${\displaystyle (\leqslant )\equiv \lambda m.\lambda n.\operatorname {isZero} \ ((-)\ 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)}$

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

${\displaystyle (<)\equiv \lambda m.\lambda n.\lnot \ ((\leqslant )\ n\ m)}$

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

${\displaystyle 0\equiv \lambda xy.x}$

${\displaystyle 1\equiv \lambda xy.y\ 0}$

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

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

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

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

${\displaystyle {\text{Nat}}\ :=\ 0\mid S\,\ {\text{Nat}}}$.

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\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]:

${\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} \ l=\operatorname {if} \ (\operatorname {isnil} l)\ 0\ (\operatorname {succ} \ (\operatorname {length} \ (\operatorname {tail} \ l)))}$

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

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

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

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

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \,\,\,\,=\ \lambda htc.c\ h\ t\\\operatorname {head} &\equiv \operatorname {first} \,\,\,\,=\ \lambda l.l\ (\lambda ht.h)\\\operatorname {tail} &\equiv \operatorname {second} \,\,\,\,=\ \lambda l.l\ (\lambda ht.t)\\\operatorname {nil} &\equiv \lambda ab.b\\\operatorname {isnil} &\equiv \lambda l.l\,(\lambda htz.\operatorname {\bot } )\,\top \\\operatorname {length} &\equiv (\lambda g.g\ g)\ (\lambda gl.l\ (\lambda htz.\operatorname {succ} \ (g\ g\ t))\ 0)\,\,\,\,=\ \operatorname {foldr} \ (\lambda h.\operatorname {succ} )\ 0\\\operatorname {map} &\equiv \lambda f.(\lambda g.g\ g)\ (\lambda gl.l\ (\lambda htz.\operatorname {cons} \ (f\ h)\ (g\ g\ t))\ \operatorname {nil} )\,\,\,\,=\ \lambda f.\operatorname {foldr} \ (\operatorname {cons} \circ f)\ \operatorname {nil} \\\operatorname {foldr} &\equiv \lambda cn.(\lambda g.g\ g)\ (\lambda gl.l\ (\lambda htz.c\ h\ (g\ g\ t))\ n)\end{aligned}}}$

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

Обобщенный образец обработки таких списков это ${\displaystyle \lambda l.(\lambda htz.\langle {\text{head-and-tail-clause}}\rangle \ )\ \langle {\text{nil-clause}}\rangle }$. Соответственно, лучше определять

${\displaystyle {\begin{aligned}\operatorname {head} &\equiv \lambda l.l\ (\lambda htz.h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \lambda l.l\ (\lambda htz.t)\ \operatorname {nil} \end{aligned}}}$

для большей надежности.

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

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \lambda ht.\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)\ \operatorname {nil} \\\operatorname {tail} &\equiv \lambda l.\lambda cn.l\ (\lambda hrg.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda hr.r)\end{aligned}}}$

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

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

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

${\displaystyle {\begin{aligned}\operatorname {singleton} &\equiv \lambda h.\lambda cn.c\ h\ n\\\operatorname {length} &\equiv \lambda l.l\ (\lambda hr.\operatorname {succ} \ r)\ 0\ \,\,\,=\operatorname {foldr} \ (\lambda h.\operatorname {succ} )\ 0\\\operatorname {toChurchNum} &\equiv \lambda lfx.l\ (\lambda h.f)\ x\\\operatorname {foldr} &\equiv \lambda cnl.l\ c\ n\\\operatorname {foldEndo} &\equiv \lambda l.l\ (\lambda h.h)\ \,\,\,=\operatorname {foldMapEndo} \ (\lambda h.h)\\\operatorname {foldMapEndo} &\equiv \lambda fl.l\ f\ \,\,\,\,\,\,\,\,\,=\lambda flx.\operatorname {foldr} \ f\ x\ l\\\operatorname {map} &\equiv \lambda fl.\lambda cn.l\ (\lambda h.c\ (f\ h))\ n\ \,\,\,=\lambda flc.l\ (c\circ f)\ =\lambda flcn.\operatorname {foldr} \ (c\circ f)\ n\ l\\\operatorname {filter} &\equiv \lambda pl.\lambda cn.l\ (\lambda h.p\ h\ (c\ h)\ (\lambda r.r))\ n\end{aligned}}}$

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

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

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

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \lambda ht.\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\ \operatorname {nil} \ (\lambda ht.h)\\\operatorname {tail} &\equiv \lambda l.l\ \operatorname {nil} \ (\lambda ht.t)\end{aligned}}}$

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

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

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

${\displaystyle {\begin{aligned}\operatorname {foldr} &\equiv \lambda cnl.(\lambda g.g\ g\ l)\ (\lambda gl.l\ n\ (\lambda ht.c\ h\ (g\ g\ t)))\\\operatorname {length} &\equiv \operatorname {foldr} \ (\lambda h.\operatorname {succ} )\ 0\\\operatorname {toChurchNum} &\equiv \lambda lfx.\operatorname {foldr} \ (\lambda h.f)\ x\ l\\\operatorname {map} &\equiv \lambda flnc.\operatorname {foldr} \ (\lambda hr.c\ (f\ h)\ r)\ n\ l\\\operatorname {filter} &\equiv \lambda plnc.\operatorname {foldr} \ (\lambda h.p\ h\ (c\ h)\ (\lambda r.r))\ n\ l\end{aligned}}}$

• 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