Я читал об исчислении лямбда, и люблю идеи, предложенные им, но есть некоторые вещи, которые я просто не могу объяснить;Как бы исчисление лямбда добавляло числа?
Как будет исчисление лямбда идти о добавлении чисел?
Я понимаю, что
(\x . + x x) 3
такая же, как 3 + 3, что 6, но как функция добавления были реализованы в первую очередь?
Должно быть, что-то компиляторы/языки должны были бы встроить или определить его только по лямбда-исчислению?
Да, вы можете определить числа (и действительно, произвольные типы данных) внутри лямбда-исчисления. Вот идея.
Прежде всего, давайте определим, какие цифры мы будем определять. Простейшими числами для работы являются натуральные цифры: 0, 1, 2, 3 и т. Д. Как мы их определяем? Обычный подход заключается в использовании Peano axioms:
Здесь S обозначает преемника п или п +1. Таким образом, первые несколько натуральных чисел Пеано равны 0, S0, SS0, SSS0 и т. Д. - это унарное представление.
Теперь, в исчислении лямбда, мы можем представить применение функции, поэтому мы можем представить S n, но мы не знаем, как представлять 0 и S сами. Но, к счастью, лямбда-исчисление предлагает нам способ отложить этот выбор: мы можем принять их в качестве аргументов и позволить кому-то решать! Давайте напишем z для 0, которые нам даны, и s для S мы даны. Тогда мы можем представить первые несколько чисел следующим образом, написание ⟦п⟧ для «лямбда-исчисление представление натурального числа п»:
Подобно тому, как натуральное число п является п приложения S 0, лямбда-исчисление представление п является приложение n копии любое правопреемник s до любой zer o z. Мы можем определить преемника, тоже:
Здесь мы видим, что преемник применяет одну дополнительную копию s к н, убедившись, н использует тот же z и s. Мы можем видеть, что это дает нам то же представление, используя ⇝ для "имеет значение":
(Да, это становится плотным и трудно читать быстро. Работа через это довольно хорошее упражнение, если вы чувствуете, как вам нужно больше практики - это привело к тому, что я ошибся в том, что я изначально написал!)
Теперь мы определили 0 и S, так что это хорошее начало, но нам нужен также принцип индукции. В конце концов, это то, что делает их натуральными. Итак, как это будет работать? Ну, оказывается, мы в основном настроены. Когда мы будем думать о нашем принципе индукции программно, нам нужна функция, которая принимает в качестве входных данных базовый случай и индуктивный случай и производит функцию от натуральных чисел до какого-то выхода. Я буду называть вывод «доказательством для n». Тогда наши входы должны быть:
Другими словами, нам нужно какое-то нулевое значение и некоторая функция-преемник. Но это только наши z и s аргументы! Итак, получается, что мы представляем натуральные числа как их принцип индукции, который я считаю довольно крутым.
А это означает, что мы можем определить основные операции. Я просто определю дополнение здесь, и оставлю все остальное как упражнение. В нашей индуктивной формулировке, мы можем определить сложение следующим образом:
Это индуктивно определено во втором аргументе. Итак, как мы это переводим? Это становится:
Где это пришло? Ну, мы применяем наш индуктивный принцип к n. В базовом случае мы возвращаем м (с использованием окружающего воздуха с и z), как указано выше. В индуктивном случае мы применяем преемника (эмбиент s) к тому, что мы выходим. Так что это должно быть правильно!
Другой способ смотреть на это является то, что, так как нсекг применяется п копии s к г, имеем п (мsz) s применяется n экземпляры s до мсек г, в общей сложности п + м копии с к г. Опять же, это правильный ответ!
(Если вы все еще не убежден, я призываю вас работать небольшой пример, как ⟦1 + 2⟧;., Которые должны быть достаточно малы, чтобы быть послушным, но достаточно большой, чтобы быть по крайней мере несколько интересно)
Итак, теперь мы видим, как определить добавление натуральных чисел внутри чистого нетипизированного лямбда-исчисления. Вот некоторые дополнительные мысли для дальнейшего чтения, если хотите; они более уплотнены и менее объяснены.
Эта техника представления более общеприменима; это не только натуральные числа. Он называется Church encoding и может быть адаптирован для произвольного отображения algebraic data types. Так же, как мы представляли натуральные числа по их принципу индукции, мы представляем все типы данных по их структурной рекурсивной схеме (своя складка): представление типа данных является функцией, которая принимает один аргумент для каждого конструктора, а затем применяет этот «конструктор» «со всеми необходимыми аргументами. Так что:
data Either a b = Left a | Right b):
data List a = Nil | Cons a (List a)):
Обратите внимание, что в последнем случае, л будет себя закодированный список.
Этот метод также работает в типизированной настройке, где мы можем говорить о складках (или катаморфизмах) для типов данных. (Я в основном упоминаю это, потому что лично считаю, что это действительно здорово.) data Nat = Z | S Nat затем изоморфен forall a. a -> (a -> a) -> a, а списки e s изоморфны forall a. e -> (e -> a -> a) -> a, что является лишь частью сигнатуры типа общего .Универсально квантифицированные a s представляют собой тип естественного числа или самого списка; они должны быть оценены по всему миру, поэтому для их прохождения требуется higher-rank types. Изоморфизм засвидетельствован тем, что foldr Cons Nil является тождественной функцией; для натурального числа, закодированного как n, мы также имеем n Z S, восстанавливая наш первоначальный список.
Если вас беспокоит тот факт, что мы использовали только натуральные числа, мы можем определить представление для целых чисел; например, общее представление унарный стиле является
data Int = NonNeg Nat | NegSucc Nat
Здесь NonNeg n представляет n и NegSucc n представляет -(n+1); дополнительный +1 в отрицательном футляре гарантирует наличие уникального 0. Вам должно быть ясно убедиться, что вы могли бы, если хотите, реализовать различные арифметические функции на Int на языке программирования с реальными типами данных; эти функции затем могут быть закодированы в нетипизированном лямбда-исчислении через церковную кодировку, и поэтому мы настроены. Фракции также представлены в виде пар, хотя я не знаю представления, которое гарантирует, что все дроби однозначно представлены. Представление реальных чисел становится сложным, но числа с плавающей запятой IEEE 754 могут быть представлены в виде 32-, 64- или 128-байтовых логических элементов, которые ужасно неэффективны и громоздки, но кодируются.
Также доступны более эффективные представления натуральных чисел (и целых чисел и т. Д.); например,
data Pos = One
| Twice Pos
| TwiceSucc Pos
кодирует положительные двоичные числа (Twice n является 2*n, или добавление 0 до конца; TwiceSucc является 2*n + 1, или добавление 1 до конца; базовый случай One, один 1). Кодирование натуральных чисел является то, как просто, как
data Nat = Zero | PosNat Pos
, но тогда наши функции, такие как сложение, получить более сложный (но быстрее).
Предполагая, что вы используете Church numerals, а не какой-то примитивный числовой тип, сложение состав:
\x \y . (\z . x(y(z)))
Если вы добавили какой-то примитивный числовой тип для вашего лямбда-исчисления, сложение придется либо быть примитивным или быть определенным в терминах чего-то вроде операции-преемника.
Это невероятно отличный ответ. +1 также для форматирования. – phg