Лямбда-исчисление

Лямбда-исчисление (также называемое λ -исчислением ) — это формальная система математической логики для выражения вычислений, основанных на абстракции функций и их применении переменных с использованием привязки и подстановки . Нетипизированное лямбда-исчисление, тема этой статьи, представляет собой универсальную модель вычислений , которую можно использовать для моделирования любой машины Тьюринга (и наоборот). Она была введена математиком Алонсо Чёрчем в 1930-х годах в рамках его исследования основ математики . В 1936 году Чёрч нашел формулировку, которая была логически последовательной , и задокументировал ее в 1940 году.

Лямбда-исчисление состоит из построения лямбда-членов и выполнения над ними операций сокращения . В простейшей форме лямбда-исчисления термы строятся с использованием только следующих правил:

1. ${\textstyle x}$: Переменная — это символ или строка, представляющая параметр.
2. ${\textstyle (\lambda x.M)}$: Лямбда-абстракция — это определение функции, принимающее в качестве входных данных связанную переменную. $x$ (между λ и точкой/точкой . ) и возврат тела ${\textstyle M}$.
3. ${\textstyle (M\ N)}$: Приложение , применяющее функцию ${\textstyle M}$ на спор ${\textstyle N}$. Оба ${\textstyle M}$ и ${\textstyle N}$ являются лямбда-термами.

К операциям сокращения относятся:

• ${\textstyle (\lambda x.M[x])\rightarrow (\lambda y.M[y])}$ : α-преобразование , переименование связанных переменных в выражении. Используется во избежание конфликтов имен .
• ${\textstyle ((\lambda x.M)\ N)\rightarrow (M[x:=N])}$ : β-редукция , замена связанных переменных выражением аргумента в теле абстракции.

Если используется индексация Де Брейна , то α-преобразование больше не требуется, поскольку не будет конфликтов имен. Если повторное применение шагов приведения в конечном итоге завершится, то по теореме Чёрча – Россера будет получена β-нормальная форма .

Имена переменных не нужны, если вы используете универсальную лямбда-функцию, такую ​​как Iota и Jot , которая может создавать любое поведение функции, вызывая ее в различных комбинациях.

Пояснения и приложения

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

Лямбда-исчисление может быть нетипизированным или типизированным . В типизированном лямбда-исчислении функции могут применяться только в том случае, если они способны принимать «тип» данных данного ввода. Типизированные лямбда-исчисления слабее , чем нетипизированные лямбда-исчисления, которые являются основной темой этой статьи, в том смысле, что типизированные лямбда-исчисления могут выражать меньше, чем нетипизированные лямбда-исчисления. С другой стороны, типизированные лямбда-исчисления позволяют доказать больше вещей. Например, в просто типизированном лямбда-исчислении существует теорема, согласно которой каждая стратегия вычисления завершается для каждого просто типизированного лямбда-терма, тогда как вычисление нетипизированных лямбда-термов не обязательно завершается (см. ниже ). Одной из причин, по которой существует множество различных типизированных лямбда-исчислений, является желание делать больше (из того, что может сделать нетипизированное исчисление), не отказываясь при этом от возможности доказать сильные теоремы об этом исчислении.

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

История

Лямбда-исчисление было введено математиком Алонзо Чёрчем в 1930-х годах как часть исследования основ математики . первоначальной системы была показана Логическая несостоятельность в 1935 году, когда Стивен Клини и Дж. Б. Россер разработали парадокс Клини-Россера .

Впоследствии, в 1936 году, Чёрч выделил и опубликовал только ту часть, которая имеет отношение к вычислениям, то, что сейчас называется нетипизированным лямбда-исчислением. В 1940 году он также представил более слабую в вычислительном отношении, но логически непротиворечивую систему, известную как просто типизированное лямбда-исчисление .

До 1960-х годов, когда была выяснена его связь с языками программирования, лямбда-исчисление было всего лишь формализмом. Благодаря приложениям Ричарда Монтегю и других лингвистов в области семантики естественного языка лямбда-исчисление начало занимать почетное место как в лингвистике, так и в лингвистике. и информатика.

Происхождение λ символа

Существует некоторая неопределенность относительно причины использования Чёрчем греческой буквы лямбда (λ) в качестве обозначения абстракции функции в лямбда-исчислении, возможно, отчасти из-за противоречивых объяснений самого Чёрча. По словам Кардоне и Хиндли (2006):

Кстати, почему Чёрч выбрал обозначение «λ»? В [неопубликованном письме Харальду Диксону от 1964 года] он ясно заявил, что оно произошло от обозначения « ${\hat {x}}$ для абстракции классов », использованный Уайтхедом и Расселом , сначала изменив « ${\hat {x}}$" к " $\land x$», чтобы отличить абстракцию функции от абстракции класса, а затем изменить « $\land$» на «λ» для удобства печати.

Об этом происхождении сообщалось также в [Россер, 1984, с.338]. С другой стороны, в более поздние годы своей жизни Чёрч сказал двум исследователям, что выбор был более случайным: нужен был символ, и случайно была выбрана λ.

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

Дорогой профессор Чёрч,

У Рассела был оператор йота , у Гильберта — оператор эпсилон . Почему вы выбрали лямбду в качестве своего оператора?

По словам Скотта, весь ответ Чёрча состоял в том, чтобы вернуть открытку со следующей пометкой: « Ини, мини, мини, мо ».

Неофициальное описание

Мотивация

Вычислимые функции являются фундаментальной концепцией в области информатики и математики. Лямбда-исчисление обеспечивает простую семантику вычислений, которая полезна для формального изучения свойств вычислений. Лямбда-исчисление включает в себя два упрощения, которые упрощают его семантику. Первое упрощение заключается в том, что лямбда-исчисление обрабатывает функции «анонимно»; он не дает им явных имен. Например, функция

$\operatorname {square\_sum} (x,y)=x^{2}+y^{2}$

можно переписать в анонимной форме как

$(x,y)\mapsto x^{2}+y^{2}$

(что читается кортеж x в и y отображается как « ${\textstyle x^{2}+y^{2}}$"). Аналогично, функция

$\operatorname {id} (x)=x$

можно переписать в анонимной форме как

$x\mapsto x$

где ввод просто сопоставляется сам с собой.

Второе упрощение заключается в том, что лямбда-исчисление использует только функции одного входа. Обычная функция, требующая два входа, например ${\textstyle \operatorname {square\_sum} }$ функция может быть переработана в эквивалентную функцию, которая принимает один входной сигнал и в качестве вывода возвращает другую функцию, которая, в свою очередь, принимает один входной сигнал. Например,

$(x,y)\mapsto x^{2}+y^{2}$

может быть переработан в

$x\mapsto (y\mapsto x^{2}+y^{2})$

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

Применение функции ${\textstyle \operatorname {square\_sum} }$ функцию на аргументы (5, 2), сразу дает

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\textstyle =29}$,

тогда как оценка каррированной версии требует еще одного шага

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$ // определение $x$ использовался с $5$ во внутреннем выражении. Это похоже на β-редукцию.

${\textstyle =5^{2}+2^{2}}$ // определение $y$ использовался с $2$. Опять же, аналогично β-редукции.

${\textstyle =29}$

чтобы прийти к тому же результату.

Лямбда-исчисление

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

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

Лямбда-термины

Синтаксис лямбда-исчисления определяет некоторые выражения как допустимые выражения лямбда-исчисления, а некоторые как недопустимые, точно так же, как некоторые строки символов являются допустимыми программами на языке C , а некоторые нет. Допустимое выражение лямбда-исчисления называется « лямбда-термом ».

Следующие три правила дают индуктивное определение , которое можно применить для построения всех синтаксически допустимых лямбда-термов:

• переменная x сама по себе является допустимым лямбда-термом.
• если t — лямбда-терм, а x — переменная, то $(\lambda x.t)$ — это лямбда-термин (называемый абстракцией );
• если t и s — лямбда-члены, то $(t$  $s)$ — это лямбда-термин (называемый приложением ).

Ничто иное не является лямбда-термом. То есть лямбда-терм действителен тогда и только тогда, когда его можно получить путем многократного применения этих трех правил. Для удобства некоторые круглые скобки при написании лямбда-терма можно опустить. Например, крайние круглые скобки обычно не пишутся. См. § Обозначения ниже, где подробно описано, какие круглые скобки являются необязательными. Также принято расширять представленный здесь синтаксис дополнительными операциями, что позволяет понять такие термины, как $\lambda x.x^{2}.$ В центре внимания этой статьи чистое лямбда-исчисление без расширений, но в пояснительных целях используются лямбда-термины, расширенные арифметическими операциями.

Абстракция ​ $\lambda x.t$ обозначает § анонимную функцию который принимает один входной сигнал x и возвращает t . Например, $\lambda x.(x^{2}+2)$ это абстракция, представляющая функцию $f$ определяется $f(x)=x^{2}+2,$ используя термин $x^{2}+2$ для т . Имя $f$ является излишним при использовании абстракции. Синтаксис $(\lambda x.t)$ связывает переменную x в терме t . Определение функции с абстракцией просто «настраивает» функцию, но не вызывает ее.

Приложение ​ $t$  $s$ представляет собой применение функции t к входу s , то есть представляет собой действие вызова функции t на входе s для получения $t(s)$.

Лямбда-терм может относиться к несвязанной переменной, например, к термину $\lambda x.(x+y)$ (который представляет собой определение функции $f(x)=x+y$). В этом термине переменная y не определена и считается неизвестной. Абстракция $\lambda x.(x+y)$ является синтаксически допустимым термином и представляет собой функцию, которая добавляет свои входные данные к еще неизвестному y .

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

1. $\lambda x.((\lambda x.x)x)$ имеет форму $\lambda x.B$ и поэтому является абстракцией, в то время как
2. $(\lambda x.(\lambda x.x))$ $x$ имеет форму $M$  $N$ и, следовательно, является приложением.

Примеры 1 и 2 обозначают разные термины, отличающиеся только расположением скобок. Они имеют разное значение: пример 1 — это определение функции, а пример 2 — применение функции. Лямбда-переменная x является заполнителем в обоих примерах.

Здесь пример 1 определяет функцию $\lambda x.B$, где $B$ является $(\lambda x.x)x$, анонимная функция $(\lambda x.x)$, с вводом $x$; а пример 2, $M$ $N$, применяется ли M к N, где $M$ это лямбда-терм $(\lambda x.(\lambda x.x))$ применяется ко входу $N$ который $x$. Оба примера 1 и 2 будут оцениваться как тождественная функция. $\lambda x.x$.

Функции, которые работают с функциями

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

Например, лямбда-терм $\lambda x.x$ представляет функцию идентичности , $x\mapsto x$. Дальше, $\lambda x.y$ представляет постоянную функцию $x\mapsto y$, функция, которая всегда возвращает $y$, независимо от ввода. В качестве примера функции, работающей с функциями, композицию функции можно определить как $\lambda f.\lambda g.\lambda x.(f(gx))$.

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

Альфа-эквивалентность

Базовой формой эквивалентности, определяемой с помощью лямбда-терминов, является альфа-эквивалентность . Он отражает интуитивное понимание того, что конкретный выбор связанной переменной в абстракции (обычно) не имеет значения. Например, $\lambda x.x$ и $\lambda y.y$ являются альфа-эквивалентными лямбда-терминами, и оба они представляют одну и ту же функцию (функцию идентичности). Условия $x$ и $y$ не являются альфа-эквивалентными, поскольку не связаны абстракцией. Во многих презентациях обычно идентифицируются альфа-эквивалентные лямбда-термины.

Для определения β-редукции необходимы следующие определения:

Свободные переменные

Свободные переменные термина — это переменные, не связанные абстракцией. Набор свободных переменных выражения определяется индуктивно:

• Свободные переменные $x$ просто $x$
• Набор переменных свободных $\lambda x.t$ представляет собой набор свободных переменных $t$, но с $x$ удаленный
• Набор переменных свободных $t$ $s$ является объединением множества свободных переменных $t$ и набор свободных переменных $s$.

Например, лямбда-терм, представляющий тождество $\lambda x.x$ не имеет свободных переменных, но функция $\lambda x.y$ $x$ имеет одну свободную переменную, $y$.

Замены, избегающие захвата

Предполагать $t$, $s$ и $r$ являются лямбда-термами, и $x$ и $y$ являются переменными. Обозначения $t[x:=r]$ указывает на замену $r$ для $x$ в $t$ способом , избегающим захвата . Это определяется так:

• $x[x:=r]=r$ ; с $r$ заменен на $x$, $x$ становится $r$
• $y[x:=r]=y$ если $x\neq y$ ; с $r$ заменен на $x$, $y$ (что не $x$) останки $y$
• $(t$ $s)[x:=r]=(t[x:=r])(s[x:=r])$ ; замена распространяется на обе стороны приложения
• $(\lambda x.t)[x:=r]=\lambda x.t$ ; переменная, связанная абстракцией, подстановке не подлежит; замена такой переменной оставляет абстракцию неизменной
• $(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])$ если $x\neq y$ и $y$ не появляется среди свободных переменных $r$ ( $y$ считается « свежим » для $r$) ; замена переменной, которая не связана абстракцией, происходит в теле абстракции, при условии, что абстрактная переменная $y$ является «свежим» на срок замены $r$.

Например, $(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x$, и $((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y$.

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

Например, замена, игнорирующая условие актуальности, может привести к ошибкам: $(\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x$. Эта ошибочная замена превратила бы постоянную функцию $\lambda x.y$ в личность $\lambda x.x$.

В общем, несоблюдение условия актуальности можно исправить сначала путем альфа-переименования с использованием подходящей свежей переменной. Например, возвращаясь к нашему правильному понятию замены, в $(\lambda x.y)[y:=x]$ абстракцию можно переименовать с помощью новой переменной $z$, чтобы получить $(\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x$, а смысл функции сохраняется при подстановке.

β-восстановление

Правило β-редукции утверждает, что приложение формы $(\lambda x.t)s$ сводится к сроку $t[x:=s]$. Обозначения $(\lambda x.t)s\to t[x:=s]$ используется, чтобы указать, что $(\lambda x.t)s$ β-редуцирует до $t[x:=s]$. Например, для каждого $s$, $(\lambda x.x)s\to x[x:=s]=s$. Это демонстрирует, что $\lambda x.x$ действительно это личность. Сходным образом, $(\lambda x.y)s\to y[x:=s]=y$, что демонстрирует, что $\lambda x.y$ является постоянной функцией.

Лямбда-исчисление можно рассматривать как идеализированную версию функционального языка программирования, такого как Haskell или Standard ML . С этой точки зрения β-редукция соответствует вычислительному шагу. Этот шаг можно повторять с помощью дополнительных β-сокращений до тех пор, пока не останется приложений для сокращения. В нетипизированном лямбда-исчислении, представленном здесь, этот процесс сокращения может не завершаться. Например, рассмотрим термин $\Omega =(\lambda x.xx)(\lambda x.xx)$. Здесь $(\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)$. То есть член сводится к самому себе за одно β-редукция, и поэтому процесс приведения никогда не завершится.

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

Формальное определение

Основная статья: Определение лямбда-исчисления

Определение

Лямбда-выражения состоят из:

• переменные v ₁ , v ₂ , ...;
• символы абстракции λ (лямбда) и . (точка);
• скобки ().

Набор лямбда-выражений Λ можно определить индуктивно :

1. Если x — переменная, то x ∈ Λ.
2. Если x переменная и M ∈ Λ, то ( λx.M — ) ∈ Λ.
3. Если M , N ∈ Λ, то ( MN ) ∈ Λ.

Экземпляры правила 2 известны как абстракции , а случаи правила 3 ​​— как приложения . См. § сокращаемое выражение.

Этот набор правил можно записать в форме Бэкуса-Наура следующим образом:

 <expression>  :== <abstraction> | <application> | <variable>
 <abstraction> :== λ <variable> . <expression>
 <application> :== ( <expression> <expression> )
 <variable>    :== v1 | v2 | ...

Обозначения

Чтобы не загромождать обозначение лямбда-выражений, обычно применяются следующие соглашения:

• Крайние круглые скобки опускаются: M N вместо ( M N ).
• Предполагается, что приложения левоассоциативны: можно писать M N P вместо (( M N ) P .
• переменные однобуквенные, пробел в приложениях можно опускать: MNP вместо MNP все Когда .
• Тело абстракции простирается насколько возможно вправо : λ x . MN означает λ x .( MN ), а не (λ x . M ) N .
• Последовательность абстракций сжимается: λ x .λ y .λ z . N сокращается как λ xyz . Н. ​

Свободные и связанные переменные

Говорят, что оператор абстракции λ связывает свою переменную, где бы она ни встречалась в теле абстракции. Переменные, попадающие в область абстракции, называются связанными . В выражении λ x . M , часть λ x часто называют связывающей что переменная x привязывается путем добавления λ x к M. , как намек на то , Все остальные переменные называются свободными . Например, в выражении λ y . xxy , y — связанная переменная, а x — свободная переменная. Также переменная связана с ближайшей к ней абстракцией. В следующем примере единственное вхождение x в выражение связано второй лямбдой: λ x . y (λ x . zx ).

Набор свободных переменных лямбда-выражения M обозначается как FV( M ) и определяется рекурсией структуры термов следующим образом:

1. FV( x ) = { x }, где x — переменная.
2. FV(λ x . M ) = FV ( M ) \ { x }.
3. FV( MN ) = FV( M )∪FV( N ).

Выражение, не содержащее свободных переменных, называется замкнутым . Закрытые лямбда-выражения также известны как комбинаторы и эквивалентны терминам комбинаторной логики .

Снижение

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

Существует три вида сокращения:

• α-преобразование : изменение связанных переменных;
• β-редукция : применение функций к их аргументам;
• η-редукция : которая отражает понятие экстенсиональности.

Мы также говорим о результирующих эквивалентностях: два выражения являются α-эквивалентными , если их можно α-преобразовать в одно и то же выражение. Аналогично определяются β-эквивалентность и η-эквивалентность.

Термин редекс , сокращение от сокращаемого выражения , относится к подтермам, которые можно сократить с помощью одного из правил сокращения. Например, (λ x . M ) N является β-редексом, выражающим замену N на x в M . Выражение, к которому сводится редекс, называется его редукцией ; сокращение (λ x . M ) N равно M [ x := N ].

Если x не свободен в M , λ x . M x также является η-редексом с редукцией M .

α-конверсия

α-конверсия ( альфа -конверсия), иногда известная как α-переименование, позволяет изменять имена связанных переменных. Например, α-преобразование λ 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 ₁ M ₂ )[ Икс := N ] знак равно М ₁ [ Икс := N ] M ₂ [ Икс := 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.

Можно рассматривать, что β-редукция — это то же самое, что и концепция локальной сводимости в естественной дедукции через изоморфизм Карри-Ховарда .

n-редукция

η-редукция ( эта -редукция) выражает идею экстенсиональности , в этом контексте две функции одинаковы тогда и только тогда, когда они дают одинаковый результат для всех аргументов. η-редукция преобразует λ 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 невозможно.)

Один из способов мышления о числительном Чёрча 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 н

Аналогично умножение можно определить как

MULT := λ м .λ п .λ ж . м ( н ж )

Альтернативно

MULT := λ м .λ п . м (ПЛЮС n ) 0

с момента умножения м и n — то же самое, что повторение добавления n функция m раз, а затем приравняв его к нулю. Возведение в степень имеет довольно простое представление цифрами Чёрча, а именно:

POW := λ б .λ е . е б

Функция-предшественник, определенная 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 .λ a .λ b . п а б

Теперь мы можем вычислять некоторые логические функции, например:

И ПРАВДА ЛОЖЬ

≡ (λ 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 с позволять . летрек конструкция позволит писать рекурсивные определения функций.

Рекурсия и фиксированные точки

Основная статья: Комбинатор с фиксированной точкой

См. Также: Комбинаторное исчисление SKI § Самостоятельное применение и рекурсия.

Рекурсия — это определение функции с использованием самой функции. Определение, содержащее себя внутри себя по значению, приводит к тому, что все значение имеет бесконечный размер. Другие нотации, поддерживающие рекурсию, преодолевают эту проблему, ссылаясь на определение функции по имени . Лямбда-исчисление не может выразить это: все функции в лямбда-исчислении анонимны, поэтому мы не можем ссылаться по имени на значение, которое еще предстоит определить, внутри лямбда-терма, определяющего это же значение. Однако лямбда-выражение может принимать себя в качестве собственного аргумента, например в (λ Икс . Икс Икс ) 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 , каждая рекурсивно определенная функция может быть выражена как лямбда-выражение. В частности, теперь мы можем четко рекурсивно определить предикаты вычитания, умножения и сравнения натуральных чисел.

Стандартные условия

Некоторые термины имеют общепринятые названия:

Я := λ Икс . х

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, определенные выше, обычно сокращаются как Т и Ф. ​

Устранение абстракции

Основная статья: Комбинаторная логика § Полнота базиса SK

Если 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 .

Типизированное лямбда-исчисление

Основная статья: Типизированное лямбда-исчисление

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

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

Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри-Говарда , и их можно рассматривать как внутренний язык классов категорий , например, просто типизированное лямбда-исчисление является языком декартовых замкнутых категорий (CCC).

Стратегии сокращения

Основная статья: Стратегия редукции § Лямбда-исчисление

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

Нормальный заказ

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

Приказы о применении

Первым сокращается самый левый и самый внутренний редекс. Как следствие, аргументы функции всегда сокращаются перед их подстановкой в ​​функцию. В отличие от нормального приведения порядка, аппликативное приведение порядка может не найти бета-нормальную форму выражения, даже если такая нормальная форма существует. Например, термин $(\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)$ сводится к себе аппликативным порядком, тогда как нормальный порядок сводит его к бета-нормальной форме. $y$.

Полное β-снижение

Любой редекс можно уменьшить в любой момент. По сути, это означает отсутствие какой-либо конкретной стратегии сокращения — что касается сокращаемости, «все ставки сделаны».

Стратегии слабой редукции не приводят к лямбда-абстракциям:

Вызов по значению

Подобен аппликативному порядку, но внутри абстракций никакие сокращения не выполняются. Это похоже на порядок вычислений в строгих языках, таких как C: аргументы функции оцениваются перед вызовом функции, а тела функции даже частично не оцениваются, пока аргументы не будут заменены.

Звонок по имени

Как обычный порядок, но внутри абстракций сокращения не выполняются. Например, λ x .(λ y . y ) x находится в нормальной форме согласно этой стратегии, хотя и содержит редекс (λ y . y ) x .

Стратегии совместного использования сокращают количество «одинаковых» параллельных вычислений:

Оптимальное сокращение

Как в обычном порядке, но вычисления с одинаковой меткой сокращаются одновременно.

Звонок по необходимости

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

Вычислимость

Не существует алгоритма, который принимал бы в качестве входных данных любые два лямбда-выражения и выходные данные. ИСТИНА или ЛОЖЬ в зависимости от того, сводится ли одно выражение к другому. Точнее, никакая вычислимая функция не может решить этот вопрос. Исторически это была первая проблема, неразрешимость которой удалось доказать. Как обычно для такого доказательства, вычислимое означает вычислимое с помощью любой модели вычислений , полной по Тьюрингу . Фактически вычислимость сама по себе может быть определена с помощью лямбда-исчисления: функция F : N → N натуральных чисел является вычислимой функцией тогда и только тогда, когда существует лямбда-выражение f такое, что для каждой пары x , y в N , F ( x )= y тогда и только тогда, когда f х = _б  й , где х и y — цифры Чёрча , соответствующие x и y соответственно, и = _β, что означает эквивалентность с β-редукцией. см . в тезисе Чёрча-Тьюринга. Другие подходы к определению вычислимости и их эквивалентности

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

Сложность

Понятие вычислительной сложности лямбда-исчисления немного сложное, поскольку стоимость β-сокращения может варьироваться в зависимости от того, как оно реализовано. Точнее, нужно каким-то образом найти расположение всех вхождений связанной переменной. В в выражении E , подразумевая временные затраты, или необходимо каким-то образом отслеживать расположение свободных переменных, подразумевая пространственные затраты. Наивный поиск местоположений и В E равно O ( n ) длины n ​ Э. ​ Строки-директора были ранним подходом, в котором временные затраты были заменены квадратичным использованием пространства. В более общем плане это привело к изучению систем, использующих явную замену .

В 2014 году было показано, что количество шагов β-редукции, предпринимаемых при сокращении нормального порядка для уменьшения члена, является разумной моделью временных затрат, то есть сокращение можно смоделировать на машине Тьюринга за время, полиномиально пропорциональное числу шаги. Это была давняя открытая проблема из-за взрыва размеров , существования лямбда-членов, размер которых растет экспоненциально для каждого β-сокращения. Результат позволяет обойти эту проблему, работая с компактным общим представлением. Результат ясно показывает, что объем памяти, необходимый для вычисления лямбда-члена, не пропорционален размеру термина во время сокращения. В настоящее время неизвестно, какой будет хорошая мера сложности пространства.

Необоснованная модель не обязательно означает неэффективную. Оптимальное сокращение сокращает все вычисления с одной и той же меткой за один шаг, избегая дублирования работы, но количество параллельных шагов β-редукции для приведения данного термина к нормальной форме примерно линейно по размеру термина. Это слишком мало, чтобы быть разумной мерой затрат, поскольку любая машина Тьюринга может быть закодирована в лямбда-исчислении с размером, линейно пропорциональным размеру машины Тьюринга. Истинная стоимость сокращения лямбда-членов связана не с β-редукцией как таковой, а скорее с управлением дублированием редексов во время β-редукции. Неизвестно, являются ли оптимальные реализации приведения разумными при измерении по отношению к разумной модели затрат, такой как количество крайних левых шагов к нормальной форме, но для фрагментов лямбда-исчисления было показано, что алгоритм оптимального приведения эффективен. и имеет не более квадратичных издержек по сравнению с крайним левым и крайним. Кроме того, реализация оптимального сокращения на прототипе BOHM превзошла как Caml Light , так и Haskell по чистым лямбда-выражениям.

Лямбда-исчисление и языки программирования

Как указано в статье Питера Ландина 1965 года «Соответствие между АЛГОЛом 60 и лямбда-нотацией Чёрча», Языки последовательного процедурного программирования можно понимать с точки зрения лямбда-исчисления, которое обеспечивает основные механизмы процедурной абстракции и применения процедур (подпрограмм).

Анонимные функции

Основная статья: Анонимная функция

Например, в Python функцию «квадрат» можно выразить как лямбда-выражение следующим образом:

(lambda x: x**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 , можно найти с требуемым свойством, тем самым предоставив модель для лямбда-исчисления.

Эта работа также легла в основу денотационной семантики языков программирования.

Вариации и расширения

Эти расширения находятся в лямбда-кубе :

• Типизированное лямбда-исчисление - лямбда-исчисление с типизированными переменными (и функциями).
• Система 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 .
• Шалк А. и Симмонс Х. (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 ) Питера Селинджера
• Графическое лямбда-исчисление Мариуса Булиги
• «Лямбда-исчисление как модель рабочего процесса» Питера Келли, Пола Коддингтона и Эндрю Вендельборна; упоминает сокращение графа как распространенное средство оценки лямбда-выражений и обсуждает применимость лямбда-исчисления для распределенных вычислений (благодаря свойству Черча-Россера , которое обеспечивает параллельное сокращение графа для лямбда-выражений).

Ссылки

Некоторые части этой статьи основаны на материалах FOLDOC , используемых с разрешения .

Внешние ссылки

• Грэм Хаттон, Лямбда-исчисление , короткое (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