ИЗВЕСТИЯ ВЫСШИХ УЧЕБНЫХ ЗАВЕДЕНИЙ СЕВЕРО-КАВКАЗСКИЙ РЕГИОН. 2017; 4: 5-12
http://dx.doi.org/10.17213/0321-2653-2017-4-5-12
ТРАССИРУЮЩАЯ НОРМАЛИЗАЦИЯ НЕТИПИЗИРОВАННОГО ЛЯМБДА-ИСЧИСЛЕНИЯ
Березун Даниил Андреевич – аспирант, Санкт-Петербургский государственный университет, г. Санкт-Петербург, Россия. E-mail: d.berezun@2009.spbu.ru
Аннотация
Трассирующая нормализация является новым подходом к нормализации λ-термов путём обхода их абстрактного синтаксического дерева. Изначально трассирующая нормализация была обоснована лишь для некоторых типизированных подмножеств λ-исчисления, а её расширение на нетипизированное λ-исчисление до сих пор не имело формального представления и обоснования. В статье приводится первое формальное представление процедуры трассирующей нормализации для нетипизированного λ-исчисления и показывается её корректность относительно линейной редукцией.
Ключевые слова: нормализация; трасса; лямбда-исчисление; линейная редукция; симуляция; семантики.
Полный текст: [in elibrary.ru]
Ссылки на литературу
- Daniil Berezun, Neil D. Jones. 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, 2017. - Luke Ong C.-H. Normalisation by Traversals. CoRR, abs /1511.02629. URL: http://arxiv.org/abs/1511.02629, 2015 (дата обращения 27.07.2017).
- William Blum. The safe lambda calculus. PhD thesis, University of Oxford, UK, 2009.
- Luke Ong C.-H. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In Logic in Computer Science, 2006 21st Annual IEEE Symposium on, pages 21 – 90, 12 – 15 Aug. 2006.
- Blum W., Luke Ong C.-H. A concrete presentation of game semantics. In Galop 2008: Games for Logic and Programming Languages, 2008.
- Березун Д. Полная головная линейная редукция // Науч-техн. ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. Вып. 3. 2017.
- Vincent Danos, Laurent Regnier. Head linear reduction. unpublished, 2004.
- Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3): 199 – 207, 2007.
- Blum W. Imaginary Traversals for the Untyped Lambda Calculus (ongoing work), 2017.
- Hendrik Pieter Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, New-York, Oxford, 1981.
- Benjamin C. Pierce. Types and Programming Languages (1st ed.). The MIT Press, 2002.
- Benjamin C. Pierce. Advanced Topics in Types and Programming Languages. The MIT Press, 2004.