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

редактировать
Формальная система в математической логике

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

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

СинтаксисИмяОписание
xПеременнаяСимвол или строка, представляющая параметр или математическое / логическое значение.
(λx.M)АбстракцияОпределение функции (M - это лямбда-термин). Переменная x становится связанной в выражении.
(M N)ПриложениеПрименение функции к аргументу. M и N - лямбда-термины.

, создавая такие выражения, как: (λx.λy. (λz. (Λx.z x) (λy.z y)) (x y)). Скобки можно опустить, если выражение однозначно. Для некоторых приложений могут быть включены термины для логических и математических констант и операций.

Операции сокращения включают:

ОперацияИмяОписание
(λx.M [x]) → (λy.M [y])α-преобразованиеПереименование связанных переменных в выражении. Используется для предотвращения конфликтов имен .
((λx.M) E) → (M [x: = E])β-редукцияЗамена связанных переменных на выражение аргумента в теле абстракции.

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

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

Содержание

  • 1 Объяснение и применение
  • 2 История
    • 2.1 Происхождение лямбда-символа
  • 3 Неформальное описание
    • 3.1 Мотивация
    • 3.2 Лямбда-исчисление
      • 3.2.1 Лямбда термины
      • 3.2.2 Функции, которые работают с функциями
      • 3.2.3 Альфа-эквивалентность
      • 3.2.4 Свободные переменные
      • 3.2.5 Подстановки без захвата
      • 3.2.6 β-редукция
  • 4 Формальное определение
    • 4.1 Определение
    • 4.2 Обозначение
    • 4.3 Свободные и связанные переменные
  • 5 Редукция
    • 5.1 α-преобразование
      • 5.1.1 Замена
    • 5.2 β-редукция
    • 5.3 η-сокращение
  • 6 Нормальные формы и слияние
  • 7 Кодирование типов данных
    • 7.1 Арифметика в лямбда-исчислении
    • 7.2 Логика и предикаты
    • 7.3 Пары
  • 8 Дополнительные методы программирования
    • 8.1 Именованные константы
    • 8.2 Рекурсия и фиксированные точки
    • 8.3 Стандартные термины
    • 8.4 Устранение абстракции
  • 9 Типизированное лямбда-исчисление
  • 10 Вычислимые функции и лямбда-исчисление
  • 11 Неразрешимость эквивалентности
  • 12 Лямбда-исчисление и программирование LAN guages ​​
    • 12.1 Анонимные функции
    • 12.2 Стратегии сокращения
    • 12.3 Замечание о сложности
    • 12.4 Параллелизм и параллелизм
    • 12.5 Оптимальное сокращение
  • 13 Семантика
  • 14 Варианты и расширения
  • 15 См. Также
  • 16 Ссылки
  • 17 Дополнительная литература
  • 18 Внешние ссылки

Объяснение и приложения

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

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

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

История

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

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

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

Происхождение символа лямбда.

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

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

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

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

Уважаемый профессор Черч,

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

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

Неформальное описание

Мотивация

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

квадрат _ сумма ⁡ (x, y) = x 2 + y 2 {\ displaystyle \ operatorname {square \ _sum} (x, y) = x ^ {2} + y ^ {2} }{\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}

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

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

(читается как "кортеж x и y отображается в x 2 + y 2 {\ textstyle x ^ {2} + y ^ {2}}{\textstyle x^{2}+y^{2}}"). Точно так же

id ⁡ (x) = x {\ displaystyle \ operatorname {id} (x) = x}\operatorname {id} (x)=x

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

x ↦ x {\ displaystyle x \ mapsto x}x \mapsto x

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

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

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

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

x ↦ (y ↦ x 2 + y 2) {\ displaystyle x \ mapsto (y \ mapsto x ^ {2} + y ^ {2})}{\displaystyle x\mapsto (y\mapsto x^{2}+y^{2})}

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

Применение функции функции square _ sum {\ textstyle \ operatorname {square \ _sum}}{\textstyle \operatorname {square\_sum} }к аргументам (5, 2) сразу возвращает

( (Икс, Y) ↦ Икс 2 + Y 2) (5, 2) {\ textstyle ((x, y) \ mapsto x ^ {2} + y ^ {2}) (5,2)}{\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}
= 5 2 + 2 2 {\ textstyle = 5 ^ {2} + 2 ^ {2}}{\textstyle =5^{2}+2^{2}}
= 29 {\ textstyle = 29}{\textstyle =29},

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

(( Икс ↦ (Y ↦ Икс 2 + Y 2)) (5)) (2) {\ textstyle {\ Bigl (} {\ bigl (} x \ mapsto (y \ mapsto x ^ {2} + y ^ {2})) {\ bigr)} (5) {\ Bigr)} (2)}{\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr)}(5){\Bigr)}(2)}
= (y ↦ 5 2 + y 2) (2) {\ textstyle = (y \ mapsto 5 ^ {2} + y ^ {2}) (2)}{\textstyle =(y\mapsto 5^{2}+y^{2})(2)}// определение x {\ displaystyle x}xбыло использовано с 5 {\ displaystyle 5}5во внутреннем выражении. Это похоже на β-редукцию.
= 5 2 + 2 2 {\ textstyle = 5 ^ {2} + 2 ^ {2}}{\textstyle =5^{2}+2^{2}}// определение y {\ displaystyle y}yиспользовался с 2 {\ displaystyle 2}2. Опять же, аналогично β-редукции.
= 29 {\ textstyle = 29}{\textstyle =29}

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

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

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

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

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

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

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

  • переменная, x {\ displaystyle x}x, сам по себе является допустимым лямбда-термином
  • , если t {\ displaystyle t}tявляется лямбда-термином, а x {\ displaystyle x}x- переменная, тогда (λ x. T) {\ displaystyle (\ lambda xt)}(\lambda x.t)- лямбда-термин (называемый абстракцией );
  • , если t {\ displaystyle t}tи s {\ displaystyle s}s- лямбда-термины, тогда (ts) {\ displaystyle (ts)}(ts)- это лямбда-термин (называемый приложением ).

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

Абстракция λ x. t {\ di splaystyle \ lambda xt}\lambda x.t- это определение анонимной функции, которая способна принимать один ввод x {\ displaystyle x}xи подставлять его в выражение т {\ Displaystyle т}t. Таким образом, он определяет анонимную функцию, которая принимает x {\ displaystyle x}xи возвращает t {\ displaystyle t}t. Например, λ x. x 2 + 2 {\ displaystyle \ lambda xx ^ {2} +2}\lambda x.x^{2}+2- абстракция для функции f (x) = x 2 + 2 {\ displaystyle f (x) = x ^ {2} +2}f(x)=x^{2}+2с использованием термина x 2 + 2 {\ displaystyle x ^ {2} +2}x^{2}+2для t {\ displaystyle t}t. Определение функции с абстракцией просто «устанавливает» функцию, но не вызывает ее. Абстракция связывает переменную x {\ displaystyle x}xв термине t {\ displaystyle t}t.

с приложением ts {\ displaystyle ts}tsпредставляет применение функции t {\ displaystyle t}tк входу s {\ displaystyle s}s, то есть он представляет собой акт вызова функции t {\ displaystyle t}tна входе s {\ displaystyle s}sдля создания t (s) {\ displaystyle t (s)}t(s).

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

скобки могут использоваться и могут быть необходимы для устранения неоднозначности терминов. Например, λ x. ((λ x. x) x) {\ displaystyle \ lambda x. ((\ lambda xx) x)}\lambda x.((\lambda x.x)x)и (λ x. (λ x. x)) x {\ displaystyle (\ lambda x. (\ lambda xx)) x}(\lambda x.(\lambda x.x))xобозначают разные термины (хотя они по совпадению сводятся к одному и тому же значению). Здесь в первом примере определяется функция, лямбда-член которой является результатом применения x к дочерней функции, а второй пример - это применение самой внешней функции к входу x, который возвращает дочернюю функцию. Следовательно, оба примера оцениваются как функция идентичности λ x. x {\ displaystyle \ lambda xx}\lambda x.x.

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

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

Например, λ x. x {\ displaystyle \ lambda xx}\lambda x.xпредставляет функцию идентичности, x ↦ x {\ displaystyle x \ mapsto x}x \mapsto xи (λ x. x) y {\ displaystyle (\ lambda xx) y}(\lambda x.x)yпредставляет функцию идентичности, применяемую к y {\ displaystyle y}y. Кроме того, (λ x. Y) {\ displaystyle (\ lambda xy)}(\lambda x.y)представляет постоянную функцию x ↦ y {\ displaystyle x \ mapsto y}{\displaystyle x\mapsto y}, функция, которая всегда возвращает y {\ displaystyle y}y, независимо от ввода. В лямбда-исчислении приложение функции рассматривается как левоассоциативное, так что stx {\ displaystyle stx}stxозначает (st) x {\ displaystyle (st) x}(st)x.

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

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

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

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

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

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

  • Свободные переменные x {\ displaystyle x}xравны всего x {\ displaystyle x}x
  • Набор свободных переменных λ x. t {\ displaystyle \ lambda xt}\lambda x.tпредставляет собой набор свободных переменных t {\ displaystyle t}t, но с x {\ displaystyle x}xудалено
  • Набор свободных переменных ts {\ displaystyle ts}tsпредставляет собой объединение набора свободных переменных t {\ displaystyle t }tи набор свободных переменных s {\ displaystyle s}s.

Например, лямбда-член, представляющий идентичность λ x. x {\ displaystyle \ lambda x.x}\lambda x.xне имеет свободных переменных, но функция λ x. yx {\ displaystyle \ lambda x.yx}{\displaystyle \lambda x.yx}имеет одну свободную переменную, y {\ displaystyle y}y.

подстановки без захвата

Предположим t { \ displaystyle t}t, s {\ displaystyle s}sи r {\ displaystyle r}r- лямбда-термины, а x {\ displaystyle x}xи y {\ displaystyle y}y- переменные. Обозначение t [x: = r] {\ displaystyle t [x: = r]}t[x:=r]указывает на замену r {\ displaystyle r}rна <255.>x {\ displaystyle x}xв t {\ displaystyle t}tспособом, исключающим захват. Это определяется так:

  • x [x: = r] = r {\ displaystyle x [x: = r] = r}x[x:=r]=r;
  • y [x: = r] = y {\ displaystyle y [x: = r] = y}y[x:=r]=yесли x ≠ y {\ displaystyle x \ neq y}x\neq y;
  • (ts) [x: = r] = (t [x: = r]) ( s [x: = r]) {\ displaystyle (ts) [x: = r] = (t [x: = r]) (s [x: = r])}(ts)[x:=r]=(t[x:=r])(s[x:=r]);
  • (λ x. t) [ х: = г] = λ х. t {\ displaystyle (\ lambda x.t) [x: = r] = \ lambda x.t}(\lambda x.t)[x:=r]=\lambda x.t;
  • (λ y. t) [x: = r] = λ y. (t [x: = r]) {\ displaystyle (\ lambda yt) [x: = r] = \ lambda y. (t [x: = r])}(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])если x ≠ y {\ displaystyle x \ neq y}x\neq yи y {\ displaystyle y}yне входит в свободные переменные r {\ displaystyle r}r. Переменная y {\ displaystyle y}yназывается «свежей» для r {\ displaystyle r}r.

Например, (λ x. X) [ у: = у] = λ х. (x [y: = y]) = λ x. x {\ displaystyle (\ lambda xx) [y: = y] = \ lambda x. (x [y: = y]) = \ lambda xx}(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.xи ((λ x. y) x) [x: = y] = ((λ x. y) [x: = y]) (x [x: = y]) = (λ x. y) y {\ displaystyle ((\ lambda xy) x) [x: = y] = ((\ lambda xy) [x: = y]) (x [x: = y]) = (\ lambda xy) y}((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y.

Условие свежести (требующее, чтобы y {\ displaystyle y}yне входит в свободные переменные r {\ displaystyle r}r) имеет решающее значение для гарантии того, что подстановка не изменит значение функций. Например, выполняется подстановка, игнорирующая условие свежести: (λ x. Y) [y: = x] = λ x. (y [y: = x]) = λ x. x {\ displaystyle (\ lambda x.y) [y: = x] = \ lambda x. (y [y: = x]) = \ lambda x.x}(\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x. Эта подстановка превращает постоянную функцию λ x. y {\ displaystyle \ lambda x.y}\lambda x.yв тождество λ x. x {\ displaystyle \ lambda x.x}\lambda x.xпутем подстановки.

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

β-редукция

Правило β-редукции утверждает, что приложение формы (λ x. T) s {\ displaystyle (\ lambda xt) s}(\lambda x.t)sсводится к термину t [x: = s] {\ displaystyle t [x: = s]}t[x:=s]. Обозначение (λ x. T) s → t [x: = s] {\ displaystyle (\ lambda xt) s \ to t [x: = s]}(\lambda x.t)s\to t[x:=s]используется для обозначения того, что (λ x. T) s {\ displaystyle (\ lambda xt) s}(\lambda x.t)sβ-уменьшает до t [x: = s] {\ displaystyle t [x: = s] }t[x:=s]. Например, для каждого s {\ displaystyle s}s, (λ x. X) s → x [x: = s] = s {\ displaystyle (\ lambda xx) s \ to x [x: = s] = s}(\lambda x.x)s\to x[x:=s]=s. Это показывает, что λ x. x {\ displaystyle \ lambda x.x}\lambda x.xна самом деле идентичность. Аналогично, (λ x. Y) s → y [x: = s] = y {\ displaystyle (\ lambda xy) s \ to y [x: = s] = y}(\l ambda x.y)s\to y[x:=s]=y, что показывает, что λ x. y {\ displaystyle \ lambda x.y}\lambda x.y- постоянная функция.

Лямбда-исчисление можно рассматривать как идеализированную версию функционального языка программирования, такого как Haskell или Standard ML. С этой точки зрения β-редукция соответствует вычислительному шагу. Этот шаг можно повторять путем дополнительных β-редукций до тех пор, пока не останется больше приложений для уменьшения. В нетипизированном лямбда-исчислении, представленном здесь, этот процесс редукции не может завершиться. Например, рассмотрим термин Ω = (λ x. Xx) (λ x. Xx) {\ displaystyle \ Omega = (\ lambda x.xx) (\ lambda x.xx)}\Omega =(\lambda x.xx)(\lambda x.xx). Здесь (λ x. X x) (λ x. X x) → (x x) [x: = λ x. хх] знак равно (х [х: = λ х. хх]) (х [х: = λ х. хх]) = (λ х. хх) (λ х. хх) {\ displaystyle (\ 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)}(\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 1, v 2,...;
  • символы абстракции λ (лямбда) и. (точка);
  • круглые скобки ().

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

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

Известны экземпляры правила 2 поскольку абстракции и экземпляры правила 3 ​​известны как приложения.

Обозначение

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

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

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

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

Набор свободных переменных лямбда-выражения, 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.y. Термины, отличающиеся только α-преобразованием, называются α-эквивалентными. Часто при использовании лямбда-исчисления α-эквивалентные термины считаются эквивалентными.

Точные правила α-преобразования не совсем тривиальны. Во-первых, при α-преобразовании абстракции переименовываются только вхождения переменных, которые связаны с той же абстракцией. Например, α-преобразование λx.λx.x может привести к λy.λx.x, но не может привести к λy.λx.y. Последний имеет значение, отличное от оригинала. Это аналогично программному понятию затенения переменных.

Во-вторых, α-преобразование невозможно, если оно приведет к захвату переменной другой абстракцией. Например, если мы заменим x на y в λx.λy.x, мы получим λy.λy.y, что совсем не то же самое.

В языках программирования со статической областью видимости можно использовать α-преобразование для упрощения разрешения имен, гарантируя, что никакое имя переменной не маскирует имя в содержащем scope (см. α-переименование, чтобы сделать разрешение имен тривиальным ).

В нотации индекса Де Брейна любые два α-эквивалента термина синтаксически идентичны.

Подстановка

Подстановка, записанная M [V: = N], - это процесс замены всех свободных вхождений переменной V в выражении M выражением N. Подстановка в терминах лямбда исчисление определяется рекурсией по структуре терминов следующим образом (примечание: x и y - только переменные, а M и N - любое лямбда-выражение):

x [x: = N] = N
y [x: = N] = y, если x ≠ y
(M1M2) [x: = N] = (M 1 [x: = N]) (M 2 [x: = N])
(λx.M) [x: = N] = λx.M
(λy.M) [x: = N] = λy. (M [x: = N]), если x ≠ y и y ∉ FV (N)

Для замены в абстракцию иногда необходимо α-преобразовать выражение. Например, неверно для (λx.y) [y: = x] приводить к λx.x, потому что замененный x должен был быть свободным, но в итоге оказался связанным. Правильная подстановка в этом случае - λz.x с точностью до α-эквивалентности. Подстановка определяется однозначно с точностью до α-эквивалентности.

β-редукция

β-редукция отражает идею применения функции. β-редукция определяется в терминах замещения: β-редукция (λV.M) N равна M [V: = N].

Например, предполагая некоторое кодирование 2, 7, ×, мы имеем следующую β-редукцию: (λn.n × 2) 7 → 7 × 2.

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

η-редукция

η-редукция выражает идею расширяемость, которая в этом контексте состоит в том, что две функции являются одинаковыми тогда и только тогда, когда они дают одинаковый результат для всех аргументов. η-редукция преобразует λx.f x в f, если x не появляется свободным в f.

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

Нормальные формы и слияние

Для нетипизированного лямбда-исчисления β-редукция как правило перезаписи не является ни строго нормализующим, ни слабо нормализующим.

. Однако можно показать, что β -редукция сливается при работе до α-преобразования (т.е. мы считаем две нормальные формы равными, если возможно α-преобразовать одну в другую).

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

Типы данных кодирования

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

Арифметика в лямбда-исчислении

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

0: = λf.λx.x
1: = λf.λx.fx
2: = λf.λx.f (fx)
3 : = λf.λx.f (f (fx))

и так далее. Или используя альтернативный синтаксис, представленный выше в Нотации :

0: = λfx.x
1: = λfx.fx
2: = λfx.f (fx)
3: = λfx. f (f (fx))

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

Односторонний Цифра Чёрча n, которая часто бывает полезна при анализе программ, воспринимается как инструкция «повторить n раз». Например, используя функции PAIRи NIL, определенные ниже, можно определить функцию, которая создает (связанный) список из n элементов, все равные x, повторяя 'добавить еще один элемент x n раз, начиная с пустого списка. Лямбда-член имеет вид

λn.λx.n (PAIR x) NIL

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

Мы можем определить функцию-преемник, которая принимает число Чёрча nи возвращает n + 1, добавляя другое приложение f, где '(mf) x' означает, что функция 'f' применяется 'm' раз к 'x':

SUCC: = λn.λf.λx.f (nfx)

Поскольку m-я композиция f, составленная из n-й композиции f, дает m + n-ю композицию f, сложение можно определить следующим образом:

PLUS: = λm.λn.λf.λx.mf (nfx)

PLUSможно рассматривать как функцию, принимающую два натуральных числа как аргументы и возвращение натурального числа; можно проверить, что

PLUS 2 3

и

5

являются β-эквивалентными лямбда-выражениями. Поскольку добавление mк числу nможет быть выполнено путем добавления 1 mраз, альтернативное определение:

PLUS: = λm.λn.m SUCC n

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

MULT: = λm.λn.λf.m (nf)

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

MULT: = λm.λn.m (PLUS n) 0

, поскольку умножение mи nаналогично повторению функции add nmраз с последующим применением к нулю. Возведение в степень имеет довольно простую визуализацию в числах Чёрча, а именно

POW: = λb.λe.eb

Функция-предшественник, определенная как PRED n = n - 1для положительного целого числа nи PRED 0 = 0значительно сложнее. Формулу

PRED: = λn.λf.λx.n (λg.λh.h (gf)) (λu.x) (λu.u)

можно проверить, индуктивно показывая, что если T означает (λg.λh.h (gf)), тогда T (λu.x) = (λh.h (f (x)))для n>0. Два других определения PREDприведены ниже, в одном используются условные выражения, а в другом - пары. С функцией-предшественником вычитание выполняется просто. Определение

SUB: = λm.λn.n PRED m,

SUB mnдает m - n, когда m>nи 0в противном случае.

Логика и предикаты

По соглашению следующие два определения (известные как логические значения Черча) используются для логических значений TRUEи FALSE:

TRUE : = λx.λy.x
ЛОЖЬ: = λx.λy.y
(Обратите внимание, что ЛОЖЬэквивалентно нулю Черча, определенному выше)

Затем с этими двумя лямбдами термины, мы можем определить некоторые логические операторы (это всего лишь возможные формулировки; другие выражения также верны):

И: = λp.λq.pqp
ИЛИ: = λp.λq.ppq
НЕ: = λp.p FALSE TRUE
IFTHENELSE: = λp.λa.λb.pab

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

AND TRUE FALSE
≡ (λp.λq.pqp) TRUE FALSE → β TRUE FALSE TRUE
≡ (λx.λy.x) FALSE TRUE → β FALSE

и мы видим, что AND TRUE FALSEэквивалентно FALSE.

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

ISZERO: = λn.n (λx.FALSE) TRUE

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

LEQ: = λm.λn.ISZERO (SUB mn),

и поскольку m = n, если LEQ m nи LEQ n m, легко построить предикат для числового равенства.

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

PRED: = λn.n (λg.λk.ISZERO (g 1) k (PLUS (gk) 1)) (λv.0) 0

, что может проверить, индуктивно показав, что n (λg.λk.ISZERO (g 1) k (PLUS (gk) 1)) (λv.0)является функцией сложения n- 1 для n>0.

Пары

Пара (2-кортеж) может быть определена в терминах ИСТИНАи ЛОЖЬ, используя кодировку Чёрча для пар. Например, PAIRинкапсулирует пару (x,y), FIRSTвозвращает первый элемент пары, а SECONDвозвращает второй.

PAIR: = λx.λy.λf.fxy
FIRST: = λp.p TRUE
ВТОРОЙ: = λp.p FALSE
NIL: = λx.TRUE
NULL: = λp. p (λx.λy.FALSE)

Связанный список может быть определен либо как NIL для пустого списка, либо как PAIRэлемента и меньшего списка. Предикат NULLпроверяет значение NIL. (В качестве альтернативы, с NIL: = FALSEконструкция l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil)устраняет необходимость в явном NULL-тесте).

В качестве примера использования пар функция сдвига и увеличения, которая отображает (m, n)в (n, n + 1), может быть определено как

Φ: = λx.PAIR (SECOND x) (SUCC (SECOND x))

, что позволяет нам дать, пожалуй, наиболее прозрачную версию функции-предшественника:

PRED: = λn.FIRST (n Φ (PAIR 0 0)).

Дополнительные методы программирования

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

Именованные константы

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

(λf.N)M

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

let f =M inN

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

Заметное ограничение этого letзаключается в том, что имя fне определено в M, поскольку M находится за пределами области привязки абстракции f; это означает, что определение рекурсивной функции не может использоваться в качестве M с let. Более продвинутая letrecсинтаксическая конструкция сахара, которая позволяет писать определения рекурсивных функций в этом наивном стиле, вместо этого дополнительно использует комбинаторы с фиксированной точкой.

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

Рекурсио n - определение функции, использующей саму функцию. Лямбда-исчисление не может выразить это так же прямо, как некоторые другие обозначения: в лямбда-исчислении все функции анонимны, поэтому мы не можем ссылаться на значение, которое еще не определено, внутри лямбда-члена, определяющего то же значение. Тем не менее, рекурсия все же может быть достигнута, если лямбда-выражение принимает само себя в качестве значения аргумента, например, в (λx.xx) E.

Рассмотрим факториал функция F (n)рекурсивно определяется как

F (n) = 1, если n = 0; else n × F (n - 1).

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

G: = λr. λn. (1, если n = 0; иначе n × (rr (n − 1)))
с rrx = F x = G rxдля удержания, поэтому r = Gи
F: = GG = (λx.xx) G

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

Это решает проблему, но требует перезаписи каждого рекурсивного вызова как самостоятельного приложения. Мы хотели бы иметь общее решение без необходимости переписывать:

G: = λr. λn. (1, если n = 0; иначе n × (r (n − 1)))
с rx = F x = G rxдля удержания, поэтому r = G r =: FIX Gи
F: = FIX Gгде FIX g: = (r, где r = gr) = g (FIX g)
, чтобы FIX G = G (FIX G) = (λn. (1, если n = 0; иначе n × ((FIX G) (n − 1))))

Дан лямбда-член с первым аргументом, представляющий рекурсивный вызов (например, Gздесь), комбинатор с фиксированной точкой FIXвернет самовоспроизводящееся лямбда-выражение, представляющее рекурсивную функцию (здесь F). Функцию не нужно явно передавать самой себе в любой момент, поскольку саморепликация организована заранее, когда она создается, чтобы выполняться каждый раз при ее вызове. Таким образом, исходное лямбда-выражение (FIX G)воссоздается внутри себя, в точке вызова, с достижением ссылки на себя.

На самом деле существует много возможных определений для этого Оператор FIX, простейший из них:

Y: = λg. (Λx.g (xx)) (λx.g (xx))

В лямбда-исчислении Ygявляется фиксированным - точка g, когда она расширяется до:

Yg
(λh. (λx.h (xx)) (λx.h (xx))) g
(λx.g (xx)) (λx.g (xx))
g ((λx.g (xx)) (λx.g (xx)))
g (Yg)

Теперь, чтобы выполнить рекурсивный вызов функции факториала, мы бы просто назвали (YG) n, где n - это число, для которого мы вычисляем факториал. Для n = 4, например, это дает:

(YG) 4
G (Y G) 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, каждый рекурсивно де Fined функция может быть выражена лямбда-выражением. В частности, теперь мы можем четко определить предикат вычитания, умножения и сравнения натуральных чисел рекурсивно.

Стандартные термины

У некоторых терминов есть общепринятые названия:

I: = λx.x
K: = λx.λy.x
S: = λx.λy.λz. xz (yz)
B: = λx.λy.λz.x (yz)
C: = λx.λy.λz.xzy
W: = λx.λy.xyy
U: = λx.xx
ω: = λx.xx
Ω: = ω ω
Y: = λg. (Λx.g (xx)) (λx.g (xx))

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

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

Если N - лямбда-член без абстракции, но, возможно, содержащий именованные константы (комбинаторы ), то существует лямбда-член T (x, N), что эквивалентно λx.N, но не имеет абстракции (кроме как части названных констант, если они считаются неатомарными). Это также можно рассматривать как анонимизирующие переменные, поскольку T (x, N) удаляет все вхождения xиз N, при этом позволяя подставлять значения аргументов в позиции, где N содержит an x. Функция преобразования T может быть определена следующим образом:

T(x, x): = I
T(x, N): = K N, если xне является свободным в N.
T(x, MN): = ST(x, M) T (x, N)

В любом случае член формы T (x, N) P может уменьшиться, если начальный комбинатор I, Kили S захватывает аргумент P, точно так же, как β-сокращение (λx.N)P будет делать. I возвращает этот аргумент. K отбрасывает аргумент, точно так же, как (λx.N)поступит, если xне имеет свободного вхождения в N. S передает аргумент к обоим подтермам приложения, а затем применяет результат первого к результату второго.

Комбинаторы B и C аналогичны S, но передают аргумент только одному подтермину приложения (B к подтерму «аргумент» и C к подтерму «функция»), таким образом сохранение последующего K, если в одном подтерме не встречается x. По сравнению с B и C, t Комбинатор S фактически объединяет две функции: переупорядочивание аргументов и дублирование аргумента, так что его можно использовать в двух местах. Комбинатор W выполняет только последнее, давая систему B, C, K, W в качестве альтернативы исчислению комбинатора SKI.

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

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

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

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

Вычислимые функции и лямбда-исчисление

Функция F: N→ Nнатуральных чисел является вычислимой функцией тогда и только тогда, когда существует лямбда-выражение f такое, что для каждой пары x, y в N, F (x) = y тогда и только тогда, когда f xy, где xи y- числа Чёрча, соответствующие x и y, соответственно, и = β означает эквивалентность с β-восстановлением. Это один из многих способов определения вычислимости; см. тезис Черча – Тьюринга для обсуждения других подходов и их эквивалентности.

Неразрешимость эквивалентности

Нет алгоритма, который принимает в качестве входных данных любые два лямбда-выражения и выводит ИСТИНАили ЛОЖЬв зависимости от того, два выражения эквивалентны. Точнее, никакая вычислимая функция не может определить эквивалентность. Исторически это была первая проблема, неразрешимость которой могла быть доказана. Как обычно для такого доказательства, вычислимость означает вычислимость с помощью любой модели вычислений, которая является полной по Тьюрингу.

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

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

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

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

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

(lambda (x) (* xx))

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

Например, Pascal и многие другие императивные языки давно поддерживают передачу подпрограмм в качестве аргументов другим подпрограммам через механизм указатели на функции. Однако указатели на функции не являются достаточным условием для того, чтобы функции были типами данных первого класса, потому что функция является типом данных первого класса тогда и только тогда, когда новые экземпляры функции могут быть созданы во время выполнения. И это создание функций во время выполнения поддерживается в Smalltalk, JavaScript, а в последнее время в Scala, Eiffel ("агенты"), C # («делегаты») и C ++ 11 и другие.

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

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

полным β-редукцией
Любой редекс можно уменьшить в любой момент. По сути, это означает отсутствие какой-либо конкретной стратегии сокращения - в отношении сводимости «все ставки отключены».
Аппликативный порядок
Самый левый, самый внутренний редекс всегда уменьшается первым. Интуитивно это означает, что аргументы функции всегда сокращаются до самой функции. Аппликативный порядок всегда пытается применить функции к нормальным формам, даже если это невозможно.
Большинство языков программирования (включая Lisp, ML и императивные языки, такие как C и Java ) описываются как " strict », что означает, что функции, применяемые к ненормализующим аргументам, не являются нормализующими. Это делается в основном с использованием аппликативного порядка, вызов по уменьшению значения (см. Ниже), но обычно называется «нетерпеливой оценкой».
Нормальный порядок
Крайний левый, крайний редекс всегда сокращается первым. То есть, когда это возможно, аргументы подставляются в тело абстракции до уменьшения аргументов.
Вызов по значению
Уменьшаются только самые внешние редексы: редекс уменьшается только тогда, когда его правая часть уменьшилась до значения (переменной или абстракции).
Вызов по имени
В обычном порядке, но внутри абстракций сокращения не выполняются. Например, λx. (Λx.x) xнаходится в нормальной форме согласно этой стратегии, хотя содержит редекс (λx.x) x.
Вызов по необходимости
В обычном порядке, но приложения-функции, которые будут дублировать термины, вместо этого называют аргумент, который затем сокращается только «когда это необходимо». В практическом контексте называется «ленивым оцениванием». В реализациях это «имя» принимает форму указателя, при этом переиндекс, представленный переходником.

Порядок аппликации, не является стратегией нормализации. Обычный контрпример выглядит следующим образом: определить Ω= ωω, где ω= λx.xx. Все это выражение содержит только один редекс, а именно все выражение; его сокращение снова Ω. Поскольку это единственное доступное сокращение, Ωне имеет нормальной формы (при любой стратегии оценки). Используя аппликативный порядок, выражение KIΩ = (λx.λy.x) (λx.x) Ωсокращается, сначала приведя Ωк нормальной форме (поскольку это крайний правый редекс), но поскольку Ωне имеет нормальной формы, аппликативный порядок не может найти нормальную форму для KIΩ.

Напротив, нормальный порядок называется так, потому что он всегда находит нормализующее сокращение, если оно существует. В приведенном выше примере KIΩпри нормальном порядке сокращается до I, нормальной формы. Недостатком является то, что редексы в аргументах могут быть скопированы, что приведет к дублированию вычислений (например, (λx.xx) ((λx.x) y)сокращается до ((λx.x) y) ((λx.x) y)с использованием этой стратегии; теперь есть два редекса, поэтому для полной оценки требуется еще два шага, но если бы аргумент был уменьшен первым, теперь не было бы ни одного).

Положительный компромисс использования аппликативного порядка заключается в том, что он не вызывает ненужных вычислений, если используются все аргументы, потому что он никогда не заменяет аргументы, содержащие редексы, и, следовательно, никогда не нужно их копировать (что может дублировать работу). В приведенном выше примере в аппликативном порядке (λx.xx) ((λx.x) y)сначала сокращается до (λx.xx) y, а затем до нормального порядка yy, делая два шага вместо трех.

Большинство чисто функциональных языков программирования (особенно Miranda и его потомки, включая Haskell) и языки доказательства программ доказательства теорем используют ленивое вычисление, которое, по сути, является то же, что и вызов по необходимости. Это похоже на обычное сокращение порядка, но вызов по необходимости позволяет избежать дублирования работы, присущего нормальному уменьшению порядка с использованием совместного использования. В приведенном выше примере (λx.xx) ((λx.x) y)сокращается до ((λx.x) y) ((λx.x) y), который имеет два редекса, но при вызове по необходимости они представляются с использованием одного и того же объекта, а не копируются, поэтому, когда один сокращается, другой тоже.

Замечание о сложности

Хотя идея β-редукции кажется достаточно простой, это не атомарный шаг, поскольку он должен иметь нетривиальные затраты при оценке вычислительной сложность. Чтобы быть точным, нужно каким-то образом найти расположение всех вхождений связанной переменной Vв выражении E, что подразумевает временные затраты, или нужно отслеживать эти местоположения в некотором роде, подразумевая стоимость помещения. Наивный поиск местоположений Vв E- это O (n) на длине n E. Это привело к изучению систем, в которых используется явная замена . Управляющие строки Sinot предлагают способ отслеживания местоположения свободных переменных в выражениях.

Параллелизм и параллелизм

Свойство Черча – Россера лямбда-исчисления означает, что вычисление (β-редукция) может выполняться в любом порядке, даже параллельно. Это означает, что релевантны различные стратегии недетерминированной оценки. Однако лямбда-исчисление не предлагает никаких явных конструкций для параллелизма. В лямбда-исчисление можно добавить такие конструкции, как Futures. Другие вычисления процессов были разработаны для описания связи и параллелизма.

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

В статье Леви 1988 г. «Совместное использование при оценке лямбда-выражений » он определяет понятие оптимального разделения, так что никакая работа не дублируется. Например, выполнение β-редукции в нормальном порядке на (λx.xx) (II)уменьшает его до II (II). Аргумент IIдублируется приложением для первого лямбда-члена. Если сокращение сначала было выполнено в аппликативном порядке, мы сохраняем работу, потому что работа не дублируется: (λx.xx) (II)сокращается до (λx.xx) I. С другой стороны, использование аппликативного порядка может привести к избыточным сокращениям или даже, возможно, никогда не привести к нормальной форме. Например, выполнение β-редукции в нормальном порядке на (λf.f I) (λy. (Λx.xx) (y I))дает (λy. (Λx.xx) ( y I)) I, (λx.xx) (II)которые, как мы знаем, можем делать без дублирования работы. Выполнение того же самого, но в аппликативном порядке дает (λf.f I) (λy.y I (y I)), (λy.y I (y I)) I, II (II), и теперь работа дублируется.

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

((λg. (G (g (λx.x)))) (λh. ((Λf. (F (f (λz.z)))) (λw. (H (w (λy.y)))))))

Он состоит из трех одинаковых членов: x = ((λg....) (λh.y))и y = ((λf....) (λw.z)), и, наконец, z = λw. (h (w (λy.y))). Здесь можно сделать только две возможные β-редукции: по x и по y. Уменьшение внешнего члена x сначала приводит к дублированию внутреннего члена y, и каждая копия должна быть уменьшена, но уменьшение сначала внутреннего члена y будет дублировать его аргумент z, что приведет к дублированию работы, когда значения h и w становятся известными. Между прочим, указанный выше термин сводится к функции идентичности (λy.y)и создается путем создания оболочек, которые делают функцию идентичности доступной для связующих g = λh..., f = λw..., h = λx.x(сначала) и w = λz.z(сначала), все из которых применительно к самому внутреннему члену λy.y.

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

Хотя Леви определяет понятие оптимального совместного использования, он не предлагает алгоритма для этого. В статье Винсента ван Острома, Киз-Яна ван де Лойя и Марийн Цвицерлоуд Лямбдаскоп: другая оптимальная реализация лямбда-исчисления они предоставляют такой алгоритм, преобразовывая лямбда-члены в сети взаимодействий, которые затем уменьшаются. Грубо говоря, результирующее сокращение является оптимальным, потому что каждый член, который будет иметь те же метки, что и в статье Леви, также будет тем же графом в сети взаимодействий. В документе они упоминают, что их прототипная реализация Lambdascope работает так же, как и оптимизированная версия эталонной оптимальной машины более высокого порядка BOHM.

Более подробную информацию можно найти в короткой статье Об эффективном сокращении лямбда-членов.

Семантика

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

В 1970-х годах, Дана Скотт показала, что, если бы были рассмотрены только непрерывные функции, можно было бы найти набор или домен D с требуемым свойством, тем самым предоставив модель для лямбда-исчисления.

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

Варианты и расширения

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

Эти формальные системы являются расширениями лямбда-исчисления, которых нет в лямбда-кубе:

Эти формальные системы являются вариациями лямбда-исчисления:

Эти формальные системы имеют отношение к лямбда-исчислению:

См. также

  • icon Портал математики

Ссылки

Дополнительная литература

Монографии / учебники для аспирантов:

  • Мортен Гейне Соренсен, Павел Уржичин, Лекции по изоморфизму Карри – Ховарда, Elsevier, 2006, ISBN 0-444-52077-5 - это недавняя монография, которая охватывает основные темы лямбда-исчисления от разнообразия безтиповых до большинства типизированных лямбда-исчислений, включая более свежие разработки, такие как системы чистых типов и лямбда-куб. Он не охватывает подтипов расширений.
  • Пирс, Бенджамин (2002), Типы и языки программирования, MIT Press, ISBN 0-262-16209-1 охватывает лямбда-исчисления с точки зрения практической системы типов; некоторые темы, такие как зависимые типы, только упоминаются, но выделение подтипов является важной темой.

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

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

На Викискладе есть средства массовой информации, связанные с лямбда-исчислением.
  1. ^Чёрч, Алонзо (1941). Исчисления лямбда-преобразования. Принстон: Издательство Принстонского университета. Retrieved 2020-04-14.
  2. ^Frink Jr., Orrin (1944). "Review: The Calculi of Lambda-Conversion by Alonzo Church" (PDF). Бык. Амер. Математика. Soc. 50(3): 169–172. doi :10.1090/s0002-9904-1944-08090-7.
Последняя правка сделана 2021-05-26 12:19:42
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте