Главная » Просмотр файлов » Диссертация

Диссертация (1150902), страница 2

Файл №1150902 Диссертация (Трассирующая нормализация) 2 страницаДиссертация (1150902) страница 22019-06-29СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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.БлагодарностиАвтор выражает благодарность Д. Ю. Булычеву и Н. Д.

Характеристики

Тип файла
PDF-файл
Размер
1,34 Mb
Высшее учебное заведение

Список файлов диссертации

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6517
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее