Формальные спецификации суперкомпиляторов методом Натуральной семантики

Андрей В. Климов

( Институт прикладной математики им. М.В.Келдыша РАН )

Суперкомпиляция -- это метод преобразования программ, направленные на решение таких задач как специализация, композиция ("сплавление"), обращение программ и т.п. Метод зародился в 70-е и 80-е годы в работах В.Ф.Турчина для языка Рефал. Родственные методы -- частичные вычисления школы Нила Джоунса (Neil Jones) и смешанные вычисления школы А.П.Ершова.

Суперкомпилятор, Scp: p -> q, по исходной программе p на некотором языке программирования выдает эквивалентную ей остаточную программу q на том же (или другом) языке. Как правило, программа q более эффективна за счет специализации кода по информации, имеющейся в самой программе, и/или за счет ограничения области определения D.

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

В качестве основы теории суперкомпиляции в докладе предлагаются спецификации суперкомпиляторов, которые определяют отношение R(p,q,D) между исходной и остаточной программами p и q, такое что p и q эквивалентны на области входных данных D. Спецификация говорит о том, что значит, что программа q является возможным результатом суперкомпиляции программы p, но не как суперкомпилятор ее строит, используя какие алгоритмы и стратегии.

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

Для слушателей желательно неформальное знакомство с общими идеями суперкомпиляции, например, на уровне доклада на данном семинаре 28 апреля 2004 года "Суперкомпиляция и частичные вычисления: введение и состояние дел".