Церковная кодировка - Church encoding - Wikipedia

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

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

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

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

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

Церковные цифры представляют собой натуральные числа под церковной кодировкой. В функция высшего порядка что представляет собой натуральное число п это функция, которая отображает любую функцию к его п-складывать сочинение.[1] Проще говоря, «значение» числа эквивалентно тому, сколько раз функция инкапсулирует свой аргумент.

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

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

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

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

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

Функция сложения использует личность .

Функция преемника является β-эквивалент к .

Функция умножения использует личность .

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

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

В функция труднее понять.

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

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

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

ФункцияАлгебраЛичностьОпределение функцииЛямбда-выражения
Преемник...
Добавление
Умножение
Возведение в степень[2]
Предшественник *

Вычитание *...

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

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

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

.

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

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

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

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

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

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

Как объяснено ниже, функции inc, в этом, const, ценить и извлекать можно определить как,

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

Контейнер значений

Контейнер значений применяет функцию к своему значению. Это определяется

так,

Inc

В inc функция должна принимать значение, содержащее v, и вернуть новое значение, содержащее f v.

Допустим, что g будет контейнером значений,

тогда,

так,

Извлекать

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

С помощью я,

так,

Const

Для реализации пред то в этом функция заменяется на const это не относится ж. Нам нужно const удовлетворить,

Что будет удовлетворено, если,

Или как лямбда-выражение,

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

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

Это более простое определение, но приводит к более сложному выражению для pred. :

Разделение

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

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

Но это условие эквивалентно , нет . Если используется это выражение, то приведенное выше математическое определение деления переводится в функцию на числах Чёрча как,

Как и следовало ожидать, это определение имеет единственный вызов . Однако в результате эта формула дает значение .

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

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

  • В левой части
  • В правой части

получить,

Потом,

куда,

Дает,

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

разделить = ( 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.  x.f (f (f (f (f (f (f (f (f x)))))))) ( f.  x.f (f (f x)))

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

 е.  x.f (е (е (х)))

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

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

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

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

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

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

Плюс и минус

Сложение определяется математически на паре как

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

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

давая

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

Умножение можно определить следующим образом:

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

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

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

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

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

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


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

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

тип Церковь а = (а -> а) -> а -> ацерковь :: Целое число -> Церковь Целое числоцерковь 0 = \ж -> \Икс -> Иксцерковь п = \ж -> \Икс -> ж (церковь (п-1) ж Икс)отлучить от церкви :: Церковь Целое число -> Целое числоотлучить от церкви сп = сп (+ 1) 0

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

Церковные логические значения являются кодировкой Чёрча булевых значений истинный и ложный. Некоторые языки программирования используют их как модель реализации для логической арифметики; примеры Болтовня и Пико.

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

  • истинный выбирает первый параметр.
  • ложный выбирает второй параметр.

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

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

оценивает затем предложение если предикат Икс оценивает истинный, и чтобы else-clause если предикат Икс оценивает ложный.

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

Некоторые примеры:

Предикаты

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

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

,

Из-за личности,

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

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

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

Например,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Представьте список с использованием кодировки Скотта

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

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

список матч {  дело Ноль        => nilCode  дело Минусы(час, т) => consCode(час,т)}

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

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

Непустой список с заголовком "h" и хвостом "t" задается следующим образом:

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

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

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

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

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

Примечания

  1. ^ а б Новый вид науки [1]
  2. ^ Эта формула является определением числа Чёрча n с f -> m, x -> f.
  3. ^ Эллисон, Ллойд. «Целые числа лямбда-исчисления».
  4. ^ Бауэр, Андрей. Ответ Андрея на вопрос: «Представление отрицательных и комплексных чисел с помощью лямбда-исчисления."".
  5. ^ «Точная действительная арифметика». Haskell.
  6. ^ Бауэр, Андрей. «Программное обеспечение для вычисления вещественных чисел».
  7. ^ Пирс, Бенджамин С. (2002). Типы и языки программирования. MIT Press. п. 500. ISBN  978-0-262-16209-8.
  8. ^ Тромп, Джон (2007). «14. Двоичное лямбда-исчисление и комбинаторная логика». В Калуде, Кристиан С. (ред.). Случайность и сложность, от Лейбница до Чайтина. World Scientific. С. 237–262. ISBN  978-981-4474-39-9.
    В формате PDF: Тромп, Джон (14 мая 2014 г.). «Двоичное лямбда-исчисление и комбинаторная логика» (PDF). Получено 2017-11-24.
  9. ^ Янсен, Ян Мартин (2013). «Программирование в λ-исчислении: от Черча до Скотта и обратно». LNCS. 8106: 168–180. Дои:10.1007/978-3-642-40355-2_12.

Рекомендации