Трассирующая нормализация является новым подходом к нормализации лямбда-термов и была предложена Онгом для просто типизированного лямбда-исчисления при анализе посредством игровой семантики рекурсивных схем высшего порядка с целью генерации древовидных структур нулевого порядка. Игровая семантика представляет собой один из способов задания семантики языков программирования, позволившим решить проблему построения полностью абстрактной модели для языка PCF (Programming Computable Functions), поставленную Плоткиным в 70-х годах. Операционный взгляд на игровую семантику простого типизированного лямбда-исчисления позволил определить для него нестандартную процедуру нормализации [1], которая может быть рассмотрена как интерпретатор: она нормализует λ-терм, манипулируя списком его подвыражении, снабжённых указателями назад (Backpointers). Такой подход к нормализации термов получил название трассирующей нормализации (Traversal-Based Normalization, Normalization by Traversals). Его отличительной особенностью является то, что он оставляет исходный терм нетронутым и позволяет реализовать интерпретатор языка без использования стандартных подходов, таких как β-редукция, окружение для связывания переменных и замыкание для вызовов функции и параметров. Более того, оказалось, что трассирующая нормализация простого типизированного лямбда-исчисления согласована с головной линейной редукцией.
В докладе будет представлено обобщение процедуры трассирующей нормализации до нетипизированного лямбда-исчисления и показана её корректность. Также будет представлено обобщение понятия головной линейной редукции до полной головной линейной редукции и установлено соответствие между полной головной линейной редукцией и трассирующей нормализацией нетипизированного лямбда-исчисления. Наконец, мы покажем, как термы нетипизированного лямбда-исчисления могут быть скомпилированы в низкоуровневое представление путём специализации на них процедуры трассирующей нормализации.
Основные результаты работы представлены в [2–4]. (Интересующимся можем прислать файлы этих статей.)
Список литературы:
[1] C.-H. Luke Ong. Normalisation by traversals. CoRR, abs/1511.02629, 2015.
[2] D. Berezun and Neil D. Jones. 2017. Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (invited paper). In Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2017). ACM, New York, NY, USA, 1-11.
[3] Д.Березун. Полная головная линейная редукция. Принята к публикации в "НТВ СПбГПУ. Информатика. Телекоммуникации. Управление.". Выпуск НТВ-ИТУ/2017 N 3. 2017.
[4] Д.Березун. Трассирующая нормализация нетипизированного лямбда-исчисления. Принята в "Известия вузов. Северо Кавказский регион. Технические науки." N 4, 2017.