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

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

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

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

Лямбда-исчисление обычно интерпретируется как использование содержательного равенства . Существуют потенциальные проблемы с интерпретацией результатов из-за разницы между интенсиональным и экстенсиональным определениями равенства.

Церковные цифры [ править ]

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

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

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

Таблица функций на цифрах Чёрча [ править ]

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

* Обратите внимание, что в церковной кодировке

• ${\displaystyle \operatorname {pred} (0)=0}$
• ${\displaystyle m<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 . Контейнерная функция называется значением . В левой части таблицы показано число 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)}$

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

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

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

${\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 также можно определить с помощью пар:

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

Подразделение [ править ]

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

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

Но это условие эквивалентно , not . Если используется это выражение, то приведенное выше математическое определение деления переводится в функцию на числах Чёрча как,${\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 перед вызовом div . Тогда определение разделения таково :

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

div1 - это рекурсивное определение. 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 (fx)))))))) (\ f. \ xf (f (fx)))

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

\ е. \ xf (е (е (х)))

Подписанные числа [ править ]

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

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

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

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

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

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

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

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

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

Церковные логические значения [ править ]

Булевы значения Чёрча - это Чёрч-кодирование логических значений истина и ложь. Некоторые языки программирования используют их как модель реализации для логической арифметики; примерами являются 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-clauses. Функция, возвращающая логическое значение, которое затем применяется к двум параметрам, возвращает либо первый, либо второй параметр:

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

оценивается как then-clause, если предикат x оценивается как true , и как else-clause, если предикат x оценивается как 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\ {\scriptstyle {\text{(This is only a correct implementation if the evaluation strategy is applicative order.)}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ {\scriptstyle {\text{(This is only a correct implementation if the evaluation strategy is normal order.)}}}\\\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}}}$

Предикаты [ править ]

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

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

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

Выражение	Описание
${\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true} }$	Первый элемент пары истинен, что означает, что список пуст.
${\displaystyle \operatorname {isnil} \equiv \operatorname {first} }$	Получить индикатор null (или пустой список).
${\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)}$	Создайте узел списка, который не является нулевым, и присвойте ему заголовок h и хвост t .
${\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}$	Второй. во- первых, это голова.
${\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}$	второй. второй - хвост.

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

Одна пара как узел списка [ править ]

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

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

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

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

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

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

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

${\displaystyle \operatorname {list} \ \operatorname {nilCode} \ (\operatorname {consCode} \ h\ t)}$

Обозначим через '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, будет иметь следующее определение рекурсивного типа, где '=>' обозначает тип функции:

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

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

См. Также [ править ]

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

Примечания [ править ]

Ссылки [ править ]

• Непосредственно отражающее метапрограммирование
• Церковные числа и логические значения объяснил Роберт Картрайт из Университета Райса
• Теоретические основы практического «полностью функционального программирования» (главы 2 и 5) Все о церковных и других подобных кодировках, в том числе о том, как их вывести и как с ними работать, из первых принципов
• Некоторые интерактивные примеры церковных цифр
• Живое руководство по лямбда-исчислению: логическая алгебра