Автореферат (Трассирующая нормализация)

На правах рукописиБерезун Даниил АндреевичТРАССИРУЮЩАЯ НОРМАЛИЗАЦИЯСпециальность 05.13.11 ––«Математическое и программное обеспечение вычислительныхмашин, комплексов и компьютерных сетей»Авторефератдиссертации на соискание учёной степеникандидата физико-математических наукСанкт-Петербург2017Работа выполнена на кафедре системного программирования СанктПетебургского государственного университетаНаучный руководитель:КОЗНОВ Дмитрий Владимирович, доктор технических наук, доцент, профессор кафедры системногопрограммированияОфициальные оппоненты: НЕПЕЙВОДА Николай Николаевич,доктор физико-математических наук, профессор,Федеральное государственное бюджетное учреждение науки Институт программных систем имениА.К.

Айламазяна Российской академии наук, главный научный сотрудникМИРОНОВ Андрей Михайлович,кандидат физико-математических наук,Федеральное государственное бюджетное образовательноеучреждениевысшегообразования“Московский государственный университет имениМ.В.Ломоносова”, доцентВедущая организация:Федеральное государственное учреждение “Федеральный исследовательский центр Институт прикладной математики им. М.В.

Келдыша Российскойакадемии наук” (ИПМ им. М.В. Келдыша РАН)Защита состоится 29 марта 2018 г. в 14 часов на заседании диссертационногосовета Д 212.232.51 на базе Санкт-Петербургского государственного университета по адресу: 198504, Санкт-Петербург, Старый Петергоф, Университетскийпр. 28, математико-механический факультет СПбГУ, ауд. 405.С диссертацией можно ознакомиться в библиотеке Санкт-Петербургского государственного университетапо адресу: 199034, Санкт-Петербург, Университетская наб., д.

7/9, а также на сайте: https://disser.spbu.ru/disser/soiskatelyu-uchjonoj-stepeni/dis-list/form/14/1545.html.Автореферат разослан __ __________ 20__ года.Ученый секретарьдиссертационного советаД 212.232.51, д.ф.-м.н., профессорДемьянович Юрий КазимировичОбщая характеристика работыАктульность темы исследованияЛямбда-исчисление, наряду с машинами Тьюринга, теорией частичнорекурсивных функций, формальными алгорифмами Маркова и Поста, являетсяодной из основных формальных моделей вычислений.

Первая модель лямбдаисчисления, предложенная A. Church в 30-х годах 20 века, оказалась противоречивой: в 1935 году S. Kleene и J. B. Rosser выявили в ней парадокс, названный в их честь. В 1936 году A. Church предложил первую непротиворечивую систему, ныне известную как нетипизированное, бестиповое или чистоелямбда-исчисление, а в 1940 году он же предложил модель простейшего типизированного исчисления — простое типизированное лямбда-исчисление. С техпор лямбда-исчисление играет особую роль в теории вычислимости и стало основой для целой парадигмы программирования — функционального программирования.Тем не менее, различные языки, основанные на лямбда-исчислении, долгое время не имели полностью абстрактных моделей вычислений, т.е. такихденотационных моделей, что существует изоморфизм между термами языкови их представлениями в этих моделях.

Впервые задача построения полностьюабстрактной модели вычислений была поставлена в 1975 году (G. Plotkin) дляязыка программирования вычислимых функций PCF (Programming ComputableFunctions). Первым подходом, предложившим решение поставленной задачи,стала игровая семантика, на основе которой были построены полностью абстрактные модели для целого спектра языков программирования.Игровая семантика определяет как денотационную, так и операционную модели языка как некоторое взаимодействие, игру, между программой и еёокружением.

Недавние работы (C.-H. L. Ong и W. Blum) показали, что игроваясемантика способна нормализовывать лямбда-термы простого типизированного лямбда-исчисления без использования стандартных подходов, таких как βредукции и окружения. Стратегия вычислений, основанная на данном подходе,получила название головная линейная редукция (Head Linear Reduction), а самподход — трассирующая нормализация (Traversal-Based Normalizarion). Головная линейная редукция играет особую роль в различных подходах к вычислениям, таких как оптимальные редукции, геометрия взаимодействия, сети доказательств и др.3Тем не менее, до сих пор оставался открытым вопрос расширения подхода трассирующей нормализации до исчисления, полного по Тьюрингу.

Такоерасширение определило бы свежий взгляд на функциональные языки программирования, позволяя исследовать их свойства с нового ракурса.Степень разработанности темы исследованияСуществует множество работ, посвящённых лямбда-исчислению и егосвойствам, начиная с классических работ A. Church, A. M. Turing и H. B. Curry.Эти работы были посвящены основам математики и математической логики, и,в частности, теориям сложности и вычислимости. Значительный вклад в теорию лямбда-исчисления внёс голландский математик H. P. Barendregt, предложив так называемый лямбда-куб.

Множество отечественных и зарубежных учёных изучали свойства языков, основанных на лямбда-исчислении, в том числеD. S. Scott и C. S. Strachey построили денотационные модели для целого ряда языков программирования. Тем не менее денотационные модели некоторыхязыков программирования не обладали свойством полной абстракции (FullAbstraction Property), задачу построения которых сформулировал G. Plotkin.В 50-х годах 20 века P.

Lorenzen предложил так называемую игровуюсемантику для логики, которая получила развитие в работах немецкого философа K. Lorenz. Дальнейшее развитие этого подхода такими учёными как S.Abramsky, C.-H. L. Ong, P. Malacaria, R. Jagadeesan и G. McCusker позволило вначале 90-х годов решить задачу, сформулированную G. Plotkin. Дальнейшееразвитие игровая семантика получила в работах J. M. E.

Hyland, A. D. Ker, H.Nickau, W. Blum и др.В последние годы исследование операционных особенностей игрой семантики стало актуальной темой исследований, о чём свидетельствуют работыD. R. Ghica, L. Ong и W. Blum. V. Danos и L. Regnier описывали игровую семантику программ с помощью абстрактных машин KAM (Krivine Abstract Machine)и PAM (Pointer Abstract Machine), а также предложили связать её с линейнойредукцией. L. Ong впервые определил трассирующую нормализацию для простого типизированного лямбда-исчисления, а W.

Blum распространил этот подход до безопасного лямбда-исчисления (Safe Lambda-Calculus). Тем не менее,вопрос распространения подхода трассирующей нормализации до полного поТьюрингу исчисления оставался открытым.4Целью данной работы является обобщение подхода трассирующей нормализации до полного по Тьюрингу исчисления, обоснование корректноститрассирующей нормализации и исследование возможности представления различных языковых конструкций в рамках предложенного подхода при компиляции функциональных языков программирования.Для достижения вышеупомянутой цели были поставлены следующиезадачи.1. Разработать в рамках стратегии вычисления нормального порядка редукций алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления.2. Формально доказать корректность предложенного алгоритма.3. Исследовать возможность адаптации трассирующей нормализациидля различных стратегий вычислений.4.

Исследовать возможность представления различных языковых конструкций в рамках предложенного подхода с точки зрения компиляции основных конструкций функциональных языков программирования.Постановка цели и задач исследования соответствует следующим пунктам паспорта специальности 05.13.11: методы, модели и алгоритмы проектирования и анализа программ и программных систем, их эквивалентных преобразований, верификации и тестирования (пункт 1); языки программирования исистемы программирования, семантика программ (пункт 2).Методология и методы исследованияМетодология исследования основана на идеях и подходах информатикик описанию и анализу понятия вычислимости.

Используются также операционная и денотационная концепции описания семантик языков программирования.В работе использовались методы синтаксического преобразованиялямбда-термов. Для формализации моделей использовался подход к описаниюсемантик в виде систем переходов, а для доказательства их корректности —метод симуляции одной системы переходов другой посредством определенияотношения, связывающего соответствующие состояния этих систем переходов.Были использованы стратегии вычислений вызова по имени, нормального порядка, вызова по значению, аппликативного порядка, головной редукции, линейной редукции и вызова по необходимости.

Для автоматического преобра5зования программ и семантик использовались методы частичных вычисленийи дефункционализации по Reynolds. Программная реализация предложенных вдиссертации результатов была выполнена с помощью языков программирования Haskell и Racket.Основные положения, выносимые на защиту1. Разработан алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления, соответствующий нормальному порядкуредукций.2. Представлена модель полной головной линейной редукции, являющаяся расширением известной модели головной линейной редукции.Предложенная модель формализована в виде системы переходов, доказана корректность этой модели относительно головной редукции.3. Доказана корректность представленного алгоритма трассирующейнормализации относительно предложенной модели полной головнойлинейной редукции путём его формализации в виде системы переходов и дальнейшей симуляции системы переходов для полной головной линейной редукции.

Таким образом, было доказано, что предложенная процедура трассирующей нормализации действительно является нормализирующей.4. Предложенный алгоритм адаптирован для других, отличных от нормального порядка, стратегий вычислений: аппликативного порядкаредукций и вызова по необходимости.5. Предложен и реализован на примере нетипизированного лямбдаисчисления новый метод компиляции функциональных языков программирования в низкоуровневое представление путём специализации представленного алгоритма трассирующей нормализации навходной терм.Научная новизна полученных в ходе исследования результатов заключается в следующем.1. Впервые было введено и формально описано понятие полной головной линейной редукции и доказана её корректность.2.

Алгоритм трассирующей нормализации, представленный в работе,отличается от аналогов (работы L. Ong и W. Blum) тем, что он не накладывает каких-либо ограничений на лямбда-термы, что позволяет6корректно нормализовывать произвольный лямбда-терм. Кроме того,алгоритмы, предложенные L. Ong и W. Blum, применяются лишь кчастным случаям, а именно, к простому типизированному лямбдаисчислению и безопасному лямбда-исчислению.3. Предложен новый подход к компиляции функциональных языковпрограммирования путём специализации процедуры трассирующейнормализации на входной терм, и исследованы её свойства.Теоретическая значимость диссертационного исследования заключается в формализации понятий головной и полной головной линейной редукций,разработке формального алгоритма, решающего задачу трассирующей нормализации, соответствующей полной головной линейной редукции, для бестипового лямбда-исчисления, а также в формальном доказательстве корректностипредставленного алгоритма.Практическая значимостьТрассирующая нормализация представляет собой новый подход к вычислениям, позволяя исследовать ряд свойства языков программирования с нового ракурса.