Подстановки

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

Лямбда-исчисление как формальная система

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

1. Переменные: обозначаются произвольными строками, составленными из букв и цифр.

2. Константы: также обозначаются строками; отличие от переменных будем определять из контекста.

3. Комбинации:, т.е. применения функции S к аргументу Т; и S и Т
могут быть произвольными лямбда-термами. Комбинация записывается как ST.

4. Абстракции произвольного лямбда-терма S по переменной х, обо
значаемые как λx.S.

Лямбда-терм определяется рекурсивно и его грамматику можно представить в виде следующей формы Бэкуса-Наура:

Ехр = Var | Const | Exp Exp | λ Var. Ехр

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

Формализуем интуитивное представление о свободных и связанных переменных. Множество свободных переменных FV(S) лямбда-терма S можно определить рекурсивно следующим образом:

FV(x) = { х }

FV(c) = Ø

FV(ST) = FV(S) U FV(T)

FV( λ x.S) = FV(S) \ { x }

Аналогично множество связанных переменных BV(S) определяется следующими формулами:

BV(x) = Ø

BV(c) = Ø

BV(ST) = BV(S) U BV(T)

BV( λ x.S) = BV(S) U{ x }

Здесь предполагается, что с — некоторая константа.

Пример. Для терма S = (λх у.х) (λx.z х) можно показать, что FV(S) = { z }и BV(S) = { x,y }.

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

Будем обозначать операцию подстановки терма S вместо переменной х в другом терме Т как Т [ х:= S ]. Правила подстановки можно определить рекурсивно. При этом необходимо наложить дополнительные ограничения, позволяющие избегать конфликта в именах переменных.