Автореферат (1150900), страница 3
Текст из файла (страница 3)
Обходом (Traversal) АСД лямбда-терма называется обоснованная последовательность его вершин, именуемых токенами.Обратные указатели используются для определения следующего токенапри построении обхода. Предложенный автором алгоритм трассирующей нормализации манипулирует двумя видами указателей: указателем стека висячихаргументов, изображаемым над обходом на диаграммах, и обобщённым связывающим указателем, изображаемым на диаграммах под обходом. Интуитивно, цепочка обобщённых связывающих указателей определяет на каждом шагемножество связанных переменных, в то время как указатели стека висячих аргументов позволяют определять простые редексы. На рис. 2 приведён примерАСД терма и его обхода.11@1λxZt = @9 λx λy x Z1λyx2345α = {2 7→ 1}, β = {4 7→ 3, 3 7→ 2}Рис.
2. АСД терма (λx.λy.x)@1 Z и его обход.Алгоритм построения обхода АСД терма является детерминированным.По его завершению из конечного обхода может быть однозначно восстановлена нормальная форма исходного терма. А именно, после удаления незначимыхтокенов из обхода оставшаяся последовательность токенов является обходом вглубину АСД нормальной формы исходного терма.В четвёртой главе доказана корректность трассирующей нормализации. Для этого приведено формальное представление процедуры нетипизированной трассирующей нормализации (UNP) и её ограниченной версии (BUNP— ограниченная процедура нетипизированной трассирующей нормализации)в виде систем переходов.Пусть V := {a,b,c, .
. . } — бесконечный алфавит имён переменных, Σ —следующий алфавит символов:Σ := {@i | i ∈ N} ∪ {x | x ∈ V} ∪ {λx | x ∈ V}.Состоянием системы переходов для трассирующей нормализации является текущий обход, формально, тройка ⟨t; α; β⟩, где t : Σ → [1..|t]] является упорядоченной последовательностью, |t| — длина последовательности t, а частичныефункции α, β : [1..|t]] ⇀ [1..|t|−1] определяют множества обратных указателей.Корректность обеих процедур относительно головной и полной головной линейных редукций соответственно доказана в теоремах 5 и 6 путём симуляций системы переходов для головной линейной редукции системой переходов для BUNP и системы переходов для полной головной линейной редукциисистемой переходов для UNP.В пятой главе приведён новый метод компиляции термов нетипизированного лямбда-исчисления в низкоуровневое представление, обладающийсвойством полу-композициональности: каждый аргумент семантической функции является подтермом вычисляемого лямбда-терма.
Таким образом, аргумент12семантической функции может принимать конечное заранее заданное множество значений (всевозможных подтермов исходного терма). Полукомпозициональность позволяет успешно специализировать процедуру трассирующейнормализации на входной лямбда-терм.Пусть процедура нормализации реализована в виде программы NP наязыке L. Тогда, применяя вторую проекцию Футамуры–Ершова–Турчина, можно преобразовать программу NP в программу на том же языке L, производящуютрансляцию термов из лямбда-исчисления в некотороый язык LLL, являющийся подмножеством языка L.LC - LLLLC, то [[spec]](spec, NP) ∈Если NP ∈.LLЗдесь LC — некоторое лямбда-исчисление (например, чистое или простое типизированное), spec – частичный вычислитель, написанный на языке L, LLL ⊂L — язык низкоуровневого представления.Шестая глава посвящена распространению подхода трассирующейнормализации для стратегий вычислений аппликативного порядка и вызова понеобходимости.
Показано, как трассирующая нормализация может быть использована для компиляции конструкций языка PCF.В заключении приводятся основные результаты, полученные в рамкахдиссертационного исследования.1. Разработан алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления, соответствующий нормальному порядкуредукций.2. Представлена модель полной головной линейной редукции, являющаяся расширением известной модели головной линейной редукции.Предложенная модель формализована в виде системы переходов, доказана её корректность относительно головной редукции.3. Доказана корректность представленного алгоритма трассирующейнормализации относительно предложенной модели полной головнойлинейной редукции.
Для этого сам алгоритм трассирующей нормализации формализован в виде системы переходов, а также приведеноотношение симуляции, с помощью которого поведение системы переходов для алгоритма трассирующей нормализации может быть симулировано системой переходов для полной головной линейной ре13дукции. Таким образом, доказано, что процедура трассирующей нормализации является нормализирующей.4. Предложенный алгоритм адаптирован для других, отличных от нормального порядка, стратегий вычислений: аппликативного порядкаредукций и вызова по необходимости.5. Предложен новый метод компиляции функциональных языков программирования в низкоуровневое представление путём специализации представленного алгоритма трассирующей нормализации навходной терм.6.
Разработана экспериментальная реализация алгоритма трассирующей нормализации нетипизированного лямбда-исчисления1 , а такжегенерирующего расширения, на ней основанного, для компиляциилямбда-термов в низкоуровневое представление, на языках Haskellи Racket.В качестве рекомендации по применению результатов работы в индустрии и научных исследованиях указывается, что предложенный алгоритмтрассирующей нормализации не преобразует исходный терм, а только посещает его в конечном числе точек, благодаря чему он успешно поддается специализации с помощью хорошо известных методов специализации программ.
Вчастности, применяя вторую проекцию Футамуры–Ершова–Турчина (специализируя специализатор на алгоритм трассирующей нормализации) становитсявозможной генерация компиляторов для языков программирования.В качестве перспектив дальнейшей разработки тематики может бытьотмечено следующее: (1) описание известных языковых конструкций и программных трансформаций с помощью подхода трассирующей нормализации;(2) разработка, на основе предложенного подхода, универсального языка промежуточного представления, который может служить базой для описания семантик широкого класса языков программирования, позволяя автоматическигенерировать компиляторы соответствующих языков, а также (3) исследованиесвойств вычислимости и сложности программ в рамках подхода трассирующейнормализации.1Исходныйкоддоступенtraversal-Based-Normalization.поссылке:14https://github.com/danyaberezun/Публикации автора по теме диссертацииНиже приведён перечень публикаций, где были представлены основныерезультаты, представленные автором в диссертации.Публикации из “Перечня рецензируемых научных изданий, в которыхдолжны быть опубликованы основные научные результаты диссертацийна соискание ученой степени кандидата наук, на соискание ученойстепени доктора наук”, сформированного согласно требованиям,установленным Министерством образования и науки РоссийскойФедерации1.
Березун, Д.А. Полная головная линейная редукция / Д.А. Березун// НТВ СПбГПУ. Информатика. Телекоммуникации. Управление.– 2017. – № 3. – C. 59–82.2. Березун, Д.А. Трассирующая нормализация нетипизированноголямбда-исчисления. / Д.А. Березун // Известия вузов. Северо Кавказский регион.
Технические науки. – 2017. – № 4. – C. 5–12.Публикации в изданиях, входящих в базы цитирования Web of Science иSCOPUS3. Berezun, D.A. Compiling Untyped Lambda Calculus to Lower-LevelCode by Game Semantics and Partial Evaluation (invited paper) / D.A.Berezun, N.D. Jones // In Proceedings of the 2017 ACM SIGPLANWorkshop on Partial Evaluation and Program Manipulation (PEPM 2017).ACM, New York, NY, USA.
– 2017. – C. 1–11.4. Berezun, D.A. Precise Garbage Collection for C++ with a NonCooperative Compiler / D.A. Berezun, D.Y. Boulytchev // Proceedings ofthe 10th Central and Eastern European Software Engineering Conferencein Russia. –2014. С. 15:1–15:8.Публикации по теме диссертации в других изданиях5. Berezun, D.A. Working Notes: Compiling ULC to Lower-level Codeby Game Semantics and Partial Evaluation. / D.A. Berezun, N.D.Jones // META 2016 Fifth International Valentin Turchin Workshop onMetacomputation.
– 2016. – С. 11–23.15.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
