Редукция лямбда-термов

Экстенсиональность

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

В силу η -конверсии отношение равенства лямбда-термов экстенсионально. Действительно, если f х и g х равны для любого х, то в частности f у = g у, где у не является свободной переменной ни в f, ни в g. Следовательно, по последнему правилу в определении равенства лямбда-термов, имеем λ y.f у = λ у.д у. Eсли несколько раз применить η -конверсию, можно получить, что f = g. И обратно, экстенсиональность дает то, что каждое применение η -конверсии приводит к равенству, поскольку по правилу β -конверсии (λх.Т х) у = Т у для любого у, если х не свободна в Т.

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

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