«ВЫЯВЛЕНИЕ И ДОКАЗАТЕЛЬСТВО СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДАМИ СУПЕРКОМПИЛЯЦИИ ...»

ИНСТИТУТ ПРИКЛАДНОЙ МАТЕМАТИКИ

им. М.В. КЕЛДЫША

РОССИЙСКОЙ АКАДЕМИИ НАУК

На правах рукописи

Ключников Илья Григорьевич

ВЫЯВЛЕНИЕ И ДОКАЗАТЕЛЬСТВО

СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ

МЕТОДАМИ СУПЕРКОМПИЛЯЦИИ

05.13.11 математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Диссертация на соискание учёной степени кандидата физико-математических наук

Научный руководитель кандидат физико-математических наук Романенко С.А.

Москва 2010 Оглавление Введение 1 Позитивная суперкомпиляция и анализ программ 1.1 Исторический обзор........................ 1.1.1 Суперкомпиляция Рефала................ 1.1.2 Суперкомпиляция функциональных языков первого порядка........................... 1.1.3 Суперкомпиляции императивных языков....... 1.1.4 Суперкомпиляция функциональных языков высшего порядка......................... 1.1.5 Другие работы....................... 1.2 Суперкомпиляция функционального языка первого порядка 1.2.1 Примеры суперкомпиляции............... 1.2.2 Синтаксис и семантика языка SLL........... 1.2.3 Обобщение и гомеоморфное вложение SLL-выражений 1.2.4 Построение дерева процессов.............. 1.2.5 Построение частичного дерева процессов....... 1.3 Анализ состояния дел в суперкомпиляции с точки зрения трансформационного анализа программ............ 1.4 Выводы............................... 2 Язык HLL: синтаксис и семантика 2.1 Формализация языка HLL.................... 2.2 Синтаксис языка HLL....................... 2.3 Подстановка............................ 2.4 Семантика языка HLL...................... 2.5 Типизация............................. 2.6 Алгебра HLL-выражений..................... 2.7 Выводы............................... 3 Структура суперкомпилятора HOSC 3.1 Устранение локальных определений.............. 3.2 Представление множеств..................... 3.3 Построение частичного дерева процессов........... 3.4 Генерация остаточной программы................ 3.5 Отношение транформации HOSC................ 3.6 Выводы............................... 4 Корректность суперкомпилятора HOSC 4.1 Операционная теория улучшений................ 4.2 Корректность отношения трансформации HOSC0...... 4.3 Корректность отношения трансформации HOSC1/2..... 4.3.1 Пример сведения отношения HOSC1/2 к отношению HOSC0........................... 4.4 Корректность отношения трансформации HOSC...... 4.5 Типизация и корректность.................... 4.6 Выводы............................... 5 Схема суперкомпилятора HOSC 5.1 Язык HLL: вложение и обобщение............... 5.2 Параметризованный HLL суперкомпилятор.......... 5.2.1 Конкретные HLL суперкомпиляторы.......... 5.3 Сравнение суперкомпиляторов................. 5.4 Усиление уточненного вложения с учетом типизации.... 6.1 Абстрактные преобразователи программ............ 6.3.1 Замена case-выражений на конструкторы....... 6.3.2 Замена имен переменных на индексы де Брюина... 6.4 Завершаемость суперкомпилятора SC........... 6.5 Пересмотр обработки ситуации зацикливания........ 6.6 Завершаемость остальных суперкомпиляторов........ 7.1 Моделирование знаний в виде программ............ 7.2 Доказательство свойств программ методами суперкомпиляции................................. 7.3 Доказательство эквивалентности выражений......... 7.3.1 Доказательство эквивалентности выражений, основанное на равенстве.................... 7.3.2 Доказательство эквивалентности выражений, основанное на нормализации................. 7.3.3 Генерация множеств эквивалентных выражений... 8.1 Многоуровневая суперкомпиляция............... 8.1.1 Накапливающий параметр: базовая суперкомпиляция 8.1.2 Накапливающий параметр: применение леммы.... 8.1.3 Соединение суперкомпиляторов, переход к многоуровневой суперкомпиляции................. 8.1.4 Генерация множества остаточных программ..... 8.2 Корректность = эквивалентность + улучшение........ 8.2.1 Распознавание улучшающих лемм........... 8.3 Модельный двухуровневый суперкомпилятор......... 8.4.1 Суперкомпиляция нелинейного выражения...... 8.4.3 Улучшение асимптотики программ........... Введение Объект исследования и актуальность работы Компьютерные программы часто содержат ошибки. В современном программирование при написании программы избежать ошибок практически невозможно. Размер промышленных программ начинается от десятков тысяч строк кода, а большие промышленные системы достигают миллионов строк кода. Мысленно охватить работу больших систем ни один человек не в состоянии. Сложность разрабатываемого программного обеспечения подошла к границе его понимания и, следовательно, управляемости.

Материальные последствия ошибок программного обеспечения могут быть весьма значительными, порой приводящими к полному провалу дорогостоящих проектов и потере репутации.

Ошибки в сложных программных и аппаратных системах не являются чем-то особенным – они регулярно появляются в сложных системах.

Их причинами являются и некорректные спецификации, и неправильное понимание спецификаций разработчиками, непредвиденные условия работы, несогласованность и многое другое. Правильность и корректность поведения систем являются более важными свойствами, чем производительность, модифицируемость, скорость разработки и т.д.

Существует потребность в инструментах анализа программ на предмет ошибок и соответствие спецификации.

Наиболее очевидным и широко распространенным методом проверки правильности систем является тестирование - проверка построенной системы в различных ситуациях, при различных исходных данных. Наиболее распространено модульное тестирование (unit testing). Инструменты для модульного тестирования существуют практически для любого языка программирования [38]. При модульном тестировании рассматривается некоторый компонент, например некоторый модуль (функция) f, принимающий на вход некоторый параметр X. Результатом работы модуля являются некоторые данные Y :

Проверяется, обладает ли ответ Y предполагаемыми свойствами, заложенными в систему. Часто проверка этих свойств кодируется на том же самом языке, на котором написана программа, в виде предиката (функции) p и считается, что на данных входных значениях модуль f работает корректно, если предикат верен:

Или:

Если при тестировании проверяется работа модуля на входных параметрах X1, X2,..., Xn, то, соответственно, рассматривается выполнение предикатов Зачастую предикат может сам зависеть от значений входного параметра:

Тогда рассматриваются выполнения предикатов Тестирование имеет множество преимуществ:

• Рассматривается реальная система.

• Проверка может выполняться в реальной среде с реальными интерфейсами.

• Проверять можно наиболее опасные или часто используемые режимы работы системы.

• Программист сам пишет тесты на том же языке, на котором написана программа.

В то же время у тестирования есть и недостатки:

• Тестированием можно проверить лишь немногие траектории вычисления системы (их обычно бесконечное множество).

• Тестированием сложно проверить редко выявляющиеся ошибки, особенно ошибки в системах реального времени.

• Тестирование не может гарантировать правильность системы: “тестированием можно доказать только наличие ошибок”. (Дейкстра).

Другим подходом к проверке корректности программ является формальная верификация продукта. Формальная верификация программ – приемы и методы формального доказательства (или опровержения) того, что программа удовлетворяет заданной формальной спецификации. Одним из распространенных методов формальной верификации программ является проверка на моделях программ (model checking) [18]. Доказать, что конкретная реализация продукта (программа) удовлетворяет некоторым формальным требованиям очень сложно, поэтому при проверке на моделях проверяется не сама программа, а ее формальная модель. Формальная модель строится вручную. Обычно такая модель значительно проще проверяемой системы, – это абстракция, которая отражает наиболее существенные характеристики системы. Как и в случае тестирования, при проверке на моделях при описании условий корректности записывается некоторый предикат (логическая формула) относительно модели, и проверяется, будет ли заданная формула выполняться всегда на данной модели. Соответственно, есть различные языки описаний моделей и логических формул (темпоральные логики, структуры Крипке, бинарные решающие диаграммы, и т.д.).

Проверка на моделях программ обладает следующими преимуществами.

• Полнота. Для многих формализаций проверка на моделях программ либо доказывает, что модель всегда удовлетворяет формуле, либо находит ошибку.

• Проверка на моделях программ может находить логические ошибки, так как работает с моделью программы, а не с реализацией.

• Можно проверять модель программы еще до написания самой программы.

Однако и у формальной верификации есть ряд недостатков:

• Проверяется не сама программа, а ее модель. Такая модель может быть неадекватной. Таким образом, ценность верификации зависит от адекватности модели. Модель - некоторое неисполняемое представление исполняемой программы. Модель в некотором смысле чужда программисту.

• Язык спецификации может быть неполным, недостаточным для формулировки всех требований.

• Процесс верификации автоматизирован, но модель программы пишет человек. Требуется очень высокая квалификация персонала, чтобы изготовить адекватную модель.

Существуют методы, в которых модель программы (вычислений) строится автоматически, – несущественные с точки зрения системы детали отбрасываются, и затем происходит моделирование вычислений. Здесь уместно упомянуть такие методы как символьное выполнение [55] и абстрактную интерпретацию [20]. В некоторых случая утверждения о корректности программ записываются практически на том же самом языке, что и верифицируемая программа [131].

Как было отмечено, главным недостатком тестирования предиката p(X, f (X)) при конкретных условиях является неполнота. Успешное выполнение тестов не гарантирует отсутствия ошибок.

Предикат p пишется обычно (и это правильно для тестирования) без учета внутренней структуры программы f. Если приглядеться к проверяемому выражению p(X, f (X)), то легко увидеть, что оно является композицией двух функций – предиката и проверяемой функций f. Существуют методы преобразований программ, способные упрощать композицию двух функций. В случае выражения p(X, f (X)) преобразование специализирует предикат p для конкретной функции f. Результатом преобразования будет некоторая функция p зависящая только от входного параметра X, но учитывающая особенности композиции конкретного предиката p и конкретной функции f. Если преобразованная программа обладает более простой и ясной структурой по сравнению с исходными программами p и f, то с помощью очень простого анализа текста программы удается показать, что преобразованная программа выдает только T rue, или найти такие входные параметры X, когда она выдает F alse.

Одним из методов преобразований программ, способных упрощать композицию функций, является суперкомпиляция. Одним из успешных применений суперкомпиляции для проверки корректности программ является верификация с помощью суперкомпиляции реализаций (на языке РЕФАЛ) ряда протоколов кэш-когерентности, выполненная Андреем Немытых [71] (при этом, в некоторых протоколах удалось найти ошибки).

Реализация протокола принимала в качестве входа конечную цепочку команд, и проверялось состояние памяти после выполнения этих команд.

Требования, которым должна удовлетворять реализация протокола, кодировались в виде предиката, проверяющего состояния ячеек.

Суть трансформационного анализа программ можно сформулировать следующим образом: вместо того, чтобы анализировать исходную программу, эта программа вначале преобразуется в эквивалентную ей программу, и затем анализируется уже преобразованная программа. Если используемый метод преобразования программ способен устранять многие избыточности исходной программы, то в некоторых случаях анализ остаточной программы становится тривиальным [127, 40].

Подчеркнем, что если утверждения о корректности программы (спецификация) закодированы на том же языке, что и сама программа, то можно преобразовывать программу с учетом спецификации, – больше шансов на то, что несущественные с точки зрения спецификации детали реализации будут отсутствовать в остаточной программе. Для плодотворности такого подхода необходимо, чтобы рассматриваемый язык программирования обладал достаточными изобразительными средствами для написания высокоуровневых спецификаций и одновременно позволял осуществлять глубокие преобразования программ с сохранением семантики.

Функциональный язык программирования Haskell можно рассматривать как язык исполняемых спецификаций [46]. Программы на языке Haskell имеют, как правило, простую и ясную структуру и в то же время достаточно хорошо поддаются упрощающим преобразованиям (с сохранением семантики). Семантика языка Haskell детально формализована [110]. Язык Haskell обладает мощными изобразительные средствами, которые облегчают написание на нем спецификаций:

• Функции высших порядков.

• Бесконечные структуры данных.

• Автоматический вывод и проверка типов.

Таким образом, существуют предпосылки для трансформационного анализа программ, написанных на языке Haskell.

В данной работе исследовались возможности применения суперкомпиляции для трансформационного анализа программ на языке Haskell.

Цели и задачи работы Исторически главной целью суперкомпиляции была оптимизация программ. Работы последних лет по созданию суперкомпиляторов также ориентированы на использование суперкомпиляции как средства оптимизации программ.

Целью данной работы является изучение возможностей применения суперкомпиляции для трансформационного анализа программ.

Стоит отметить, что цели оптимизации программ и анализа программ в некоторой степени противоречат друг другу. Главная цель оптимизации программы – получить небольшую и быструю программу, которая может быть труднопонимаемой для человека, иметь запутанную и странную структуру. Более того, оптимизатор не обязательно выдает программу, эквивалентную исходной! Если исходная успешно программа завершается на некоторых входных данных и выдает осмысленный результат, то, несомненно, оптимизированная программа также должна завершаться и выдавать тот же результат. Однако, если исходная программа не завершается, или завершается аварийно, оптимизированной программе позволительно завершаться и выдавать некоторый произвольный результат (особенно, если это позволяет ускорить программу или уменьшить ее размер). Например, суперкомпилятор SCP4 [71, 72] часто осуществляет преобразования функций с расширением области определения.

Если же некоторый метод преобразования программ используется не для оптимизации программ, а для анализа программ, то не предполагается выполнения преобразованных программ. Таким образом, размер и скорость выполнения преобразованной программы больше не играют главной роли. В частности, при преобразованиях позволительно дублировать код. Например, следующее выражение let определенно можно преобразовать в С другой стороны, желательно, чтобы преобразованная программа имела тот же смысл (ту же семантику), что и исходная программа, когда метод преобразования программ используется для анализа.

Суперкомпилятор, применяемый для трасформационного анализа программ должен удовлетворять следующим требованиям:

• Гарантированно сохранять семантику программы. В противном случае выводы, сделанные из анализа остаточной программы могут быть необоснованными или ошибочными.

• Гарантированно завершаться на любой входной программе. Иначе сложно распознавать ситуации, когда для суперкомпилятора требуется дополнительное время и когда суперкомпилятор зациклился.

• Иметь доступный исходный код. Иначе нет возможности формально убедиться в корректности реализации суперкомпилятора.

Как показал анализ положения дел в суперкомпиляции (см. следующую главу), такого суперкомпилятора на момент начала диссертационной работы (2007 год) не существовало1. В тоже время, как отмечено в предыдущем разделе, существуют предпосылки для трансформационного анализа программ, написанных на языке Haskell.

Поэтому автор поставил перед собой следующие задачи:

1. Разработать метод суперкомпиляции функциональных программ, ориентированный на трансформационный анализ.

2. Разработать на базе метода алгоритм суперкомпиляции программ, написанных на ядре языка Haskell, сохраняющий семантику программ и гарантированно завершающийся на любой входной программе.

3. Реализовать разработанный алгоритм в экспериментальном суперкомпиляторе.

4. Апробировать экспериментальный суперкомпилятор на модельных задачах по выявлению и доказательству свойств программ.

1 Вообще, а не только для языка Haskell.

Научная новизна работы Структура суперкомпилятора, предложенная в работе, допускает более глубокие преобразования программ, чем методы суперкомпиляции, ориентированные на оптимизацию, с помощью двух приемов:

1. Рассматривается операционная семантика вызова по имени (callby-name), а не семантика вызова по необходимости (call-by-need)2.

Непосредственно перед суперкомпиляцией все локальные определения (let-выражения) поднимаются на верхний уровень методом лифтинга, что позволяет существенно упростить дальнейший конфигурационный анализ и агрессивно распространять информацию о текущей конфигурации вниз по дереву процессов.

2. Частичное дерево процессов, напротив, преобразуется в программу без глобальных определений, – одно самодостачное выражение, где рекурсивные функции определяются в том же месте, где и используются. Вместе с первым приемом это позволяет приводить одинаковые по смыслу, но текстуально разные программы к одной и той же синтаксической форме.

В отличие от других работ, где суперкомпилятор рассматривается как фиксированная монолитная конструкция, в данной работе вначале определяется структура суперкомпилятора HOSC в виде отношения трансформации HOSC, – фиксируются методы (без деталей реализации) построения частичного дерева процессов и преобразования частичного дерева процессов в остаточную программу, доказывается корректность отношения трансформации HOSC. То есть доказывается корректность не конкретного алгоритма, а множества алгоритмов, удовлетворяющих отношению трансформации HOSC.

Доказательство корректности отношения трансформации HOSC опирается на операционную теорию улучшений Дэвида Сэндса. Стандартный способ доказать корректность трансформации – показать, что остаточная программа является улучшением исходной (в терминологии Сэндса).

2 Конечные результаты работы программы при семантике вызова по имени и вызова по необходимости совпадают В работе показана корректность трансформации HOSC в общем случае – включая те случаи, когда остаточная программа не является улучшением (в терминологии Сэндса) исходной программы.

Все определенные далее алгоритмы суперкомпиляции удовлетворяют отношению трансформации HOSC и, следовательно, корректны.

Язык Haskell является функциональным языком высшего порядка. На момент начала диссертационной работы методы и алгоритмы суперкомпиляции для языков высшего порядка были слабо разработаны, – в существовавших работах использовались алгоритмы суперкомпиляции для языка первого порядка, адаптированные для языков высшего порядка, не учитывающие всех синтаксических и семантических особенностей языков высших порядков.

В данной работе при разработке алгоритмов для суперкомпиляции ядра языка Haskell была произведена ревизия классических алгоритмов суперкомпиляции с учетом работы с функциями высших порядков:

1. Сделана ревизия обработки ситуации зацикливания, – использование -абстракций и функций как данных позволяет писать рекурсивные “функции” без явного использования рекурсии. Как результат во время построения дерева процессов необходимо чаще делать проверку на возможное зацикливание.

2. В выражениях присутствуют связанные переменные: сделаны ревизии гомеоморфного вложения и обобщения, учитывающие свойства связанных переменных.

Классическое гомеоморфное вложение является вполне-квазиупорядочением на всем множестве выражений языка при использовании конечного числа конструкторов и функций. Уточненное гомеоморфное вложение не является вполне-квазиупорядочением на всем множестве выражений языка. Однако, как показано в работе, уточненное гомеоморфное вложение является вполне-квазиупорядочением множестве выражений, возникающих при построении дерева процессов, что достаточно для доказательства завершаемости алгоритмов суперкомпилятора HOSC.

В результате выбранные методы и алгоритмы обеспечивают способность суперкомпилятора HOSC к нормализации выражений, что позволяет свести задачу распознавания эквивалентных программ к автоматическому распознаванию синтаксической эквивалентности текстов преобразованных суперкомпилятором программ.

В результате обобщения в дереве процессов появляются лишние трассы и как результат в остаточной программе появляется недостижимый код, который, как правило, затрудняет анализ остаточной программы.

Чем меньше в остаточной программе недостижимого кода, тем легче она поддается анализу. Цель предложенного метода многоуровневой суперкомпиляции – получить в результате суперкомпиляции программу с как можно меньшим объемом недостижимого кода. Средство достижения цели – избежать (или как минимум отложить) обобщения конфигураций (“уход из под свистка”) с помощью замены конфигурации, вынуждающей суперкомпилятор сделать обобщение на эквивалентную ей, которая позволяет продвинуться дальше без обобщений. Эквивалентные конфигурации (для замены) распознаются методом нормализацией через суперкомпиляцию. Корректность многоуровневой суперкомпиляции обеспечивается тем, что конфигурация может заменяться только на “улучшение” (в терминологии Сэндса).

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

Практическая значимость работы Диссертационная работа дает положительный ответ на вопрос о возможности использования суперкомпиляции для трансформационного анализа программ.

На основе разработанных алгоритмов и методов создан экспериментальный суперкомпилятор HOSC для ядра языка Haskell.

Показано, что распознавание эквивалентных выражений методом нормализации суперкомпиляцией может происходить в полностью автоматическом режиме. Распознавание улучшающих лемм с помощью суперкомпиляции происходит также в полностью автоматическом режиме.

На базе суперкомпилятора HOSC создан многоуровневый суперкомпилятор TLSC, способный производить более глубокие преобразования программ, в частности, улучшать асимптотику программ.

Апробация работы и публикации Результаты работы докладывались на следующих конференциях и семинарах:

• Международный семинар “First International Workshop on Metacomputation in Russia, META’08”, Россия, Переславль-Залесский, 2008.

• Научный семинар по языкам программирования “Copenhagen Programming Language Seminar (COPLAS)” на факультете информатики Копенгагенского университета, Дания, Копенгаген, 2008.

• Седьмая международная конференция памяти Андрея Ершова “Perspectives of System Informatics, PSI’09”, Россия, Новосибирск, 2009.

• Международный семинар “International Workshop on Program Understanding, PU’09”, Россия, Алтай, 2009.

• Объединенный научный семинар по робототехническим системам ИПМ им. М.В. Келдыша РАН, МГУ им. М.В. Ломоносова, МГТУ им. Н.Э. Баумана, ИНОТиИ РГГУ и отделения “Программирование” ИПМ им. М.В. Келдыша РАН, Россия, Москва, 2009.

• Семинар московской группы пользователей языка Haskell (MskHUG), Москва, 2009.

• Международный семинар “Second International Workshop on Metacomputation in Russia, META’10”, Россия, Переславль-Залесский, 2010.

• Научный семинар ИСП РАН, Россия, Москва, 2010.

По результатам работы имеются четыре публикации, включая одну статью в рецензируемом научном журнале из списка ВАК (1), одну статью в международном периодическом издании (3), две статьи в сборниках трудов международных научных семинаров (2, 4):

1. Ключников И.Г., Романенко С.А. SPSC: Суперкомпилятор на языке Scala // Программные продукты и системы. – 2009. – №2 (86). – С. 74-80.

2. Klyuchnikov I., Romanenko S. SPSC: a Simple Supercompiler in Scala // International Workshop on Program Understanding, PU 2009, Altai Mountains, Russia, June 19-23, 2009. – Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009. – Pp. 5-17.

3. Klyuchnikov I., Romanenko S. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation // Perspectives of Systems Informatics. 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. – Vol. 5947 of LNCS. – Springer, 2010. – Pp. 193-205.

4. Klyuchnikov I., Romanenko S. Towards Higher-Level Supercompilation // Proceedings of the second International Workshop on Metacomputation in Russia. Pereslavl-Zalessky, Russia, July 1-5, 2010. – Pereslavl-Zalessky:

Ailamazyan University of Pereslavl, 2010. – Pp. 82-101.

Глава Позитивная суперкомпиляция и анализ программ В данной работе исследуется возможности применения суперкомпиляции для трансформационного анализа программ.

Суперкомпиляция является одним из методов метавычислений. Теория метавычислений занимается построением конструктивных и эффективных метапрограмм, способных осуществлять вычисление, преобразование и анализ программ.

Метапрограмма (суперкомпилятор) является метасистемой над программами. Процитируем В.Ф. Турчина:

Представим себе некоторую систему S. И представим, что какоето число систем S или систем типа S соединены в единое целое и снабжены вдобавок какой-то управляющей ими системой. Образованную таким образом систему S+ назовем метасистемой по отношению к системе S. Метасистема S+ содержит ряд систем S в качестве своих подсистем и содержит также средства, позволяющие управлять этими подсистемами – в самом широком смысле: координировать их работу, модифицировать их, генерировать и т. д. Переход от системы S к метасистеме S+ мы называем метасистемным переходом.

В книге “Феномен науки” [124] утверждается, что метасистемный переход является квантом эволюции и любое качественное изменение является метасистемным переходом. Таким образом, предметом рассмотрения метавычислений является автоматическая эволюция программ.

1.1 Исторический обзор В данном кратком обзоре мы затрагиваем только работы, посвященные суперкомпиляции и оставляем в стороне работы, посвященные другим методам метавычислений.

1.1.1 Суперкомпиляция Рефала Творческое наследие В.Ф. Турчина по суперкомпиляции (а более обще – по метавычислениям) необычайно многогранно. Как показали дальнейшие исследования, в работах В.Ф. Турчина рассыпано множество плодотворных идей, которые требует переосмысления. Многие концепции описаны недостаточно формально или частично, и чаще всего в терминах языка Рефал. Чрезвычайно интересно отделить эти идеи от языка Рефал и рассмотреть их в контексте современных языков программирования. Эти концепции требуют дальнейшей разработки и ждут своего исследователя. Поскольку для Турчина суперкомпиляция была неразрывно связана с языком Рефал, в данном разделе мы рассматриваем только основные вехи работы В.Ф. Турчина по суперкомпиляции, не затрагивая связь с Рефалом.

Первым шагом на пути к метасистемным переходам в программировании, по словам Турчина [125], явилось создание языка программирования, предназначенного для определения семантик других языков. Первая версия такого языка называлась метаалгоритмическим языком [136, 138], который затем стал называться Рефал [137]. Первый эффективный интепретатор языка Рефал был реализован в 1968 [141]. Компиляторы с языка Рефал были созданы для большинства вычислительных машин того времени. Библиография работ, посвященных разработке и использованию Рефала насчитывает более двухсот единиц [125].

В 1972 году выходят работы, описывающие преобразование Рефалпрограмм [139, 140], в частности, в работе [140] описывается прогонка, – главная составляющая суперкомпиляции.

В конце 70-х - начале 80-х выходят публикации, описывающие идею суперкомпиляции [112, 114].

В 1982 эксперименты с суперкомпилятором были описаны Турчиным и его коллегами [123].

В 1986 году выходят статьи, описывающие в подробностях прогонку [116, 115].

В работе [117] Турчин формулирует основания математики в терминах теории метасистемных переходов.

В 1988 году выходит работа, посвященная проблеме завершаемости суперкомпилятора, и описывается автоматический алгоритм обобщения [118].

В 1989 году Турчин (совместно с Робертом Глюком) добился самоприменения суперкомпилятора [36].

В 1990 году Турчин (совместно с Робертом Глюком) в работе [37] продемонстрировал, что суперкомпилятор способен автоматически генерировать из наивного распознавателя подстроки в строке KMP-алгоритм.

В 1993 Турчин описывает расширение суперкомпиляции [119]. В этом расширении суперкомпилятор применяется не напрямую к функции, а к метафункции (интерпретатору, который вычисляет функцию по ее определению и абстрактным данным).

В отчете [122] описывается работа с метакодом, поднятыми переменными1 и метасистемными прыжками, в отчете также вводится язык MSTсхем2. Рассмотрение плоского3 Рефала и метасистемных прыжков позволяет добиться самоприменения суперкомпилятора [84].

В отчете [120] описываются различия между списками (данными языка LISP) и строками (данными языка Рефал) с точки зрения распознавания вложения и обобщения.

В работе [121] описывается ориентированный на программирование суперкомпилятора язык SPCL4. Язык SPCL позволяет более ясно и модульно разрабатывать суперкомпиляторы.

1 elevatedvariables 2 MST = MetaSystem Transition 3 Разрешается использовать только хвостовую рекурсию 4 a supercompilation language В [125] рассматривается совмещение суперкомпиляции и многократных метасистемных переходов.

В работе [83] продемонстрированы эксперименты по увеличению возможностей суперкомпилятора методом, описанным в [119], – добавить интерпретатор между суперкомпилятором и преобразуемой программой.

Суперкомпилятор SCP4 [80, 82] для языка Рефал-5, использует свойства языка Рефал (ассоциативность конкатенации) и помимо методов суперкомпиляции включает дополнительные инструменты: распознавание частично рекурсивных константных функций, распознавание частично рекурсивных мономов конкатенации, нахождение и анализ выходных форматов. Мономы конкатенации описываются в [81]. Стоит отметить, что суперкомпилятор SCP4 может расширять область определения программы в следующем смысле: если на каком-то входном данном исходная программа завершалась с ошибкой или зацикливалась, то преобразованная программа может завершаться и выдавать некоторое значение.

В работах [69, 71, 70, 72] задача верификации рассматривается как задача параметризованного тестирования, и показывается, как параметризованное тестирование может быть осуществлено средствами суперкомпиляции.

1.1.2 Суперкомпиляция функциональных языков первого порядка Изначально суперкомпиляция была неотделима от языка Рефал и формулировалась в его терминах.

Рефал является чистым функциональным языком с сопоставлением по образцу. Для операций с символьной информацией Рефал использует R-выражения. Исследователи отмечают, что по сравнению с другими функциональными языками в языке Рефал образец определяется достаточно сложным образом, одной из причин этой сложности является неортогональность образцов, – алгоритм сопоставления с образцом зависит от порядка их перечисления. Как следствие, алгоритмы сопоставления с образцом и любые метаалгоритмы, рассматривающие Рефал-программы как входные данные, сложно сформулировать и объяснить.

К сожалению, как отмечает Сёренсен, механизмы конкретизации и развертки, лежащие в основе прогонки, сильно зависят от сопоставления с образцом. Таким образом, даже прогонка для Рефала формулировалась достаточно сложным образом, не говоря об обобщении. Также, ни в одной работе, посвященной суперкомпиляции Рефала, алгоритм суперкомпиляции не приведен полностью. По этим причинам, несмотря на значительное количество опубликованных работ, к началу 1990-х суперкомпиляция не обрела признания за пределами узкого круга экспертов. Более того, практически все основные составляющие суперкомпиляции описывались без должной доли формализма – зачастую неформально и расплывчато, По мнению многих (в том числе западных) исследователей, основным трудом, описывающим идеи суперкомпиляции является статья Турчина 1986 года “The concept of a supercompiler” [116]. Статья обобщает идеи суперкомпиляции в достаточно сжатом виде. И, к сожалению, затрудняет восприятие из-за отсутствия хорошо проработанной терминологии (и формализации) для представления новых понятий5.

В упомянутой классической работе Турчина [116] используется достаточно сложный язык для представления конфигураций (в силу сложности алгоритмов сопоставления с образцом в Рефале). Из-за неортогональности образцов сильно усложняется и конфигурационный анализ, – из графа конфигураций сложно вычленить конфигурацию как таковую, – конфигурация определяется не только путем от начального узла до текущего узла, – необходимо учитывать и структуру всего графа (следствие того, что важен порядок задания образцов). В результате определяется достаточно сложный обобщенный алгоритм сопоставления с образцом, лежащий в основе прогонки.

Работа [33] Андрея Климова и Роберта Глюка о сущности прогонки рассматривала в качестве входного языка S-Graph, который можно рассматривать как подмножество языка программирования LISP, – по сути, эта была одна из первых работ, нацеленных на понимание суперкомпиляНапример, в терминологии Турчина в результате прогонки получается граф состояний и переходов. В результате суперкомпиляции также получается граф состояний и переходов. Дальнейшие исследователи более тщательно проработали терминологию, – в современных понятиях в результате прогонки получается дерево процессов, а целью суперкомпиляции является превращение потенциально бесконечного дерева процессов в конечное частичное дерево процессов (иногда таже называемое графом конфигураций).

ции как общего метода – без привязки к языку Рефал. В работе Климова и Глюка показано, что если взять язык с более очевидным сопоставлением с образцом (полный интерпретатор языка S-Graph занимает треть страницы6 ), то работа с конфигурациями сильно упрощается, – (1) можно вычленить рассмотрение конфигурации (обобщенного состояния) от дерева процессов, (2) можно достаточно просто определить язык для конфигураций и (3) обобщенный алгоритм сопоставления с образцом становится тривиальным. В работе явным образом разделяются понятия дерева процессов и графа процессов (частичного дерева процессов). Статья [33] является первой работой, где прогонка и суперкомпиляция (без обобщения) описаны формально (в виде алгоритмов на языке Haskell). Конфигурация представлена как место в программе (program point) и обобщенная среда. Обобщенная среда состоит из связей (позитивной информации) и рестрикций (негативной информации, ограничений на переменные).

В магистерская диссертация Морте Х. Сёренсена [103], рассматривается простой функциональный язык первого порядка (язык Miranda без функций высшего порядка с семантикой вызова по имени). В работе Сёренсена впервые целиком и формально описываются все составляющие суперкомпиляции – прогонка, обобщение, генерация остаточной программы, и приводятся доказательство корректности суперкомпилятора и доказательство его завершаемости на любой входной программе. Особое внимание уделяется языку M0, в котором при описании условий должны быть разобраны все случаи (нет if -выражений). В этом случае понятие негативной информации не имеет смысла, и достаточно распространять только позитивную информацию. По сравнению с работой Климова и Глюка конфигурации представляются еще более простым образом – конфигурация является просто выражением языка со свободными переменными. Также в работе Сёренсена дается хороший обзор исторических взаимосвязей с другими методами метавычислений. Сёренсоном рассматриваются языки M1/2 и M1, и суперкомпиляция описывается для них только с распространением позитивной информации, – чтобы сохранить простоту конфигурационного анализа. За таким видом суперкомпиляции закрепилось название позитивная суперкомпиляция.

6 Сложно представить себе интерпретатор языка Рефал такого размера Работы [33] и [103] открывают целую серию работ, направленных на лучшее понимание суперкомпиляции и ее связь с другими методами метавычислений (преобразований программ).

В статьях [31, 32] иллюстрируется применение интерпретационного подхода, описанного Турчиным в работе [119]: показано, как с помощью добавления слоя интерпретации можно из частичного вычислителя получить дефорестатор и суперкомпилятор.

В работе [34] на основе анализа определений и принципов построения показывается, что частичная дедукция логических программ аналогична прогонке функциональных программ и обе техники имеют общий принцип – распространение информации.

В статье [48] прогонка рассматривается с фундаментальной точки зрения – с точки зрения семантики и без привязки к конкретному языку программирования и структурам данным.

В работе [106] суперкомпиляция сравнивается с частичными вычислениями, дефорестацией и обобщенными частичными вычислениями с точки зрения количества информации, накапливаемой и используемой во время преобразований.

В статье [104] подробно описывается использование гомеоморфного вложения как синтаксического критерия для принятия решения о необходимости обобщения конфигураций. Использования отношения гомеоморфного вложения сравнивается со стековым обобщением, предложенным в [118].

Работа 1996 “A positive supercompiler” [107] обобщает суть позитивной суперкомпиляции – рассматривается модельный суперкомпилятор для простого функционального языка первого порядка. Рассматривается KMPтест – автоматический вывод эффективного алгоритма нахождения подстроки в строке из наивного алгоритма.

Статья 1996 года “A Roadmap to Metacomputation by Supercompilation” [35] рассматривает суперкомпиляцию в перспективе метавычислений и три задачи метавычислений: специализацию программ, композицию программ и инверсное вычисление программ. Также суперкомпиляция сравнивается другими методами преобразования программ.

Работа 1998 “Introduction to Supercompilation” [105] помимо введения в суперкомпиляцию обозначивает, что разбиение узлов на локальные и глобальные и последующая обработка такого разбиения повышает глубину преобразования программ и во многих случаях помогает избежать слишком поспешного обобщения.

В статье 1998 года “Convergence of Program Transformers in the Metric Space of Trees” [108] рассматривается задача доказательства завершаемости преобразователя и разрабатывается соответствующий инструментарий. Приводится пример использования разработанного инструментария для доказательства завершаемости простого суперкомпилятора.

В 1999 Йенс Зехер завершает магистерскую диссертацию, посвященную перфектной суперкомпиляции – “Perfect Supercompilation” [100]. Перфектный суперкомпилятор распространяет не только позитивную, но и негативную информацию при прогонке. Отличия данной работы от предыдущих в следующем: (1) рассматривается типизированный (с поддержкой полиморфных данных и функций) язык первого порядка, (2) конфигурация теперь является выражением со свободными переменными и рестрикциями – вводится система рестрикций и алгебра работы с ними, (3) явным образом определяется алгоритм генерации остаточной программы из частичного дерева процессов. Магистерская диссертация Зехера является первой работой, в которой описан суперкомпилятор, учитывающий негативную информацию и доказана его завершаемость. Обзор диссертации опубликован в виде статьи – [102].

В работе Зехера 2001 года “Driving in the Jungle” описывается вариант позитивной прогонки со стратегией вычислений в схлопнутых джунглях (collapsed jungle evaluation). Конфигурация представляет из себя уже не выражение (дерево), а направленный ациклический граф (DAG).

Докторская диссертация Зехера “Driving-Based program transformation in theory and practice” [101] рассматривает методы преобразования программ (в том числе и суперкомпиляцию) для случаев, когда выражения представляются в виде направленного ациклического графа. Особого внимания заслуживают определение вложения и обощения таких выражений.

В книге Абрамова и Пармёновой “Метавычисления и их применения.

Суперкомпиляция” [134] рассматривается суперкомпилятор для плоского функционального языка первого порядка TSG7, варианта языка S-Graph, используемого в работе [33]. Приведены алгоритмы обнаружения вложения и обобщения. Можно сказать, что работа [134] является в некотором смысле завершением работы [33].

В работе [56] Андрей Климов рассмативает суперкомпиляцию в общем виде – как отношение специализации и исследует его свойства.

1.1.3 Суперкомпиляции императивных языков Традиционно суперкомпиляция рассматривается как метод преобразавания функциональных программ.

Прогонка для языка простого императивного языка Flowchart рассматривается в работе Нила Джонса [48].

Интересны работы Андрея Климова по применению идей суперкомпиляции к специализации объектно-ориентированного языка Java [57], [58].

Отдельно стоит упомянуть работу Димитура Крустева [65], в которой рассматривается вопрос механической верификации суперкомпилятора для простого императивного языка.

1.1.4 Суперкомпиляция функциональных языков высшего порядка В конце 2000-х годов возникает большой интерес к применению методов суперкомпиляции для оптимизации программ на функциональных языках первого порядка.

Питер Джонсон и Йохан Нордландер разрабатывают суперкомпилятор для языка Timber (язык высшего порядка с семантикой вызова по имени), алгоритмы суперкомпилятора представлены в серии работ, озаглавленных “Positive Supercompilation for a Higher Order Call-By-Value Language” [50, 51, 49, 52]. Главной задачей этих работ является обеспечить полную эквивалентность исходной и остаточной программ (сохранить свойства завершаемости) и одновременно обеспечить глубину преобразования, близкую к глубине преобразования программ с ленивой сеTSG = Typed S-Graph мантикой вычислений. Основное средство – использовать анализ завершаемости при анализе конфигураций.

В 2008 году Митчел сообщил о суперкомпиляторе для языка Haskell Supero [78], особенностью которого являлась работа с let-выражениями (сохранение семантики вызова по необходимости). Другой особенностью являлся отказ от тесного обобщения в случае, если верхняя конфигурация вложена в нижнюю через погружение.

В статье “Rethinking Supercompilation” [77] изложено переосмысление частей суперкомпилятора с целью создания быстро работающего и робастного суперкомпилятора. (1) Для представления конфигураций выбрано специальное синтаксическое подмножество ядра языка Haskell – “Simplied Core”. На каждом шаге осуществляется преобразование текущей конфигурации в “Simplied Core” 8. (2) Отказ от использования гомеоморфного вложения как синтаксического критерия для свистка, – каждому выражению (конфигурации) ставится в соответствие мультимножество меток (tag-bag) и в качестве свистка используется сравнения этих мультимножеств.

На практичность рассчитан и CHSC9, описанный в работе “Supercompilation by Evaluation” [15]. Конфигурация представляется обобщенным состоянием абстрактной машины Кривина - кучей, активным подвыражением и стеком. В качестве свистка также используется упорядочение над мультимножествами меток. Особенностью CHSC является отсутствие обобщения с учетом истории вычислений – конфигурация обобщается безотносительно истории вычислений. Также CHSC поддерживает суперкомпиляцию рекурсивных let-выражений с сохранением семантики вызова по необходимости.

Стоит также упомянуть работы [53], [54], [89], [75].

При суперкомпиляции делается однократная прогонка. Идея дистилляции – осущетвлять двойную прогонку. Прогонка (построение дерева процессов) в дистилляции происходит также как и в суперкомпиляции. А 8 Хотя “Simplied Core” и является алгоритмически полным языком, не каждое Haskell-выражение можно перевести в “Simplied Core” – поэтому реально рассматриваются не любые программы. К счастью, непереводимые в “Simplied Core” Haskellпрограммы экзотичны и достаточно редки.

9 CHSC = Cambridge Haskell SuperCompiler вот при обработке возможного вложения и зацикливания используются не сами конфигурации, а их суперкомпилированные версии. В статье [39] показано, как дистилляция может изменять асимптотику программ. Формализм описания дистилляции находится пока еще в крайне сыром виде и претерпевает существенные изменения от публикации к публикации. Например, в работе [39] перед каждым шагом прогонки выражение суперкомпилировалось и дальше шаг прогонки осуществлялся относительно суперкомпилированного выражения. В работе [41] зацикливание и обобщение осуществляется не над выражениями, а над соответствующими им (в общем случае бесконечными) деревьями процессов. В работе [42] сравниваются не выражения, а графы процессов. В докладе по материалам работы [42], представленном Гамильтоном на семинаре по метавычислениям META’2010 сравнивались и обобщались системы переходов. Дистилляция – многообещающее развитие идей суперкомпиляции, требующее пока соответствующей формализации.

1.1.5 Другие работы В 1970-х годах при разработке методов суперкомпиляции был предложен метод окрестностного анализа для аппроксимации алгоритмически неразрешимой проблемы останова. Суть окрестностного анализа – определить какая информация о тексте text была использована, и какая информация о тексте text не была использована в некотором процессе обработки текста text. Окрестностный анализ основан на прогонке.

Окрестностный анализ разрабатывается в работах Сергея Абрамова “Metacomputation and program testing” [2], “Метавычисления и их применение” [133]. В частности, показано, как окрестностный анализ может использоваться для организации “предельно надежного тестирования”.

Задачу инвертирования программ (вычислений) можно определить как нахождения входных данных (множества входных) по результату вычисления. Проблемами инверсного вычисления детально занимались Александр Романенко, Сергей Абрамов и Роберт Глюк, придерживаясь идеи синтаксической инверсии программ. А. Романенко в работах “The generation of inverse functions in Refal” [91], “Inversion and metacomputation” [92] разрешает некоторые сложности текстуальной инверсии программ на Рефале.

Инверсный Рефал рассматривается в работе Абрамова “Метавычисления и логическое программирование” [132] как язык логического программирования и сравнивается с другими языками логического программирования.

Технические вопросы организации инверсных вычислений для языка TSG исследуются в работах Сергея Абрамова и Роберта Глюка “The Universal Resolving Algorithm: Inverse Computation in a Functional Language” [5], “Inverse Computation and the Universal Resolving Algorithm” [7], “Principles of inverse computation and the universal resolving algorithm” [8], “Faster Answers and Improved Termination in Inverse Computation of NonFlat Languages” [9].

Инверсное вычисления и окрестностный анализ, по сути, для данной (стандартной) семантики языка определяют другие (нестандартные) семантики вычислений. Нестандартные семантики и принципы работы с ними исследуются в работах Сергея Абрамова и Роберта Глюка “Semantics modiers: an approach to non-standard semantics of programming languages” [3], “Combining Semantics with Non-standard Interpreter Hierarchies” [4], “From standard to non-standard semantics by semantics modiers” [6].

1.2 Суперкомпиляция функционального языка первого порядка В качестве отправной точки рассмотрим, как устроена позитивная суперкомпиляция для простого функционального языка SLL. Материал этого разделан основан на работах [105, 107, 103, 62, 135].

Данные языка SLL – константы и простые структуры. Простая структура – это именованный конструктор с фиксированным и упорядоченным набором полей. Каждое поле в свою очередь, – некоторые данные (конструктор или константа). Константа есть нуль-арный конструктор.

Вычисления в данном языке организованы через вызовы функций.

Каждая функция имеет строго заданное количество аргументов. Для реализации ветвления функциям разрешается заглядывать в первый аргумент и, в зависимости от того, в какой конструктор обернут первый аргумент, – выполнять различные вычисления. Функция конструирует результат вычислений из констант, конструкторов, вызовов функций и аргументов. При заглядывании в первый аргумент функции становятся доступны части этого аргумента. Тело функции – одно выражение.

Например, если рассматривать алфавит из двух букв (констант) – A и B, то слова этого алфавита логично представлять в виде списка. Пустой список - константа Nil, непустой список - структура из двух частей, первая часть - первый элемент списка, вторая часть - остальные элементы (хвост). Непустые списки создаются с помощью бинарного конструктора Cons(head, tail).

Тогда слова алфавита из двух букв представляются так:

Nil() - пустое слово “” Cons(A(), Nil()) - слово “A” Cons(A(), Cons(B(), Nil())) - “AB” Cons(B(), Cons(B(), Cons(B, Nil()))) - “BBB” Например функция, приписывающий элемент x к списку xs, записывается так:

prepend(x, xs) = Cons(x, xs);

Функция app, конкатенирующая списки, записывается так:

app(Nil(), vs) = vs;

app(Cons(u, us), vs) = Cons(u, app(us, vs));

Здесь константа Nil используется для представления пустых списков.

Конструктор Cons(x, xs) представляет непустой список, где x – первый элемент списка, а xs – остальная часть.

Для того, чтобы синтаксически различать функции и конструкторы, принято следующее соглашение: имена конструкторов начинаются с заглавной буквы, а функций – с прописной. Можно не писать скобки для нуль-арных конструкторов (констант).

Конкатенация строк Cons(A, Cons(B, Nil)) и Cons(B, Cons(A, Nil)) происходит так:

app(Cons(A, Cons(B, Nil())), Cons(B, Cons(A, Nil()))) Cons(A, app(Cons(B, Nil()), Cons(B, Cons(A, Nil())))) Cons(A, Cons(B, app(Nil(), Cons(B, Cons(A, Nil()))))) Cons(A, Cons(B, Cons(B, Cons(A, Nil())))) Состояние вычисления – выражение. Вычисление – последовательность переходов между состояниями в соответствии с правилами, описанными в программе. Порядок вычислений – ленивый (снаружи-внутрь).

1.2.1 Примеры суперкомпиляции Пример Допустим, что нам требуется получить результат конкатенации трёх списков. Это можно сделать, вычислив выражение app(app(xs, ys), zs).

Однако, при этом элементы списка xs будут анализироваться два раза (сначала - внутренним вызовом app, а потом - наружным). Покажем, как с помощью суперкомпиляции можно получить более эффективное вычисление. Начнем “символически” интерпретировать выражение (конфигурацию) app(app(xs, ys), zs). Сначала попробуем раскрыть внутренний вызов app(xs, ys). Однако, из-за того, что app проверяет, какой вид имеет её первый аргумент - Nil() или Cons(u, us), нам придётся рассмотреть два случая (или, выражаясь языком, принятым среди специалистов по суперкомпиляции, “расщепить конфигурацию”):

 Правую нижнюю конфигурацию теперь можно однозначно развернуть – раскрыть наружный вызов app:

  Новое выражение содержит конструктор на верхнем уровне, – мы переходим к “символическому” вычислению аргументов конструктора:

В этот момент обнаруживается, что конфигурация в нижнем правом узле получившегося дерева совпадает с конфигурацией в корне дерева (с точностью до переименования переменных). Понятно, что нет смысла второй раз пытаться вычислить ту же самую конфигурацию. Обозначим конфигурацию в верхнем узле a3 и с помощью обратной дуги изобразим совпадение конфигураций:

Повторяем те же операции для левого узла. После нескольких шагов также обнаруживаем совпадение конфигураций в листе дерева с конфигурацией в одном из предков. Обозначаем верхнюю конфигурация a2 и также проводим обратную дугу:

Построение “дерева конфигураций” завершено: каждый лист дерева содержит либо уже ранее встречавшуюся конфигурацию (с точностью до переименования переменных), либо переменную, либо нуль-арный конструктор. Можно сказать, что построенное таким образом дерево представляет все возможные пути вычисления выражения, находящегося в корне дерева. Ветвления в дереве получаются из разбора возможных значений переменных.

Однако, в получившемся дерева есть избыточность – есть узел (с конфигурацией app(Cons(u, app(us, ys)), zs)), через который трасса вычисления проходит безусловно. Этот узел можно безопасно удалить и спрямить входящую и выходящую из него дуги. В результате получится упрощенное дерево:

Удаленный нами узел называется в терминологии суперкомпиляции транзитным узлом. Удаление транзитных узлов – главный механизм оптимизации с помощью суперкомпиляции.

В получившемся частичном дереве процессов достаточно информации (в узлах и на дугах), чтобы превратить его в программу. В итоге получаем следующую программу:

a3(Cons(u, us), ys, zs) = Cons(u, a3(us, ys, zs));

Вычисление выражения a3(xs, ys, zs) в новой программе эффективнее, чем вычисление выражения app(app(xs, ys), zs) в первоначальной. При вычисления исходного выражения делалось O(2|xs| + |ys|) шагов вычислений, в то время, как для вычисления нового выражения требуется O(|xs| + |ys|) шагов вычислений, где |xs| – длина списка xs Произведенный процесс преобразований можно рассматривать как состоящий из трех этапов: символическое вычисление, поиск повторений и построение новой программы.

Пример Однако, в большинстве случаев при построении частичного дерева процессов таким образом будут возникать бесконечные ветви, на которых не будет точных повторений конфигураций. Рассмотрим вычисление выражения app(app(xs, ys), xs) для программы из первого примера.

Повторяем те же самые шаги и получаем следующее дерево:

Конфигурация в нижнем правом узле похожа на конфигурацию в верхнем узле, но не совпадает с ней (нижнее выражение не является переименованием верхнего выражения). При продолжении символического вычисления правого нижнего выражения не получится добиться, чтобы конфигурация в листе совпала с конфигурацией в предках, и процесс построения конечного дерева (используя только символическое вычисление и поиск повторений) не завершится. Тот факт, что две конфигурации похожи, но не совпадают является (эвристическим) сигналом10 того, что дальнейшее построение ветви может не завершится. Обозначим это:

10 исторически называемого в суперкомпиляции свистком Причина возникновения бесконечной ветви – повторная переменная xs в начальном выражении. Однако, как мы видели, если проигнорировать повторную переменную и считать разные вхождения переменной xs в начальной конфигурации разными переменными, процесс построения частичного дерева процессов завершается. Поэтому одним из выходов из сложившейся ситуации является рассмотрение более общей начальной конфигурации – обобщение. Будем рассматривать второе вхождение переменной xs как переменную zs, – для обозначения обобщения используются специальный let-узел. После обобщения и дальнейшего построения дерева получается дерево, аналогичное дереву из первого примера:

При генерации нового выражения и программы из полученного дерева let-выражения могут быть устранены подстановкой соответствующего нового выражения вместо переменной из привязки. В итоге получается Рис. 1.1 SLL: грамматика новое выражение a3(xs, ys, xs) и новая программа:

a3(Cons(u, us), ys, zs) = Cons(u, a3(us, ys, zs));

Как и раньше, преобразование проходило в три этапа, но второй этап (поиск повторений) был более сложным – при обнаружении “почти повторения” мы заменяли целое поддерево на новый узел в результате обобщения.

1.2.2 Синтаксис и семантика языка SLL Рассмотрим теперь суперкомпиляцию для языка SLL более формально. Для этого нам необходимо вначале определить синтаксис и семантику языка.

На Рис. 1.1 показан синтаксис языка SLL, рассматриваемого в работах [103, 108].

SLL – ленивый функциональный язык первого порядка. В языке SLL используется перечислимое множество символов для представления переменных v V, конструкторов C C, и имён функций f F и g F.

Рис. 1.2 SLL: подстановка Все символы имеют фиксированную арность. SLL-программы обрабатывают данные, представляющие собой конечные деревья, построенные с помощью конструкторов. Выражение языка SLL – либо переменная, либо конструктор, либо вызов функции. Программа состоит из набора определений функций. Причем функции делятся на два класса: f -функции и g-функции. Определение g-функции состоит из одного или нескольких правил, при этом в каждом правиле присутствует образец, с помощью которого анализируется структура первого аргумента. Определение f функции состоит из одного правила, в котором все аргументы являются переменными. В левой части правила не допускаются повторные переменные. Все переменные, присутствующие в правых частях правил, должны быть определены в левой части.

Как было отмечено раньше, синтаксически функции не отличаются от конструкторов (единственное отличие – то, что имена конструкторов начинаются с заглавной буквы, а функций – с прописной), поэтому далее будем использовать запись h(e1,.., en ) для обозначения и конструкторов, и функций.

Определение 1 (SLL-подстановка). Подстановкой будем называть конечный список пар вида = {vi := ei }, каждая пара в котором связывает переменную vi с ее значением ei. Область определения определяется как domain() = {vi }. Область значений определяется как range() = {ei }.

Результат применения подстановки к выражению e записывается e.

Определение 2 (Применение SLL-подстановки). Результат применения подстановки к выражению e, e вычисляется по правилам на Рис. 1.2.

Любое выражение языка SLL можно представить либо в виде наблюдаемого выражения, либо в виде контекста редукции с помещенным в дыру редексом. Грамматика такой декомпозиции представлена на Рис. 1.3.

Рис. 1.3 SLL: декомпозиция выражений con ::= Рис. 1.4 Операционная семантика SLL con g(C(e1,..., em ), em+1,..., en ) con e{v1 := e1,..., vn := en } Определение 3 (Слабая головная нормальная форма). Выражение e языка SLL находится в слабой головной нормальной форме, если в нем на верхнем уровне находится конструктор (то есть e = C(e1,..., en )).

Определение 4 (Шаг редукции). Шаг редукции – наименьшее отношение на множестве SLL выражений, удовлетворяющее правилам на Рис. 1.4.

Шаг редукции определяет семантику вычисления. Значением вычисления является выражение в слабой головной нормальной форме (конструктор). В обычном случае вычисляются выражения без переменных (объектные выражения). Обратите внимание, что если на каком-то шаге вычисляемое выражение становится конструктором, то вычисления заканчиваются.

Определение 5 (Равенство SLL-выражений). Два выражения e1 и e считаются равными, если они различаются совпадают текстуально. Равенство выражений e1 и e2 записывается как e1 e2.

Определение 6 (Частный случай SLL-выражения). Выражение e2 называется частным случаем выражения e1, e1 e2, если существует подстановка такая, что e1 e2. Для выражений языка SLL такая подстановка Определение 7 (Переименование SLL-выражения). Выражение e2 называется переименованием выражения e1, e1 e2, если e1 e2, и e2 e1.

Другими словами, e1 и e2 различаются только именами свободных переменных.

1.2.3 Обобщение и гомеоморфное вложение SLL-выражений В данном разделе даются определения, необходимые для формулировки алгоритма построения частичного дерева процессов.

Определение 8 (Строгая декомпозиция SLL-выражения). Let-выражение и e = e0 {vi := ei }.

Определение 9 (Обобщение SLL-выражений). Обобщением выражений e1 и e2, называется тройка (eg, 1, 2 ), где eg – выражение, 1 и 2 – подстановки, такие, что eg 1 e1 и eg 2 e2. Множество всех обобщений Определение 10 (Тесное обобщение двух SLL-выражений). Обобщение (eg, 1, 2 ) называется тесным обобщением выражений e1 и e2, если для частным случаем eg. Мы предполагаем, что определена операция такая, Определение 11 (Несопоставимые выражения). Выражения e1 и e2 называются несопоставимыми, e1 e2, если e1 e2 = (v, 1, 2 ), то есть обощенное выражение является переменной.

Известным результатом является алгоритм нахождения тесного обобщения выражений первого порядка без связанных переменных [66].

Определение 12 (Итеративный алгоритм обобщения SLL-выражений).

Тесное обобщение выражений e и e, e e находится с помощью применений правил общего функтора и общего подвыражения (Рис. 1.5) к начальному тривиальному обобщению (v, {v := e }, {v := e }).

Рис. 1.5 SLL: итеративное обобщение выражений e и e Начальное тривиальное обобщение (v, {v := e1 }, {v := e2 }) Правило общего функтора Правило общего подвыражения Рис. 1.6 SLL: рекурсивный алгоритм обобщения Тесное обобщение Правило общего функтора Правило общего подвыражения • s(e, {}, {}) = s(e, {}, {}) Алгоритм 12 является традиционной ([104, 105, 108]) записью алгоритма обобщения в итеративной форме (определяется “малый шаг” обобщения).

Однако, процесс обобщения удобнее (как мы увидим в дальнейшем) Рис. 1.7 SLL: гомеоморфное вложение Embedding Variables Coupling определить напрямую через рекурсивные функции (семантика “большого шага”):

Определение 13 (Рекурсивный алгоритм обобщения SLL-выражений).

Процесс нахождения обобщения происходит в 2 этапа: первый этап соответствует применению правила общего выражения, – нахождение обобщения (вычисление e1 e2 ) двух совпадающих по оболочке выражений сводится к задаче нахождения обобщений их частей. Второй этап (упрощение обобщения с помощью операции s) заключается в удалении из результата повторяющихся частей и соответствует правилу общего подвыражения. Правила применяются в порядке их перечисления.

Определение 14 (Гомеоморфное вложение SLL-выражений). Простое вложение HLL-выражений определяется индуктивно в соответствии с правилами на Рис. 1.7.

Свойства вложения и обобщения SLL-выражений Будем рассматривать SLL-выражения из множества ECF V, где C – множество имен конструкторов, F – множество имен функций, V – множество имен переменных (см. Рис. 1.1).

Теорема 15 (Крускал, Хигман). Пусть C и F – конечные множества.

В любой бесконечной последовательности SLL-выражений e1, e2,... из множества ECF V найдутся ei и ej такие, что i < j и ei ej.

Доказательство можно найти в [26].

Отношение также является вполне-квазиупорядочением на ECF V.

Если два SLL-выражения вложены через сцепление, то их тесное обобщение нетривиально (не является переменной). Использование отношения в качестве свистка имеет следующие плюсы:

1. Позволяет гарантировать завершаемость суперкомпилятора (в силу 2. Позволяет в случае обобщения всегда учитывать историю вычислений.

Нам хотелось сохранить это свойство при определении гомеоморфного вложения для выражение языка HLL.

Выражения со связанными переменными В работе [104] рассматривается язык SLL, дополненный case-выражениями (со связанными переменными), но отношение вложения и алгоритм обобщения приводятся только для случая выражений без связанных переменных, – читателю предлагается самостоятельно расширить приведенные соотношения на случай связанных переменных в case-выражениях, поэтому в данном разделе мы не затрагиваем вопросы вложения и обобщения выражений со связанными переменными.

1.2.4 Построение дерева процессов Рассмотрим сначала, как строится дерево процессов для SLL-программ.

В случае плоского функционального языка, такого как S-Graph [33] или TSG [134], где можно использовать только хвостовую рекурсию, понятие дерева процессов для конфигурации c0 определяется достаточно просто – метками дерева процессов являются конфигурации и на дугах дерева процессов обозначены сужения конфигураций. Пути в дереве процессов представляют множество трасс вычисления. Любому объектному выражение e c0 из начальной конфигурации соответствует некоторый путь в дереве процессов.

Рис. 1.8 SLL: шаг прогонки D[[con g(C(e1,..., em ), em+1,..., en ) ]] [con e{v1 := e1,..., vn := en } ] Концептуально это означает, что дерева процессов для конфигурации c0 достаточно для вычисления любого выражения e c0. То есть, в некотором смысле, дерево процессов заменяет программу.

Для языка SLL дерева процессов для конфигурации c0 должно быть достаточно для вычисления любого выражения e c0 в любом контексте – обычное вычисление выражения завершается, когда на верхнем уровне появляется конструктор, однако при вычислении этого выражения в контексте нам может потребоваться вычислить аргумент конструктора.

Определение 16 (SLL-сужение). SLL-cужением называется пара (v, p), где v – переменная, а p – образец. Для удобства SLL-cужение записывается как v = p.

Определение 17 (Дерево процессов для SLL-выражений). Дерево процессов представляет собой ориентированное (возможно – бесконечное) дерево, каждому узлу n которого приписано некоторое выражение. Для некоторых узлов всем исходящим из ним дугам приписаны сужения. Мы будем обозначать выражение, помещенное в узел n, как n.expr. Пусть дано SLL-выражение e. Дерево процессов pt для SLL-выражения e определяется следующим образом:

• Выражение e находится в корневом узле pt.

• В листьях pt находятся только переменные и нуль-арные конструкторы.

• Для каждого узла, имеющего дочерние узлы i выражение в узле и выражения в дочерних узлах связаны как D[[.expr]] = [i.expr], где оператор D (шаг прогонки) определен на Рис. 1.8.

• Если на дугах, исходящих из узла имеются сужения ri, то [ri ] = R[[.expr]], где оператор R определен на Рис. 1.8.

Дерево процессов строится однозначным образом и в общем случае является бесконечным.

1.2.5 Построение частичного дерева процессов Конечная цель суперкомпиляции – превратить дерево процессов в конечный (возможно, циклический) граф, который называется частичным деревом процессов:

Определение 18 (Частичное дерево процессов). Частичное дерево процессов – дерево процессов, в котором:

• допускаются специальные обратные дуги, проведенные от листьев • узлы могут быть помечены let-выражениями (Определение 8).

Мы будем обозначать специальные обратные дуги как в тексте и штрихованными дугами на диаграммах.

Определение 19 (Обработанный лист). Узел считается обработанным, если выполняется одно из следующих условий:

• Узел уже “зациклен”: из узла выходит двойная дуга, •.expr является нуль-арным конструктором, •.expr является переменной.

Определение 20 (Тривиальный узел). Узел считается тривиальным, если выполняется одно из следующих условий:

Рис. 1.9 Операции над частичным деревом процессов

3. abstract(t,, ) = 6. f old(t,, ) =

• Узел помечен let-выражением.

• Узел помечен конструктором.

Рассмотрим самый простой алгоритм построения частичного дерева процессов для SLL-конфигурации.

Определение 21 (Алгоритм построения частичного дерева процессов).

Рис. 1.10 Алгоритм построения частичного дерева процессов для конфигурации c

t = abstract(t,, )

t = abstract(t,, )

Частичное дерево процессов строится по алгоритму на Рис. 1.10. В самом начале конструируется дерево t = c0 из одного узла, в который помещается рассматриваемая конфигурация.

В алгоритме используются следующие операции над частичным деревом процессов:

• incomplete(t) – возвращает T rue, если есть хотя бы один необработанный лист дерева t.

• unprocessed – возвращает необработанный лист в дереве t.

• f ind(, ) – находит среди предков узла первый узел такой, • drive(t, ) – делает шаг прогонки выражения, находящегося в узле : подвешивает к узлу дочерние узлы и помещает в них выражения D[[.expr]].

• abstract(t,, ) – обобщает конфигурацию в узле с учетом конфигурации в узле : заменяет выражение в на выражение корнем некоторого поддерева, то это поддерево уничтожается.

• f old(t,, ) – “зацикливает” и : конструирует специальную обратную дугу –.

• split(t, ) – делает декомпозицию текущей конфигурации: заменяет находящееся в узле выражение h(e1,..., en ) на выражение Некоторый операции показаны схематично на Рис.1.9.

Теорема 22. Построение частичного дерева процессов по алгоритму на Рис. 1.10 завершается.

Доказательство можно найти в [108].

Все операции и шаги в алгоритме строго формализованы и однозначны. Алгоритм преобразования полученного частичного дерева процессов в новое выражение и новую программу можно найти в [103, 100, 62]. Мы не будем подробно останавливаться на этом алгоритме.

Рассмотренный алгоритм – самый простой. В литературе рассматриваются приемы, повышающие глубину преобразований суперкомпилятора. Перечислим следующие:

1. Использование (см. Рис. 1.7) вместо – тогда нет нужды в опеc рации split, так как обобщение вложенных через сцепление конфигураций нетривиально.

2. Разбиение всех конфигурации на конечное число классов и поиск вложения только в своем классе.

3. Рассмотрение в некоторых случаях не всех предков, а лишь ближайших (глобальный-локальный контроль).

Рис. 1.11 Сравнение суперкомпиляторов Стоит отметить, что все эти дополнительные приемы не влияют на завершаемость суперкомпилятора.

1.3 Анализ состояния дел в суперкомпиляции с точки зрения трансформационного анализа программ Суперкомпилятор, применяемый для трасформационного анализа программ, должен удовлетворять следующим требованиям:

• Гарантированно сохранять семантику программы. В противном случае выводы, сделанные из анализа остаточной программы, могут быть необоснованными или ошибочными.

• Гарантированно завершаться на любой входной программе. Логически это требование не является абсолютно необходимым, но весьма важно с прагматической точки зрения.

• Иметь доступный исходный код. Без этого отсутствует сама возможность убедиться в корректности реализации суперкомпилятора.

Как было отмечено, использование трансформационного анализа плодотворно, если язык предлагает изобразительные средства, облегчающие написание спецификаций, такие как:

• Функции высших порядков. Появляется возможность иметь кванторы по функциям в спецификациях.

• Работа с бесконечными данными. Признак ленивого языка – ленивые языки лучше поддаются преобразованиям.

Сравнение суперкомпиляторов по перечисленным критериям приведено в таблице на Рис. 1.11.

К сожалению, на 2007 год не существовало суперкомпилятора, удовлетворяющим даже обязательным требованиям. Поэтому в первую очередь автор поставил перед собой задачу разработать такой суперкомпилятор для языка Haskell.

1.4 Выводы В главе рассмотрен позитивный суперкомпилятор для функционального языка первого порядка SLL. Все алгоритмы суперкомпилятора представлены полностью и формально. В работе [62] данный суперкомпилятор приведен в виде программы.

Приведен анализ существовавших суперкомпиляторов с точки зрения трансформационного анализа. Из анализа следует, что полноценного суперкомпилятора, пригодного для использования в трансформационном анализе, не было.

С другой стороны, в последнее время появились суперкомпиляторы для языков высших порядков, многие части которых описаны неформально или неполностью, что затрудняет воспроизвести описываемые авторами результаты.

Поэтому автор поставил перед собой цель создать полноценный суперкомпилятор, ориентированный на трансформационный анализ программ на языке высшего порядка (Haskell) и имеющий полное и формальное описание своего устройства.

Глава Язык HLL: синтаксис и семантика В данной главе формально описывается выбранный объект анализа – язык HLL.

2.1 Формализация языка HLL Одна из целей данной диссертации – полное и формальное описание методов и алгоритмов суперкомпиляции функций высших порядков, используемых в суперкомпиляторе HOSC, вместе c полным и формальным доказательством их корректности и завершаемости. Очевидно, что для достижения этой цели необходимо четко и формально определить рассматриваемый язык и описать его семантику.

Язык программирования Haskell обладает достаточно богатым синтаксисом. Однако, из этого богатого синтаксиса выделяется так называемое ядро языка Haskell (Haskell Kernel [110]), которое лежит в основе практически любой реализации языка Haskell [111]. Ядро языка Haskell достаточно высокоуровнево, чтобы быть реальным языком программирования. Программы на ядре Haskell читабельны и могут быть предметом анализа.

В основе языка Haskell лежат алгебраические типы данных, при определении которых явным образом перечисляются конструкторы этих данных (всегда конечный набор конструкторов). Представленные в данной работе методы и алгоритмы суперкомпиляции основаны на конечности числа рассматриваемых конструкторов и распространении позитивной информации.

Однако, как и в любом практическом языке программировании в языке Haskell есть заранее определенные типы данных – символы, строки, целые числа, действительные числа и т.д. (будем их называть далее для краткости литералами). Количество объектов-литералов в принципе бесконечно. Также в языке Haskell есть заранее определенные стандартные операции над литеральными объектами. Мы не рассматриваем литеральные объекты и заранее определенные данные над ними.

Поддержка литеральных объектов и примитивных операциq концептуально проста, но сильно увеличила бы формальное описание синтаксиса языка, семантики, алгоритмов суперкомпиляции. То же самое относится и к заранее определенным в языке функциям.

Haskell предусматривает возможность аварийного останова программ:

это может случиться явным образом, – инициирована исключительная ситуация, или, например, из-за отсутствия разбора определенного случая (образца) в программе. Мы не рассматриваем такие ситуации. Предполагается, что любая программа завершается естественным образом, либо зацикливается. Добавление поддержки аварийных завершений также концептуально просто, но сильно бы затруднило задачу формального и полного описания всех частей суперкомпилятора.

Таким образом, мы рассматриваем ядро языка Haskell без:

1. Литеральных объектов (чисел, символов, строк).

2. Заранее заданных функций (в том числе, выброс ошибок).

3. Неполного набора образцов в case-выражениях.

Можно сказать, что рассматривается “чистое” (pure) подмножество языка Haskell. Это позволяет достаточно кратко описать методы и алгоритмы суперкомпиляции.

Мы намеренно добавили в язык HLL специальный вариант let-выражения – letrec, чтобы иметь возможность различать рекурсивные и нерекурсивные локальные определения на синтаксическом уровне. Также для простоты работы с языком, в HLL вводятся некоторые ограничения (letвыражение не может быть рекурсивным). Это позволяет достаточно кратко формально описать семантику языка и обойтись без введения лишних понятий при доказательстве корректности суперкомпилятора.

Язык HLL выбран таким образом, чтобы минимизировать количество рассматриваемых сущностей в описании синтаксиса, семантики языка и при доказательствах корректности и завершаемости, оставаясь в то же время максимально приближенным к ядру языку Haskell.

Таким образом, любая HLL-программа является исполняемой Haskеllпрограммой1. А любая программа на чистом ядре Haskell без труда переводится в HLL.

В основе системы типизации языка Haskell лежит полиморфная типизация по Хиндли-Милнеру [22, 44]. Также Haskell поддерживает механизм перегрузки имен с помощью классов, так называемый ad-hoc полиморфизм [129]. Однако ad-hoc полиморфизм легко транслируется в ядро Haskell (с помощью таблиц функций). Поэтому мы будем рассматривать только алгебраические типы данных, определяемые пользователем, и полиморфную типизацию по Хиндли-Милнеру и не будем рассматривать классы языка Haskell и ad-hoc полиморфизм.

Для полного и формального определения семантики и понятия эквивалентных программ нам будет легче вначале рассмотреть бестиповый вариант языка HLL, определить для него перечисленные понятия, а затем сделать их ревизию с учетом типизации.

2.2 Синтаксис языка HLL Синтаксис бестипового варианта языка HLL. представлен на Рис. 2.1.

Будем считать (вплоть до раздела 2.5) язык HLL бестиповым и игнорировать определения типов и вопросы типизации.

Программа на языке HLL состоит из целевого выражения и определений верхнего уровня. Выражение – это локальная переменная, конструктор, глобальная переменная, -абстракция, аппликация, case-выражение, локальное рекурсивное определение (letrec-выражение), локальное определение переменных (let-выражение) или выражение в скобках.

1 После простой механической замены letrec на let, замены свободных переменных в целевой выражении на их значения и “оборачивания” целевого выражения в функцию main.

Рис. 2.1 Язык HLL (бестиповый) prog ::= e where fi = ei ; программа | case e0 of {pi ei ;} case-выражение | letrec f = e0 in e1 локальное определение Выражение e0 в case-выражении называется селектором, выражения ei – ветвями. Мы будем использовать две записи для обозначения аппликации: e1 e2 и e0 ei. В первом случае e1 может быть любым выражением.

Во втором случае мы требуем, чтобы список аргументов ei был непустым, а выражение e0 не было аппликацией.

Глобальное определение задает соответствие между глобальной переменной и выражением в правой части. Локальные определения связывают локальную переменную с выражением в данном контексте. Образец в case-выражении также связывает локальные переменные с частями сопоставленного выражения.

Неотъемлемой частью описанных далее алгоритмов является работа с переменными. Поскольку в HLL-выражениях присутствуют связанные переменные, нам необходимо детально формализовать работу со связанными переменными, а также ввести соглашения, уточняющие работу с переменными.

Замечание 23 (Три типа переменных). В языке SLL переменные в выражениях не отличаются друг от друга. В выражениях языка HLL могут встречаться переменные трех типов. Переменная является связанной переменной, если (1) она является аргументом объемлющей -абстракции, либо (2) определяется в образце объемлющей ветви case-выражения или (3) связана через let-выражение или letrec-выражение. Переменная fg Рис. 2.2 HLL: множество связанных переменных выражения bv[[fg ]] bv[[v]] bv[[e1 e2 ]] bv[[case e0 of {ci vik ei ;}]] = bv[[e0 ]] ( bv[[ei ]]) ( vik ) bv[[let vi = ei ; in e]] bv[[letrec f = e1 in e2 ]] считается глобальной, если в программе есть определение fg = e. Все остальные переменные – свободные.

Неформальное разделение переменных на три типа в замечании ведет к неоднозначностям, – приходится разделять понятие переменной и вхождение переменной.

В приведенной ниже простой программе переменная bottom в целевом выражении может считаться как глобальной, так и связанной.

let bottom = x in bottom where bottom = bottom;

Мы введем несколько соглашений, устраняющих неоднозначности в вопросе классификации переменных и не требующих явного рассмотрения областей видимости переменных. Для этого мы вначале формально (и несколько волюнтаристски) определим как вычисляются множества свободных, глобальных и связанных переменных выражения. Определения данных множеств также позволит просто и формально разделить рекурсивные и нерекурсивные локальные определения.

Мы обозначаем переменную с индексом fg, если в программе есть определение fg = e; и без индекса, v в противном случае.

Определение 24 (Множества связанных, глобальных и свободных переменных выражения). Множества bv[[e]], gv[[e]], f v[[e]] связанных, глобальных и свободных переменных выражения e определяются по правилам, представленных на Рис. 2.2, Рис. 2.3 и Рис. 2.4 соответственно.

Рис. 2.3 HLL: множество глобальных переменных выражения gv[[fg ]] gv[[v]] gv[[e1 e2 ]] gv[[case e of {ci vik ei ;}]] = gv[[e]] ( gv[[ei ]]) gv[[let vi = ei ; in e]] gv[[letrec f = e1 in e2 ]] Рис. 2.4 HLL: множество свободных переменные выражения f v[[fg ]] f v[[v]] f v[[e1 e2 ]] f v[[case e of {ci vik ei ;}]] = f v[[e]] ( f v[[ei ]]\{vik }) f v[[let vi = ei ; in e]] f v[[letrec f = e1 in e2 ]] Соглашение 25 (Именование переменных). Чтобы избежать возможного конфликта имен, мы требуем, чтобы для любого выражения e множества bv[[e]], gv[[e]], f v[[e]] попарно не пересекались. Дополнительно, каждая связанная переменная может быть определена в выражении не более одного раза.

Соглашение 25 не только устраняет неоднозначность в классификации переменных, но также накладывает дополнительное ограничение на letвыражение: локальная переменная, введенная в let-выражении может использоваться только в теле let-выражения и не может использоваться в определении другой переменной того же let-выражения, – это гарантирует независимость локальных переменных let-выражения друг от друга.

Глобальные определения программы должны быть замкнутыми, то есть множество свободных переменных правой части глобального определения должно быть пустым. Целевое выражение e в программе prog на языке HLL может содержать свободные переменные.

2.3 Подстановка Определение 26 (HLL-подстановка). Подстановкой будем называть конечный список пар вида = {vi := ei }, каждая пара в котором связывает переменную vi с ее значением ei. Область определения определяется как domain() = {vi }. Область значений определяется как range() = {ei }.

Результат применения подстановки к выражению e записывается e.

Язык HLL основан на -исчислении. В -исчислении подстановка является фундаментальной операцией. Чтобы обеспечить корректность подстановки, выражения рассматриваются с точностью до переименования связанных переменных, то есть с точностью до ([12], 2.1.11). Таким образом, операция подстановки должна быть корректной на классах эквивалентности ([12], Приложение C). То есть:

Существуют различные способы решения этой задачи:

1. Можно рассматривать “канонические” безымянные выражения, где связанные переменные не имеют имен [25]. В данном подходе целый класс -конгруэнтных обычных выражений соответствует ровно одному выражению с безымянными переменными. Такой подход хорош для машинных преобразований, но затруднителен для восприятия человеком.

2. Можно при применении операции подстановки заменять связанные переменные на “свежие” переменные по мере необходимости, чтобы избежать “захвата” связанных переменных [21, 109]. Такой подход неудобен в случае, когда подстановка является результатом некоторой операции (например, обобщения), – нужно учитывать, что какая-то составляющая подстановки реально не будет применяться.

3. Можно вообще избежать подстановок, используя механизм наподобие явных подстановок [1, 94]. Однако в случае суперкомпиляции применение такого подхода сильно бы усложнило конфигурационный анализ.

Рис. 2.5 HLL: подстановка 4. Можно расширить Соглашение 25 на случай применения подстановки – определить понятие корректной (или допустимой) подстановки по отношению к выражению e и рассматривать только корректные подстановки.

В контексте суперкомпиляции (точнее, – в контексте нахождения тесного обобщения двух выражений) наиболее удобен последний вариант.

Определение 27 (Допустимая HLL-подстановка). HLL-подстановка допустима по отношению к выражению e, если 1. bv[[e]] domain() = 2. ei range() : bv[[e]] f v[[ei ]] = Соглашение 28 (Использование подстановок). В дальнейшем мы рассматриваем только допустимые подстановки.

Соглашение 28 сродни так называемому соглашению Барендрегта ([12], 2.1.13). Использование соглашений 25 и 28 позволяет нам обеспечить корректность простого (“наивного”) применения подстановки:

Определение 29 (Применение HLL-подстановки). Результат применения подстановки к выражению e, e вычисляется по правилам на Рис. 2.5.

2.4 Семантика языка HLL В данном разделе описывается семантика языка HLL с вызовом по имени.

Рис. 2.6 HLL: декомпозиция выражений obs ::= v ei con ::= red ::= fg Определение 30 (Замкнутое HLL-выражение). HLL-выражение называется замкнутым, если множество его свободных переменных пусто, т.е.

Определение 31 (Контекст). Контекст – выражение с дырой [ ] вместо одного из подвыражений. C[e] - выражение, полученное из контекста заменой дыры на выражение e.

Любое выражение языка HLL можно представить либо в виде наблюдаемого выражения, либо в виде контекста редукции с помещенным в дыру редексом. Грамматика такой декомпозиции представлена на Рис. 2.6.

Определение 32 (Оператор неподвижной точки). Оператор неподвижной точки определяется как специальная функция f ix:

Замечание 33 (Letrec). Мы рассматриваем letrec-выражения как макрос (синтаксический сахар), который раскрывается следующим образом:

Определение 34 (Слабая головная нормальная форма). Выражение Рис. 2.7 Операционная семантика HLL e языка HLL находится в слабой головной нормальной форме, если в нем на верхнем уровне находится конструктор (то есть e = c ei ) или абстракция (то есть e = v e1 ).

Определение 35 (Шаг редукции). Шаг редукции – наименьшее отношение на множестве замкнутых HLL выражений, удовлетворяющее правилам на Рис. 2.7.

Определение 36 (Сходимость). Замкнутое выражение e сходится к слабой головной нормальной форме w, e w, если e w.

e обозначает, что существует w такое, что e w.

Определение 37 (Аварийное завершение с ошибкой времени выполнения). Вычисление замкнутого выражения e завершается с ошибкой времени выполнения, e error, если e e, e не является слабой головной формой и к e не применимо ни одно из правил Рис. 2.7.

Определение 38 (Запуск HLL-программы). Запуск HLL-программы с целевым выражением e состоит в задании такой подстановки, что e = e – замкнутое выражение. Если e w, то w является результатом запуска.

Определение 39 (Аппроксимация). Выражение e1 является операционной аппроксимацией выражения e2, e1 e2, если в любом контексте C, таком, что C[e1 ] и C[e2 ] – замкнутые выражения, из C[e1 ] следует C[e2 ] и из C[e1 ] error следует C[e2 ] error.

Определение 40 (Эквивалентность). Выражение e1 операционно эквивалентно выражению e2, e1 = e2, если e1 e2 и e2 e1.

Рис. 2.8 Язык HLL (типизированный) type ::= tv | tCon | type type | (type) типовое выражение 2.5 Типизация Типизированный вариант языка HLL представлен на Рис. 2.8.

Программа на языке HLL состоит из определений типов данных, целевого выражения и определений верхнего уровня.

Левая часть определения типа содержит имя типа (точнее, имя конструктора типа), за которым следует список типовых переменных. Правая часть – декларации конструкторов данных (разделенные вертикальной чертой, то есть dConi dCon1 |... | dConn ).

Мы требуем, чтобы в case-выражении были перечислены все конструкторы соответствующего типа данных – т.е. образцы в case-выражении должны быть полны и ортогональны. Также для упрощения последующих записей введем соглашение о порядке образцов в case-выражениях:

Соглашение 41 (Порядок образцов в case-выражениях). Будем считать, что в case-выражениях образцы перечислены в том же порядке, что и конструкторы в декларации соответствующего типа данных.

Язык HLL типизирован по Хиндли-Милнеру [22, 44, 110].

В HLL (как и в Haskell) программист может явно приписать тип выражению. При типизации по Хиндли-Милнеру это не является обязательным, – если программа корректно типизирована, то можно указать самые общие (principal) типы для всех выражений в программе. В случае наличия явных типов у выражений, происходит дополнительная проверка того, что указанные типы соответствуют выведенным типам. Однако, явное указание типов выражений и функций позволяет огранить контекст, в котором выражение может быть использовано. (Это также, как мы увидим, окажется необходимым для ограничения контекста, в котором может использоваться остаточная программа.) С учетом типизации необходимо уточнить семантику языка HLL.

Определение 42 (Аварийное завершение с ошибкой типизации). Вычисление замкнутого выражения e моментально завершается с ошибкой типизации, e typingError, если e не является корректно типизированным выражением.

В дальнейшем будем рассматривать только корректно типизированные программы. Корректно типизированная программа p может аварийно завершиться с ошибкой типизации, если пользователь указал означивание для свободных переменных целевого выражения e программы p, несовместимое по типам (выражение e нельзя корректно типизировать).

С другой стороны, типизация гарантирует, что типизированная программа не может аварийно завершится с ошибкой времени выполнения. Таким образом, при рассмотрении эквивалентности выражений в соответствии с определением 40 необходимо принимать во внимание только возможные ошибки типизации выражений C[e1 ] и C[e2 ] и можно не рассматривать ошибки времени выполнения этих выражений (так как они не могут произойти в силу типизации).

Очевидно, что если все свободные переменные выражений e1 и e2 имеют одинаковый выведенный (или явно указанный) тип, то в любом контексте C из C[e1 ] typingError следует C[e2 ] typingError и наоборот.

Как мы увидим далее, в результате суперкомпиляции может получиться программа с более общими выведенными типами, нежели типы в исходной программе.

Замечание 43. До раздела 4.5 “Типизация и корректность” мы рассматриваем только неявно типизированные программы (в стиле Карри). И считаем, что мы рассматриваем только такие контексты C для выражения e, что выражение C[e] корректно типизировано. В разделе 4.5 мы уточним вопрос типизации и корректности.

2.6 Алгебра HLL-выражений Определение 44 (Равенство выражений). Два выражения e1 и e2 считаются равными, если они различаются только именами связанных переменных. Равенство выражений e1 и e2 записывается как e1 e2.

Определение 45 (Частный случай выражения). Выражение e2 называется частным случаем выражения e1, e1 e2, если существует подстановка такая, что e1 e2. Для выражений языка HLL такая подстановка является единственной и обозначается = e1 e2.

Определение 46 (Переименование выражения). Выражение e2 называется переименованием выражения e1, e1 e2, если e1 e2, и e2 e1.

Другими словами, e1 и e2 различаются только именами свободных переменных.

Определение 47 (Строгая декомпозицией). Let-выражение называется строгой декомпозицией выражения e, el e если e0 e, e0 e и e = e0 {vi := ei }.

Определение 48 (Обобщение). Обобщением выражений e1 и e2, называется тройка (eg, 1, 2 ), где eg – выражение, 1 и 2 – подстановки, такие, что eg 1 e1 и eg 2 e2. Множество всех обобщений для выражений e и e2 обозначается как e1 e2.

Определение 49 (Тесное обобщение). Обобщение (eg, 1, 2 ) называется тесным обобщением выражений e1 и e2, если для любого обобщения (eg, 1, 2 ) e1 e2 верно, что eg eg, т.е. eg является частным случаем eg. Мы предполагаем, что определена операция такая, что e1 e2 = (eg, 1, 2 ).

В данном разделе формально и полностью описаны синтаксис и семантика языка HLL, близкого ядру языка Haskell.