Диссертация (1150902), страница 2
Текст из файла (страница 2)
Абрамски (S. Abramsky), Л. Онг (C.-H. L. Ong), П. Малакария (P.Malacaria), Р. Джагадесан (R. Jagadeesan) и Г. МакКускер (G. McCusker) [39–41],позволило в начале 90-х годов решить задачу, сформулированную Плоткиным.Дальнейшее развитие игровая семантика получила в работах Д. М. Э. Хуланда (J.7M.
E. Hyland), А. Кера (A. D. Ker), Х. Никау (H. Nickau), В. Блюма (W. Blum), Д.Гика (D. Ghica) и др [10, 39, 42–49].В последние годы исследование операционных особенностей игрой семантики стало актуальной темой исследований, о чём свидетельствуют работы Д.Р. Гика (D. R. Ghica), Л. Онга и В. Блюма [10, 46–50]. В. Данос (V. Danos)и Л. Ренье (L.
Regnier) описывали игровую семантику программ с помощьюабстрактных машин KAM (Krivine Abstract Machine) и PAM (Pointer AbstractMachine) [8, 9, 51], а также предложили связать её с линейной редукцией. Л. Онгвпервые определил трассирующую нормализацию для простого типизированного лямбда-исчисления [6], а В. Блюм распространил этот подход до безопасноголямбда-исчисления (Safe Lambda-Calculus) [44, 52]. Тем не менее, вопрос распространения подхода трассирующей нормализации до полного по Тьюрингу исчисления оставался открытым.Целью данной работы является обобщение подхода трассирующей нормализации до полного по Тьюрингу исчисления, обоснование корректности трассирующей нормализации и исследование возможности представления различныхязыковых конструкций в рамках предложенного подхода при компиляции функциональных языков программирования.Для достижения вышеупомянутой цели были поставлены следующие задачи.1.
Разработать в рамках стратегии вычисления нормального порядка редукции алгоритм трассирующей нормализации для нетипизированного лямбдаисчисления.2. Формально доказать корректность предложенного алгоритма.3. Исследовать возможность адаптации трассирующей нормализации для различных стратегий вычислений.4. Исследовать возможность представления различных языковых конструкций в рамках предложенного подхода с точки зрения компиляции основныхконструкций функциональных языков программирования.Постановка цели и задач исследования соответствует следующим пунктампаспорта специальности 05.13.11: методы, модели и алгоритмы проектированияи анализа программ и программных систем, их эквивалентных преобразований,8верификации и тестирования (пункт 1); языки программирования и системы программирования, семантика программ (пункт 2).Методология и методы исследованияМетодология исследования основана на идеях и подходах информатики к описанию и анализу понятия вычислимости.
Используются также операционная и денотационная концепции описания семантик языков программирования.В работе использовались методы синтаксического преобразования лямбдатермов [30,53–56]. Для формализации моделей использовался подход к описаниюсемантик в виде систем переходов [57, 58], а для доказательства их корректности— метод симуляции одной системы переходов другой посредством определенияотношения, связывающего соответствующие состояния этих систем переходов.Были использованы стратегии вычислений вызова по имени, нормального порядка, вызова по значению, аппликативного порядка, головной редукции, линейнойредукции и вызова по необходимости.
Для автоматического преобразования программ и семантик использовались методы частичных вычислений и дефункционализации по Рейнольдсу (Reynolds) [59–61]. Программная реализация предложенных в диссертации результатов была выполнена с помощью языков программирования Haskell [62] и Racket [63].Основные положения, выносимые на защиту1. Разработан алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления, соответствующий нормальному порядку редукций.2. Представлена модель полной головной линейной редукции, являющаясярасширением известной модели головной линейной редукции. Предложенная модель формализована в виде системы переходов, доказана корректность этой модели относительно головной редукции.3. Доказана корректность представленного алгоритма трассирующей нормализации относительно предложенной модели полной головной линейнойредукции путём его формализации в виде системы переходов и дальнейшей симуляции системы переходов для полной головной линейной редукции.
Таким образом, было доказано, что предложенная процедура трассирующей нормализации действительно является нормализирующей.94. Предложенный алгоритм адаптирован для других, отличных от нормального порядка, стратегий вычислений: аппликативного порядка редукций ивызова по необходимости.5. Предложен и реализован на примере нетипизированного лямбдаисчисления новый метод компиляции функциональных языков программирования в низкоуровневое представление путём специализациипредставленного алгоритма трассирующей нормализации на входной терм.Научная новизна полученных в ходе исследования результатов заключаетсяв следующем.1. Впервые было введено и формально описано понятие полной головной линейной редукции и доказана её корректность.2.
Алгоритм трассирующей нормализации, представленный в работе, отличается от аналогов (работы Л. Онга и В. Блюма [6, 7, 52]) тем, что он не накладывает каких-либо ограничений на лямбда-термы, что позволяет корректно нормализовывать произвольный лямбда-терм. Кроме того, алгоритмы,предложенные Л. Онгом и В. Блюмом, применяются лишь к частным случаям, а именно, к простому типизированному лямбда-исчислению и безопасному лямбда-исчислению.3. Предложен новый подход к компиляции функциональных языков программирования путём специализации процедуры трассирующей нормализациина входной терм, и исследованы её свойства.Теоретическая значимость диссертационного исследования заключается вформализации понятий головной и полной головной линейной редукций, разработке формального алгоритма, решающего задачу трассирующей нормализации,соответствующей полной головной линейной редукции, для бестипового лямбдаисчисления, а также в формальном доказательстве корректности представленногоалгоритма.Практическая значимостьТрассирующая нормализация представляет собой новый подход к вычислениям, позволяя исследовать ряд свойства языков программирования с нового ракурса.
Как показано в диссертации, применение частичных вычислений [64–72]10к предложенному в диссертации алгоритму трассирующей нормализации позволяет производить трансляцию лямбда-термов в низкоуровневое представление,сохраняя исходную семантику программы [73]. Такой подход к компиляции является перспективным направлением в области автоматической генерации компиляторов на основе семантики (Semantics-Directed Compiler Generation) [74–79].Описание известных языковых конструкций и программных трансформаций припомощи нового подхода открывает перспективы к проектированию языка промежуточного представления, являющегося базой для описания семантик широкогокласса языков программирования и позволяющего автоматически генерироватькомпиляторы соответствующих языков.Степень достоверности результатовДостоверность и обоснованность результатов исследования опирается на использование формальных методов исследуемой области, выполнение формальных доказательств и инженерные эксперименты.Основные результаты работы были представлены на следующих научных конференциях и семинарах: семинар “Математические вопросы информатики” (27октября 2017, МГУ им.
М.В. Ломоносова, мех.-мат. ф-т, Москва, Россия), семинар в ИПС им. А.К. Айламазяна РАН (26 октября 2017, Переславль-Залесский,Россия), семинар в ИПМ им. М.В. Келдыша РАН (25 октября 2017, Москва,Россия), конференция “Языки программирования и компиляторы” (PLC 2017,3–5 апреля 2017, Ростов-на-Дону, Россия), Games for Logic and ProgrammingLanguages XII (GaLoP 2017, 22-23 апреля 2017, Уппсала, Швеция), PEPM 2017Workshop on Partial Evaluation and Program Manipulation (16 – 17 января, 2017, Париж, Франция), внутренние семинары Department of Computer Science of OxfordUniversity (февраль 2016, апрель 2016, март 2017, Оксфорд, Великобритания),Fifth International Valentin Turchin Workshop on Metacomputation (Meta 2016,27 июня – 1 июля, 2016, Переславль-Залесский, Россия), Games for Logic andProgramming Languages XI (GaLoP 2016, 2-3 апреля 2016, Эйндховен, Нидерланды) и внутренние семинары Department of Computer Science of DIKU (октябрьноябрь 2015 и ноябрь 2017, Копенгаген, Дания).Публикации по теме диссертацииВсе результаты диссертации опубликованы в пяти печатных работах, зарегистрированных в РИНЦ.
Две единоличные статьи изданы в журналах из “Перечня11российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание учёных степеней доктора и кандидата наук”. Две статьи опубликованы в изданиях, входящихв базы цитирования SCOPUS и Web of Science.Вклад автора в публикациях, написанных в соавторстве, распределён следующим образом. В работе [73] автору принадлежит формализация метода трассирующей нормализации, реализация предложенных семантических преобразований,идея и формализация метода трассирующей нормализации для языка PCF. Соавторы предложили схему представления нормализирующей процедуры, описали применение частичных вычислений к процедуре нормализации с целью компиляции термов лямбда-исчисления, сформулировали направления дальнейшихисследований.
В работе [80] автору принадлежит реализация инструментальныхсредств, разработка и реализация модели представления программной кучи и проведение экспериментов.Объем и структура работыДиссертация состоит из введения, шести глав, заключения и двух приложений. Полный объём диссертации составляет 130 страниц с 34 рисунками и 1 таблицей.
Список литературы содержит 107 наименований. В первой главе приводится обзор области исследования. Рассматриваются существующие подходы кредукции термов, а также описываются существующие подходы к трассирующейнормализации. Во второй главе приводится модель головной линейной редукции,согласованная с классическим определение В.
Даноса и Л. Ренье [8], в виде системы переходов, а также модель полной головной линейной редукции, являющаясярасширением модели головной линейной редукции и устанавливается корректность предложенных моделей относительно головной редукции. В третьей главепредставлен разработанный автором алгоритм трассирующей нормализации длянетипизированного лямбда-исчисления. В четвёртой главе представлена формализация предложенного алгоритма трассирующей нормализации в виде системыпереходов, а также установлена её корректность путём определения отношениясимуляции между системами переходов для полной головной линейной редукциии трассирующей нормализации. В пятой главе показано, как алгоритм трассирующей нормализации может быть использован для генерации компилятора нетипизированного лямбда-исчисления в низкоуровневое представление с помощью12известных методов специализации программ.
Наконец, в шестой главе показано,как предложенный алгоритм трассирующей нормализации может быть адаптирован для различных стратегий редукции и поддержки различных языковых конструкций на примере языка PCF.БлагодарностиАвтор выражает благодарность Д. Ю. Булычеву и Н. Д.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
