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

http://akoub.narod.ru/funcbook/chapter3/c3.htm

Глава 3. Лямбда-исчисление

3.1. Формальные  теории в программировании

Функциональные языки  программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий  ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения  состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в  качестве теоретической основы и "минимального" функционального языка программирования. В конечном итоге любую программу, написанную на языке Haskell или любом другом функциональном языке программирования, можно сравнительно несложными преобразованиями свести к формуле лямбда-исчисления.

Разумеется, ни Черч, ни Клини  не создавали язык программирования. Вопрос, которым они интересовались - это вопрос о формализации понятия  вычислимой функции и создания универсального математического аппарата для определения  и работы с вычислимыми функциями. В то время эта область математики активно развивалась в трудах уже упомянутых Черча и Клини, а также Тьюринга (Alan Turing), Поста (Emil Post) и других. Во многих работах предлагался  следующий подход к формализации понятия функции: в качестве основы берется некоторый "минимальный" набор базовых функций и предлагаются способы построения из них более  сложных функций с помощью  тех или иных комбинаторов (функций высшего порядка). Таков, например, подход, использованный Геделем при создании им теории рекурсивных функций. Напротив, в созданном им лямбда-исчислении Черч сумел построить такую систему, при которой базовых функций нет вовсе, а вместо способов построения сложных функций из простых (комбинаторов) используются правила преобразований, с помощью которых можно получать из одних функций другие, эквивалентные им. Такой процесс преобразования формул напоминает процесс вычисления функции, происходящий при исполнении программы, написанной на функциональном языке программирования. Рассмотрим теорию Черча более подробно.

Основным понятием в лямбда-исчислении является понятие выражения или формулы. Его можно определить рекурсивно. Прежде всего, зафиксируем набор идентификаторов, которые в дальнейшем будем называть переменными. Мы будем использовать в качестве имен латинские буквы x, y, f и др. В формулах переменные обычно обозначают аргументы функций, задаваемых лямбда-выражениями, однако сама по себе переменная является простейшим видом выражения. Два других вида выражений - это определение безымянной функции (лямбда-выражение) и применение функции.

Лямбда-выражение имеет  вид (λx.e), где x - имя переменной, а e - выражение. Семантически такое выражение обозначает функцию с аргументом x и телом e. Применение функции записывается в виде (e1 e2), где e1 и e2 - выражения (e1 - функция, а e2 - ее аргумент). Приведем несколько примеров.

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

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

Многие примитивные функции  уже хорошо нам знакомы по языку Haskell и многим другим языкам программирования. Это обычные арифметические операции сложения, умножения и другие, операции сравнения величин "больше", "меньше", "равны" и другие, операции над логическими значениями "и", "или" и другие. Мы будем пользоваться ими без какого-либо объяснения. Единственное отличие от стандартного использования этих и других операций от их использования в других языках программирования будет заключаться в том, что мы всегда будем использовать только префиксную запись операций, то есть вместо привычного 3+5 будем записывать выражение + 3 5. Конечно, все функции в нашем расширенном лямбда-исчислении будут карринговыми, то есть выражение + 3 также имеет смысл и представляет собой применение функции + к константе 3, в результате которого получается функция увеличения целого аргумента на 3.

Следует заметить также и  то, что если в классическом лямбда-исчислении применение любой функции к любому аргументу всегда осмысленно, поскольку  любой "объект" - как аргумент, так и результат - всегда представляет собой функцию одного аргумента, то в нашем расширенном лямбда-исчислении примитивные функции можно применять  только к "правильным" аргументам. Так, бессмысленным будет выражение + TRUE 0, поскольку невозможно выполнить сложение логического значения TRUE с числом 0. Также бессмысленным будет выражение / 3 0, поскольку результат деления числа 3 на число 0 не определен. Мы не будем рассматривать бессмысленные выражения.

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

3.2. Система вывода  результатов

Прежде, чем рассматривать  преобразования выражений, введем важное понятие свободной и связанной переменной. Неформально говоря, вхождение переменной в некоторое выражение будет связанным, если оно находится внутри некоторого лямбда-выражения, в заголовке которого эта переменная упомянута в качестве аргумента. Другими словами, если имеется выражение, в которое в качестве подвыражения входит λx.e, то все вхождения переменной x в выражении e будут связанными. Если переменная не является связанной в некотором выражении, то она в нем будет свободной. Можно определить понятия свободных и связанных переменных и более формально. Для этого рассмотрим понятие "множества свободных переменных" некоторого выражения. Те переменные, которые не будут входить в это множество, будут в этом выражении связанными.

Итак, если выражение E представляет собой переменную x, то множество свободных переменных этого выражения F(E) содержит только эту переменную: F(E) = { x }. Если выражение представляет собой одну из стандартных констант нашего расширенного лямбда-исчисления, то оно не содержит ни свободных, ни связанных вхождений переменных, F(c) = {}. Если выражение является применением функции к аргументу и имеет вид E = e1 e2, то множество свободных переменных этого выражения является объединением множеств свободных переменных выражений e1и e2: F(E) = F(e1)  È F(e2). Наконец, если выражение имеет вид лямбда-выражения E = λx.e, то его множество свободных переменных получится, если из множества свободных переменных выражения e убрать переменную x: F(E) = F(e) \ { x }.

Следует отметить, что одна и та же переменная может быть связанной  в некотором выражении и одновременно свободной в некотором его  подвыражении. Так, например, в выраженииλf.f x переменная x - свободная, а переменная f - связанная. Однако если рассматривать только тело этого лямбда-выражения f x, то в нем обе переменных f и x свободные. Вообще говоря, выражения, содержащие свободные переменные, хотя и являются формально допустимыми, но, как правило, бессмысленны. Например, выражение λf.f x представляет собой функцию, которая применяет свой аргумент к переменной "x". Поскольку переменная x - свободная, то ее смысл в этом выражении не определен. Если же связать эту переменную, то мы получим уже вполне осмысленное выражение λx.λf.f x, представляющее собой функцию, которая применяет свой второй аргумент к первому. Обычно мы рассматриваем выражения, содержащие свободные переменные, только в качестве составных частей других выражений, в которых рассматриваемые переменные уже являются связанными.

Мы рассмотрим четыре способа  преобразования выражений в лямбда-исчислении. Первое из рассматриваемых преобразований называется переименованием переменных или α-преобразованием. Смысл этого преобразования состоит в том, что суть функции не меняется, если заменить имя ее формального аргумента. Формально α-преобразование заключается в замене в выражении λx.e имени переменной x на любое другое имя с одновременной заменой всех свободных вхождений этой переменной в выражение e. Преобразование возможно, если только новая переменная уже не входит свободно в выражение e, а также если при этом свободное вхождение переменной не окажется связанным. Так, например, в выражении λx.λf.f x y можно заменить переменную x, скажем, на переменную z. В результате получится выражение λz.λf.f z y. Разумеется, новое выражение эквивалентно исходному и имеет тот же смысл. Однако, в том же выражении переменную x нельзя заменить на y, поскольку переменная y входит в тело лямбда-выражения свободно, так что получившееся после замены выражение λy.λf.f y y уже будет иметь другой смысл - в нем оба вхождения переменной y оказываются связанными. Нельзя также произвести и замену x на f, поскольку это приведет к тому, что в теле лямбда-выражения свободное вхождение переменной x превратится в связанное вхождение переменной f, и получившееся выражение λf.λf.f f y также будет иметь уже другой смысл.

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

Преобразование, называемое δ-редукцией, соответствует применению "встроенной" функции к константным аргументам. Правило δ-редукции имеет следующий вид. Пусть имеется выражение e e1 e2... ek, где e - константа, представляющее имя "встроенной" функции с k аргументами, а e1, e2,... ek - значения, могущие служить аргументами этой функции. Тогда такое выражение можно заменить на эквивалентное ему выражение, представленное значением, получающимся как результат применения функции к заданным значениям аргумента. Так, например, если константа+ представляет функцию арифметического сложения целых, а константа OR - функцию логического "или", то в результате δ-редукции выражение + 1 4 может быть преобразовано к выражению 5, а выражение OR TRUE FALSE - к выражению TRUE. Теоретически δ-редукция обратима, то есть можно действовать и наоборот, представляя константы в виде применения встроенных функций к аргументам-константам. Однако на практике желание представить константу 5 в виде + 2 3 никогда не возникает.

Преобразование, называемое β-редукцией, соответствует применению функции, представленной лямбда-выражением, к аргументу. Если исходное выражение имело вид (λx.e) a, то в результате применения β-редукции оно будет преобразовано в e{x|a} - выражение e, в котором все свободные вхождения переменной x заменены на выражение a. Например, выражение((λx.+ x x) 3) в результате применения β-редукции будет преобразовано в (+ 3 3), которое, в свою очередь, может быть преобразовано в (6) с помощью применения δ-редукции.

Если в некоторое выражение  входит в качестве подвыражения такое  выражение, к которому можно применить  одну из редукций, то такое подвыражение называется редуцируемым или сокращенно редексом (от redex - reducible expression). Таким образом, процесс преобразования выражения сводится, в основном, к применению β- и δ-редукций к редексам, содержащимся в исходном выражении.

Заметим, что при применении β-редукции замене подлежат именно свободные переменные тела лямбда-выражения. Рассмотрим, например, следующее выражение:((λx.+ x ((λx.* x x) 2)) 4). В этом выражении имеются два подвыражения-редекса, к которым можно применить β-редукцию. Первый из этих редексов - это само выражение целиком, второй - подчеркнутое подвыражение. Если применить β-редукцию к первому из этих редексов - внешнему, - то получится выражение (+ 4 ((λx.* x x) 2)). Здесь при применении редукции свободное вхождение переменной x было заменено константой 4, а связанное вхождение этой переменной во внутреннем редексе осталось неизменным. Мы можем, однако, применить β-редукцию к внутреннему редексу, тогда исходное выражение будет преобразовано в выражение ((λx.+ x (* 2 2)) 4).