Множество свободных переменных

FV – free value

FV(x) = {x}

FV(lamda x.M) = FV(M) \ {x} (за исключением х, вычитание множества)

FV( M N) = FV(M) u FV(N)

Подстановка

Результат подстановки терма L вместо всех свободных вхождений y в M (обозначается M[L/y]), определяется рекурсивно:

x [L/y] Ξ L, если xΞy

x –иначе

X,y – метасимволы, обознач переменные, их можно сравнивать…

(lambda x.M) [L/y] Ξ (lambda x.M) если xΞy

Lambda x.(M[L/y]) – иначе

(M N) [L/y] Ξ (M[L/y] N[L/y])

Конфликт имен(захват переменных)

Может возникать при подстановке.

Подстановка не должна изменять связи переменных.

Пример.

(lambda y.x)[y/x] Ξ (lambda y.y)

Выполнив подстановку, мы получили другую функцию…

Назовем функции спец терминам

1 константная функция (lambda y.x) z => x, одно и то же значение не зависимо от аргумента.

2 тождественная функция (lambda y.y) z => z, одно и то же значение не зависимо от аргумента. ( выдает то же самое что получает в качестве параметра)

Условие отсутствия конфликта имен в подстановке M[N/x]:

BV[M] пересечение FV[N] = o ( пустое множество).

Рассмотрим операции, которые можно выполнять с лямбда термами.

Термы можно редуцировать(упрощать), делать преобразования.

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

Преобразование термов

• Это редукция

(ДАЛЕЕ lambda = h)

1 альфа редукция

(hx.M) ->_a (hy.M[y/x])

Сут ьв переименовании связанных переменных. Альфа редукцию можно применять если y не встречается в M не свободно, не связанно. (свежая переменная)

Обычно в h исчислении термы сравниваются с точностью до имен связанных переменных.

(hx.x), (hy.y) одинаковы с точки зрения имен связ переменных….

2 бетта редукция. Это применение h абстракции к какому либо аргументу. Если есть терм, то…. h прим в M……. Должно вып условие что связ пременные от …

B V (M) пересечение FV(N) = O . Это обязательное условие при бета редукции.

((hx.M)N) ->_b M[N/x]

3 n (этта) редукция.

(hx. (M x))->_n M

Еть ф hx, она получ аргумент и передает его функции M, но в M и сама может этот аргумент получить. Лишний этап передачи параметра здесь не нужен. Этта редукция применяется при условии что x не принадлежит FV(M)

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

M -> N

Если M->_b N

Или M->_n N

Как правило редукция терма заключается в редуцировании его подтерма.

M->M’

(hx.M) -> (hx.M’)

………….

M->M’

(M N) -> (M’ N)

…если N->N’ то…. (M N) -> (M N’)

…………..

Если терм не возможно редуцировать то говорят что он находится в нормальной форме.

(hx.x) редуцировать нельзя.

((x y) z) нельзя, не явл лямбда абстракцией.

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

Нормальная форма – это представление данных. Терм который можно редуцировать – это программа.

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

(hx.(x x)) (hx. (x x)) этот терм редуц беск число раз. Если применим функцию, то получим то е самое, такой терм называется АМЕГА. Ω

Редукция стрелочкой.

Нормальная форма – это терм, который нельзя редуцировать.

Не все термы имеют нормальную форму. Терм Амега преобразуется сам в себя. Процесс редукции будет бесконечным.

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

В хаскеле мы уже пользовались элементами лямбда исчисления.

Мы использовали Карриевы функции.

f(x,y)=M

f = hx.(hy. L)

((((hx. (hy. M)) M) N)

Это применение функции 2х аргументов.

Здесь мы можем применить бета-редукцию.

((((hx. (hy. M)) M) N) ->_B

Тогда получим

((hy. L [M/x])N) ->_B

Получим терм L [M/x][N/y]

Каррирование - процесс построения карриевой функции.

Поговорим о соглашениях о скобках.

(hx₁.(hx₂. … (hx_n. M)..))

Это представление карииеровой функции.

Мы будем записывать его в виде

(hx₁ x₂…x_n . M)

Точно также применение карриеровой функции требует большого количества скобок, но если принять оператор применения функции(пустое место) ассоциативным влево, то вместо записи

(((M1 M2) M3) M4)

Функция M1 применяется к трем аргументам.

Мы бкдем писать просто

(M1 M2 M3 M4)

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

Считается что лямбда абстракция имеет максимально возможное тело.

(hx. (x (hy. (y x))))

Можно записать в виде

hx. x (hy . y x)

Отсутствие скобок говорит что надо взять тело….

Если брать максимальное тело в лямбда абстракции то количество скобок можно уменьшить.

Рассмотрим терм….

Пусть есть

hz. (hx. M) N

это все лямбда абстракция, (hx. M) N – одно большое тело. Тело можно редуцировать. Моженм сделать бета-редукцию, и получим

(тело будет M)

hz. M [N/x]

если был бы такой терм:

hz. Z (hx. M) N

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

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

Вспомним об этом. Если есть терм (где L тело, и применяем терм к M..N)

(Hx y . L) M N

И если y принадлежит к FV(M) то возникнет конфликт имен.

Т.е. если M имеет свободную переменную Y, то когда она будет вставлена в L вместо X, то возникнет конфликт………

Чтобы этого не происходило, надо переменные переименовывать.

Возьмем терм (hx (hy . x y) Z) Y

Y – свободна.

Нужно выполнить альфа-редукцию, просто переименовать переменную Y

(hx (hy . x y) Z) Y ->_A

(hx (hu . x u) Z) Y ->_B

Y должен стать вместо X, получим выражение

(hu. Y u) z ->_B y z

То имя u исчезло и оказалось y z.

Лямбда исчисление явл теорией, в основе которой лежит равенство термов. Т.е. теория с равенством.

Как эти равенства доказываются. Если два терма M и M’ можно преобразовать к одному и тому же терму N, то термы M и M’ считаются равными.

->* обозначается редуцируется за 0 или более шагов. (редуцивно-транзетивное замыкание, либо тот же самый терм, либо терм, который получен за несколько шагов)

M=M’

Если M->* N и M’->*N

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

Благодаря этой теореме – программа, написанная на лямбда исчислении может дать единственный результат, а может и не дать.

Рассмотрим терм.

(hy. a) Ω

Здесь если мы выполним бета - редукцию, мы получим терм а.

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

При редуцировании мы должны учитывать возможность беск цикла и идти к результату…