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

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

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

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

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

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

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

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

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

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

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

${\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 означает просто сделать что-либо три раза. Это наглядная демонстрация того, что подразумевается под «три раза».

Расчет с цифрами Чёрча

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

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

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

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

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

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

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

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

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

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

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

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

$\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 , который инициализируется таким образом, чтобы исключить применение функции в первый раз. См. предшественник для более подробного объяснения.

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

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

Таблица функций цифр Чёрча

Функция	Алгебра	Личность	Определение функции	Лямбда-выражения
Преемник	$n+1$	$f^{n+1}\ x=f(f^{n}x)$	$\operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)$	$\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)$	...
Добавление	$m+n$	$f^{m+n}\ x=f^{m}(f^{n}x)$	$\operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.n\operatorname {succ} m$
Умножение	$m*n$	$f^{m*n}\ x=(f^{m})^{n}\ x$	$\operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.m\ (n\ f)$
Возведение в степень	$m^{n}$	$n\ m\ f=m^{n}\ f$	$\operatorname {exp} \ m\ n\ f\ x=(n\ m)\ f\ x$	$\lambda m.\lambda n.\lambda f.\lambda x.(n\ m)\ f\ x$	$\lambda m.\lambda n.n\ m$
Предшественник	$n-1$	$\operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)$	$\operatorname {if} (n==0)\ 0\ \operatorname {else} \ (n-1)$	$\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$
Вычитание ( Монус )	$m-n$	$f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)$	$\operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m$	...	$\lambda m.\lambda n.n\operatorname {pred} m$

Примечание:

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

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

$\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 .

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

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

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

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

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

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

$\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 в выражении для той же функции, мы получим функцию-предшественницу:

$\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 могут быть определены как:

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

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

Контейнер значений Контейнер значений применяет функцию к своему значению. Это определяется, $\operatorname {value} \ v\ h=h\ v$ так, $\operatorname {value} =\lambda v.(\lambda h.h\ v)$ Инк Функция inc должна принимать значение, содержащее v , и возвращать новое значение, содержащее fv . $\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$ Пусть g будет контейнером значений, $g=\operatorname {value} \ v$ затем, $g\ f=\operatorname {value} \ v\ f=f\ v$ так, $\operatorname {inc} \ g=\operatorname {value} \ (g\ f)$ $\operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)$

Извлекать Значение можно извлечь, применив функцию идентификации: $I=\lambda u.u$ Используя Я , $\operatorname {value} \ v\ I=v$ так, $\operatorname {extract} \ k=k\ I$ Конст Для реализации pred функция init заменяется константой , которая не применяет f . Нам нужна константа , чтобы удовлетворить, $\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x$ $\lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x$ Что будет удовлетворено, если $\operatorname {const} \ f=x$ Или как лямбда-выражение, $\operatorname {const} =\lambda u.x$

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

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

${\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. Расширение для $\operatorname {pred} \operatorname {three}$:

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

Разделение

Деление натуральных чисел может быть реализовано с помощью:

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

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

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

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

$\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)$

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

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

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

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

• В левой части $\operatorname {divide1} \rightarrow \operatorname {div} \ c$
• В правой части $\operatorname {divide1} \rightarrow c$

получить,

$\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)$

Затем,

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

где,

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

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

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

Дает,

$\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)$

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

divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

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

divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

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

\f.\x.f (f (f (x)))

Числа со знаком

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

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

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

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

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

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

$\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-комбинатора,

$\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))))$

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

Плюс и минус

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

$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}]$

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

$\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)))$

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

$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}]$

предоставление,

$\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)))$

Умножить и разделить

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

$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}]$

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

$\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 позволяет нам игнорировать значение, имеющее нулевую составляющую.

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

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

$\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)))$

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

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

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

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

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

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

Церковные логические значения

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

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

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

Эти два определения известны как церковные логические значения:

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

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

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

возвращается к предложению then, если значение predicate-x равно true , и к предложению else, если значение predicate-x равно false .

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

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

Несколько примеров:

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

Предикаты

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

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

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

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

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

$x=y\equiv (x\leq y\land y\leq x)$

Проверка на равенство может быть реализована как:

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

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

См. также: Минусы

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

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

Например,

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

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

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

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

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

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

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

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

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

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

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

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

Выражение	Описание
$\operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true}$	Первый элемент пары имеет значение true , что означает, что список имеет значение NULL.
$\operatorname {isnil} \equiv \operatorname {first}$	Получите индикатор null (или пустой список).
$\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\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)$	секунда.секунда — это хвост.

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

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

В качестве альтернативы определите

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

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

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

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

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

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

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

list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}

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

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

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

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

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

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

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

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

type List = 
  C =>                    // nil argument
  (E => List => C) =>     // cons argument
  C                       // result of pattern matching

Список, который можно использовать для вычисления произвольных типов, будет иметь тип, C. Общий список в E тоже взял бы E в качестве аргумента типа.

См. также

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

Ссылки

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