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

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

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .125Обзор области исследования . . . . . . . . . . . . . . . . . . . . . . . . 131.1Лямбда-исчисление . . . . . . . . . . . . . . . . . . . . . . . . . . . 131.2Простое типизированное лямбда-исчисление . . . . .

. . . . . . . . 171.3Стратегии вычислений . . . . . . . . . . . . . . . . . . . . . . . . . 191.3.1Слабые порядки редукции . . . . . . . . . . . . . . . . . . . 211.3.2Сильные порядки редукции . . . . . . . . . . . . . . . . . . 221.4Головная нормальная форма и дерево Бёма . . . . . . . . . . . . . . 231.5η-длинная форма терма . . . . . . .

. . . . . . . . . . . . . . . . . . 241.6Головная линейная редукция . . . . . . . . . . . . . . . . . . . . . . 261.6.1Головная линейная редукция: классическое определение . . 271.6.2Трассирующая нормализация . . . . . . . . . . . . . . . . . 291.7Системы переходов . . . . . .

. . . . . . . . . . . . . . . . . . . . . 311.8Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31Полная головная линейная редукция . . . . . . . . . . . . . . . . . . . 332.1Модель головной линейной редукции . . . . . . .

. . . . . . . . . . 332.1.1Головная линейная редукция как система переходов . . . . . 332.1.2Согласованность головной и головной линейной стратегийредукции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 372.23Модель полной головной линейной редукции . . . .

. . . . . . . . . 412.2.1Система переходов для полной головной линейной редукции 412.2.2Корректность модели полной головной линейной редукции43Алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4633.1Семантика, основанная на подстановке . . . . . .

. . . . . . . . . . 473.2Вычисление с окружением . . . . . . . . . . . . . . . . . . . . . . . 473.3Хвосто-рекурсивная семантика . . . . . . . . . . . . . . . . . . . . . 503.4Семантика, основанная на истории и окружении . . . . . . . . . . .

503.5Алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления или семантика, основанная только на истории . 524Корректность алгоритма трассирующей нормализации для нетипизированного лямбда-исчисления . . . . . . . . . . . . . . . . . . . . . . 574.1Головная линейная редукция и ограниченная версия алгоритматрассирующей нормализации . . . . . . . . . . . .

. . . . . . . . . . 594.1.1Система переходов для BUNP . . . . . . . . . . . . . . . . . 594.1.2Соответствие между головной линейной редукцией и ограниченной версией алгоритма трассирующей нормализациидля нетипизированного лямбда-исчисления . . . .

. . . . . 614.2Алгоритм трассирующей нормализации для нетипизированноголямбда-исчисления и полная головная линейная редукция . . . . . 6454.2.1UNP в виде системы переходов . . . . . . . . . . . . . . . . 654.2.2Соответствие между CHLR и UNP . . . . . . . . . . . . . . 67Компиляция путём специализации . . . . . . . . . .

. . . . . . . . . . 715.1Частичные вычисления . . . . . . . . . . . . . . . . . . . . . . . . . 715.2Проекции Футамуры или проекции Футамуры–Ершова–Турчина . 735.3Компиляция нетипизированного лямбда-исчисления путём специализации алгоритма трассирующей нормализации . . . . . . . . . . 7665.3.1Преобразование нормализирующей процедуры в компилятор 765.3.2Специализация UNP на входной лямбда-терм . .

. . . . . . 77Трассирующая нормализация и стратегии вычислений . . . . . . . . 846.1Алгоритм трассирующей нормализации, соответствующий аппликативному порядку редукции . . . . . . . . . . . . . . . . . . . . . . 856.2Об адаптации алгоритма трассирующей нормализации для стратегии вызова по значению . . . . . . . .

. . . . . . . . . . . . . . . . . 906.3Трассирующая нормализация для PCF-подобного языка . . . . . . . 934Заключение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98Список рисунков . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . 110Список таблиц . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112Приложение А. Пример исполнения программ на LLL . . . . . . . . . . . 113Приложение Б. Пример работы системы переходов для алгоритма трассирующей нормализации, соответствующего аппликативному порядку редукции . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . 1205ВведениеАктуальность работыЛямбда-исчисление, наряду с машинами Тьюринга, теорией частичнорекурсивных функций, формальными алгорифмами Маркова и Поста, является одной из основных формальных моделей вычислений [1–3]. Первая модельлямбда-исчисления, предложенная А. Чёрчем (A. Church) в 30-х годах 20 века,оказалась противоречивой: в 1935 году С.

Клини (S. Kleene) и Д. Б. Россер (J. B.Rosser) выявили в ней парадокс, названный в их честь. В 1936 году Чёрч предложил первую непротиворечивую систему, ныне известную как нетипизированное, бестиповое или чистое лямбда-исчисление, а в 1940 году он же предложилмодель простейшего типизированного исчисления — простое типизированноелямбда-исчисление [4]. С тех пор лямбда-исчисление играет особую роль в теории вычислимости и стало основой для целой парадигмы программирования —функционального программирования.Тем не менее, различные языки, основанные на лямбда-исчислении, долгоевремя не имели полностью абстрактных моделей вычислений, т.е.

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

Недавние работы Л. Онга и В. Блюма (C.-H. L. Ong и W. Blum) показали, что игровая семантика способна нормализовывать лямбда-термы просто-6го типизированного лямбда-исчисления без использования стандартных подходов, таких как β-редукции и окружения [6, 7]. Стратегия вычислений, основаннаяна данном подходе, получила название головная линейная редукция (Head LinearReduction) [8–10], а сам подход — трассирующая нормализация (Traversal-BasedNormalizarion) [6, 11, 12]. Головная линейная редукция играет особую роль в различных подходах к вычислениям, таких как оптимальные редукции [13–16], геометрия взаимодействия [17, 18], сети доказательств [19, 20] и др.Тем не менее, до сих пор оставался открытым вопрос расширения подходатрассирующей нормализации до исчисления, полного по Тьюрингу.

Такое расширение определило бы свежий взгляд на функциональные языки программирования, позволяя исследовать их свойства с нового ракурса.Степень разработанности темы исследованияСуществует множество работ, посвящённых лямбда-исчислению и его свойствам, начиная с классических работ А. Чёрча [4, 21, 22], А. М. Тьюринга (A.

M.Turing) [23–25] и Х. Б. Карри (H. B. Curry) [26–29]. Эти работы были посвящены основам математики и математической логики, и, в частности, теориям сложности и вычислимости. Значительный вклад в теорию лямбда-исчисления внёсголландский математик Х. П. Барендрегт (H. P. Barendregt), предложив так называемый лямбда-куб [30, 31]. Множество отечественных и зарубежных учёныхизучали свойства языков, основанных на лямбда-исчислении, в том числе Д. С.Скотта (D. S. Scott) и К. Страчей (C. S.

Strachey) построили денотационные моделидля целого ряда языков программирования [32–35]. Тем не менее, денотационныемодели некоторых языков программирования не обладали свойством полной абстракции (Full-Abstraction Property), задачу построения которых сформулировалG. Plotkin [5, 36].В 50-х годах 20 века П. Лоренсен (P. Lorenzen) предложил так называемую игровую семантику для логики [37], которая получила развитие в работах немецкогофилософа К. Лоренца (K. Lorenz) [38]. Дальнейшее развитие этого подхода такимиучёными как С.