Лямбда-исчисление
Лямбда-исчисление (также называемое λ -исчислением ) — это формальная система математической логики для выражения вычислений функций , основанных на абстракции и их применении переменных с использованием привязки и подстановки . Нетипизированное лямбда-исчисление, тема этой статьи, представляет собой универсальную модель вычислений , которую можно использовать для моделирования любой машины Тьюринга (и наоборот). Она была введена математиком Алонзо Чёрчем в 1930-х годах в рамках его исследования основ математики . формулировку В 1936 году Чёрч нашел логически последовательную и задокументировал ее в 1940 году.
Лямбда-исчисление состоит из построения лямбда-членов и выполнения сокращения над ними операций . В простейшей форме лямбда-исчисления термы строятся с использованием только следующих правил: [а]
- : Переменная — это символ или строка, представляющая параметр.
- : Лямбда-абстракция — это определение функции, принимающее в качестве входных данных связанную переменную. (между λ и точкой/точкой . ) и возврат тела .
- : Приложение , применяющее функцию на спор . Оба и являются лямбда-термами.
К операциям сокращения относятся:
- : α-преобразование , переименование связанных переменных в выражении. Используется во избежание конфликтов имен .
- : β-редукция , [б] замена связанных переменных выражением аргумента в теле абстракции.
Если используется индексация Де Брейна , то α-преобразование больше не требуется, поскольку не будет конфликтов имен. Если повторное применение шагов приведения в конечном итоге завершится, то по теореме Чёрча – Россера будет получена β-нормальная форма .
Имена переменных не нужны, если вы используете универсальную лямбда-функцию, такую как Iota и Jot , которая может создавать любое поведение функции, вызывая ее в различных комбинациях.
Пояснения и приложения [ править ]
Лямбда-исчисление является полным по Тьюрингу , то есть представляет собой универсальную модель вычислений , которую можно использовать для моделирования любой машины Тьюринга . [3] Его тезка, греческая буква лямбда (λ), используется в лямбда-выражениях и лямбда-терминах для обозначения привязки переменной в функции .
Лямбда-исчисление может быть нетипизированным или типизированным . В типизированном лямбда-исчислении функции могут применяться только в том случае, если они способны принимать «тип» данных данного ввода. Типизированные лямбда-исчисления слабее , чем нетипизированные лямбда-исчисления, которые являются основной темой этой статьи, в том смысле, что типизированные лямбда-исчисления могут выражать меньше , чем нетипизированные лямбда-исчисления. С другой стороны, типизированные лямбда-исчисления позволяют доказать больше вещей. Например, в просто типизированном лямбда-исчислении существует теорема, согласно которой каждая стратегия вычисления завершается для каждого просто типизированного лямбда-термина, тогда как вычисление нетипизированных лямбда-термов не обязательно завершается (см. ниже ). Одной из причин, по которой существует множество различных типизированных лямбда-исчислений, является желание делать больше (из того, что может нетипизированное исчисление), не отказываясь при этом от возможности доказать сильные теоремы об этом исчислении.
Лямбда-исчисление имеет применение во многих различных областях математики , философии , [4] лингвистика , [5] [6] и информатика . [7] [8] Лямбда-исчисление сыграло важную роль в развитии теории языков программирования . Языки функционального программирования реализуют лямбда-исчисление. Лямбда-исчисление также является актуальной темой исследований в теории категорий . [9]
История [ править ]
Лямбда-исчисление было введено математиком Алонзо Чёрчем в 1930-х годах как часть исследования основ математики . [10] [с] первоначальной системы была показана Логическая несостоятельность в 1935 году, когда Стивен Клини и Дж. Б. Россер разработали парадокс Клини-Россера . [11] [12]
Впоследствии, в 1936 году, Чёрч выделил и опубликовал только ту часть, которая имеет отношение к вычислениям, — то, что сейчас называется нетипизированным лямбда-исчислением. [13] В 1940 году он также представил более слабую в вычислительном отношении, но логически непротиворечивую систему, известную как просто типизированное лямбда-исчисление . [14]
До 1960-х годов, когда была выяснена его связь с языками программирования, лямбда-исчисление было всего лишь формализмом. Благодаря приложениям Ричарда Монтегю и других лингвистов в области семантики естественного языка лямбда-исчисление начало занимать почетное место как в лингвистике, так и в лингвистике. [15] и информатика. [16]
Происхождение λ символа [ править ]
Существует некоторая неопределенность относительно причины использования Чёрчем греческой буквы лямбда (λ) в качестве обозначения абстракции функции в лямбда-исчислении, возможно, отчасти из-за противоречивых объяснений самого Чёрча. По словам Кардоне и Хиндли (2006):
Кстати, почему Чёрч выбрал обозначение «λ»? В [неопубликованном письме Харальду Диксону от 1964 года] он ясно заявил, что оно произошло от обозначения « для абстракции классов », использованный Уайтхедом и Расселом , сначала изменив « " к " », чтобы отличить абстракцию функции от абстракции класса, а затем изменить « » на «λ» для удобства печати.
Об этом происхождении сообщалось также в [Россер, 1984, с.338]. С другой стороны, в более поздние годы своей жизни Чёрч сказал двум исследователям, что выбор был более случайным: нужен был символ, и случайно была выбрана λ.
Дана Скотт также затрагивала этот вопрос в различных публичных лекциях. [17] Скотт вспоминает, что однажды он задал вопрос о происхождении лямбда-символа бывшему студенту и зятю Черча Джону Аддисону-младшему, который затем написал своему тестю открытку:
Дорогой профессор Чёрч,
У Рассела был оператор йота , у Гильберта — оператор эпсилон . Почему вы выбрали лямбду в качестве своего оператора?
По словам Скотта, весь ответ Чёрча состоял в том, чтобы вернуть открытку со следующей пометкой: « Ини, мини, мини, мо ».
Неофициальное описание [ править ]
Мотивация [ править ]
Вычислимые функции являются фундаментальной концепцией в области информатики и математики. Лямбда-исчисление обеспечивает простую семантику вычислений, которая полезна для формального изучения свойств вычислений. Лямбда-исчисление включает в себя два упрощения, которые упрощают его семантику. Первое упрощение заключается в том, что лямбда-исчисление обрабатывает функции «анонимно»; он не дает им явных имен. Например, функция
можно переписать в анонимной форме как
что читается как кортеж x и ( y отображается в « "). [д] Аналогично, функция
можно переписать в анонимной форме как
где ввод просто сопоставляется сам с собой. [д]
Второе упрощение заключается в том, что лямбда-исчисление использует только функции одного входа. Обычная функция, требующая два входа, например функция может быть переработана в эквивалентную функцию, которая принимает один входной сигнал и в качестве вывода возвращает другую функцию, которая, в свою очередь, принимает один входной сигнал. Например,
может быть переработан в
Этот метод, известный как каррирование , преобразует функцию, принимающую несколько аргументов, в цепочку функций, каждая из которых имеет один аргумент.
функции Применение функцию на аргументы (5, 2), сразу дает
- ,
тогда как оценка каррированной версии требует еще одного шага
- // определение использовался с во внутреннем выражении. Это похоже на β-редукцию.
- // определение использовался с . Опять же, аналогично β-редукции.
чтобы прийти к тому же результату.
Лямбда-исчисление [ править ]
Лямбда-исчисление состоит из языка лямбда-терминов , которые определяются определенным формальным синтаксисом, и набора правил преобразования для манипулирования лямбда-термами. Эти правила преобразования можно рассматривать как эквациональную теорию или как операционное определение .
Как описано выше, все функции лямбда-исчисления не имеют имен и являются анонимными. Они принимают только одну входную переменную, поэтому каррирование используется для реализации функций нескольких переменных.
Лямбда-термины [ править ]
Синтаксис лямбда-исчисления определяет некоторые выражения как допустимые выражения лямбда-исчисления, а некоторые как недопустимые, точно так же, как некоторые строки символов являются допустимыми программами на языке C , а некоторые нет. Допустимое выражение лямбда-исчисления называется « лямбда-термом ».
Следующие три правила дают индуктивное определение , которое можно применить для построения всех синтаксически допустимых лямбда-термов: [Это]
- переменная x сама по себе является допустимым лямбда-термом.
- если t — лямбда-терм, а x — переменная, то [ф] — это лямбда-термин (называемый абстракцией );
- если t и s — лямбда-члены, то — это лямбда-термин (называемый приложением ).
Ничто иное не является лямбда-термом. То есть лямбда-терм действителен тогда и только тогда, когда его можно получить путем многократного применения этих трех правил. Для удобства некоторые круглые скобки при написании лямбда-терма можно опустить. Например, крайние круглые скобки обычно не пишутся. См. § Обозначения ниже, где подробно описано, какие круглые скобки являются необязательными. Также принято расширять представленный здесь синтаксис дополнительными операциями, что позволяет понять такие термины, как В центре внимания этой статьи чистое лямбда-исчисление без расширений, но в пояснительных целях используются лямбда-термины, расширенные арифметическими операциями.
Абстракция обозначает § анонимную функцию [г] который принимает один входной сигнал x и возвращает t . Например, это абстракция, представляющая функцию определяется используя термин для т . Имя является излишним при использовании абстракции. Синтаксис связывает переменную x в термине t . Определение функции с абстракцией просто «настраивает» функцию, но не вызывает ее.
Приложение представляет собой применение функции t к входу s , то есть представляет собой действие вызова функции t на входе s для получения .
Лямбда-терм может относиться к несвязанной переменной, например, к термину (который представляет собой определение функции ). В этом термине переменная y не определена и считается неизвестной. Абстракция является синтаксически допустимым термином и представляет собой функцию, которая добавляет свои входные данные к еще неизвестному y .
Круглые скобки могут использоваться и могут быть необходимы для устранения неоднозначности терминов. Например,
- имеет форму и поэтому является абстракцией, в то время как
- имеет форму и, следовательно, является приложением.
Примеры 1 и 2 обозначают разные термины, отличающиеся только расположением скобок. Они имеют разное значение: пример 1 — это определение функции, а пример 2 — применение функции. Лямбда-переменная x является заполнителем в обоих примерах.
Здесь пример 1 определяет функцию , где является , анонимная функция , с вводом ; а пример 2, , применяется ли M к N, где это лямбда-терм применяется ко входу который . Оба примера 1 и 2 будут оцениваться как тождественная функция. .
Функции, которые работают с функциями [ править ]
В лямбда-исчислении функции считаются « значениями первого класса », поэтому функции могут использоваться в качестве входных данных или возвращаться в качестве выходных данных из других функций.
Например, лямбда-терм представляет функцию идентичности , . Дальше, представляет постоянную функцию , функция, которая всегда возвращает , независимо от ввода. В качестве примера функции, работающей с функциями, композицию функции можно определить как .
Существует несколько понятий «эквивалентности» и «редукции», которые позволяют «свести» лямбда-термины к «эквивалентным» лямбда-терминам.
Альфа-эквивалентность [ править ]
Базовой формой эквивалентности, определяемой с помощью лямбда-терминов, является альфа-эквивалентность . Он отражает интуитивное понимание того, что конкретный выбор связанной переменной в абстракции (обычно) не имеет значения. Например, и являются альфа-эквивалентными лямбда-терминами, и оба они представляют одну и ту же функцию (функцию идентичности). Условия и не являются альфа-эквивалентными, поскольку не связаны абстракцией. Во многих презентациях обычно идентифицируются альфа-эквивалентные лямбда-термины.
Для определения β-редукции необходимы следующие определения:
Свободные переменные [ править ]
Свободные переменные [час] термина — это переменные, не связанные абстракцией. Набор свободных переменных выражения определяется индуктивно:
- Свободные переменные просто
- Набор свободных переменных представляет собой набор свободных переменных , но с удаленный
- Набор свободных переменных является объединением множества свободных переменных и набор свободных переменных .
Например, лямбда-терм, представляющий тождество не имеет свободных переменных, но функция имеет одну свободную переменную, .
Замены, избегающие захвата [ править ]
Предполагать , и являются лямбда-термами, и и являются переменными. Обозначения указывает на замену для в способом , избегающим захвата . Это определяется так:
- ; с заменен на , становится
- если ; с заменен на , (который не ) останки
- ; замена распространяется на обе стороны приложения
- ; переменная, связанная абстракцией, подстановке не подлежит; замена такой переменной оставляет абстракцию неизменной
- если и не появляется среди свободных переменных ( считается « свежим » для ) ; замена переменной, которая не связана абстракцией, происходит в теле абстракции, при условии, что абстрактная переменная является «свежим» на срок замены .
Например, , и .
Состояние свежести (требующее, чтобы не находится в переменных свободных ) имеет решающее значение для обеспечения того, чтобы замена не меняла смысл функций.
Например, замена, игнорирующая условие актуальности, может привести к ошибкам: . Эта ошибочная замена превратила бы постоянную функцию в личность .
В общем, несоблюдение условия актуальности можно исправить сначала путем альфа-переименования с использованием подходящей свежей переменной. Например, возвращаясь к нашему правильному понятию замены, в абстракцию можно переименовать с помощью новой переменной , чтобы получить , а смысл функции сохраняется при подстановке.
β-редукция [ править ]
Правило β-редукции [б] утверждает, что приложение формы сводится к сроку . Обозначения используется, чтобы указать, что β-редуцирует до . Например, для каждого , . Это демонстрирует, что действительно это личность. Сходным образом, , что демонстрирует, что является постоянной функцией.
Лямбда-исчисление можно рассматривать как идеализированную версию функционального языка программирования, такого как Haskell или Standard ML . С этой точки зрения β-редукция соответствует вычислительному шагу. Этот шаг можно повторять с помощью дополнительных β-сокращений до тех пор, пока не останется приложений для сокращения. В нетипизированном лямбда-исчислении, представленном здесь, этот процесс сокращения может не завершаться. Например, рассмотрим термин . Здесь . То есть член сводится к самому себе за одно β-редукция, и поэтому процесс приведения никогда не завершится.
Другой аспект нетипизированного лямбда-исчисления заключается в том, что оно не различает разные типы данных. Например, может быть желательно написать функцию, которая работает только с числами. Однако в нетипизированном лямбда-исчислении нет способа предотвратить применение функции к значениям истинности , строкам или другим нечисловым объектам.
Формальное определение [ править ]
Определение [ править ]
Лямбда-выражения состоят из:
- переменные v 1 , v 2 , ...;
- символы абстракции λ (лямбда) и . (точка);
- круглые скобки ().
Набор лямбда-выражений Λ можно определить индуктивно :
- Если x — переменная, то x ∈ Λ.
- Если x переменная и M ∈ Λ, то (λx.M ) — ∈ Λ.
- Если M , N ∈ Λ, то ( MN ) ∈ Λ.
Экземпляры правила 2 известны как абстракции , а случаи правила 3 — как приложения . [18] См. § сокращаемое выражение.
Этот набор правил можно записать в форме Бэкуса-Наура следующим образом:
< выражение > :== < абстракция > | < приложение > | < переменная >
< абстракция > :== λ < переменная > . < выражение >
< приложение > :== ( < выражение > < выражение > )
< переменная > :== v1 | версия 2 | ...
Обозначения [ править ]
Чтобы не загромождать обозначение лямбда-выражений, обычно применяются следующие соглашения:
- Крайние круглые скобки опускаются: M N вместо ( M N ).
- Предполагается, что приложения левоассоциативны: можно писать M N P вместо (( M N ) P . [19]
- Когда все переменные однобуквенные, пробел в приложениях можно MNP вместо MNP опускать : . [20]
- Тело абстракции простирается насколько возможно вправо : λ x . MN означает λ x .( MN ), а не (λ x . M ) N .
- Последовательность абстракций сжимается: λ x .λ y .λ z . N сокращается как λ xyz . Н. [21] [19]
Свободные и связанные переменные [ править ]
Говорят, что оператор абстракции λ связывает свою переменную, где бы она ни встречалась в теле абстракции. Переменные, попадающие в область абстракции, называются связанными . В выражении λ x . M , часть λ x часто называют связывающей как намек на то, что переменная x привязывается путем добавления λ x к M. , Все остальные переменные называются свободными . Например, в выражении λ y . xxy , y — связанная переменная, а x — свободная переменная. Также переменная связана с ближайшей к ней абстракцией. В следующем примере единственное вхождение x в выражение связано второй лямбдой: λ x . y (λ x . zx ).
Набор свободных переменных лямбда-выражения M обозначается как FV( M ) и определяется рекурсией структуры термов следующим образом:
- FV( x ) = { x }, где x — переменная.
- FV(λ x . M ) = FV ( M ) \ { x }. [я]
- FV( MN ) = FV( M )∪FV( N ). [Дж]
Выражение, не содержащее свободных переменных, называется закрытым . Закрытые лямбда-выражения также известны как комбинаторы и эквивалентны терминам комбинаторной логики .
Сокращение [ править ]
Значение лямбда-выражений определяется тем, как выражения можно сократить. [22]
Существует три вида сокращения:
- α-преобразование : изменение связанных переменных;
- β-редукция : применение функций к их аргументам;
- η-редукция : которая отражает понятие экстенсиональности.
Мы также говорим о результирующих эквивалентностях: два выражения являются α-эквивалентными , если их можно α-преобразовать в одно и то же выражение. Аналогично определяются β-эквивалентность и η-эквивалентность.
Термин редекс , сокращение от сокращаемого выражения , относится к подтермам, которые можно сократить с помощью одного из правил сокращения. Например, (λ x . M ) N является β-редексом, выражающим замену N на x в M . Выражение, к которому сводится редекс, называется его редукцией ; сокращение (λ x . M ) N равно M [ x := N ]. [б]
Если x не свободен в M , λ x . M x также является η-редексом с редукцией M .
α-конверсия [ править ]
α-конверсия ( альфа -конверсия), иногда известная как α-переименование, [23] позволяет изменять имена связанных переменных. Например, α-преобразование λ x . x может дать λ y . й . Термы, отличающиеся только α-конверсией, называются α-эквивалентными . Часто при использовании лямбда-исчисления α-эквивалентные термины считаются эквивалентными.
Точные правила α-конверсии не совсем тривиальны. Во-первых, при α-преобразовании абстракции переименовываются только те вхождения переменных, которые привязаны к той же абстракции. Например, α-преобразование λ x .λ x . x может привести к λ y .λ x . x , но это не могло привести к λ y .λ x . й . Последнее имеет иное значение, чем оригинал. Это аналогично программному понятию затенения переменных .
Во-вторых, α-преобразование невозможно, если оно приведет к тому, что переменная будет захвачена другой абстракцией. Например, если мы заменим x на y в λ x .λ y . x , мы получаем λ y .λ y . й , что совсем не то.
В языках программирования со статической областью действия α-преобразование можно использовать для упрощения разрешения имен , гарантируя, что никакое имя переменной не маскирует имя в содержащей области видимости (см. α-переименование, чтобы сделать разрешение имен тривиальным ).
В обозначениях индекса Де Брейна любые два α-эквивалентных термина синтаксически идентичны.
Замена [ править ]
Замена, записываемая M [ x := N ], — это процесс замены всех свободных вхождений переменной x в выражении M выражение N. на Замена в терминах лямбда-исчисления определяется рекурсией структуры терминов следующим образом (примечание: x и y — это только переменные, а M и N — любое лямбда-выражение):
- Икс [ Икс := Н ] = Н
- y [ x := N ] = y , если x ≠ y
- ( M 1 M 2 )[ Икс := N знак равно М 1 [ Икс := N ] М 2 [ Икс := N ]
- (λ Икс . M )[ Икс := N ] знак равно λ Икс . М
- (λ y . M )[ x := N ] = λ y .( M [ x := N ]), если x ≠ y и y ∉ FV( N ) См. выше FV
Чтобы подставить выражение в абстракцию, иногда необходимо α-преобразовать выражение. Например, неверно, что (λ x . y )[ y := x ] приводит к λ x . x , потому что замененный x должен был быть свободным, но в итоге оказался связанным. Правильная замена в этом случае — λ z . x с точностью до α-эквивалентности. Замена определяется однозначно с точностью до α-эквивалентности. замены, избегающие захвата. См. выше
β-редукция [ править ]
β-редукция ( бета- редукция) отражает идею применения функции.
β-редукция определяется в терминах замены: β-редукция (λ x . M ) N равна M [ x := N ]. [б]
Например, предполагая некоторое кодирование 2, 7, ×, мы имеем следующую β-редукцию: (λ n . n × 2) 7 → 7 × 2.
Можно рассматривать, что β-редукция — это то же самое, что и концепция локальной сводимости в естественной дедукции через изоморфизм Карри-Ховарда .
η-редукция [ править ]
η-редукция ( эта- редукция) выражает идею экстенсиональности , [24] в этом контексте две функции одинаковы тогда и только тогда, когда они дают одинаковый результат для всех аргументов. η-редукция преобразует λ x . f x и f всякий раз, когда x не появляется свободным в f .
η-редукция может рассматриваться как то же самое, что и концепция локальной полноты в естественной дедукции через изоморфизм Карри – Говарда .
Нормальные слияние формы и
Для нетипизированного лямбда-исчисления β-редукция как правило переписывания не является ни строго нормализующей , ни слабо нормализующей .
Однако можно показать, что β-редукция конфлюэнтна при работе до α-конверсии (т. е. мы считаем две нормальные формы равными, если возможно α-преобразовать одну в другую).
Следовательно, как сильно нормализующие, так и слабо нормализующие члены имеют единственную нормальную форму. Для сильно нормализующих членов любая стратегия редукции гарантированно приведет к нормальной форме, тогда как для слабо нормализующих членов некоторые стратегии редукции могут не найти ее.
Типы данных кодирования [ править ]
Базовое лямбда-исчисление можно использовать для моделирования арифметики , логических значений, структур данных и рекурсии, как показано в следующих подразделах i , ii , iii и § iv .
Арифметика в лямбда-исчислении [ править ]
Существует несколько возможных способов определения натуральных чисел в лямбда-исчислении, но наиболее распространенными являются цифры Чёрча , которые можно определить следующим образом:
- 0 := λ ж .λ Икс . Икс
- 1 == λ ж .λ Икс . е х
- 2 == λ ж .λ Икс . ж ( ж Икс )
- 3 == λ ж .λ Икс . ж ( ж ( ж Икс ))
и так далее. Или используя альтернативный синтаксис, представленный выше в разделе «Нотации» :
- 0 := λ fx . Икс
- 1 := λ fx . е х
- 2 := λ fx . ж ( ж Икс )
- 3 := λ fx . ж ( ж ( ж Икс ))
Числа Чёрча — это функция более высокого порядка , она принимает функцию с одним аргументом. f и возвращает другую функцию с одним аргументом. Церковная цифра n — функция, которая принимает функцию f в качестве аргумента и возвращает n -й состав f , т.е. функция f составлен сам с собой n раз. Это обозначается ж ( н ) и на самом деле является n -я степень f (рассматривается как оператор); ж (0) определяется как тождественная функция. Такие повторяющиеся композиции (одной функции е ) подчиняются законам показателей степени , поэтому эти цифры можно использовать для арифметических действий. (В исходном лямбда-исчислении Чёрча формальный параметр лямбда-выражения должен был встречаться хотя бы один раз в теле функции, поэтому приведенное выше определение 0 невозможно.)
Один из способов мышления о числительном Чёрча n , который часто бывает полезен при анализе программ, представляет собой инструкцию «повторить n раз». Например, используя ПАРА и NIL- функции, определенные ниже, можно определить функцию, которая создает (связный) список из n элементов, все равных x, путем повторения команды «добавить еще один x элемент » n раз, начиная с пустого списка. Лямбда-член
- λ п .λ Икс . n (ПАРА x ) НОЛЬ
Варьируя то, что повторяется, и изменяя аргумент, к которому применяется повторяемая функция, можно добиться множества различных эффектов.
Мы можем определить функцию-преемницу, которая принимает число Чёрча. n и возвращает n + 1 , добавив еще одно приложение f , где «(mf)x» означает, что функция «f» применяется «m» раз к «x»:
- SUCC:= λ n .λ f .λ x . ж ( п ж Икс )
Поскольку m -й состав f состоит из n -й состав f дает m + n -й состав f , сложение можно определить следующим образом:
- ПЛЮС := λ м .λ п .λ ж .λ x . м ж ( п ж Икс )
PLUS можно рассматривать как функцию, принимающую в качестве аргументов два натуральных числа и возвращающую натуральное число; можно убедиться, что
- ПЛЮС 2 3
и
- 5
являются β-эквивалентными лямбда-выражениями. С момента добавления м в число n можно получить, добавив 1 m раз, альтернативное определение:
- ПЛЮС := λ м .λ п . м SUCC н [25]
Аналогично умножение можно определить как
- MULT := λ м .λ п .λ ж . м ( н ж ) [21]
Альтернативно
- MULT := λ м .λ п . м (ПЛЮС n ) 0
с момента умножения м и n — то же самое, что повторение добавления n функция m раз, а затем приравняв его к нулю. Возведение в степень имеет довольно простое представление цифрами Чёрча, а именно:
- POW := λ б .λ е . е б [1]
Функция-предшественник, определенная PRED n = n - 1 для положительного целого числа н и PRED 0 = 0 значительно сложнее. Формула
- PRED := λ n .λ f .λ x . п (λ г .λ час . час ( г ж )) (λ ты . Икс ) (λ ты . ты )
можно проверить, показав индуктивно, что если T обозначает (λ г .λ час . час ( г ж )) , то Т ( н ) (λ ты . Икс ) знак равно (λ час . час ( ж ( п -1) ( х ))) для п > 0 . Два других определения PRED приведены ниже: один использует условные выражения , а другой — пары . С функцией предшественника вычитание выполняется просто. Определение
- SUB := λ м .λ п . п ПРЕДМ ,
SUB m n дает доходность м - п , когда м > п и 0 иначе.
Логика и предикаты [ править ]
По соглашению для логических значений используются следующие два определения (известные как логические значения Черча). ПРАВДА и ЛОЖЬ :
- ИСТИНА := λ x .λ y . Икс
- ЛОЖЬ := λ x .λ y . й
Затем с помощью этих двух лямбда-членов мы можем определить некоторые логические операторы (это всего лишь возможные формулировки; другие выражения могут быть столь же правильными):
- И := λ п .λ q . п q п
- ИЛИ := λ п .λ q . п п q
- НЕ := λ п . p ЛОЖЬ ИСТИНА
- РАЗНИЦА := λ п .λ а .λ б . п а б
Теперь мы можем вычислять некоторые логические функции, например:
- И ПРАВДА ЛОЖЬ
- ≡ (λ p .λ q . p q p ) ИСТИНА ЛОЖЬ → β ИСТИНА ЛОЖЬ ИСТИНА
- ≡ (λ x .λ y . x ) ЛОЖЬ ИСТИНА → β ЛОЖЬ
и мы видим это AND TRUE FALSE эквивалентно ЛОЖЬ .
Предикат . — это функция, которая возвращает логическое значение Самым фундаментальным предикатом является ISZERO , который возвращает ИСТИННО , если его аргументом является число Чёрча. 0 , но ЛОЖЬ, если его аргументом было любое другое число Чёрча:
- ISZERO := λ n . n (λ x .FALSE) ИСТИНА
Следующий предикат проверяет, меньше ли первый аргумент второго или равен ему:
- LEQ := λ m .λ n .ISZERO (SUB m n ) ,
и с тех пор m = n , если LEQ м н и LEQ n m , построить предикат численного равенства несложно.
Наличие предикатов и приведенное выше определение ПРАВДА и Значение FALSE позволяет удобно писать выражения «если-то-иначе» в лямбда-исчислении. Например, функцию-предшественницу можно определить как:
- ПРЕД := λ n . n (λ g .λ k .ISZERO ( g 1) k (ПЛЮС ( g k ) 1)) (λ v .0) 0
в чем можно убедиться, показав индуктивно, что n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) — это добавление n - 1 функция для п > 0.
Пары [ править ]
Пара (двойка) может быть определена в терминах ПРАВДА и ЛОЖЬ , используя кодировку Чёрча для пар . Например, PAIR инкапсулирует пару ( Икс , и ), FIRST возвращает первый элемент пары, а SECOND возвращает второе значение.
- ПАРА := λ x .λ y .λ f . ж х у
- ПЕРВЫЙ := λ п . р ВЕРНО
- ВТОРОЙ := λ п . р ЛОЖЬ
- НОЛЬ := λ x .ИСТИНА
- НОЛЬ := λ п . p (λ x .λ y .ЛОЖЬ)
Связанный список может быть определен либо как NIL для пустого списка, либо как ПАРА элемента и меньшего списка. Предикат NULL проверяет значение НОЛЬ . (Альтернативно, с NIL := FALSE , конструкция l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil) устраняет необходимость в явном NULL-тесте).
В качестве примера использования пар можно привести функцию сдвига и приращения, отображающую ( м , п ) до ( n , n + 1) можно определить как
- Φ := λ x .ПАРА (ВТОРОЙ x ) (SUCC (ВТОРОЙ x ))
что позволяет нам дать, пожалуй, наиболее прозрачную версию функции-предшественника:
- PRED := λ n .FIRST ( n Φ (ПАРА 0 0)).
Дополнительные методы программирования [ править ]
Существует значительное количество идиом программирования для лямбда-исчисления. Многие из них изначально были разработаны в контексте использования лямбда-исчисления в качестве основы для семантики языка программирования , эффективно используя лямбда-исчисление в качестве языка программирования низкого уровня . Поскольку некоторые языки программирования включают лямбда-исчисление (или что-то очень похожее) в качестве фрагмента, эти методы также находят применение в практическом программировании, но тогда могут восприниматься как непонятные или чуждые.
Именованные константы [ править ]
В лямбда-исчислении библиотека принимает форму набора ранее определенных функций, которые в качестве лямбда-терминов представляют собой просто определенные константы. В чистом лямбда-исчислении нет концепции именованных констант, поскольку все атомарные лямбда-термы являются переменными, но можно имитировать наличие именованных констант, выделив переменную в качестве имени константы, используя абстракцию для привязки этой переменной в основном теле. и применить эту абстракцию к предполагаемому определению. Таким образом, использовать f означает N (некоторый явный лямбда-терм) в M (другой лямбда-терм, «основная программа»), можно сказать
- (λ f . M ) Н
Авторы часто вводят синтаксический сахар , например: позволять , [к] чтобы разрешить запись вышеизложенного в более интуитивном порядке
- пусть f = N в М
Объединив такие определения в цепочку, можно написать «программу» лямбда-исчисления в виде нуля или более определений функций, за которыми следует один лямбда-термин, использующий эти функции, которые составляют основную часть программы.
Заметное ограничение этого пусть это имя f не определено в N , чтобы N выходило за рамки привязки абстракции ж ; это означает, что определение рекурсивной функции не может использоваться как N с позволять . летрек [л] конструкция позволит писать рекурсивные определения функций.
Рекурсия и фиксированные точки [ править ]
Рекурсия — это определение функции с использованием самой функции. Определение, содержащее себя внутри себя по значению, приводит к тому, что все значение имеет бесконечный размер. Другие нотации, поддерживающие рекурсию, преодолевают эту проблему, ссылаясь на определение функции по имени . Лямбда-исчисление не может выразить это: все функции в лямбда-исчислении анонимны, поэтому мы не можем ссылаться по имени на значение, которое еще предстоит определить, внутри лямбда-терма, определяющего это же значение. Однако лямбда-выражение может принимать себя в качестве собственного аргумента, например в (λ Икс . Икс Икс ) E . Здесь E должно быть абстракцией, применяющей свой параметр к значению для выражения рекурсии.
Рассмотрим факториал F( n ) рекурсивно определяется формулой
- F( n ) = 1, если n = 0; иначе n × F( n - 1) .
В лямбда-выражении, которое должно представлять эту функцию, предполагается, что параметр (обычно первый) получает само лямбда-выражение в качестве своего значения, поэтому его вызов – применение его к аргументу – будет равносилен рекурсии. Таким образом, для достижения рекурсии аргумент «задуманный как самоссылающийся» (называемый r здесь) всегда должен передаваться самому себе внутри тела функции, в точке вызова:
- г := λ р . λ n .(1, если n = 0; иначе n × ( r r ( n −1)))
- с r r x = F x = G r x , поэтому г = G и
- F := GG = (λ x . x x ) G
Здесь самоприложение достигает репликации, передавая лямбда-выражение функции следующему вызову в качестве значения аргумента, делая его доступным для ссылки и вызова там.
Это решает проблему, но требует перезаписи каждого рекурсивного вызова как самостоятельного применения. Мы хотели бы иметь общее решение без необходимости каких-либо переписываний:
- г := λ р . λ n .(1, если n = 0; иначе n × ( r ( n −1)))
- с r x = F x = G r x , поэтому r = G r =: FIX G и
- F := ИСПРАВИТЬ 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 вернет самовоспроизводящееся лямбда-выражение, представляющее рекурсивную функцию (здесь Ф ). Функцию не нужно явно передавать самой себе в любой момент, поскольку саморепликация заранее запланирована при ее создании и будет выполняться каждый раз при ее вызове. Таким образом, исходное лямбда-выражение (FIX G) воссоздается внутри себя, в точке вызова, достигая самореференции .
На самом деле существует множество возможных определений этого понятия. FIX , самый простой из них:
- Y := λ г .(λ x . g ( x x )) (λ x . g ( x x ))
В лямбда-исчислении Y g – фиксированная точка g , поскольку он расширяется до:
- Да г
- (λ h .(λ x . h ( x x )) (λ x . h ( x x ))) г
- (λ x . g ( x x )) (λ x . g ( x x ))
- г ((λ x . g ( x x )) (λ x . g ( x x )))
- г ( Y г )
Теперь, чтобы выполнить наш рекурсивный вызов функции факториала, мы просто вызовем ( Y G) n , где n — число, факториал которого мы вычисляем. при n Например, = 4 это дает:
- ( Д Г ) 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 , каждая рекурсивно определенная функция может быть выражена как лямбда-выражение. В частности, теперь мы можем четко рекурсивно определить предикаты вычитания, умножения и сравнения натуральных чисел.
Стандартные условия [ править ]
Некоторые термины имеют общепринятые названия: [27] [28] [29]
- Я := λ Икс . Икс
- S := λ Икс .λ y .λ z . Икс z ( у z )
- K := λ Икс .λ y . Икс
- B := λ Икс .λ y .λ z . х ( у я )
- C знак равно λ Икс .λ y .λ z . х z y
- W := λ Икс .λ y . х у у
- ω или Δ или U := λ x . х х
- Ох := ох ох
I — функция идентичности. СК и BCKW образует полные системы комбинаторного исчисления , которые могут выражать любой лямбда-член - см. следующий раздел . Ом UU — наименьший термин, не имеющий нормальной формы. YI — еще один такой термин. Y является стандартным и определен выше , а также может быть определен как Y = BU(CBU) , так что Y г=г( Y г) . ПРАВДА и FALSE, определенные выше, обычно сокращаются как Т и Ф.
Устранение абстракции [ править ]
Если N — лямбда-терм без абстракции, но, возможно, содержащий именованные константы ( комбинаторы ), то существует лямбда-терм T ( x , N ), что эквивалентно λ х . N , но ему не хватает абстракции (за исключением именованных констант, если они считаются неатомарными). Это также можно рассматривать как анонимизирующие переменные, поскольку T ( x , N ) удаляет все вхождения x из N , при этом позволяя подставлять значения аргументов в позиции, где N содержит Икс . Функция преобразования T может быть определена следующим образом:
- Т ( Икс , х ) := я
- Т ( x , N ) := K N если x не является свободным N. в
- Т ( Икс , M N ) := S T ( х , М ) Т ( х , Н )
В любом случае член вида T ( x , N ) P можно уменьшить, если исходный комбинатор I , K или S захватит аргумент P , точно так же, как β-редукция (λ x . N ) П подойдёт. Я возвращаю этот аргумент. К. отбрасывает аргумент, как и (λ x . N ) сделал бы, если бы x не имеет свободного вхождения N. в S передает аргумент обоим подтермам приложения, а затем применяет результат первого к результату второго.
Комбинаторы B и C аналогичны S , но передают аргумент только одному подтермину приложения ( B в подтермин «аргумент» и C в подтермин «функция»), таким образом сохраняя последующий K , если нет вхождения из х в одном подтермоне. По сравнению с B и C , комбинатор S фактически объединяет две функции: перестановку аргументов и дублирование аргумента, чтобы его можно было использовать в двух местах. Комбинатор W делает только последнее, создавая систему B, C, K, W в качестве альтернативы исчислению комбинатора SKI .
Типизированное лямбда-исчисление [ править ]
Типизированное лямбда-исчисление — это типизированный формализм , в котором используется лямбда-символ ( ) для обозначения абстракции анонимной функции. В этом контексте типы обычно представляют собой объекты синтаксической природы, которые присваиваются лямбда-термам; точная природа типа зависит от рассматриваемого исчисления (см. Виды типизированных лямбда-исчислений ). С определенной точки зрения типизированные лямбда-исчисления можно рассматривать как усовершенствования нетипизированного лямбда-исчисления, но с другой точки зрения их также можно считать более фундаментальной теорией, а нетипизированное лямбда-исчисление - особым случаем только с одним типом. [30]
Типизированные лямбда-исчисления являются основополагающими языками программирования и основой типизированных функциональных языков программирования , таких как ML и Haskell , а также, косвенно, типизированных императивных языков программирования. Типизированные лямбда-исчисления играют важную роль в разработке систем типов для языков программирования; здесь типизация обычно отражает желаемые свойства программы, например, программа не вызывает нарушения доступа к памяти.
Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри-Ховарда , и их можно рассматривать как внутренний язык классов категорий , например, просто типизированное лямбда-исчисление является языком декартовых замкнутых категорий (CCC).
Стратегии сокращения [ править ]
Является ли термин нормализующимся или нет, и сколько работы необходимо проделать для его нормализации, если это так, зависит в значительной степени от используемой стратегии редукции. Общие стратегии сокращения лямбда-исчисления включают: [31] [32] [33]
- Нормальный заказ
- Первым сокращается самый левый внешний редекс. То есть, когда это возможно, аргументы подставляются в тело абстракции до того, как аргументы будут сокращены. Если терм имеет бета-нормальную форму, нормальное понижение порядка всегда будет достигать этой нормальной формы.
- Приказы о применении
- Первым сокращается самый левый и самый внутренний редекс. Как следствие, аргументы функции всегда сокращаются перед их подстановкой в функцию. В отличие от нормального приведения порядка, аппликативное приведение порядка может не найти бета-нормальную форму выражения, даже если такая нормальная форма существует. Например, термин сводится к себе аппликативным порядком, тогда как нормальный порядок сводит его к бета-нормальной форме. .
- Полное β-снижение
- Любой редекс можно уменьшить в любой момент. По сути, это означает отсутствие какой-либо конкретной стратегии сокращения — что касается сокращаемости, «все ставки сделаны».
Стратегии слабой редукции не приводят к лямбда-абстракциям:
- Вызов по значению
- Подобен аппликативному порядку, но внутри абстракций никакие сокращения не выполняются. Это похоже на порядок вычислений в строгих языках, таких как C: аргументы функции оцениваются перед вызовом функции, а тела функции даже частично не оцениваются, пока аргументы не будут заменены.
- Звонок по имени
- Как обычный порядок, но внутри абстракций сокращения не выполняются. Например, λ x .(λ y . y ) x находится в нормальной форме согласно этой стратегии, хотя и содержит редекс (λ y . y ) x .
Стратегии совместного использования сокращают количество «одинаковых» параллельных вычислений:
- Оптимальное сокращение
- Как в обычном порядке, но вычисления с одинаковой меткой сокращаются одновременно.
- Звонок по необходимости
- Как вызов по имени (следовательно, слабый), но приложения-функции, которые дублируют термины, вместо этого называют аргумент. Аргумент может быть оценен «при необходимости», после чего привязка имени обновляется уменьшенным значением. Это может сэкономить время по сравнению с обычной оценкой заказа.
Вычислимость [ править ]
Не существует алгоритма, который принимал бы в качестве входных данных любые два лямбда-выражения и выходные данные. ИСТИНА или ЛОЖЬ в зависимости от того, сводится ли одно выражение к другому. [13] Точнее, никакая вычислимая функция не может решить этот вопрос. Исторически это была первая проблема, неразрешимость которой удалось доказать. Как обычно для такого доказательства, вычислимое означает вычислимое с помощью любой модели вычислений , полной по Тьюрингу . Фактически вычислимость сама по себе может быть определена с помощью лямбда-исчисления: функция F : N → N натуральных чисел является вычислимой функцией тогда и только тогда, когда существует лямбда-выражение f такое, что для каждой пары x , y в N , F ( x )= y тогда и только тогда, когда f х = б й , где х и y — цифры Чёрча , соответствующие x и y соответственно, и = β , что означает эквивалентность с β-редукцией. см . в тезисе Чёрча-Тьюринга. Другие подходы к определению вычислимости и их эквивалентности
Доказательство невычислимости Чёрча сначала сводит проблему к определению того, имеет ли данное лямбда-выражение нормальную форму . Затем он предполагает, что этот предикат вычислим и, следовательно, может быть выражен в лямбда-исчислении. Опираясь на более раннюю работу Клини и построив нумерацию Гёделя для лямбда-выражений, он строит лямбда-выражение. e , что близко соответствует доказательству первой теоремы Гёделя о неполноте . Если e применяется к собственному числу Гёделя, возникает противоречие.
Сложность [ править ]
Понятие вычислительной сложности лямбда-исчисления немного сложное, поскольку стоимость β-сокращения может варьироваться в зависимости от того, как оно реализовано. [34] Точнее, нужно каким-то образом найти расположение всех вхождений связанной переменной. В в выражении E , подразумевая временные затраты, или необходимо каким-то образом отслеживать расположение свободных переменных, подразумевая пространственные затраты. Наивный поиск местоположений В в E равно O ( n ) длины n Э. Строки-директора были ранним подходом, в котором временные затраты были заменены квадратичным использованием пространства. [35] В более общем плане это привело к изучению систем, использующих явную замену .
В 2014 году было показано, что количество шагов β-редукции, выполняемых при сокращении нормального порядка для сокращения члена, является разумной моделью временных затрат, то есть сокращение можно смоделировать на машине Тьюринга за время, полиномиально пропорциональное числу шаги. [36] Это была давняя открытая проблема из-за взрыва размеров , существования лямбда-членов, размер которых растет экспоненциально для каждого β-сокращения. Результат позволяет обойти эту проблему, работая с компактным общим представлением. Результат ясно показывает, что объем памяти, необходимый для вычисления лямбда-члена, не пропорционален размеру термина во время сокращения. В настоящее время неизвестно, какой будет хорошая мера сложности пространства. [37]
Неразумная модель не обязательно означает неэффективную. Оптимальное сокращение сокращает все вычисления с одной и той же меткой за один шаг, избегая дублирования работы, но количество параллельных шагов β-редукции для приведения данного термина к нормальной форме примерно линейно по размеру термина. Это слишком мало, чтобы быть разумной мерой затрат, поскольку любая машина Тьюринга может быть закодирована в лямбда-исчислении с размером, линейно пропорциональным размеру машины Тьюринга. Истинная стоимость сокращения лямбда-членов связана не с β-редукцией как таковой, а скорее с управлением дублированием редексов во время β-редукции. [38] Неизвестно, являются ли оптимальные реализации приведения разумными при измерении по отношению к разумной модели затрат, такой как количество крайних левых и крайних шагов к нормальной форме, но для фрагментов лямбда-исчисления было показано, что алгоритм оптимального приведения эффективен. и имеет не более квадратичных издержек по сравнению с крайним левым и крайним. [37] Кроме того, реализация оптимального сокращения на прототипе BOHM превзошла как Caml Light , так и Haskell по чистым лямбда-выражениям. [38]
Лямбда-исчисление и языки программирования [ править ]
Как указано в статье Питера Ландина 1965 года «Соответствие между АЛГОЛом 60 и лямбда-нотацией Чёрча», [39] Языки последовательного процедурного программирования можно понимать с точки зрения лямбда-исчисления, которое обеспечивает основные механизмы процедурной абстракции и применения процедур (подпрограмм).
Анонимные функции [ править ]
Например, в Python функцию «квадрат» можно выразить как лямбда-выражение следующим образом:
( лямбда х : х ** 2 )
Приведенный выше пример представляет собой выражение, результатом которого является функция первого класса. Символ lambda
создает анонимную функцию, учитывая список имен параметров, x
– в данном случае только один аргумент и выражение, которое вычисляется как тело функции, x**2
. Анонимные функции иногда называют лямбда-выражениями.
Например, Паскаль и многие другие императивные языки уже давно поддерживают передачу подпрограмм в качестве аргументов другим подпрограммам через механизм указателей на функции . Однако указатели на функции не являются достаточным условием для того, чтобы функции были типами данных первого класса , поскольку функция является типом данных первого класса тогда и только тогда, когда новые экземпляры функции могут быть созданы во время выполнения. И такое создание функций во время выполнения поддерживается в Smalltalk , JavaScript и Wolfram Language , а с недавних пор в Scala , Eiffel («агенты»), C# («делегаты») и C++11 и других.
Параллелизм и параллелизм [ править ]
Свойство Чёрча -Россера лямбда-исчисления означает, что вычисление (β-редукция) может осуществляться в любом порядке , даже параллельно. Это означает, что различные стратегии недетерминированной оценки актуальны . Однако лямбда-исчисление не предлагает каких-либо явных конструкций для параллелизма . можно добавить такие конструкции, как Futures К лямбда-исчислению . Другие исчисления процессов были разработаны для описания взаимодействия и параллелизма.
Семантика [ править ]
Тот факт, что термины лямбда-исчисления действуют как функции на другие термины лямбда-исчисления и даже на самих себя, привел к вопросам о семантике лямбда-исчисления. Можно ли придать разумное значение терминам лямбда-исчисления? Естественная семантика заключалась в том, чтобы найти множество D , изоморфное функциональному пространству D → D функций на самом себе. Однако нетривиальный такой D не может существовать из-за ограничений мощности , поскольку набор всех функций от D до D имеет большую мощность, чем D , если только D не является одноэлементным множеством .
В 1970-х годах Дана Скотт показала, что если рассматривать только непрерывные функции , можно найти множество или область D с требуемым свойством, тем самым предоставив модель для лямбда-исчисления. [40]
Эта работа также легла в основу денотационной семантики языков программирования.
Вариации и расширения [ править ]
Эти расширения находятся в лямбда-кубе :
- Типизированное лямбда-исчисление - лямбда-исчисление с типизированными переменными (и функциями).
- Система F – типизированное лямбда-исчисление с переменными типа.
- Исчисление конструкций - типизированное лямбда-исчисление с типами в качестве значений первого класса.
Эти формальные системы являются расширениями лямбда-исчисления, которых нет в лямбда-кубе:
- Бинарное лямбда-исчисление — версия лямбда-исчисления с двоичным вводом-выводом, двоичным кодированием терминов и назначенной универсальной машиной.
- Лямбда-мю-исчисление - расширение лямбда-исчисления для рассмотрения классической логики.
Эти формальные системы являются вариациями лямбда-исчисления:
- Каппа-исчисление - аналог лямбда-исчисления первого порядка.
Эти формальные системы связаны с лямбда-исчислением:
- Комбинаторная логика - обозначение математической логики без переменных.
- Комбинаторное исчисление SKI — вычислительная система, основанная на комбинаторах S , K и I , эквивалентная лямбда-исчислению, но приводимая без подстановок переменных.
См. также [ править ]
- Аппликативные вычислительные системы – Обработка объектов в стиле лямбда-исчисления.
- Декартова замкнутая категория - основа лямбда-исчисления в теории категорий.
- Категориальная абстрактная машина - модель вычислений , применимая к лямбда-исчислению.
- Клоюр , язык программирования
- Изоморфизм Карри – Говарда. Формальное соответствие между программами и доказательствами.
- Индекс Де Брейна - обозначение, устраняющее неоднозначность альфа-конверсий
- Обозначение Де Брейна - обозначение с использованием функций постфиксной модификации.
- Теория предметной области - исследование некоторых частично упорядоченных наборов , дающих денотационную семантику для лямбда-исчисления.
- Стратегия оценки . Правила оценки выражений в языках программирования.
- Явное замещение - теория замещения, используемая при β-редукции.
- Функциональное программирование
- Формула Харропа - разновидность конструктивной логической формулы, доказательства которой представляют собой лямбда-члены.
- Сети взаимодействия
- Парадокс Клини-Россера - демонстрация несогласованности некоторой формы лямбда-исчисления.
- Рыцари лямбда-исчисления - полувымышленная организация LISP и Scheme. хакеров
- Машина Кривина - абстрактная машина для интерпретации вызова по имени в лямбда-исчислении.
- Определение лямбда-исчисления . Формальное определение лямбда-исчисления.
- Let выражение – выражение, тесно связанное с абстракцией.
- Минимализм (компьютерный)
- Переписывание - преобразование формул в формальных системах.
- SECD-машина – виртуальная машина , предназначенная для лямбда-исчисления.
- Теорема Скотта – Карри - Теорема о множествах лямбда-членов.
- Посмеяться над пересмешником – Введение в комбинаторную логику
- Универсальная машина Тьюринга - формальная вычислительная машина, эквивалентная лямбда-исчислению.
- Unlambda – эзотерический функциональный язык программирования, основанный на комбинаторной логике.
Дальнейшее чтение [ править ]
- Абельсон, Гарольд и Джеральд Джей Сассман. Структура и интерпретация компьютерных программ . Массачусетский технологический институт Пресс . ISBN 0-262-51087-1 .
- Барендрегт, Хендрик Питер Введение в лямбда-исчисление .
- Барендрегт, Хендрик Питер, Влияние лямбда-исчисления на логику и информатику . Бюллетень символической логики, том 3, номер 2, июнь 1997 г.
- Барендрегт, Хендрик Питер, « Лямбда-исчисление без типов», стр. 1091–1132, из «Справочника по математической логике» , Северная Голландия (1977). ISBN 0-7204-2285-X
- Кардоне, Феличе и Хиндли, Дж. Роджер, 2006. История лямбда-исчисления и комбинаторной логики. Архивировано 6 мая 2021 г. в Wayback Machine . В книге Габбая и Вудса (ред.), «Справочник по истории логики» , том. 5. Эльзевир.
- Черч, Алонзо, Неразрешимая проблема элементарной теории чисел , Американский журнал математики , 58 (1936), стр. 345–363. Эта статья содержит доказательство того, что эквивалентность лямбда-выражений, вообще говоря, неразрешима.
- Черч, Алонсо (1941). Исчисления лямбда-конверсии . Принстон: Издательство Принстонского университета . Проверено 14 апреля 2020 г. ( ISBN 978-0-691-08394-0 )
- Фринк младший, Оррин (1944). «Обзор: Исчисления лямбда-преобразования Алонзо Чёрча» (PDF) . Бык. амер. Математика. Соц . 50 (3): 169–172. дои : 10.1090/s0002-9904-1944-08090-7 .
- Клини, Стивен, Теория положительных целых чисел в формальной логике , Американский журнал математики , 57 (1935), стр. 153–173 и 219–244. Содержит определения лямбда-исчисления нескольких знакомых функций.
- Ландин, Питер , Переписка между АЛГОЛом 60 и лямбда-нотацией Чёрча , Сообщения ACM , том. 8, нет. 2 (1965), страницы 89–101. Доступно на сайте ACM . Классическая статья, подчеркивающая важность лямбда-исчисления как основы языков программирования.
- Ларсон, Джим, Введение в лямбда-исчисление и схему . Небольшое введение для программистов.
- Майклсон, Грег (10 апреля 2013 г.). Введение в функциональное программирование с помощью лямбда-исчисления . Курьерская корпорация. ISBN 978-0-486-28029-5 . [41]
- Шалк А. и Симмонс Х. (2005) Введение в λ-исчисления и арифметику с достойным выбором упражнений . Заметки к курсу магистратуры по математической логике в Манчестерском университете.
- де Кейроз, Руи ЖГБ (2008). «О правилах редукции, значении как использовании и семантике теории доказательства». Студия Логика . 90 (2): 211–247. дои : 10.1007/s11225-008-9150-5 . S2CID 11321602 . Статья, дающая формальное обоснование идеи «значение есть использование», которая, даже если она основана на доказательствах, отличается от теоретико-доказательной семантики, как в традиции Даммета-Правица, поскольку она принимает редукцию в качестве правил, придающих смысл.
- Хэнкин, Крис, Введение в лямбда-исчисление для компьютерщиков, ISBN 0954300653
- Монографии/учебники для аспирантов
- Соренсен, Мортен Хейне и Уржичин, Павел (2006), Лекции по изоморфизму Карри – Ховарда , Elsevier, ISBN 0-444-52077-5 — это недавняя монография, которая охватывает основные темы лямбда-исчисления, от бестиповой разновидности до большинства типизированных лямбда-исчислений , включая более поздние разработки, такие как системы чистых типов и лямбда-куб . Он не охватывает расширения подтипов .
- Пирс, Бенджамин (2002), Типы и языки программирования , MIT Press, ISBN 0-262-16209-1 охватывает лямбда-исчисления с точки зрения практической системы типов; некоторые темы, такие как зависимые типы, только упоминаются, но подтипирование — важная тема.
- Документы
- Краткое введение в лямбда-исчисление - ( PDF ) Ахим Юнг
- Хронология лямбда-исчисления - ( PDF ) Даны Скотт
- Учебное пособие «Введение в лямбда-исчисление» - ( PDF ) Рауля Рохаса
- Конспект лекций по лямбда-исчислению - ( PDF ) Питера Селинджера
- Графическое лямбда-исчисление Мариуса Булиги
- «Лямбда-исчисление как модель рабочего процесса » Питера Келли, Пола Коддингтона и Эндрю Вендельборна; упоминает сокращение графа как распространенное средство оценки лямбда-выражений и обсуждает применимость лямбда-исчисления для распределенных вычислений (благодаря свойству Черча-Россера , которое обеспечивает параллельное сокращение графа для лямбда-выражений).
Примечания [ править ]
- ^ Эти правила создают такие выражения, как: . Круглые скобки можно опустить, если выражение однозначно. Для некоторых приложений могут быть включены термины для логических и математических констант и операций.
- ^ Перейти обратно: а б с д Барендрегт, Барендсен (2000) называют эту форму
- ^ Полную историю см. в книге Кардоне и Хиндли «История лямбда-исчисления и комбинаторной логики» (2006).
- ^ Перейти обратно: а б произносится как « карты на ».
- ^ Выражение e может быть: переменными x, лямбда-абстракциями или приложениями — в BNF, .— из Википедии « Просто типизированное лямбда-исчисление#Синтаксис для нетипизированного лямбда-исчисления»
- ^ иногда записывается в ASCII как
- ^ Лямбда-член представляет функцию написано анонимно.
- ^ свободные переменные в лямбда-нотации и ее исчислении сравнимы с линейной алгеброй и одноименными математическими понятиями.
- ^ Набор свободных переменных M, но с { x } удаленным
- ^ Объединение множества свободных переменных и набор свободных переменных [1]
- ^ (λ f . M ) N можно произносить как «пусть f будет N в M».
- ^ Ариола и Блом [26] использовать 1) аксиомы для репрезентативного исчисления с использованием правильно сформированных циклических лямбда-графов, расширенных с помощью letrec , чтобы обнаружить возможно бесконечное разматывание деревьев; 2) репрезентативное исчисление с β-редукцией лямбда-графов с ограниченной областью действия представляет собой циклическое расширение лямбда-исчисления Ариолы/Блома; 3) Ариола/Блом рассуждают о строгих языках, используя § вызов по значению , и сравнивают их с исчислением Могги и исчислением Хасэгавы. Выводы на стр. 111. [26]
Ссылки [ править ]
Некоторые части этой статьи основаны на материалах FOLDOC , используемых с разрешения .
- ^ Перейти обратно: а б с Барендрегт, Хенк ; Барендсен, Эрик (март 2000 г.), Введение в лямбда-исчисление (PDF)
- ^ явная замена в n Lab
- ^ Тьюринг, Алан М. (декабрь 1937 г.). «Вычислимость и λ-определимость». Журнал символической логики . 2 (4): 153–163. дои : 10.2307/2268280 . JSTOR 2268280 . S2CID 2317046 .
- ^ Коканд, Тьерри (8 февраля 2006 г.). Залта, Эдвард Н. (ред.). «Теория типов» . Стэнфордская энциклопедия философии (изд. лета 2013 г.) . Проверено 17 ноября 2020 г.
- ^ Муртгат, Майкл (1988). Категориальные исследования: логические и лингвистические аспекты исчисления Ламбека . Публикации Фориса. ISBN 9789067653879 .
- ^ Бунт, Гарри; Маскенс, Рейнхард, ред. (2008). Вычислительный смысл . Спрингер. ISBN 978-1-4020-5957-5 .
- ^ Митчелл, Джон К. (2003). Концепции языков программирования . Издательство Кембриджского университета. п. 57. ИСБН 978-0-521-78098-8 . .
- ^ Чакон Сартори, Камило (05 декабря 2023 г.). Введение в лямбда-исчисление с использованием Racket (технический отчет). Архивировано из оригинала 07 декабря 2023 г.
- ^ Пирс, Бенджамин К. Базовая теория категорий для специалистов по информатике . п. 53.
- ^ Черч, Алонзо (1932). «Набор постулатов для обоснования логики». Анналы математики . Серия 2. 33 (2): 346–366. дои : 10.2307/1968337 . JSTOR 1968337 .
- ^ Клини, Стивен С .; Россер, Дж. Б. (июль 1935 г.). «Непоследовательность некоторых формальных логик». Анналы математики . 36 (3): 630. дои : 10.2307/1968646 . JSTOR 1968646 .
- ^ Черч, Алонсо (декабрь 1942 г.). «Обзор Хаскелла Б. Карри, Несогласованность некоторых формальных логик ». Журнал символической логики . 7 (4): 170–171. дои : 10.2307/2268117 . JSTOR 2268117 .
- ^ Перейти обратно: а б Черч, Алонсо (1936). «Неразрешимая проблема элементарной теории чисел». Американский журнал математики . 58 (2): 345–363. дои : 10.2307/2371045 . JSTOR 2371045 .
- ^ Черч, Алонсо (1940). «Формулировка простой теории типов». Журнал символической логики . 5 (2): 56–68. дои : 10.2307/2266170 . JSTOR 2266170 . S2CID 15889861 .
- ^ Парти, BBH; тер Мейлен, А .; Уолл, RE (1990). Математические методы в лингвистике . Спрингер. 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 г.
- ^ «Основная грамматика лямбда-выражений» . Мягкий вариант .
Некоторые другие системы используют сопоставление для обозначения применения, поэтому «ab» означает «a@b». Это нормально, за исключением того, что требуется, чтобы переменные имели длину один, чтобы мы знали, что «ab» — это две переменные, расположенные рядом, а не одна переменная длины 2. Но мы хотим, чтобы метки типа «firstVariable» обозначали одну переменную, поэтому мы не можем использовать это соглашение о сопоставлении.
- ^ Перейти обратно: а б Селинджер, Питер (2008), Конспект лекций по лямбда-исчислению (PDF) , том. 0804, факультет математики и статистики, Оттавский университет, с. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S
- ^ де Кейрос, Руи ЖГБ (1988). «Теоретико-доказательное описание программирования и роли правил сокращения». Диалектика . 42 (4): 265–282. дои : 10.1111/j.1746-8361.1988.tb00919.x .
- ^ Турбак, Франклин; Гиффорд, Дэвид (2008), Концепции дизайна в языках программирования , MIT Press, стр. 251, ISBN 978-0-262-20175-9
- ↑ Люк Палмер (29 декабря 2010 г.) Haskell-cafe: Какова мотивация правил η?
- ^ Феллейзен, Матиас; Флатт, Мэтью (2006), Языки программирования и лямбда-исчисления (PDF) , стр. 26, заархивировано из оригинала (PDF) 5 февраля 2009 г .; В примечании (по состоянию на 2017 г.) в исходном месте предполагается, что авторы считают, что первоначально упомянутая работа была заменена книгой.
- ^ Перейти обратно: а б Зена М. Ариола и Стефан Блом, Proc. TACS '94 Сендай, Япония, 1997 (1997) Циклические лямбда-исчисления 114 страниц.
- ^ Кер, Эндрю Д. «Лямбда-исчисление и типы» (PDF) . п. 6 . Проверено 14 января 2022 г.
- ^ Дезани-Чианкаглини, Марианджола; Гилезан, Сильвия (2014). «Точность подтипирования типов пересечений и объединений» (PDF) . Переписывание и типизация лямбда-исчислений . Конспекты лекций по информатике. Том. 8560. с. 196. дои : 10.1007/978-3-319-08918-8_14 . hdl : 2318/149874 . ISBN 978-3-319-08917-1 . Проверено 14 января 2022 г.
- ^ Форстер, Янник; Смолка, Герт (август 2019 г.). «Лямбда-исчисление с вызовом по значению как модель вычислений в Coq» (PDF) . Журнал автоматизированного рассуждения . 63 (2): 393–413. дои : 10.1007/s10817-018-9484-2 . S2CID 53087112 . Проверено 14 января 2022 г.
- ^ Типы и языки программирования, с. 273, Бенджамин К. Пирс
- ^ Пирс, Бенджамин К. (2002). Типы и языки программирования . МТИ Пресс . п. 56. ИСБН 0-262-16209-1 .
- ^ Сестофт, Питер (2002). «Демонстрация сокращения лямбда-исчисления» (PDF) . Сущность вычислений . Конспекты лекций по информатике. Том. 2566. стр. 420–435. дои : 10.1007/3-540-36377-7_19 . ISBN 978-3-540-00326-7 . Проверено 22 августа 2022 г.
- ^ Берначка, Малгожата; Харатоника, Витольд; Драб, Томаш (2022). Андроник, июнь; де Моура, Леонардо (ред.). «Зоопарк стратегий сокращения лямбда-исчисления и Coq» (PDF) . 13-я Международная конференция по интерактивному доказательству теорем (ITP 2022) . 237 . Замок Дагштуль – Центр информатики Лейбница: 7:1–7:19. дои : 10.4230/LIPIcs.ITP.2022.7 . Проверено 22 августа 2022 г.
- ^ Франдсен, Гудмунд Сковбьерг; Стертивант, Карл (26 августа 1991 г.). «Какова эффективная реализация λ-исчисления?» . Языки функционального программирования и компьютерная архитектура: 5-я конференция ACM. Кембридж, Массачусетс, США, 26-30 августа 1991 г. Материалы . Конспекты лекций по информатике. Том. 523. Шпрингер-Верлаг. стр. 289–312. CiteSeerX 10.1.1.139.6913 . дои : 10.1007/3540543961_14 . ISBN 9783540543961 .
- ^ Сино, Ф.-Р. (2005). «Возвращение к строкам директора: общий подход к эффективному представлению свободных переменных при переписывании высшего порядка» (PDF) . Журнал логики и вычислений . 15 (2): 201–218. дои : 10.1093/logcom/exi010 .
- ^ Аккаттоли, Бениамино; Даль Лаго, Уго (14 июля 2014 г.). «Бета-редукция действительно инвариантна». Материалы совместного заседания двадцать третьей ежегодной конференции EACSL по логике компьютерных наук (CSL) и двадцать девятого ежегодного симпозиума ACM / IEEE по логике в компьютерных науках (LICS) . стр. 1–10. arXiv : 1601.01233 . дои : 10.1145/2603088.2603105 . ISBN 9781450328869 . S2CID 11485010 .
- ^ Перейти обратно: а б Аккаттоли, Бениамино (октябрь 2018 г.). «(Не)Модели эффективности и разумной стоимости» . Электронные заметки по теоретической информатике . 338 : 23–43. дои : 10.1016/j.entcs.2018.10.003 .
- ^ Перейти обратно: а б Асперти, Андреа (16 января 2017 г.). «Об эффективном сокращении лямбда-членов». arXiv : 1701.04240v1 [ cs.LO ].
- ^ Ландин, П.Дж. (1965). «Соответствие между АЛГОЛом 60 и лямбда-нотацией Чёрча» . Коммуникации АКМ . 8 (2): 89–101. дои : 10.1145/363744.363749 . S2CID 6505810 .
- ^ Скотт, Дана (1993). «Теоретико-типовая альтернатива ISWIM, CUCH, OWHY» (PDF) . Теоретическая информатика . 121 (1–2): 411–440. дои : 10.1016/0304-3975(93)90095-Б . Проверено 1 декабря 2022 г. Написано в 1969 году, широко распространено как неопубликованная рукопись.
- ^ «Домашняя страница Грега Майклсона» . Математические и компьютерные науки . Риккартон, Эдинбург: Университет Хериот-Ватт . Проверено 6 ноября 2022 г.
Внешние ссылки [ править ]
![](http://upload.wikimedia.org/wikipedia/en/thumb/4/4a/Commons-logo.svg/30px-Commons-logo.svg.png)
- Грэм Хаттон, Лямбда-исчисление , короткое (12 минут) компьютерное видео о лямбда-исчислении
- Хельмут Брандл, «Пошаговое введение в лямбда-исчисление»
- «Лямбда-исчисление» , Математическая энциклопедия , EMS Press , 2001 [1994]
- Дэвид К. Кинан, Препарировать пересмешника: графическое обозначение лямбда-исчисления с анимированной редукцией
- Л. Эллисон, Некоторые исполняемые примеры λ-исчисления
- Георг П. Лочевски, Лямбда-исчисление и A++
- Брет Виктор, « Яйца аллигатора: игра-головоломка, основанная на лямбда-исчислении»
- Лямбда-исчисление. Архивировано 14 октября 2012 г. на Wayback Machine на веб-сайте Safalra. Архивировано 2 мая 2021 г. на Wayback Machine.
- LCI Lambda Interpreter — простой, но мощный интерпретатор чистого исчисления.
- Ссылки на лямбда-исчисление на Lambda-the-Ultimate
- Майк Тайер, Lambda Animator , графический Java-апплет, демонстрирующий альтернативные стратегии сокращения.
- Реализация лямбда-исчисления с использованием шаблонов C++
- Шейн Стейнерт-Трелкельд, «Лямбда-исчисления» , Интернет-энциклопедия философии
- Антон Салихметов, Macro Lambda Calculus