Автореферат (1150900), страница 2
Текст из файла (страница 2)
Как показано в диссертации, применение частичных вычисленийк предложенному в диссертации алгоритму трассирующей нормализации позволяет производить трансляцию лямбда-термов в низкоуровневое представление, сохраняя исходную семантику программы. Такой подход к компиляции является перспективным направлением в области автоматической генерации компиляторов на основе семантики (Semantics-Directed Compiler Generation). Описание известных языковых конструкций и программных трансформаций припомощи нового подхода открывает перспективы к проектированию языка промежуточного представления, являющегося базой для описания семантик широкого класса языков программирования и позволяющего автоматически генерировать компиляторы соответствующих языков.Степень достоверности и апробация результатовДостоверность и обоснованность результатов исследования опираетсяна использование формальных методов исследуемой области, выполнение формальных доказательств и инженерные эксперименты.Основные результаты работы были представлены на следующих научных конференциях и семинарах: семинар “Математические вопросы информатики” (27 октября 2017, МГУ им.
М.В. Ломоносова, мех.-мат. ф-т, Москва, Рос7сия), семинар в ИПС им. А.К. Айламазяна РАН (26 октября 2017, ПереславльЗалесский, Россия), семинар в ИПМ им. М.В. Келдыша РАН (25 октября2017, Москва, Россия), конференция “Языки программирования и компиляторы” (PLC 2017, 3–5 апреля 2017, Ростов-на-Дону, Россия), Games for Logicand Programming Languages XII (GaLoP 2017, 22-23 апреля 2017, Уппсала,Швеция), PEPM 2017 Workshop on Partial Evaluation and Program Manipulation(16 – 17 января, 2017, Париж, Франция), внутрениие семинары Departmentof Computer Science of Oxford University (февраль 2016, апрель 2016, март2017, Оксфорд, Великобритания), Fifth International Valentin Turchin Workshopon Metacomputation (Meta 2016, 27 июня – 1 июля, 2016, Переславль-Залесский,Россия), Games for Logic and Programming Languages XI (GaLoP 2016, 2-3 апреля2016, Эйндховен, Нидерланды) и внутренние семинары Department of ComputerScience of DIKU (октябрь-ноябрь 2015 и ноябрь 2017, Копенгаген, Дания).Публикации по теме диссертацииВсе результаты диссертации опубликованы в пяти печатных работах, зарегистрированных в РИНЦ.
Две единоличные статьи изданы в журналах из“Перечня российских рецензируемых научных журналов, в которых должныбыть опубликованы основные научные результаты диссертаций на соисканиеучёных степеней доктора и кандидата наук”. Две статьи опубликованы в изданиях, входящих в базы цитирования SCOPUS и Web of Science.Вклад автора в публикациях, написанных в соавторстве, распределёнследующим образом. В работе [3] автору принадлежит формализация методатрассирующей нормализации, реализация предложенных семантических преобразований, идея и формализация метода трассирующей нормализации дляязыка PCF. Соавторы предложили схему представления нормализирующейпроцедуры, описали применение частичных вычислений к процедуре нормализации с целью компиляции термов лямбда-исчисления, сформулировали направления дальнейших исследований. В работе [4] автору принадлежит реализация инструментальных средств, разработка и реализация модели представления программной кучи и проведение экспериментов.Объем и структура работыДиссертация состоит из введения, 6 глав, заключения и 2 приложений.Полный объем диссертации составляет 130 страниц, включая 34 рисунка и1 таблицу.
Список литературы содержит 107 наименований.8Содержание работыВо введении обосновывается актуальность исследований, выполненных в рамках данной диссертационной работы, приводится обзор научной литературы по изучаемой проблеме, формулируется цель, ставятся задачи работы,формулируются научная новизна и практическая значимость.В первой главе приводится обзор области исследования. Рассматриваются существующие подходы к нормализации лямбда-термов и, в том числе, к трассирующей нормализации. Описывается игровая семантика и алгоритмы трассирующей нормализации для простого типизированного лямбдаисчисления и безопасного лямбда-исчисления, предложенные C.-H.
L. Ong иW. Blum соответственно. Также показано, что предложенные подходы трассирующей нормализации соответствуют известной модели головной линейнойредукции, предложенной L. Regnier и V. Danos. На основе проделанного обзорасделаны следующие выводы.– Существующие алгоритмы трассирующей нормализации определенылишь для некоторых неполных по Тьюрингу исчислений. При этомориентированность этих алгоритмов на системы типов и статическиеограничения на структуру исходного терма осложняют их обобщениедля поддержки исчислений, полных по Тьюрингу.– Задача построения алгоритмов трассирующей нормализации длянетипизированного лямбда-исчисления для стратегий вычисленийнормального и аппликативного порядков, а также стратегии вызова понеобходимости, является актуальной задачей в области анализа языков программирования.– Алгоритмы трассирующей нормализации требуют формального операционного доказательства корректности.Вторая глава содержит описание предложенной автором модели полной головной линейной редукции.
Она является расширением известной модели головной линейной редукции, предложенной V. Danos и L. Regnier. Обемодели основаны на понятиях простого редекса и линейной редукции.Определение. Хребетными или спинальными подтермами (Spine SubTerms) лямбда-терма T называются сам терм T , а также все спинальные подтермы терма U , если T = U V или T = λx.U соответственно. Заметим, чтолюбой лямбда-терм имеет ровно один спинальный подтерм-переменную. Такое9Терм T Условиеλh (T )pr(T )x[][]UVλh (U ) = [ ][]pr(U )UVλh (U ) = λx : ll(λx, V ) : pr(U )λx.Uλx : λh (U )pr(U )Рис. 1. Определение списков головных абстракций и простых редексов.вхождение переменной, так же как и сам подтерм, называется головным (HeadOccurrence, HOC).Определение.
Cписки головных абстракций (Head λ List, λh (T )) и простых редексов (Prime Redexes) определяются совместно индукцией по структуре терма T . Простой редекс представляет собой пару (λx, N ), первый и второйэлементы которой называются абстракцией и аргументом простого редекса соответственно. Индуктивное определение списков простых редексов и головныхабстракций приведены на рис.
1, где pr(T ) обозначает список простых редексовтерма T .Редексом головного вхождения переменной (HOC Redex) терма T называется простой редекс (λx, V ), где x является головной переменной, а V — соответствующий аргумент, если таковой редекс существует.Интуитивно, головная линейная редукция линеаризует последовательность подстановок путём замены на каждом шаге лишь одного вхождения переменной — головного — оставляя сам головной редекс нетронутым. Если жеон не определён, головная линейная редукция завершается в так называемойпсевдоголовной нормальной форме (Quasi-Head-Normal Form, QHN).В данной главе предлагается модель полной головной линейной редукции, являющаяся обобщением модели головной линейной редукции. Приведены формальное представление обеих моделей в виде систем переходов, причёмсистемы переходов для головной линейной редукции является частным случаем системы переходов для полной головной линейной редукции.
Доказаны следующие теоремы о корректности моделей.Теорема 2 устанавливает соответствие между представленной модельюголовной линейной редукцией и головной редукцией: 1) если головная линейная редукция завершается, то её результат находится в псевдо-головной нормальной форме; 2) головная линейная редукция завершается тогда и только тогда, когда завершается головная редукция.10Теорема 3 устанавливает соответствие между предложенной модельюполной головной линейной редукцией и головной редукцией: 1) если полнаяголовная линейная редукция завершается, то её результат находится в нормальной форме; 2) полная головная линейная редукция завершается тогда и толькотогда, когда завершается головная редукция.Обе теоремы доказаны методом симуляции соответствующей системойпереходов головной редукции лямбда-термов.В третьей главе приводится разработанный автором алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления.
Предлагаемый алгоритм реализует стратегию нормального порядка редукции. Отличительной особенностью трассирующей нормализации является то, что в то время как классическая β-редукция путём произведения подстановок изменяет исходный терм, трассирующая нормализация, напротив — оставляет его нетронутым. В главе приведено обобщение трассирующей нормализации до нетипизированного лямбда-исчисления, являющегося истинным надмножеством вышеуказанных исчислений.Трассирующая нормализация нормализует лямбда-терм путём построения обхода его абстрактного синтаксического дерева (АСД).Определение. Обоснованной последовательностью (Justified Sequence)называется упорядоченная последовательность, каждый элемент которой может быть снабжён одним или несколькими указателями на более ранние элементы.Определение.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
