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

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

Ссылка при цитировании: Березун Д.А. Полная головная линейная редукция // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 2017. Т. 10. № 3. С. 59–82. DOI: 10.18721/JCSTCS.10306