Лямбда исчисление (также записываются в виде Л-исчисление ) представляет собой формальная система , в математической логике для выражения вычисления на основе функции абстракции и приложение , используя переменные связывания и замену . Это универсальная модель вычислений, которую можно использовать для моделирования любой машины Тьюринга . Он был введен математиком Алонзо Черчем в 1930-х годах в рамках его исследования основ математики .
Лямбда-исчисление состоит из построения лямбда-членов и выполнения над ними операций редукции. В простейшей форме лямбда-исчисления термины строятся с использованием только следующих правил:
Синтаксис | Имя | Описание |
---|---|---|
Икс | Переменная | Символ или строка, представляющая параметр или математическое / логическое значение. |
(λ x . M ) | Абстракция | Определение функции ( M - лямбда-термин). Переменная x становится связанной в выражении. |
( M N ) | Заявление | Применение функции к аргументу. M и N - лямбда-термины. |
продуцирующие такие выражения, как: (λ х .λ у . (Х г . (λ х . гй ) (λ у . ZY )) ( х )). Скобки можно опустить, если выражение однозначно. Для некоторых приложений могут быть включены термины для логических и математических констант и операций.
Операции восстановления включают:
Операция | Имя | Описание |
---|---|---|
(λ x . M [ x ]) → (λ y . M [ y ]) | α-преобразование | Переименование связанных переменных в выражении. Используется, чтобы избежать коллизии имен . |
((λ x . M ) E ) → ( M [ x : = E ]) | β-редукция | Замена связанных переменных выражением аргумента в теле абстракции. |
Если используется индексирование по Де Брёйну , то α-преобразование больше не требуется, поскольку не будет конфликтов имен. Если повторное применение шагов редукции в конце концов прекратится, то по теореме Черча – Россера это приведет к β-нормальной форме .
Имена переменных не нужны при использовании универсальной лямбда-функции, такой как Iota и Jot , которая может создавать любое поведение функции, вызывая ее в различных комбинациях.
Объяснение и приложения
Лямбда-исчисление является полным по Тьюрингу , то есть это универсальная модель вычислений, которую можно использовать для моделирования любой машины Тьюринга . [1] Его тезка, греческая буква лямбда (λ), используется в лямбда-выражениях и лямбда-терминах для обозначения привязки переменной в функции .
Лямбда-исчисление может быть нетипизированным или типизированным . В типизированном лямбда-исчислении функции могут применяться только в том случае, если они способны принимать заданный "тип" входных данных. Типизированные лямбда-исчисления слабее, чем нетипизированное лямбда-исчисление, которое является основной темой этой статьи, в том смысле, что типизированные лямбда-исчисления могут выразить меньше, чем нетипизированное исчисление, но, с другой стороны, типизированные лямбда-исчисления позволяют доказать больше вещей. ; в простом типизированном лямбда-исчислении это, например, теорема, что каждая стратегия оценки завершается для каждого просто типизированного лямбда-члена, тогда как оценка нетипизированных лямбда-членов не должна завершаться. Одной из причин, по которой существует множество различных типизированных лямбда-исчислений, было желание сделать больше (того, что может делать нетипизированное исчисление), не отказываясь от возможности доказать сильные теоремы об исчислении.
Лямбда - исчисление имеет приложения во многих различных областях , в математике , философии , [2] лингвистика , [3] [4] и информатика . [5] Лямбда-исчисление сыграло важную роль в развитии теории языков программирования . Языки функционального программирования реализуют лямбда-исчисление. Лямбда-исчисление также является актуальной темой исследований в теории категорий . [6]
История
Лямбда-исчисление было введено математиком Алонсо Черчем в 1930-х годах в рамках исследования основ математики . [7] [a] Исходная система оказалась логически несовместимой в 1935 году, когда Стивен Клини и Дж. Б. Россер разработали парадокс Клини – Россера . [8] [9]
Впоследствии, в 1936 году, Черч выделил и опубликовал только ту часть, которая относится к вычислениям, то, что сейчас называется нетипизированным лямбда-исчислением. [10] В 1940 году он также представил более слабую в вычислительном отношении, но логически последовательную систему, известную как просто типизированное лямбда-исчисление . [11]
До 1960-х годов, когда было выяснено его отношение к языкам программирования, лямбда-исчисление было всего лишь формализмом. Благодаря приложениям Ричарда Монтегю и других лингвистов к семантике естественного языка лямбда-исчисление стало занимать почетное место как в лингвистике [12], так и в информатике. [13]
Происхождение символа лямбда
Существует некоторое противоречие по поводу того, почему Черч использовал греческую букву лямбда (λ) в качестве обозначения абстракции функции в лямбда-исчислении, возможно, частично из-за противоречивых объяснений самого Черча. Согласно Кардоне и Хиндли (2006):
Кстати, почему Черч выбрал обозначение «λ»? В [неопубликованном письме 1964 года Харальду Диксону] он ясно заявил, что это произошло из обозначения «», Использованный для абстракции классов Уайтхедом и Расселом , сначала изменив«»На« ∧», Чтобы отличить абстракцию функции от абстракции класса, а затем измените« ∧ »на« λ »для облегчения печати.
Об этом происхождении также сообщалось в [Россер, 1984, с.338]. С другой стороны, в последние годы своей жизни Черч сказал двум вопрошающим, что выбор был более случайным: нужен был символ и просто случайно был выбран λ.
Дана Скотт также обращалась к этому противоречию в различных публичных лекциях. [14] Скотт вспоминает, что однажды он задал вопрос о происхождении лямбда-символа зятю Черча Джону Аддисону, который затем написал своему тестю открытку:
Уважаемый профессор Черч,
У Рассела был оператор йота , у Гильберта был оператор эпсилон . Почему вы выбрали лямбду для своего оператора?
По словам Скотта, весь ответ Черча состоял в том, чтобы вернуть открытку со следующей пометкой : « Ини, миини, мини, мо ».
Неформальное описание
Мотивация
Вычислимые функции - это фундаментальное понятие в компьютерных науках и математике. Лямбда-исчисление обеспечивает простую семантику вычислений, позволяя формально изучать свойства вычислений. Лямбда-исчисление включает два упрощения, которые упрощают эту семантику. Первое упрощение состоит в том, что лямбда-исчисление обрабатывает функции «анонимно», не давая им явных имен. Например, функция
можно переписать в анонимной форме как
(который читается как «кортеж х и у будет отображаться в"). Аналогично функция
можно переписать в анонимной форме как
где ввод просто сопоставляется сам с собой.
Второе упрощение состоит в том, что лямбда-исчисление использует только функции одного входа. Обычная функция, требующая двух входов, напримерфункция, может быть преобразована в эквивалентную функцию, которая принимает один ввод, а поскольку вывод возвращает другую функцию, которая, в свою очередь, принимает один ввод. Например,
может быть переработан в
Этот метод, известный как каррирование , преобразует функцию, которая принимает несколько аргументов, в цепочку функций, каждая из которых имеет один аргумент.
Функция приложения из функция к аргументам (5, 2), сразу дает
- ,
тогда как оценка каррированной версии требует еще одного шага
- // определение использовался с во внутреннем выражении. Это похоже на β-редукцию.
- // определение использовался с . Опять же, аналогично β-редукции.
чтобы прийти к тому же результату.
Лямбда-исчисление
Лямбда-исчисление состоит из языка лямбда-терминов , которые определяются определенным формальным синтаксисом, и набора правил преобразования, которые позволяют манипулировать лямбда-терминами. Эти правила преобразования можно рассматривать как эквациональную теорию или как операционное определение .
Как описано выше, все функции в лямбда-исчислении являются анонимными функциями, не имеющими имен. Они принимают только одну входную переменную, а каррирование используется для реализации функций с несколькими переменными.
Лямбда-термины
Синтаксис лямбда-исчисления определяет некоторые выражения как допустимые выражения лямбда-исчисления, а некоторые как недопустимые, точно так же, как некоторые строки символов являются допустимыми программами C , а некоторые - нет. Правильное выражение лямбда-исчисления называется «лямбда-членом».
Следующие три правила дают индуктивное определение, которое можно применять для построения всех синтаксически правильных лямбда-терминов:
- Переменная, , сам по себе является допустимым лямбда-термином
- если - лямбда-член, а переменная, то (иногда записывается в ASCII как) является лямбда-термином (называемым абстракцией );
- если а также являются лямбда-членами, тогда является лямбда-термином (называемым приложением ).
Ничто иное не является лямбда-термином. Таким образом, лямбда-член действителен тогда и только тогда, когда он может быть получен повторным применением этих трех правил. Однако некоторые скобки можно опустить по определенным правилам. Например, крайние круглые скобки обычно не пишутся. См. Обозначения ниже.
абстракция это определение анонимной функции, которая может принимать один ввод и подставив его в выражение . Таким образом, он определяет анонимную функцию, которая принимает и возвращается . Например, является абстракцией для функции используя термин для . Определение функции с абстракцией просто «устанавливает» функцию, но не вызывает ее. Абстракция связывает переменную в срок .
приложение представляет собой приложение функции к входу , то есть представляет собой акт вызова функции на входе производить .
В лямбда-исчислении не существует концепции объявления переменных. В таком определении, как (т.е. ) лямбда-исчисление рассматривает как переменная, которая еще не определена. Абстракция синтаксически действителен и представляет функцию, которая добавляет свой ввод к еще неизвестному .
Могут использоваться скобки, которые могут потребоваться для устранения неоднозначности терминов. Например, а также обозначают разные термины (хотя они по совпадению сводятся к одному и тому же значению). Здесь в первом примере определяется функция, лямбда-член которой является результатом применения x к дочерней функции, а второй пример - это применение самой внешней функции к входу x, который возвращает дочернюю функцию. Таким образом, оба примера оцениваются как функция идентичности .
Функции, которые работают с функциями
В лямбда-исчислении функции считаются « значениями первого класса », поэтому функции могут использоваться в качестве входных данных или возвращаться в качестве выходных данных из других функций.
Например, представляет функцию идентичности ,, а также представляет собой функцию идентичности, применяемую к . Способствовать,представляет постоянную функцию , функция, которая всегда возвращает , независимо от ввода. В лямбда - исчислении применение функции рассматриваются как левоассоциативные , так что средства .
Существует несколько понятий «эквивалентности» и «редукции», которые позволяют «свести» лямбда-термины к «эквивалентным» лямбда-членам.
Альфа-эквивалентность
Основная форма эквивалентности, определяемая с помощью лямбда-терминов, - это альфа-эквивалентность. Он улавливает интуицию, что конкретный выбор связанной переменной в абстракции (обычно) не имеет значения. Например, а также являются альфа-эквивалентными лямбда-терминами, и оба они представляют одну и ту же функцию (функцию идентичности). Условия а также не являются альфа-эквивалентами, потому что они не связаны в абстракции. Во многих презентациях обычно используются альфа-эквивалентные лямбда-термины.
Для определения β-редукции необходимы следующие определения:
Бесплатные переменные
В свободном переменных из термина являются теми переменными , которые не связаны абстракциями. Набор свободных переменных выражения определяется индуктивно:
- Свободные переменные просто
- Набор свободных переменных - множество свободных переменных , но с удаленный
- Набор свободных переменных является объединением множества свободных переменных и набор свободных переменных .
Например, лямбда-термин, представляющий личность не имеет свободных переменных, но функция имеет единственную свободную переменную, .
Замены с избеганием захвата
Предполагать , а также являются лямбда-терминами и а также являются переменными. Обозначение указывает на замену для в в захват, избегая таким образом. Это определяется так, что:
- ;
- если ;
- ;
- ;
- если а также не входит в свободные переменные . Переменная считается "свежим" для .
Например, , а также .
Состояние свежести (требующее, чтобы не входит в свободные переменные ) имеет решающее значение для гарантии того, что подстановка не изменит смысл функций. Например, делается подстановка, игнорирующая условие свежести:. Эта замена превращает постоянную функцию в личность заменой.
В общем, несоблюдение условия свежести можно исправить путем альфа-переименования с подходящей переменной fresh. Например, возвращаясь к нашему правильному представлению о подстановке, в абстракцию можно переименовать с помощью новой переменной , чтобы получить , а смысл функции сохраняется подстановкой.
β-редукция
Правило β-редукции гласит, что приложение формы сводится к сроку . Обозначение используется, чтобы указать, что β-сводится к . Например, для каждого, . Это демонстрирует, чтодействительно личность. По аналогии,, что демонстрирует, что - постоянная функция.
Лямбда-исчисление можно рассматривать как идеализированную версию функционального языка программирования, такого как Haskell или Standard ML . С этой точки зрения β-редукция соответствует вычислительному шагу. Этот шаг можно повторять с помощью дополнительных β-редукций, пока не останется больше приложений для уменьшения. В нетипизированном лямбда-исчислении, представленном здесь, этот процесс редукции не может завершиться. Например, рассмотрим термин. Здесь. То есть этот член сводится к самому себе за одно β-восстановление, и, следовательно, процесс восстановления никогда не завершится.
Другой аспект нетипизированного лямбда-исчисления заключается в том, что оно не делает различий между разными типами данных. Например, может быть желательно написать функцию, которая работает только с числами. Однако в нетипизированном лямбда-исчислении нет способа предотвратить применение функции к значениям истинности , строкам или другим нечисловым объектам.
Формальное определение
Определение
Лямбда-выражения состоят из:
- переменные v 1 , v 2 , ...;
- символы абстракции λ (лямбда) и. (точка);
- круглые скобки ().
Набор лямбда-выражений Λ можно определить индуктивно :
- Если x - переменная, то x ∈ Λ.
- Если x - переменная и M ∈ Λ, то (λ x . M ) ∈ Λ.
- Если M , N ∈ Λ, то ( MN ) ∈ Λ.
Экземпляры правила 2 известны как абстракции, а экземпляры правила 3 называются приложениями . [15] [16]
Обозначение
Чтобы не загромождать нотацию лямбда-выражений, обычно применяются следующие соглашения:
- Крайние круглые скобки опускаются: M N вместо ( M N ).
- Заявки считаются левоассоциативно: М Н Р может быть записан вместо (( М N ) P ). [17]
- Тело абстракции простирается как можно дальше вправо : λ x . МН означает λ х . ( МН ) , а не (λ х . М ) Н .
- Сжимается последовательность абстракций: λ x .λ y .λ z . N сокращенно обозначается λ xyz . N . [18] [17]
Свободные и связанные переменные
Говорят, что оператор абстракции λ связывает свою переменную везде, где она встречается в теле абстракции. Переменные, попадающие в область действия абстракции, называются связанными . В выражении λ x . М , то часть λ х часто называют связующее , как намек , что переменное й становится связанным с добавлением λ х к М . Все остальные переменные называются свободными . Например, в выражении λ y . xxy , y - связанная переменная, а x - свободная переменная. Также переменная привязана к ближайшей абстракции. В следующем примере единственное вхождение x в выражение связано со второй лямбдой: λ x . у (λ х . zx ).
Набор свободных переменных лямбда-выражения M обозначается как FV ( M ) и определяется рекурсией по структуре терминов следующим образом:
- FV ( x ) = { x }, где x - переменная.
- FV (λ x . M ) = FV ( M ) \ { x }.
- FV ( MN ) = FV ( M ) ∪ FV ( N ). [19]
Выражение, не содержащее свободных переменных, называется закрытым . Замкнутые лямбда-выражения также известны как комбинаторы и эквивалентны терминам комбинаторной логики .
Снижение
Значение лямбда-выражений определяется тем, как выражения могут быть сокращены. [20]
Есть три вида сокращения:
- α-преобразование : изменение связанных переменных;
- β-редукция : применение функций к их аргументам;
- η-редукция : захватывает понятие протяженности.
Мы также говорим о результирующих эквивалентностях: два выражения являются α-эквивалентными , если их можно α-преобразовать в одно и то же выражение. Аналогично определяются β-эквивалентность и η-эквивалентность.
Термин « редекс» , сокращение от сокращаемого выражения , относится к подтерминам, которые могут быть сокращены с помощью одного из правил сокращения. Так , например, (λ х . М ) Н является β-REDEX в выражении о замене N для й в М . Выражение, к которому сводится редекс, называется его редукцией ; редукция (λ x . M ) N есть M [ x : = N ].
Если x не свободен в M , λ x . М х также η-REDEX, с редуктом М .
α-преобразование
α-преобразование, иногда известное как α-переименование [21], позволяет изменять имена связанных переменных. Например, α-преобразование λ x . x может дать λ y . у . Термины, отличающиеся только α-преобразованием, называются α-эквивалентными . Часто при использовании лямбда-исчисления α-эквивалентные термины считаются эквивалентными.
Точные правила α-преобразования не совсем тривиальны. Во-первых, при α-преобразовании абстракции переименовываются только вхождения переменных, которые связаны с той же абстракцией. Например, α-преобразование λ x .λ x . x может привести к λ y .λ x . х , но это может не привести к λ у .λ х . у . Последний имеет значение, отличное от оригинала. Это аналогично программному понятию затенения переменных .
Во-вторых, α-преобразование невозможно, если оно приведет к захвату переменной другой абстракцией. Например, если мы заменим x на y в λ x .λ y . x , получаем λ y .λ y . y , что совсем не одно и то же.
В языках программирования со статической областью видимости α-преобразование может использоваться для упрощения разрешения имен , гарантируя, что никакое имя переменной не маскирует имя в содержащей области (см. Α-переименование, чтобы сделать разрешение имен тривиальным ).
В обозначении индекса Де Брёйна любые два α-эквивалентных термина синтаксически идентичны.
Замена
Замена, написанный М [ V : = N ], представляет собой процесс замены всех свободных вхождений переменной V в выражении М с выражением N . Подстановка терминов лямбда-исчисления определяется рекурсией по структуре терминов следующим образом (примечание: x и y - только переменные, а M и N - любое лямбда-выражение):
- x [ x : = N ] = N
- y [ x : = N ] = y , если x ≠ y
- ( M 1 M 2 ) [ x : = N ] = ( M 1 [ x : = N ]) ( M 2 [ x : = N ])
- (λ x . M ) [ x : = N ] = λ x . M
- (λ y . M ) [ x : = N ] = λ y . ( M [ x : = N ]), если x ≠ y и y ∉ FV ( N )
Чтобы заменить абстракцию, иногда необходимо α-преобразовать выражение. Например, неверно для (λ x . Y ) [ y : = x ] приводить к λ x . x , потому что замененный x должен был быть свободным, но в итоге оказался связанным. Правильная подстановка в этом случае - λ z . x , с точностью до α-эквивалентности. Подстановка определяется однозначно с точностью до α-эквивалентности.
β-редукция
β-редукция отражает идею применения функции. β-восстановительный определяется в терминах Замена: β-восстановительный (λ V . M ) N является М [ V : = N ].
Например, предполагая некоторую кодировку 2, 7, ×, мы имеем следующую β-редукцию: (λ n . N × 2) 7 → 7 × 2.
β-редукция может рассматриваться как то же самое, что и концепция локальной сводимости в естественной дедукции , через изоморфизм Карри – Ховарда .
η-редукция
η-редукция выражает идею протяженности , которая в данном контексте состоит в том, что две функции одинаковы тогда и только тогда, когда они дают одинаковый результат для всех аргументов. η-редукция преобразует λ x . f x и f всякий раз, когда x не появляется свободным в f .
Можно увидеть, что η-редукция совпадает с концепцией локальной полноты в естественной дедукции через изоморфизм Карри – Ховарда .
Нормальные формы и слияние
Для нетипизированного лямбда-исчисления β-редукция как правило переписывания не является ни строго нормализующим, ни слабо нормализующим .
Однако можно показать, что β-восстановление сливается при работе до α-преобразования (т. Е. Мы считаем две нормальные формы равными, если возможно α-преобразовать одну в другую).
Следовательно, как сильно нормализующие члены, так и слабо нормализующие члены имеют единственную нормальную форму. Для строго нормализующих членов любая стратегия редукции гарантированно дает нормальную форму, тогда как для слабо нормализующих членов некоторые стратегии редукции могут не найти ее.
Кодирование типов данных
Базовое лямбда-исчисление может использоваться для моделирования логических значений, арифметики , структур данных и рекурсии, как показано в следующих подразделах.
Арифметика в лямбда-исчислении
Существует несколько возможных способов определения натуральных чисел в лямбда-исчислении, но наиболее распространенными являются числа Чёрча , которые можно определить следующим образом:
- 0: = λ f. Λ x . Икс
- 1: = λ f. Λ x . f x
- 2: = λ f. Λ x . f ( f x )
- 3: = λ f. Λ x . f ( f ( f x ))
и так далее. Или используя альтернативный синтаксис, представленный выше в Обозначении :
- 0: = λ fx . Икс
- 1: = λ fx . f x
- 2: = λ fx . f ( f x )
- 3: = λ fx . f ( f ( f x ))
Числительное Чёрча - это функция высшего порядка, она принимает функцию с одним аргументом. f и возвращает другую функцию с одним аргументом. Церковная цифра n - функция, которая принимает функцию f в качестве аргумента и возвращает n -я композиция f , т.е. функция f составлен сам с собой п раз. Это обозначается f ( n ) и фактически является n -я степень f (рассматривается как оператор); f (0) определяется как функция идентичности. Такие повторяющиеся композиции (одной функции е ) подчиняются законам экспонент , поэтому эти числа можно использовать в арифметике. (В исходном лямбда-исчислении Черча формальный параметр лямбда-выражения должен был встречаться хотя бы один раз в теле функции, что сделало приведенное выше определение 0 невозможно.)
Один из способов думать о церковной цифре n , которое часто бывает полезно при анализе программ, представляет собой инструкцию «повторить n раз». Например, используя ПАРА и Функции NIL, определенные ниже, можно определить функцию, которая создает (связанный) список из n элементов, все равные x , повторяя «добавить еще один элемент x » n раз, начиная с пустого списка. Лямбда-член
- λ п .λ х . n (PAIR x ) NIL
Изменяя то, что повторяется, и варьируя аргумент, к которому применяется эта повторяющаяся функция, можно достичь множества различных эффектов.
Мы можем определить функцию-преемник, которая принимает числительное Чёрча п и возвращается n + 1 , добавив еще одно приложение f , где '(mf) x' означает, что функция 'f' применяется m раз к 'x':
- SUCC: = λ n .λ f .λ x . f ( n f x )
Поскольку m -й состав f составлен с n -я композиция f дает m + n -я композиция f , сложение можно определить следующим образом:
- ПЛЮС: = λ m .λ n .λ f .λ x . м ж ( п е х )
PLUS можно рассматривать как функцию, принимающую в качестве аргументов два натуральных числа и возвращающую натуральное число; можно проверить, что
- PLUS 2 3
а также
- 5
являются β-эквивалентными лямбда-выражениями. С момента добавления м до ряда n можно получить, добавив 1 m раз альтернативное определение:
- PLUS: = λ m. Λ n . m SUCC n [22]
Точно так же умножение можно определить как
- MULT: = λ m .λ n .λ f . m ( n f ) [18]
Альтернативно
- МУЛЬТ: = λ m. Λ n . м (ПЛЮС n ) 0
с момента умножения м и n то же самое, что и повторение добавления функция nm раз, а затем применяя его к нулю. Возведение в степень выражается довольно просто в числах Чёрча, а именно:
- POW: = λ b. Λ e . e b [19]
Функция-предшественник, определяемая PRED n = n - 1 для положительного целого числа п и PRED 0 = 0 значительно сложнее. Формула
- PRED: = λ n .λ f .λ x . н (λ г .λ ч . ч ( г е )) (λ ц . х ) (λ U . U )
можно проверить, индуктивно показав, что если T обозначает (λ g .λ h . h ( g f )) , то T ( n ) (λ u . X ) = (λ h . H ( f ( n −1) ( x ))) для п > 0 . Два других определения Ниже приведены PRED , в одном из которых используются условные выражения , а в другом - пары . С функцией-предшественником вычитание выполняется просто. Определение
- SUB: = λ m. Λ n . n ПРЕД м ,
SUB m n урожайности м - п когда m > n и 0 в противном случае.
Логика и предикаты
По соглашению для логических значений используются следующие два определения (известные как логические значения Черча). ИСТИНА и ЛОЖЬ :
- ИСТИНА: = λ x .λ y . Икс
- НЕВЕРНО : = λ x .λ y . у
- (Обратите внимание, что ЛОЖЬ эквивалентно нулю Черча, определенному выше)
Затем с помощью этих двух лямбда-терминов мы можем определить некоторые логические операторы (это всего лишь возможные формулировки; другие выражения также верны):
- И: = λ p .λ q . p q p
- ИЛИ: = λ p. Λ q . p p q
- НЕ: = λ p . p ЛОЖЬ ИСТИНА
- IFTHENELSE: = λ p .λ a .λ b . п а б
Теперь мы можем вычислять некоторые логические функции, например:
- И ИСТИННАЯ ЛОЖЬ
- ≡ (λ p. Λ q . P q p ) ИСТИНА ЛОЖЬ → β ИСТИНА ЛОЖЬ ИСТИНА
- ≡ (λ x .λ y . X ) ЛОЖНО ИСТИНА → β ЛОЖНО
и мы видим, что И ИСТИНА ЛОЖЬ эквивалентно ЛОЖЬ .
Предикат является функцией , которая возвращает логическое значение. Самый фундаментальный предикат - это ISZERO , который возвращает ИСТИНА, если аргумент - цифра Чёрча 0 и ЛОЖЬ, если его аргумент - любое другое число Чёрча:
- ISZERO: = λ n . n (λ x .FALSE) ИСТИНА
Следующий предикат проверяет, меньше ли первый аргумент второму или равен ему:
- LEQ: = λ m. Λ n .ISZERO (SUB m n ) ,
и с тех пор m = n , если LEQ m n и LEQ n m , легко построить предикат для числового равенства.
Доступность предикатов и приведенное выше определение ИСТИНА и FALSE позволяет писать выражения типа «если-то-еще» в лямбда-исчислении. Например, функцию-предшественницу можно определить как:
- PRED: = λ n . п (λ г .λ к .ISZERO ( г 1) к (плюс ( г к ) 1)) (λ v 0,0) 0
что можно проверить, индуктивно показав, что п (λ г .λ к .ISZERO ( г 1) к (плюс ( г к ) 1)) (λ v 0,0) является дополнением n - 1 функция для п > 0.
Пары
Пару (2-кортеж) можно определить в терминах ИСТИНА и ЛОЖЬ , используя кодировку Чёрча для пар . Например, PAIR инкапсулирует пару ( х , у ), FIRST возвращает первый элемент пары, а СЕКУНДА возвращает вторую.
- ПАРА: = λ x .λ y .λ f . f x y
- ПЕРВЫЙ: = λ p . p ИСТИНА
- ВТОРОЙ: = λ p . p ЛОЖЬ
- NIL: = λ x .TRUE
- NULL: = λ p . p (λ x .λ y. ЛОЖНО)
Связанный список может быть определен либо как NIL для пустого списка, либо как ПАРА элемента и меньшего списка. Предикат NULL проверяет значение НЕТ . (В качестве альтернативы, с NIL: = FALSE , конструкция l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil) устраняет необходимость в явном NULL-тесте).
В качестве примера использования пар функция сдвига и приращения, отображающая ( m , n ) к ( n , n + 1) можно определить как
- Φ: = λ x .PAIR (ВТОРОЙ x ) (SUCC (ВТОРОЙ x ))
что позволяет нам дать, пожалуй, наиболее прозрачную версию функции-предшественника:
- PRED: = λ n. ПЕРВЫЙ ( n Φ (PAIR 0 0)).
Дополнительные техники программирования
Существует множество идиом программирования для лямбда-исчисления. Многие из них были первоначально разработаны в контексте использования лямбда-исчисления в качестве основы для семантики языка программирования , эффективно используя лямбда-исчисление как язык программирования низкого уровня . Поскольку несколько языков программирования включают лямбда-исчисление (или что-то очень похожее) в качестве фрагмента, эти методы также находят применение в практическом программировании, но затем могут восприниматься как непонятные или чужеродные.
Именованные константы
В лямбда-исчислении библиотека могла бы иметь форму набора ранее определенных функций, которые в качестве лямбда-терминов являются просто частными константами. Чистое лямбда-исчисление не имеет концепции именованных констант, поскольку все атомарные лямбда-термины являются переменными, но можно имитировать именованные константы, установив переменную в качестве имени константы, используя абстракцию для привязки этой переменной в основном теле. , и примените эту абстракцию к предполагаемому определению. Таким образом, чтобы использовать f означает M (некоторый явный лямбда-член) в N (другой лямбда-член, «основная программа»), можно сказать
- (λ ф . N) M
Авторы часто вводят синтаксический сахар , например пусть , чтобы можно было писать вышеизложенное в более интуитивном порядке
- пусть f = Mв N
Объединив такие определения, можно написать «программу» лямбда-исчисления как ноль или более определений функций, за которыми следует один лямбда-член, использующий те функции, которые составляют основную часть программы.
Заметное ограничение этого пусть это имя f не определен в M , так как M находится вне области привязки абстракции f ; это означает, что определение рекурсивной функции не может использоваться как M с пусть . Более продвинутый Синтаксическая сахарная конструкция letrec, которая позволяет писать определения рекурсивных функций в этом наивном стиле, вместо этого дополнительно использует комбинаторы с фиксированной точкой.
Рекурсия и фиксированные точки
Рекурсия - это определение функции с помощью самой функции. Лямбда-исчисление не может выразить это так же прямо, как некоторые другие обозначения: все функции в лямбда-исчислении анонимны, поэтому мы не можем ссылаться на значение, которое еще не определено, внутри лямбда-члена, определяющего то же значение. Однако рекурсию по-прежнему можно достичь, настроив лямбда-выражение для получения самого себя в качестве значения аргумента, например, в (λ х . х х ) Е .
Рассмотрим факториальную функцию F ( n ) рекурсивно определяется как
- F ( n ) = 1, если n = 0; иначе n × F ( n - 1) .
В лямбда-выражении, которое должно представлять эту функцию, предполагается, что параметр (обычно первый) принимает само лямбда-выражение в качестве своего значения, так что его вызов - применение его к аргументу - приведет к рекурсии. Таким образом, для достижения рекурсии аргумент, предполагаемый как самореференция (называемый r здесь) всегда должен передаваться самому себе в теле функции в точке вызова:
- G: = λ r . λ n . (1, если n = 0; иначе n × ( r r ( n −1)))
- с участием r r x = F x = G r x , поэтому {{{1}}} и
- F: = GG = (λ x . X x ) G
Самоприложение выполняет здесь репликацию, передавая лямбда-выражение функции следующему вызову в качестве значения аргумента, делая его доступным для ссылки и вызова.
Это решает проблему, но требует перезаписи каждого рекурсивного вызова как самостоятельного приложения. Мы хотели бы иметь общее решение без необходимости переписывать:
- G: = λ r . λ n . (1, если n = 0; иначе n × ( r ( n −1)))
- с участием r x = F x = G r x , поэтому r = G r =: FIX G и
- F: = FIX G где FIX g : = ( r, где r = g r ) = g (FIX g )
- чтобы FIX G = G (FIX G) = (λ n . (1, если n = 0; иначе n × ((FIX G) ( n −1))))
Учитывая лямбда-член с первым аргументом, представляющим рекурсивный вызов (например, G здесь) комбинатор неподвижной точкиFIX вернет самовоспроизводящееся лямбда-выражение, представляющее рекурсивную функцию (здесь F ). Функция не нуждается в явной передаче самой себе в любой момент, поскольку саморепликация организована заранее, когда она создается, чтобы выполняться каждый раз при ее вызове. Таким образом, исходное лямбда-выражение (FIX G) воссоздается внутри себя, в точке вызова, достигая самоотнесения .
На самом деле существует множество возможных определений этого Оператор FIX , самый простой из которых:
- Y : = λ g . (Λ x . G ( x x )) (λ x . G ( x x ))
В лямбда-исчислении Y g - неподвижная точка g , когда он расширяется до:
- Г г
- (λ h . (λ x . h ( x x )) (λ x . h ( x x ))) g
- (λ x . g ( x x )) (λ x . g ( x x ))
- g ((λ x . g ( x x )) (λ x . g ( x x )))
- г ( У г )
Теперь, чтобы выполнить рекурсивный вызов функции факториала, мы просто вызовем ( Y G) n , где n - это число, для которого мы вычисляем факториал. При п = 4, например, это дает:
- ( Y G) 4
- Г ( Г Г) 4
- (λ r .λ n . (1, если n = 0; иначе n × ( r ( n −1)))) ( Y G) 4
- (λ n . (1, если n = 0; иначе n × (( Y G) ( n −1)))) 4
- 1, если 4 = 0; иначе 4 × (( Y G) (4−1))
- 4 × (G ( Y G) (4-1))
- 4 × ((λ n . (1, если n = 0; иначе n × (( Y G) ( n −1)))) (4−1))
- 4 × (1, если 3 = 0; иначе 3 × (( Y G) (3−1)))
- 4 × (3 × (G ( Y G) (3−1)))
- 4 × (3 × ((λ n . (1, если n = 0; иначе n × (( Y G) ( n −1)))) (3−1)))
- 4 × (3 × (1, если 2 = 0; иначе 2 × (( Y G) (2−1))))
- 4 × (3 × (2 × (G ( Y G) (2−1))))
- 4 × (3 × (2 × ((λ n . (1, если n = 0; иначе n × (( Y G) ( n −1)))) (2−1))))
- 4 × (3 × (2 × (1, если 1 = 0; иначе 1 × (( Y G) (1−1)))))
- 4 × (3 × (2 × (1 × (G ( Y G) (1−1)))))
- 4 × (3 × (2 × (1 × ((λ n . (1, если n = 0; иначе n × (( Y G) ( n −1)))) (1−1)))))
- 4 × (3 × (2 × (1 × (1, если 0 = 0; иначе 0 × (( Y G) (0−1))))))
- 4 × (3 × (2 × (1 × (1))))
- 24
Каждую рекурсивно определенную функцию можно рассматривать как фиксированную точку некоторой подходящим образом определенной функции, закрывающейся по рекурсивному вызову с дополнительным аргументом, и, следовательно, с использованием Y каждая рекурсивно определенная функция может быть выражена как лямбда-выражение. В частности, теперь мы можем четко определить предикат вычитания, умножения и сравнения натуральных чисел рекурсивно.
Стандартные условия
У некоторых терминов есть общепринятые названия: [ необходима ссылка ]
- I : = λ x . Икс
- K : = λ x. Λ y . Икс
- S : = λ x. Λ y. Λ z . х г ( у г )
- B : = λ x. Λ y. Λ z . х ( у z )
- C : = λ x. Λ y. Λ z . х г у
- W : = λ x. Λ y . x y y
- U : = λ x . х х
- ω : = λ x . х х
- Ω : = ω ω
- Y : = λ g . (Λ x . G ( x x )) (λ x . G ( x x ))
Некоторые из них имеют прямое применение в устранении абстракции, которая превращает лямбда-члены в термины комбинаторного исчисления .
Устранение абстракции
Если N - лямбда-член без абстракции, но, возможно, содержащий именованные константы ( комбинаторы ), то существует лямбда-член T ( x , N ), что эквивалентно λ х . N, но в нем отсутствует абстракция (кроме как части именованных констант, если они считаются неатомарными). Это также можно рассматривать как анонимизирующие переменные, так как T ( x , N ) удаляет все вхождения x из N , при этом позволяя подставлять значения аргументов в позиции, где N содержит х . Функция преобразования T может быть определена следующим образом:
- Т ( х , х ): = I
- Т ( x , N ): = K N, если х не свободен в N .
- Т ( x , M N ): = S T ( х , М ) Т ( х , N )
В любом случае член вида T ( x , N ) P можно уменьшить, если начальный комбинатор I , K или S захватит аргумент P , точно так же, как β-редукция (λ x . N) P подойдет. Я возвращаю этот аргумент. K отбрасывает аргумент, как и (λ x . N) подойдет, если х не имеет свободное вхождение в N . S передает аргумент обоим подтермам приложения, а затем применяет результат первого к результату второго.
Комбинаторы B и C аналогичны S , но передают аргумент только одному подтерму приложения ( B к подтерму «аргумент» и C к подтерму «функция»), таким образом сохраняя последующий K, если нет вхождения из x за один субтерм. По сравнению с B и C , то S комбинатор фактически смешивает две функциональные: переставляя аргументы, и дублировать аргументтак что он может быть использован в двух местах. Вт комбинатор делает только последним, получая B, C, K, W систему в качестве альтернативы SKI комбинатора исчисления .
Типизированное лямбда-исчисление
Типизированного лямбда - исчисление является типизированным формализм , который использует лямбда-символ () для обозначения абстракции анонимной функции. В этом контексте типы обычно являются объектами синтаксического характера, которые присваиваются лямбда-терминам; точная природа типа зависит от рассматриваемого исчисления (см. Виды типизированных лямбда-исчислений ). С определенной точки зрения типизированные лямбда-исчисления можно рассматривать как уточнения нетипизированного лямбда-исчисления, но с другой точки зрения их также можно рассматривать как более фундаментальную теорию, а нетипизированное лямбда-исчисление - как частный случай только с одним типом. [23]
Типизированные лямбда-исчисления являются основополагающими языками программирования и составляют основу типизированных функциональных языков программирования, таких как ML и Haskell, и, что более косвенно, типизированных императивных языков программирования . Типизированные лямбда-исчисления играют важную роль в разработке систем типов для языков программирования; здесь типизируемость обычно фиксирует желаемые свойства программы, например, программа не вызовет нарушения доступа к памяти.
Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри – Ховарда, и их можно рассматривать как внутренний язык классов категорий , например, просто типизированное лямбда-исчисление является языком декартовых замкнутых категорий (CCC).
Вычислимые функции и лямбда-исчисление
Функция натуральных чисел F : N → N является вычислимой тогда и только тогда, когда существует лямбда-выражение f такое, что для каждой пары x , y в N , F ( x ) = y тогда и только тогда, когда fх = β y , где х и y - числа Чёрча, соответствующие x и y , соответственно, а = β означает эквивалентность с β-редукцией. Это один из многих способов определения вычислимости; см. тезис Черча – Тьюринга для обсуждения других подходов и их эквивалентности.
Неразрешимость эквивалентности
Не существует алгоритма, который принимает на вход любые два лямбда-выражения и выходные данные. ИСТИНА или ЛОЖЬ в зависимости от того, эквивалентны ли два выражения. [10] Точнее, никакая вычислимая функция не может определить эквивалентность. Исторически это была первая проблема, неразрешимость которой могла быть доказана. Как обычно для такого доказательства, вычислимость означает вычислимость с помощью любой модели вычислений , полной по Тьюрингу .
Доказательство Черча сначала сводит проблему к определению, имеет ли данное лямбда-выражение нормальную форму . Нормальная форма - это эквивалентное выражение, которое не может быть сокращено в соответствии с правилами, налагаемыми формой. Затем он предполагает, что этот предикат вычислим и, следовательно, может быть выражен в лямбда-исчислении. Основываясь на более ранней работе Клини и создавая нумерацию Гёделя для лямбда-выражений, он конструирует лямбда-выражение e, который следует за доказательством первой теоремы Гёделя о неполноте . Если e применяется к своему собственному числу Гёделя, получаем противоречие.
Лямбда-исчисление и языки программирования
Как указано в статье Питера Ландина 1965 года «Соответствие между АЛГОЛОМ 60 и лямбда-нотацией Черча» [24], последовательные процедурные языки программирования можно понимать в терминах лямбда-исчисления, которое обеспечивает основные механизмы процедурной абстракции и процедуры. (подпрограмма) приложение.
Анонимные функции
Например, в Лиспе "квадратная" функция может быть выражена как лямбда-выражение следующим образом:
( лямбда ( х ) ( * х х ))
Приведенный выше пример представляет собой выражение, оценивающее функцию первого класса. Символ lambda
создает анонимную функцию, учитывая список имен параметров, (x)
- только один аргумент в этом случае, и выражение , которое оценивается как тело функции, (* x x)
. Анонимные функции иногда называют лямбда-выражениями.
Например, Паскаль и многие другие императивные языки давно поддерживают передачу подпрограмм в качестве аргументов другим подпрограммам через механизм указателей на функции . Однако указатели на функции не являются достаточным условием для того, чтобы функции были типами данных первого класса , потому что функция является типом данных первого класса тогда и только тогда, когда новые экземпляры функции могут быть созданы во время выполнения. И это создание функций во время выполнения поддерживается, в частности , в Smalltalk , JavaScript и Wolfram Language , а в последнее время в Scala , Eiffel («агенты»), C # («делегаты») и C ++ 11 .
Стратегии сокращения
Является ли термин нормализующим или нет, и сколько работы необходимо сделать для его нормализации, если это так, в значительной степени зависит от используемой стратегии сокращения. Различие между стратегиями сокращения связано с различием в языках функционального программирования между активным вычислением и ленивым вычислением .
- Полные β-редукции
- Любой редекс можно уменьшить в любой момент. По сути, это означает отсутствие какой-либо конкретной стратегии сокращения - что касается сводимости, «все ставки отключены».
- Заявочный порядок
- Самый левый, самый внутренний редекс всегда уменьшается первым. Интуитивно это означает, что аргументы функции всегда сокращаются перед самой функцией. Аппликативный порядок всегда пытается применить функции к нормальным формам, даже если это невозможно.
- Большинство языков программирования (включая Lisp, ML и императивные языки, такие как C и Java ) описываются как «строгие», что означает, что функции, применяемые к ненормализующим аргументам, не являются нормализующими. По сути, это делается с использованием аппликативного порядка, сокращение от вызова к значению ( см. Ниже ), но обычно это называется «нетерпеливой оценкой».
- Нормальный порядок
- Самый левый, крайний редекс всегда уменьшается первым. То есть, когда это возможно, аргументы подставляются в тело абстракции до того, как аргументы будут сокращены.
- Звоните по цене
- Уменьшаются только крайние редексы: редекс уменьшается только тогда, когда его правая часть уменьшена до значения (переменной или абстракции).
- Звоните по имени
- В обычном порядке, но внутри абстракций сокращения не выполняются. Например, λ x . (λ x . x ) x находится в нормальной форме в соответствии с этой стратегией, хотя содержит редекс (λ х . х ) х .
- Звоните по необходимости
- В обычном порядке, но приложения-функции, которые будут дублировать термины, вместо этого называют аргумент, который затем сокращается только «тогда, когда это необходимо». В практическом контексте называется «ленивым оцениванием». В реализации этого «название» принимает форму указателя, с Redex , представленным в стуке .
Аппликативный порядок - это не нормализующая стратегия. Обычный контрпример выглядит следующим образом: определить Ω = ωω, где ω = λ x . хх . Все это выражение содержит только один редекс, а именно все выражение; его редукция снова Ω . Поскольку это единственное доступное сокращение, Ω не имеет нормальной формы (при любой стратегии оценки). Используя аппликативный порядок, выражение KIΩ = (λ x .λ y . X ) (λ x . X ) Ω сокращается сначала приведением Ω к нормальной форме (так как это крайний правый редекс), но поскольку Ω не имеет нормальной формы, аппликативный порядок не может найти нормальную форму для KIΩ .
Напротив, нормальный порядок называется так, потому что он всегда находит нормализующее сокращение, если оно существует. В приведенном выше примере KIΩ при нормальном порядке сводится к I , нормальной форме. Недостатком является то, что редексы в аргументах могут быть скопированы, что приведет к дублированию вычислений (например, (λ x . xx ) ((λ x . x ) y ) сводится к ((λ x . x ) y ) ((λ x . x ) y ) с использованием этой стратегии; теперь есть два редекса, поэтому для полной оценки требуется еще два шага, но если бы аргумент был уменьшен первым, теперь не было бы ни одного).
Положительный компромисс использования аппликативного порядка заключается в том, что он не вызывает ненужных вычислений, если используются все аргументы, потому что он никогда не заменяет аргументы, содержащие редексы, и, следовательно, никогда не нужно их копировать (что может дублировать работу). В приведенном выше примере в аппликативном порядке (λ x . xx ) ((λ x . x ) y ) сначала сводится к (λ x . xx ) y, а затем в нормальный порядок yy , делая два шага вместо трех.
Большинство чисто функциональных языков программирования (особенно Miranda и его потомки, включая Haskell) и языки доказательства программ доказательства теорем используют ленивое вычисление , которое по сути то же самое, что и вызов по необходимости. Это похоже на обычное сокращение порядка, но при вызове по необходимости удается избежать дублирования работы, присущего нормальному уменьшению порядка с использованием совместного использования . В приведенном выше примере (λ x . xx ) ((λ x . x ) y ) сводится к ((λ x . x ) y ) ((λ x . x ) y ) , который имеет два редекса, но при вызове по необходимости они представляются с использованием одного и того же объекта, а не копируются, поэтому, когда один сокращается, другой тоже.
Замечание о сложности
Хотя идея β-редукции кажется достаточно простой, это не атомарный шаг, поскольку он должен иметь нетривиальную стоимость при оценке вычислительной сложности . [25] Чтобы быть точным, нужно каким-то образом найти расположение всех вхождений связанной переменной V в выражении E , подразумевая временные затраты, или нужно каким-то образом отслеживать эти местоположения, подразумевая затраты на пространство. Наивный поиск локаций V в Е представляет О ( п ) в длину п из E . Это привело к изучению систем, использующих явную замену . Управляющие строки Sinot [26] позволяют отслеживать расположение свободных переменных в выражениях.
Параллелизм и параллелизм
Свойство Чёрча – Россера лямбда-исчисления означает, что вычисление (β-редукция) может выполняться в любом порядке , даже параллельно. Это означает, что актуальны различные недетерминированные стратегии оценки . Однако лямбда-исчисление не предлагает никаких явных конструкций для параллелизма . В лямбда-исчисление можно добавить такие конструкции, как Futures . Для описания взаимодействия и параллелизма были разработаны другие вычисления процессов .
Оптимальное сокращение
В статье Леви 1988 г. « Совместное использование при оценке лямбда-выражений » он определяет понятие оптимального совместного использования, при котором работа не дублируется . Например, выполнение β-восстановления в нормальном порядке на (λ x . xx ) (II) сводит его к II (II) . Аргумент II дублируется приложением к первому лямбда-члену. Если сокращение сначала было выполнено в аппликативном порядке, мы сохраняем работу, потому что работа не дублируется: (λ x . xx ) (II) сводится к (λ х . хх ) I . С другой стороны, использование аппликативного порядка может привести к избыточным сокращениям или даже, возможно, никогда не привести к нормальной форме. Например, выполнение β-восстановления в нормальном порядке на (λ f .f I) (λy. (λ x . xx ) (y I)) дает (λy. (λ x . xx ) (y I)) I , (λ x . xx ) (II), которую, как мы знаем, можно сделать без дублирования работы. То же самое, но в прикладном порядке дает (λ f .f I) (λy.y I (y I)) , (λy.y I (y I)) I , II (II) , и теперь работа дублируется.
Леви показывает существование лямбда-терминов, в которых не существует последовательности сокращений, которая сокращает их без дублирования работы. Приведенный ниже лямбда-член является таким примером.
((λg. (g (g (λx.x)))) (λh. ((λf. (f (f (λz.z)))) (λw. (h (w (λy.y)))) )))
Он состоит из трех одинаковых терминов: x = ((λg. ...) (λh.y)) и y = ((λf. ...) (λw.z)) , и, наконец, z = λw. (h (w (λy.y))) . Здесь можно сделать только две возможные β-редукции: по x и по y. Уменьшение внешнего члена x сначала приводит к дублированию внутреннего члена y, и каждая копия должна быть уменьшена, но уменьшение сначала внутреннего члена y будет дублировать его аргумент z, что приведет к дублированию работы, когда значения h и w становятся известными. Между прочим, этот член сводится к тождественной функции (λy.y) , и создается путем создания оберток, которые делают функцию идентификации доступной для связывателей. g = λh ... , f = λw ... , h = λx.x (сначала) и w = λz.z (сначала), все из которых применяются к самому внутреннему члену λy.y .
Точное представление о дублировании работы основывается на замечании того, что после первого сокращения II сделано, ценность другого II можно определить, потому что они имеют одинаковую структуру (и фактически имеют одинаковые значения) и являются результатом общего предка. Каждой такой похожей структуре можно присвоить метку, которую можно отслеживать при сокращении. Если имя присвоено редексу, который производит все результирующие II , а затем все повторяющиеся вхождения II можно отследить и уменьшить за один раз. Однако не очевидно, что редекс приведет к II семестр. Выявление структур, которые похожи в разных частях лямбда-члена, может включать сложный алгоритм и, возможно, иметь сложность, равную истории самого сокращения.
Хотя Леви определяет понятие оптимального совместного использования, он не предлагает алгоритма для этого. В статье Винсента ван Острома, Кеса-Яна ван де Лойя и Марийн Цвицерлоуд «Лямбдаскоп: еще одна оптимальная реализация лямбда-исчисления» они предоставляют такой алгоритм, преобразуя лямбда-члены в сети взаимодействия , которые затем сокращаются. Грубо говоря, результирующее сокращение является оптимальным, потому что каждый член, который будет иметь те же метки, что и в статье Леви, также будет тем же графом в сети взаимодействий. В документе они упоминают, что их прототипная реализация Lambdascope работает так же, как и оптимизированная версия эталонной оптимальной машины более высокого порядка BOHM. [b]
Семантика
Тот факт, что термы лямбда-исчисления действуют как функции на других термах лямбда-исчисления и даже на самих себя, привел к вопросам о семантике лямбда-исчисления. Можно ли придать разумное значение терминам лямбда-исчисления? Естественная семантика заключалась в том, чтобы найти множество D, изоморфное функциональному пространству D → D , функций на самом себе. Однако такой нетривиальный D не может существовать из-за ограничений мощности, потому что набор всех функций от D до D имеет большую мощность, чем D , если D не является одноэлементным набором .
В 1970-х Дана Скотт показала, что, если бы рассматривались только непрерывные функции, можно было бы найти набор или область D с требуемым свойством, тем самым предоставив модель лямбда-исчисления.
Эта работа также легла в основу денотационной семантики языков программирования.
Варианты и расширения
Эти расширения находятся в лямбда-кубе :
- Типизированное лямбда-исчисление - лямбда-исчисление с типизированными переменными (и функциями)
- Система F - типизированное лямбда-исчисление с переменными типа
- Исчисление конструкций - типизированное лямбда-исчисление с типами как первоклассными значениями.
Эти формальные системы являются расширениями лямбда-исчисления, которых нет в лямбда-кубе:
- Двоичное лямбда-исчисление - версия лямбда-исчисления с двоичным вводом-выводом, двоичным кодированием терминов и назначенной универсальной машиной.
- Лямбда-мю исчисление - расширение лямбда-исчисления для лечения классической логики
Эти формальные системы представляют собой разновидности лямбда-исчисления:
- Исчисление Каппа - аналог первого порядка лямбда-исчисления
Эти формальные системы связаны с лямбда-исчислением:
- Комбинаторная логика - обозначение математической логики без переменных
- Комбинаторное исчисление SKI - вычислительная система, основанная на комбинаторах S , K и I , эквивалентная лямбда-исчислению, но приводимая без подстановки переменных.
Смотрите также
- Аппликативные вычислительные системы - Обработка объектов в стиле лямбда-исчисления.
- Декартова закрытая категория - настройка лямбда-исчисления в теории категорий
- Категориальная абстрактная машина - модель вычислений, применимая к лямбда-исчислению.
- Изоморфизм Карри – Ховарда - Формальное соответствие между программами и доказательствами
- Индекс Де Брёйна - обозначение, устраняющее неоднозначность альфа-преобразований
- Нотация де Брёйна - нотация с использованием функций модификации постфикса
- Дедуктивное лямбда-исчисление - рассмотрение проблем, связанных с рассмотрением лямбда-исчисления как дедуктивной системы .
- Теория предметной области - Изучение определенных положений, дающих денотационную семантику для лямбда-исчисления.
- Стратегия оценки - Правила оценки выражений в языках программирования
- Явная замена - теория замещения, используемая в β-редукции.
- Функциональное программирование
- Формула Харропа - своего рода конструктивная логическая формула, в которой доказательства являются лямбда-терминами.
- Сети взаимодействия
- Парадокс Клини – Россера - демонстрация непоследовательности некоторой формы лямбда-исчисления.
- Knights of the Lambda Calculus - полу-вымышленная организация хакеров LISP и Scheme.
- Машина Кривина - Абстрактная машина для интерпретации вызова по имени в лямбда-исчислении.
- Определение лямбда-исчисления - Формальное определение лямбда-исчисления.
- Let выражение - выражение, тесно связанное с абстракцией.
- Минимализм (вычисления)
- Переписывание - преобразование формул в формальных системах
- Машина SECD - виртуальная машина, разработанная для лямбда-исчисления.
- Теорема Скотта – Карри - теорема о множествах лямбда-членов
- Поиздеваться над пересмешником - Введение в комбинаторную логику
- Универсальная машина Тьюринга - формальная вычислительная машина, эквивалентная лямбда-исчислению.
- Unlambda - эзотерический функциональный язык программирования, основанный на комбинаторной логике.
Заметки
- ^ Для полной истории см. Кардоне и Хиндли «История лямбда-исчисления и комбинаторной логики» (2006).
- ^ Более подробную информацию можно найти в небольшой статье Об эффективном сокращении лямбда-членов .
Рекомендации
- ↑ Тьюринг, Алан М. (декабрь 1937 г.). «Вычислимость и λ-определимость». Журнал символической логики . 2 (4): 153–163. DOI : 10.2307 / 2268280 . JSTOR 2268280 .
- ^ Кокван, Тьерри . Залта, Эдвард Н. (ред.). «Теория типов» . Стэнфордская энциклопедия философии (издание летом 2013 г.) . Проверено 17 ноября 2020 года .
- ^ Мортгат, Майкл (1988). Категориальные исследования: логические и лингвистические аспекты исчисления Ламбека . Публикации Foris. ISBN 9789067653879.
- ^ Бунт, Гарри; Маскенс, Рейнхард, ред. (2008). Вычислительный смысл . Springer. ISBN 978-1-4020-5957-5.
- ^ Митчелл, Джон С. (2003). Концепции языков программирования . Издательство Кембриджского университета. п. 57. ISBN 978-0-521-78098-8..
- ^ Пирс, Бенджамин С. Основная теория категорий для компьютерных ученых . п. 53.
- ^ Церковь, Алонсо (1932). «Набор постулатов в основу логики». Анналы математики . Series 2. 33 (2): 346–366. DOI : 10.2307 / 1968337 . JSTOR 1968337 .
- ^ Клини, Стивен К .; Россер, Дж. Б. (июль 1935 г.). «Несогласованность некоторых формальных логик». Анналы математики . 36 (3): 630. DOI : 10,2307 / 1968646 . JSTOR 1968646 .
- ^ Церковь, Алонсо (декабрь 1942 г.). "Обзор Хаскелла Б. Карри, Несогласованность некоторых формальных логик ". Журнал символической логики . 7 (4): 170–171. DOI : 10.2307 / 2268117 . JSTOR 2268117 .
- ^ а б Церковь, Алонсо (1936). «Неразрешимая проблема элементарной теории чисел». Американский журнал математики . 58 (2): 345–363. DOI : 10.2307 / 2371045 . JSTOR 2371045 .
- ^ Церковь, Алонсо (1940). «Формулировка простой теории типов». Журнал символической логики . 5 (2): 56–68. DOI : 10.2307 / 2266170 . JSTOR 2266170 .
- ^ Парти, BBH; ter Meulen, A .; Wall, RE (1990). Математические методы в лингвистике . Springer. ISBN 9789027722454. Дата обращения 29 декабря 2016 .
- ^ Альма, Джесси. Залта, Эдвард Н. (ред.). «Лямбда-исчисление» . Стэнфордская энциклопедия философии (издание летом 2013 г.) . Проверено 17 ноября 2020 года .
- ^ Дана Скотт, « Оглядываясь назад; глядя вперед », приглашенный доклад на семинаре в честь 85-летия Даны Скотт и 50-летия теории предметной области, 7–8 июля, FLoC 2018 (выступление 7 июля 2018 г.). Соответствующий отрывок начинается в 32:50 . (См. Также этот отрывок из выступления в мае 2016 г. в Бирмингемском университете, Великобритания.)
- ^ Барендрегт, Хендрик Питер (1984). Лямбда-исчисление: его синтаксис и семантика . Исследования по логике и основам математики. 103 (Пересмотренное изд.). Северная Голландия. ISBN 0-444-87508-5.
- ^ Исправления .
- ^ а б «Пример правил ассоциативности» . Lambda-bound.com . Проверено 18 июня 2012 .
- ^ а б Селинджер, Питер (2008), Конспект лекций по лямбда-исчислению (PDF) , 0804 , Департамент математики и статистики, Университет Оттавы, стр. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S
- ^ а б Барендрегт, Хенк ; Барендсен, Эрик (март 2000 г.), Введение в лямбда-исчисление (PDF)
- ^ де Кейруш, Руй Дж.Б. (1988). "Теоретико-доказательственное рассмотрение программирования и роль правил редукции". Диалектика . 42 (4): 265–282. DOI : 10.1111 / j.1746-8361.1988.tb00919.x .
- ^ Турбак, Франклин; Гиффорд, Дэвид (2008), Концепции дизайна в языках программирования , MIT Press, стр. 251, ISBN 978-0-262-20175-9
- ^ Фелляйзен, Матиас; Флатт, Мэтью (2006), Языки программирования и лямбда-исчисления (PDF) , стр. 26, архивировано из оригинального (PDF) 05.02.2009; Примечание (по состоянию на 2017 г.) в исходном местоположении предполагает, что авторы считают работу, на которую первоначально ссылались, замененной книгой.
- ^ Типы и языки программирования, стр. 273, Бенджамин К. Пирс
- ^ Ландин, П.Дж. (1965). «Соответствие АЛГОЛА 60 и лямбда-нотации Чёрча». Коммуникации ACM . 8 (2): 89–101. DOI : 10.1145 / 363744.363749 . S2CID 6505810 .
- ^ Статман, Ричард (1979). «Типизированное λ-исчисление не является элементарно рекурсивным» . Теоретическая информатика . 9 (1): 73–81. DOI : 10.1016 / 0304-3975 (79) 90007-0 . ЛВП : 2027,42 / 23535 .
- ^ Синот, Ф.-Р. (2005). «Пересмотренные строки директора: общий подход к эффективному представлению свободных переменных при перезаписи более высокого порядка» . Журнал логики и вычислений . 15 (2): 201–218. DOI : 10,1093 / logcom / exi010 .[ постоянная мертвая ссылка ]
дальнейшее чтение
- Абельсон, Гарольд и Джеральд Джей Сассман. Структура и интерпретация компьютерных программ . MIT Press . ISBN 0-262-51087-1 .
- Хендрик Питер Барендрегт Введение в лямбда-исчисление .
- Хенк Барендрегт , Влияние лямбда-исчисления в логике и информатике . Бюллетень символической логики, том 3, номер 2, июнь 1997 г.
- Барендрегт, Хендрик Питер , Лямбда-исчисление без типов, стр. 1091–1132 Справочника по математической логике , Северная Голландия (1977) ISBN 0-7204-2285-X
- Кардоне и Хиндли, 2006. История лямбда-исчисления и комбинаторной логики . В Габбай и Вудс (ред.), Справочник по истории логики , т. 5. Эльзевир.
- Черч, Алонзо, Неразрешимая проблема элементарной теории чисел , Американский журнал математики , 58 (1936), стр. 345–363. Эта статья содержит доказательство того, что эквивалентность лямбда-выражений, вообще говоря, неразрешима.
- Алонсо Чёрч, Исчисления лямбда-преобразования ( ISBN 978-0-691-08394-0 ) [1]
- Фринк-младший, Оррин, Обзор: исчисления лямбда-преобразования [2]
- Клини, Стивен, Теория натуральных чисел в формальной логике , Американский журнал математики , 57 (1935), стр. 153–173 и 219–244. Содержит определения лямбда-исчисления для нескольких знакомых функций.
- Ландин, Питер , Соответствие между АЛГОЛОМ 60 и лямбда-нотацией Чёрча , Сообщения ACM , т. 8, вып. 2 (1965), страницы 89–101. Доступно на сайте ACM . Классическая статья, подчеркивающая важность лямбда-исчисления как основы для языков программирования.
- Ларсон, Джим, Введение в лямбда-исчисление и схемы . Мягкое введение для программистов.
- Шалк А. и Симмонс Х. (2005) Введение в λ-исчисления и арифметику с приличным набором упражнений . Примечания к курсу магистра математической логики в Манчестерском университете.
- де Кейруш, Руи JGB (2008). "О правилах редукции, использовании смысла и теоретической семантике". Studia Logica . 90 (2): 211–247. DOI : 10.1007 / s11225-008-9150-5 . S2CID 11321602 . Документ, в котором формально обосновывается идея «значение-есть-использование», которая, даже если основана на доказательствах, отличается от теоретико-доказательной семантики, как в традиции Даммета – Правица, поскольку она рассматривает редукцию как правила, придающие смысл.
- Ханкин, Крис, Введение в лямбда-исчисления для компьютерных ученых,ISBN 0954300653
Монографии / учебники для аспирантов:
- Мортен Гейне Соренсен, Павел Уржичин, Лекции по изоморфизму Карри – Ховарда , Elsevier, 2006, ISBN 0-444-52077-5 - это недавняя монография, охватывающая основные темы лямбда-исчисления, от безтипового до наиболее типизированных лямбда-исчислений , включая более свежие разработки, такие как системы чистых типов и лямбда-куб . Он не распространяется на расширения подтипов .
- Пирс, Бенджамин (2002), Типы и языки программирования , MIT Press, ISBN 0-262-16209-1охватывает лямбда-исчисления с точки зрения практической системы типов; некоторые темы, такие как зависимые типы, только упоминаются, но выделение подтипов является важной темой.
Некоторые части этой статьи основаны на материалах FOLDOC , используемых с разрешения .
Внешние ссылки
- Грэм Хаттон, Лямбда-исчисление , короткое (12 минут) видео для компьютерных фанатов о лямбда-исчислении
- Гельмут Брандл, Пошаговое введение в лямбда-исчисление
- "Лямбда-исчисление" , Энциклопедия математики , EMS Press , 2001 [1994]
- Ахим Юнг, Краткое введение в лямбда-исчисление - ( PDF )
- Дана Скотт, Хронология лямбда-исчисления - ( PDF )
- Дэвид К. Кинан, Рассечение пересмешника: графическая нотация лямбда-исчисления с анимированной редукцией
- Рауль Рохас, Введение в лямбда-исчисление - ( PDF )
- Питер Селинджер, Конспект лекций по лямбда-исчислению - ( PDF )
- Л. Эллисон, Некоторые примеры исполняемых λ-исчислений
- Георг П. Лочжевский, Лямбда-исчисление и A ++
- Брет Виктор, « Яйца аллигатора: игра-головоломка, основанная на лямбда-исчислении»
- Лямбда-исчисление на веб-сайте Safalra
- LCI Lambda Interpreter - простой, но мощный интерпретатор чистого исчисления.
- Ссылки на лямбда-исчисление на Lambda-the-Ultimate
- Майк Тайер, Lambda Animator , графический Java-апплет, демонстрирующий альтернативные стратегии сокращения.
- Реализация лямбда-исчисления с использованием шаблонов C ++
- Мариус Булига, Графическое лямбда-исчисление
- Лямбда-исчисление как модель рабочего процесса Питера Келли, Пола Коддингтона и Эндрю Венделборна; упоминает сокращение графа как распространенное средство оценки лямбда-выражений и обсуждает применимость лямбда-исчисления для распределенных вычислений (благодарясвойству Черча – Россера , которое позволяетсокращать параллельный граф для лямбда-выражений).
- Шейн Штайнерт-Трелкельд, «Лямбда-исчисления» , Интернет-энциклопедия философии
- Антон Салихметов, Макро-лямбда-исчисление
- ^ Церковь, Алонсо (1941). Исчисления лямбда-преобразования . Принстон: Издательство Принстонского университета . Проверено 14 апреля 2020 .
- ^ Фринк-младший, Оррин (1944). "Обзор: исчисления лямбда-преобразования Алонсо Чёрчем" (PDF) . Бык. Амер. Математика. Soc . 50 (3): 169–172. DOI : 10.1090 / s0002-9904-1944-08090-7 .