О лямбда-исчислении | Кодементор

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

Вот три синтаксических конструкции лямбда-исчисления:

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

Переменные

Переменные могут иметь любое имя, но обычно это одна буква, например x, y а иногда ⨍ для обозначения переменной, которая рассматривается как функция.

Абстракция

Форма абстракции позволяет нам определять функции. В лямбда-исчислении абстракция (функция) принимает один параметр — x в (λ x . M ) и имеет тело — M. M любое возможное выражение в лямбда-исчислении.

Заявление

Форма заявки идет вразрез с абстракцией. В приложении мы предоставляем значение для параметра функции — значением может быть любое лямбда-выражение, которое мы можем написать. Приложение просто предоставляет значение параметра; он не «вызывает» функцию автоматически, как можно было бы ожидать в C (это делается позже).

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

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

𝞪 — преобразование (альфа-преобразование)

Эта операция используется для устранения конфликтов имен переменных. В нем говорится, что две абстракции эквивалентны: одна использует некоторое имя переменной, например xкак параметр и внутри тела M (например, некоторые M с точки зрения переменной xпишется как M[x]), и еще один с использованием другого имени переменной, например yхотя в остальном с точно таким же M (например M[y]).

𝞫—редукция (бета-редукция)

Эта операция используется для упрощения приложения, применяемого к абстракции. В некотором смысле приложение может отменить абстракцию (предоставив значение для параметра). Таким образом, у нас есть два эквивалентных выражения: одно с применением к абстракции, а другое, в котором пара приложение и абстракция исключены. Для того, чтобы иметь эквивалентность, последние должны иметь одинаковые M кроме как с N (предоставленный параметр) заменяет переменную параметра x в Mпишется как M[x:=N].

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

Мы можем определить глагол «абстрагироваться» следующим образом: взять выражение и заменить некоторую его фиксированную часть переменной, а затем обернуть это в функцию, которая принимает переменную в качестве параметра. Для эквивалента на языке программирования C представим оператор
printf ( "%d", 100 );
Теперь, чтобы абстрагироваться от этого, мы могли бы заменить 100 с xа затем оберните это в функцию:
int printx ( int x ) { printf ( "%d", x ); };
Мы «абстрагировали» наш исходный оператор printf!

Выражения, в том числе и переменные, не имеют определенного типа или, скорее, просто типизированы: все переменные и выражения берутся в качестве следующего типа: функция — принимающая один аргумент — и возвращающая выражение (типом которого также является функция, принимающая один аргумент).

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

Переменная, наблюдаемая одна, называется несвязанной переменной. Это соответствует понятию глобальной переменной в языках программирования, таких как C, и статической переменной в таких языках, как Java и C#. (В отличие от C, где необходимо объявить глобальную переменную, несвязанные переменные не объявляются, они просто используются.)

Абстракция вводит лексический охват для переменной параметра. Область видимости — это часть текста, в которой переменные должны понимать, являются ли они связанными или несвязанными. В теле абстракции появление параметра абстракции называется связанной переменной, и это соответствует понятию формального параметра в функции или методе в C, Java и C#. На параметр, введенный конструкцией абстракции, можно ссылаться только в рамках абстракции, например, в теле абстракции (M). (Помимо тела абстракции, параметр больше не входит в область видимости!)

Scope вводит возможность конфликтов имен переменных! Одно и то же имя переменной может быть привязано к одной функции, к другой или быть несвязанным — следовательно, мы должны помнить об области видимости, и во время манипуляций с выражениями нам, возможно, придется переименовывать переменные (используя 𝞪 — преобразование), чтобы избежать именования конфликты и сохраняйте выражения, с которыми мы работаем, как эквивалентные, т.е. имеющие одинаковое значение! Если мы становимся жертвой конфликта имен во время преобразования, результирующее выражение не будет эквивалентно первому, что делает преобразование ошибочным.

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

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

Применим к этой вложенной функции:
( ( λ х . ( λ y . (xy) ) ) y)
Вот, финал y является несвязанной переменной, тогда как предыдущая yсвязаны. Здесь мы можем увидеть начало конфликта имен. Давайте сделаем 𝞫 — сокращение, и посмотрим, что получится. Во-первых, давайте вспомним, что редукция работает, когда мы применяем приложение к абстракции формы: ( (λx. M) N )
Здесь, M ( λ y . (xy) ), и N это несвязанная переменная yпоэтому бета-редукция
M[x:=N] ( λ y . (xy))[x:=y]то есть: ( ( λ y . (yy)) ) — но это неправильный потому что в этом выражении все ys связаны, а один из y не должен быть привязан (он должен относиться к несвязанному (глобальному) y). Мы случайно преобразовали несвязанный y в ограниченный y, и результат не эквивалентен. Когда мы выполняем бета-редукции, нам нужно сначала проверить, может ли это произойти: не будем ли мы менять привязку переменной, так как это делать неправильно. Если это произойдет, то мы сначала используем 𝞪 — преобразование, чтобы переименовать переменную абстракции и любое использование в ее теле, здесь M is ( λ y . (xy)) ) мы переименуем y к zа сейчас M ( λ z . (xz) ) . Теперь мы можем ввести несвязанный y в это вместо x чтобы
M[x:=N] ( λ z . (xz))[x:=y]что приводит к соответствующему эквивалентному выражению:
( ( λ z . (yz) ) , в котором y остается несвязанным.

С технической точки зрения круглые скобки не являются обязательными в лямбда-исчислении — они являются обязательной частью различных синтаксических конструкций. Однако, если мы видим подобное приведенному выше без круглых скобок, как в:
х . λ у . ху
как бы ни было сложно M то есть, я считаю, что мы должны воспринимать это так:
( λ х . ( λ у . (ху )) )
а не как:
( λ Икс . ( λ у . Икс ) у)
потому что, если бы это было задумано, круглые скобки были бы абсолютно необходимы, чтобы разделить часть выражения на одну абстракцию, а остальную часть — на другую.

Аналогично, если у нас есть
xyz
Это неоднозначное и технически недействительное лямбда-исчисление, хотя, если нам приходится с ним работать, мы должны воспринимать его как ((xy)z), а не (x(yz))

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