α- и η-конверсии

В предыдущей главе мы осознали важную проблему, возникающую при подстановке. Тут поговорим подробнее о методе решения этой проблемы.

α-конверсия

Имя связанной переменной — не более чем метка: $\lambda x.\,x$ и $\lambda y.\,y$ — одна и та же функция.

Особо одарённые товарищи от возни с переименованием избавляются и используют индексы де Брёйна: сами лямбды остаются, но становятся безымянными, а каждое вхождение переменной записывается числом — сколько лямбд нужно пройти от него вверх до связывателя (отсчёт с нуля, $0$ — ближайшая охватывающая лямбда). Тогда α-эквивалентные термы получают одинаковую запись, и α-конверсия как понятие исчезает.

• $\lambda x.\,x$ → $\lambda.\,0$ (единственная переменная указывает на свою лямбду);
• $\lambda x.\,\lambda y.\,x\,y$ → $\lambda.\,\lambda.\,1\,0$ ($x$ стало $1$, а $y$ — $0$).

η-конверсия

На самом деле это совсем мелочь, но всё равно надо коротко сказать. η-конверсия говорит, что «обёртка» $\lambda x.\,M\,x$ ничем не отличается от самого $M$.

η-редукция сворачивает такую обёртку влево, а η-экспансия разворачивает её вправо.

В Haskell это знакомый point-free стиль:

sum xs = foldr (+) 0 xs
-- превращается в
sum = foldr (+) 0