Полная головная линейная редукция

Головная линейная редукция (head linear reduction) представляет собой стратегию редукции лямбда-термов, производящую минимальное количество подстановок для достижения псевдоголовной нормальной формы (quasi-head normal form). Статья посвящена обобщению понятия головной линейной редукции до полной головной линейной редукции (complete head linear reduction), позволяющей полностью нормализовать лямбда-терм и определить новый подход к вычислениям – трассирующую нормализацию (traversal-based normalization). Оба подхода формализованы в виде систем переходов (transition system). В статье также показана корректность обеих стратегий редукций: головной линейной редукции относительно головной редукции – головная линейная редукция завершается в псевдоголовной нормальной форме терма тогда и только тогда, когда завершается головная, и полной головной линейной редукции относительно эффективной редуцирующей стратегии – головная линейная редукция завершается в нормальной форме терма тогда и только тогда, когда последняя существует.