Равенство лямбда-термов

Используя введенные правила конверсии, можно формально определить понятие равенства лямбда-термов. Два терма равны, если от одного из них можно перейти к другому с помощью конечной последовательности конверсии. Определим понятие равенства следующими выражениями, в которых горизонтальные линии следует понимать как «если утверждение над чертой выполняется, то выполняется и утверждение под ней»:

Следует отличать понятие равенства, определяемое этими формулами, от понятия синтаксической эквивалентности, которую будем обозначать специальным символом ≡. Например, λх.х ≠ λу.у, но λх.х = λу.у. Можно рассматривать синтаксическую эквивалентность термов с точностью до α -конверсий. Такую эквивалентность обозначают символом ≡ _а. Это отношение определяется так же, как равенство лямбда-термов, за тем исключением, что из всех конверсий допустимы только α -конверсии. Таким образом, λх.х ≡ _а λу.у.