Комментарий к бессловесному определению

Выношу построчный комментарий к бессловесному определению чистого бестипового экстенсионального лямбда-исчисления «From ordinary variables x, y, z… to λβη», составленному мной больше года назад. Доступен также вариант в два столбика.

Лямбда-выражения строятся из переменных
с помощью абстракций и аппликаций;
причем аппликация лево-ассоциативна.

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

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

Вхождения связанной переменной можно заменить на другую переменную (альфа-конверсия).

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

Выражение считается подвыражением самого себя; тело абстракции
и обе части аппликации также являются подвыражениями;
данное отношение транзитивно.

Определение нормальной стратегии: переменная не может быть редексом;
если выражение является редексом, то за ним приоритет;
если абстракция не является эта-редексом, то следует рассмотреть ее тело;
если аппликация не является бета-редексом, то приоритет за левой ее частью с подвыражением-редексом,
иначе остается лишь правая часть аппликации.