ПРОГРАММИРОВАНИЕ, 2015, N° 3, с. 73^87
- ПЕРСПЕКТИВЫ СИСТЕМ ИНФОРМАТИКИ
УДК 004.421.6
СУПЕРКОМПИЛЯЦИЯ ДЛЯ ТЕОРИИ ТИПОВ МАРТИНА^ЛЁФА *
© 2015 г. И.Г. Ключников, С.А. Романенко
Институт прикладной математики им. М.В. Келдыша РАН 125047 Москва, Миусская пл., 4 E-mail: ilya.klyuchnikov&gmail.com Поступила в редакцию 01.12.2014
Описывается структура и реализация сертифицирующего суперкомпилятора ТТ Lite, преобразующего исходную программу в пару, содержащую остаточную программу и доказательство того, что остаточная программа эквивалентна исходной. Насколько можно судить по существующим публикациям. сертифицирующая суперкомпиляция для нетривиального функционального языка высшего порядка реализована впервые. Доказательства, порождаемые суперкомпилятором ТТ Lite, могут быть верифицированы проверялыциком типов, который независим от суперкомпилятора и но основан на супоркомпнляцнн. Это существенно в ситуациях, когда решающее значение имеет надежность результатов, полученных с помощью супоркомпнляцнн.
1. ВВЕДЕНИЕ
Суперкомпиляция [1| это метод преобразования программ, первоначально разработанный В.Ф. Турчиным для языка программирования Рефал (функциональный язык нервохх) порядка с вызовом но имени) [2|, и первые супер компиляторы разрабатывались и реализовывались для языка Рефал.
Существующие сей час суперкомпиляторы можно условно разделить на две большие группы оптимизирующие суперкомпиляторы и суперкомпиляторы, трансформирующие программы с целью их последующих) анализа и/или верификации (трансформационный подход).
1.1. Трансформационный анализ и проблема корректности
Примеры применения суперкомпиляции в трансформационном подходе:
• Верификация протоколов [3, 4].
* Работа выполнена при поддержке гранта РФФИ .Л- 12-01-00972-а и гранта Президента РФ для ведущих научных школ Л» НШ-4307.2012.9.
грамм [5]. леммы) [9].
Грубо говоря, суперкомпилятор упрощает и нормализует программу (убирая уровни абстракции и модульности, введенные программистом). Во многих случая преобразованная суперкомпилятором программа более иригодна для автоматического анализа, чем исходная (и, соответственно, преобразованную программу сложнее понять человеку).
Однако трансформационный подход для анализа и верификации программ с помощью суперкомпиляции основан на предположении: суперкомпилятор сохраняяет семантику программ (делает эквивалентные преобразования).
II все дальнейшие рассуждения базируются на этом предположении.
Таким образом, остро встает проблема корректности. II она проявляется так:
• Нетривиальный суперкомпилятор — сложная конструкция, доказательство корректности такого суперкомпилятора даже в математической нотации достаточно объемно и затрагивает разные области информатики (например, доказательство корректности суперкомпилятора HOSC занимает более 30 страниц [10]).
•
ализация суперкомпилятора может содержать ошибки.
•
компилятора — нетривиальная техническая задача [11].
1.2. Суперкомпиляция с доказательством
корректности
Вместо того, чтобы решать нетривиальные технические проблемы с кодированием формально корректного суперкомпилятора на Coq или Agda, мы предлагаем следующий подход:
Пусть суперкомпилятор помимо преобразованной программы выдает также и доказательство корректности преобразования, которое может быть проверено независимым proof checker (например, на Coq или Agda).
Преимущества такого подхода:
•
любом языке (не ограничевается эффективность программиста, пишущего суперкомпилятор).
•
компилятора выявляются независимо.
•
суперкомпиляции (для некоторых задач можно ослаблять требования на корректность) .
1.3. Суперкомпиляция для теории типов
Мартина-Лёфа
Очевидно, что многие проблемы исчезают, если объектный язык суперкомпилятора совпадает с языком для формальных доказательств. Однако принципиальным моментом остается то, что
суперкомпилятор может быть написан на каком угодно языке.
Можно было бы взять уже существующий инструмент, применяемый как для программирования, так и для формальных доказательств (Agda, Coq, Idris, Twelf, Epigram,... ), однако исследовательская цель данной работы — опробовать сам подход сертифицирующего суперкомпилятора, и реализация такого суперкомпилятора для уже существующего инструмента вылилась бы в большое количество технической работы.
Поэтому мы решили реализовать такой суперкомпилятор с нуля. Как оказалось, такой выбор имеет свои преимущества. В качестве базы мы выбрали теориию типов Мартина-Лёфа.
Насколько нам известно, это первый суперкомпилятор, способный сгенерировать автоматически верифицируемое доказательство корректности преобразований.
Важно отметить, что сама суперкомпиляция как трансфрормация является внешней — она происходит вне теории типов, однако доказательство корректности выражено внутри теории типов. По сути дела, мы взяли подход, провозглашенный в статье [12], и применили его к суперкомпиляции.
2. ТТ LITE SC НА ПРИМЕРЕ
Идеи, изложенные в статье, реализованы в суперкомпиляторе для теории типов. Изделие состоит из двух модулей:
•
ция теории типов: проверка типов, вычислитель, интерактивная консоль.
Результаты работы ТТ Lite SC проверяются проверялыциком типов из ядра. (Классическая схема — небольшое ядро и надстройки над ним.)
В ТТ Lite реализованы основные конструкции теории типов, которые излагаются в учебниках по теории типов — зависимые функции, зависимые пары, суммы, произведения, натуральные числа, списки, пропозициональное равенство, пустой тип и единичный тип.
В ТТ Lite SC реализован суперкомпилятор в виде встроенной константы se (реализованной
Рис. 1. Доказательство ассоциативности сложения через нормализацию суперкомпиляцией.
на Scala), которая для любого выражения выдает трансформированное выражение и доказательство того, что трансформированное выражение эквивалентно исходному. И трансформированное выражение, и доказательство являются полноправными объектами языка, которыми можно оперировать.
Рассмотрим вначале пример, показывающий использование ТТ Lite SC для доказательства теорем (рис. 1).
Здесь мы на практике иллюстрируем подход, изложенный в [5]. Сперва (строка 1) мы импортируем определения из файла examples/id.tt (определения из id.tt становятся видны в данном файле).
Так же, как и в Haskell, и в Agda, в ТТ Lite можно не указывать явным образом типы для определений, однако делать это полезно по тем же соображениям, что и для Haskell and Agda для документирования (с типом легче понять, что функция делает) и для тестирования (если тип выражает утверждение о свойствах программы) .
Далее определяется функция сложения двух натуральных чисел. Типизация тривиальна. В ТТ Lite разбор случаев и кодирование рекурсивных определений происходят через один и тот же механизм элиминаторы. Первый аргумент элиминатора тип того, что элиминируется, второй мотив, далее соответствующие ветки вычисления и последний аргумент то, что нужно разобрать по образцу. Далее идет объявление свободных переменных вводятся переменные типа Nat ($х, $х, $х), принято соглашение, что свободные переменные начинаются с доллара. Далее мы определяем, соответственно, два выражения, эквивалентность которых мы хотим показать.
Теперь самое интересное вызывается функция sc (которая реализована как "внешняя функция"), которая для терма el выдает его еуперкомпилированную версию resl и доказательство proof1 того, что el эквивалентно resl. То же самое делается для е2. По сути дела строка 11 просто связывает переменные resl и proof 1 с некоторыми термами, сгенерированными суперкомпилятором.
Всо дальнейшее проверка того, что сгенерированные термы отвечают нашим ожиданиям. Строки 14 15 el и resl эквивалентны (Проверка проводится ядром ТТ Lite Core!). Далее мы проверяем, что el и е2 трансформировались в совпадающие выражения. Ну а далее мы просто конструируем доказательство эквивалентности исходных выражений через библиотечные функции.
Это был пример на доказательство эквивалентности через нормализацию суперкомпиляцией. Как мы видим, рутинная часть генерация доказательства была сделана автоматически.
.3. ТТ LITE: СИНТАКСИС II СЕМАНТИКА
Дальнейший текст предполагает, что читатель знаком с основами теории типов с программистской точки зрения (рекомендуется [1.3] или [14]).
ТТ Lite модульная расширяемая реализация теории типов. Технически говоря, ТТ Lite реализует мономорфную (т.е. тип любого подвыражения устанавливается однозначно) теорию типов с интенсиональным равенством и универсумами.
Описываемый далее суперкомпилятор (ТТ Lite SC) весьма сильно использует вычислитель (нормализатор) и проверялыцик типов. Значит, нам необходимо детально описать правила нормализации и проверки (вывода) типов ТТ Lite.
3.1. Синтаксис
Синтаксис программ на языке ТТ Lite приведен на рис. 2. Программа состоит из списка определений (def) и объявлений (dec). Определения бывают двух видов (в стиле Haskell) с явным указанием типа идентификатора и без него. В ТТ Lite можно объявить идентификатор, указав его тип, но не давая ему определения (первым символом идентификатора в таком случае должен быть $).
Выражение языка ТТ Lite это либо переменная, либо встроенная константа, либо связывание переменной через некоторую встроенную константу b (используется подход абстрактных связывающих деревьев [15]), либо аппликация,
Рис. 2. ТТ Lite language.
Рис. 3. ТТ Lite: встроенные константы.
либо применение элиминатора, либо выражение в скобках.
Синтаксис дружественен программисту на функциональных языках знакомые вещи: переменная, аппликация, связывание обобщает понятие A-абстракции. Eliminator аналогичен case-выражению (через него также выражается примитивная рекурсия, известная функциональному программисту как fold [16]). В [1.3, 14] вводится много "неканонических констант" для вычислений — natrec, listres, ... — мы их заменяем на "универсальный элиминатор" в форме elim etemeie¿. Тогда et — тип "элиминируемых данных", em — явный мотив [17], е- — соответствующая ветка разбора, e¿ — элиминируемые данные.1
Встроенные константы и связывателп ТТ Lite приведены на рис. .3.
Сайт проекта https://github.
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.