Церковное кодирование

Представление натуральных чисел в виде функций высшего порядка

В математике кодировка Чёрча — это способ представления данных и операторов в лямбда-исчислении . Числа Чёрча — это представление натуральных чисел с использованием лямбда-нотации. Метод назван в честь Алонзо Чёрча , который впервые закодировал данные в лямбда-исчислении таким образом.

Термины, которые обычно считаются примитивными в других нотациях (такие как целые числа, булевы значения, пары, списки и помеченные объединения), отображаются в функции более высокого порядка в кодировке Чёрча. Тезис Чёрча–Тьюринга утверждает, что любой вычислимый оператор (и его операнды) могут быть представлены в кодировке Чёрча. ^{[ dubious – discussion ]} В нетипизированном лямбда-исчислении единственным примитивным типом данных является функция.

Использовать

Простая реализация кодировки Чёрча замедляет некоторые операции доступа от до , где — размер структуры данных, что делает кодировку Чёрча непрактичной. ^[1] Исследования показали, что эту проблему можно решить с помощью целевых оптимизаций, но большинство функциональных языков программирования вместо этого расширяют свои промежуточные представления, чтобы они содержали алгебраические типы данных . ^[2] Тем не менее кодировка Чёрча часто используется в теоретических рассуждениях, поскольку она является естественным представлением для частичной оценки и доказательства теорем. ^[1] Операции можно типизировать с использованием типов более высокого ранга , ^[3] и примитивная рекурсия легко доступна. ^[1] Предположение, что функции являются единственными примитивными типами данных, упрощает многие доказательства. ${\displaystyle O(1)}$ ${\displaystyle O(n)}$ ${\displaystyle n}$

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

Церковные цифры

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

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

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

Начиная с 0, не применяя функцию вообще, продолжаем с 1, применяя функцию один раз, 2, применяя функцию дважды, 3, применяя функцию трижды и т. д .:

${\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 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))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}$

Числовое значение 3 в трактовке Чёрча представляет собой действие применения любой заданной функции три раза к значению. Предоставленная функция сначала применяется к предоставленному параметру, а затем последовательно к своему собственному результату. Конечным результатом не является число 3 (если только предоставленный параметр не равен 0, а функция не является функцией- последователем ). Сама функция, а не ее конечный результат, является числительным значением 3 в трактовке Чёрча . Числительное значение 3 в трактовке Чёрча просто означает сделать что-либо три раза. Это наглядная демонстрация того, что подразумевается под «тремя разами».

Расчет с помощью церковных цифр

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

Функция сложения использует тождество . ${\displaystyle \operatorname {plus} (m,n)=m+n}$ ${\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}$

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

Функция преемника β - эквивалентна . ${\displaystyle \operatorname {succ} (n)=n+1}$ ${\displaystyle (\operatorname {plus} \ 1)}$

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

Функция умножения использует тождество . ${\displaystyle \operatorname {mult} (m,n)=m*n}$ ${\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}$

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

Функция возведения в степень задается определением чисел Чёрча, . В определении подставим, чтобы получить и, ${\displaystyle \operatorname {exp} (m,n)=m^{n}}$ ${\displaystyle n\ h\ x=h^{n}\ x}$ ${\displaystyle h\to m,x\to f}$ ${\displaystyle n\ m\ f=m^{n}\ f}$

${\displaystyle \operatorname {exp} \ m\ n=m^{n}=n\ m}$

что дает лямбда-выражение,

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

Функцию понять сложнее. ${\displaystyle \operatorname {pred} (n)}$

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

Число Чёрча применяет функцию n раз. Функция-предшественник должна возвращать функцию, которая применяет свой параметр n - 1 раз. Это достигается путем построения контейнера вокруг f и x , который инициализируется таким образом, что пропускает применение функции в первый раз. См. previous для более подробного объяснения.

Функцию вычитания можно записать на основе предшествующей функции.

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

Таблица функций над церковными числами

Примечания :

1. Эта формула является определением числа Чёрча n с . ${\displaystyle f\to m,x\to f}$
2. В церковной кодировке,
   • ${\displaystyle \operatorname {pred} (0)=0}$
   • ${\displaystyle m\leq n\to m-n=0}$

Вывод функции-предшественника

Функция-предшественник, используемая в кодировке Чёрча, следующая:

${\displaystyle \operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}$.

Нам нужен способ применения функции на 1 раз меньше для построения предшественника. Число n применяет функцию f n раз к x . Функция-предшественник должна использовать число n для применения функции n -1 раз.

Перед реализацией функции-предшественника, вот схема, которая оборачивает значение в функцию-контейнер. Мы определим новые функции для использования вместо f и x , называемые inc и init . Функция-контейнер называется value . В левой части таблицы показано число n , примененное к inc и init .

${\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}$

Общее правило повторения таково:

${\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}$

Если также имеется функция для извлечения значения из контейнера (называемая extract ),

${\displaystyle \operatorname {extract} \ (\operatorname {value} \ v)=v}$

Тогда extract может быть использован для определения функции samenum следующим образом:

${\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}$

Функция samenum сама по себе бесполезна. Однако, поскольку inc делегирует вызов f своему аргументу-контейнеру, мы можем организовать так, чтобы при первом применении inc получал специальный контейнер, который игнорирует свой аргумент, позволяя пропустить первое применение f . Назовем этот новый начальный контейнер const . Правая часть приведенной выше таблицы показывает расширения n inc const . Затем, заменив init на const в выражении для той же функции, мы получим функцию-предшественника,

${\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)}$

Как поясняется ниже, функции inc , init , const , value и extract могут быть определены следующим образом:

${\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}$

Что дает лямбда-выражение для pred как,

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

Другой способ определения pred

Pred также можно определить с помощью пар:

${\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}$

Это более простое определение, но приводит к более сложному выражению для pred. Расширение для : ${\displaystyle \operatorname {pred} \operatorname {three} }$

${\displaystyle {\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}}$

Разделение

Деление натуральных чисел можно реализовать с помощью, ^[4]

${\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}$

Вычисление требует много бета-сокращений. Если только вы не делаете сокращение вручную, это не имеет большого значения, но предпочтительнее не делать это вычисление дважды. Простейшим предикатом для проверки чисел является IsZero , поэтому рассмотрим условие. ${\displaystyle n-m}$

${\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}$

Но это условие эквивалентно , а не . Если использовать это выражение, то математическое определение деления, данное выше, переводится в функцию над числами Чёрча как, ${\displaystyle n\leq m}$ ${\displaystyle n<m}$

${\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}$

Как и ожидалось, это определение имеет один вызов . Однако результатом является то, что эта формула дает значение . ${\displaystyle \operatorname {minus} \ n\ m}$ ${\displaystyle (n-1)/m}$

Эту проблему можно исправить, добавив 1 к n перед вызовом деления . Определение деления тогда следующее:

${\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}$

divide1 — рекурсивное определение. Для реализации рекурсии можно использовать комбинатор Y. Создайте новую функцию с именем div by;

• С левой стороны ${\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}$
• С правой стороны ${\displaystyle \operatorname {divide1} \rightarrow c}$

получить,

${\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}$

Затем,

${\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}$

где,

${\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}$

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

${\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}$

Дает,

${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}$

Или как текст, используя \ вместо λ ,

делим = (\n.((\f.(\xx x) (\xf (xx))) (\c.\n.\m.\f.\x.(\d.(\nn (\x .(\a.\bb)) (\a.\ba)) d ((\f.\xx) fx) (f (cdmfx))) ((\m.\nn (\n.\f.\ xn (\g.\hh (gf)) (\ux) (\uu)) m) nm))) ((\n.\f.\x. f (nfx)) n))

Например, 9/3 представлено как

делим (\f.\xf (f (f (f (f (f (f (f (f (fx))))))))) (\f.\xf (f (fx)))

Используя калькулятор лямбда-исчисления, приведенное выше выражение сокращается до 3, используя обычный порядок.

\ф.\хф (ф (ф (х)))

Подписанные числа

Одним из простых подходов к расширению чисел Чёрча до знаковых чисел является использование пары Чёрча, содержащей числа Чёрча, представляющие положительное и отрицательное значение. ^[5] Целое значение представляет собой разницу между двумя числами Чёрча.

Натуральное число преобразуется в число со знаком с помощью,

${\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}$

Отрицание выполняется путем перестановки значений.

${\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}$

Целочисленное значение представляется более естественно, если одно из пары равно нулю. Функция OneZero достигает этого условия,

${\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}$

Рекурсию можно реализовать с помощью комбинатора Y,

${\displaystyle \operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}$

${\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }$

Плюс и минус

Сложение определяется математически по паре следующим образом:

${\displaystyle x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]}$

Последнее выражение переводится в лямбда-исчисление как:

${\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}$

Аналогично определяется вычитание,

${\displaystyle x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]}$

давая,

${\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

Умножение и деление

Умножение может быть определено как,

${\displaystyle x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]}$

Последнее выражение переводится в лямбда-исчисление как:

${\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

Аналогичное определение дано здесь для деления, за исключением того, что в этом определении одно значение в каждой паре должно быть равно нулю (см. OneZero выше). Функция divZ позволяет нам игнорировать значение, имеющее нулевой компонент.

${\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}$

Затем divZ используется в следующей формуле, которая аналогична формуле умножения, но с заменой mult на divZ .

${\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

Рациональные и действительные числа

Рациональные и вычислимые действительные числа также могут быть закодированы в лямбда-исчислении. Рациональные числа могут быть закодированы как пара знаковых чисел. Вычислимые действительные числа могут быть закодированы с помощью ограничивающего процесса, который гарантирует, что разница с действительным значением отличается на число, которое может быть сделано настолько малым, насколько нам нужно. ^{[6] [7]} Приведенные ссылки описывают программное обеспечение, которое теоретически может быть переведено в лямбда-исчисление. После определения действительных чисел комплексные числа естественным образом кодируются как пара действительных чисел.

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

Перевод с другими представлениями

Большинство реальных языков поддерживают машинно-родные целые числа; функции church и unchurch преобразуют неотрицательные целые числа в соответствующие им числительные Church. Функции приведены здесь на Haskell , где \соответствует λ лямбда-исчисления. Реализации на других языках аналогичны.

тип Церковь а = ( а -> а ) -> а -> а          церковь :: Целое число -> Церковь Целое число церковь 0 = \ f -> \ x -> x церковь n = \ f -> \ x -> f ( церковь ( n - 1 ) f x )                       unchurch :: Церковь Целое число -> Целое число unchurch cn = cn ( + 1 ) 0           

Церковные булевы операторы

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

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

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

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

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

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

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

оценивается как then-clause, если predicate-x оценивается как true , и как else-clause, если predicate-x оценивается как false .

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

${\displaystyle {\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\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}$

Вот несколько примеров:

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

Предикаты

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

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

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

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

Из-за идентичности,

${\displaystyle x=y\equiv (x\leq y\land y\leq x)}$

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

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

Церковные пары

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

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

Например,

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

Список кодировок

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

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

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

Две пары как узел списка

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

• Первый содержит голову.
• Во втором случае имеется хвост.

Однако это не дает представления пустого списка, поскольку нет указателя "null". Для представления null пара может быть обернута в другую пару, что даст три значения:

• Сначала — нулевой указатель (пустой список).
• Во-вторых, во-первых, содержится голова.
• Во-вторых. Во-вторых, содержится хвост.

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

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

Одна пара как узел списка

В качестве альтернативы, определите ^[9]

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

где последнее определение является частным случаем общего

${\displaystyle \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 возвращает cx (cy (czn)).

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

Этому списковому представлению можно присвоить тип в Системе F.

Представьте список с помощью кодировки Скотта

Альтернативным представлением является кодирование Скотта, которое использует идею продолжений и может привести к более простому коду. ^[10] (см. также кодирование Могенсена–Скотта ).

В этом подходе мы используем тот факт, что списки можно наблюдать с помощью выражения сопоставления с образцом. Например, используя нотацию Scala , если listобозначает значение типа Listс пустым списком Nilи конструктором, Cons(h, t)мы можем проверить список и вычислить, nilCodeесли список пуст и consCode(h, t)когда список не пуст:

список совпадений { case Nil => nilCode case Cons ( h , t ) => consCode ( h , t ) }           

Задается listтем, как он действует на nilCodeи consCode. Поэтому мы определяем список как функцию, которая принимает такие nilCodeи consCodeв качестве аргументов, так что вместо приведенного выше сопоставления с образцом мы можем просто написать:

${\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }$

Обозначим через nпараметр, соответствующий nilCode, а через cпараметр, соответствующий consCode. Пустой список — это тот, который возвращает аргумент nil:

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

Непустой список с головой hи хвостом tзадается формулой

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

В более общем смысле, алгебраический тип данных с альтернативами становится функцией с параметрами. Когда конструктор th имеет аргументы, соответствующий параметр кодировки также принимает аргументы. ${\displaystyle m}$ ${\displaystyle m}$ ${\displaystyle i}$ ${\displaystyle n_{i}}$ ${\displaystyle n_{i}}$

Кодирование Скотта может быть выполнено в нетипизированном лямбда-исчислении, тогда как его использование с типами требует системы типов с рекурсией и полиморфизмом типов. Список с типом элемента E в этом представлении, который используется для вычисления значений типа C, будет иметь следующее рекурсивное определение типа, где '=>' обозначает тип функции:

тип List = C => // аргумент nil ( E => List => C ) => // аргумент cons C // результат сопоставления с образцом               

Список, который может быть использован для вычисления произвольных типов, будет иметь тип, который квантифицирует по C. Список generic ^{[ необходимо пояснение ]} в Eтакже будет принимать Eв качестве аргумента типа.

Смотрите также

• Лямбда-исчисление
• Система F для чисел Чёрча в типизированном исчислении
• Кодировка Могенсена–Скотта
• Определение фон Неймана ординалов — еще один способ кодирования натуральных чисел: как наборов

Ссылки

1. Trancón y Widemann, Baltasar; Parnas, David Lorge (2008). "Tabular Expressions and Total Functional Programming". В Olaf Chitil; Zoltán Horváth; Viktória Zsók (ред.). Implementation and Application of Functional Languages. 19-й международный семинар, IFL 2007, Фрайбург, Германия, 27–29 сентября 2007 г. Пересмотренные избранные статьи. Lecture Notes in Computer Science. Том 5083. С. 228–229. doi :10.1007/978-3-540-85373-2_13. ISBN 978-3-540-85372-5.
2. Янсен, Ян Мартин; Купман, Питер ВМ; Пласмейер, Маринус Дж. (2006). «Эффективная интерпретация путем преобразования типов данных и шаблонов в функции». В Нильссон, Хенрик (ред.). Тенденции в функциональном программировании. Том 7. Бристоль: Intellect. стр. 73–90. CiteSeerX 10.1.1.73.9841 . ISBN  978-1-84150-188-8.
3. «Предшественник и списки не могут быть представлены в простом типизированном лямбда-исчислении». Лямбда-исчисление и лямбда-калькуляторы . okmij.org.
4. Эллисон, Ллойд. «Лямбда-исчисление целых чисел».
5. Бауэр, Андрей. «Ответ Андрея на вопрос: «Представление отрицательных и комплексных чисел с помощью лямбда-исчисления»».
6. "Точная вещественная арифметика". Haskell . Архивировано из оригинала 2015-03-26.
7. Бауэр, Андрей (26 сентября 2022 г.). "Программное обеспечение для вычисления действительных чисел". GitHub .
8. Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press . стр. 500. ISBN 978-0-262-16209-8.
9. Тромп, Джон (2007). "14. Двоичное лямбда-исчисление и комбинаторная логика". В Calude, Cristian S (ред.). Случайность и сложность, от Лейбница до Хайтина . World Scientific. стр. 237–262. ISBN 978-981-4474-39-9.
   В формате PDF: Тромп, Джон (14 мая 2014 г.). «Двоичное лямбда-исчисление и комбинаторная логика» (PDF) . Получено 24.11.2017 .
10. Янсен, Ян Мартин (2013). «Программирование в λ-исчислении: от Чёрча до Скотта и обратно». В Ахтен, Питер; Купман, Питер ВМ (ред.). Красота функционального кода — эссе, посвящённые Ринусу Пласмейеру по случаю его 61-го дня рождения . Конспект лекций по информатике. Том 8106. Springer. С. 168–180. doi :10.1007/978-3-642-40355-2_12.

• Stump, A. (2009). «Прямо рефлексивное метапрограммирование» (PDF) . High-Order Symb Comput . 22 (2): 115–144. CiteSeerX  10.1.1.489.5018 . doi :10.1007/s10990-007-9022-0. S2CID  16124152.
• Картрайт, Роберт. "Объяснение церковных цифр и булевых значений" (PDF) . Comp 311 — Обзор 2 . Университет Райса .
• Кемп, Колин (2007). "§2.4.1 Church Naturals, §2.4.2 Church Booleans, Гл. 5 Методы вывода для TFP". Теоретические основы практического "полностью функционального программирования"(PhD). Факультет информационных технологий и электротехники, Университет Квинсленда. С. 14–17, 93–145. CiteSeerX  10.1.1.149.3505 . Все о кодировках Чёрча и других подобных кодировках, включая способы их получения и операции над ними, из первых принципов
• Некоторые интерактивные примеры церковных цифр
• Учебное пособие по лямбда-исчислению: Булева алгебра