Развитие производительных сил или Типизация при помощи суперкомпиляции

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

http://www.evil-wire.org/~jacobian/Productive.pdf

Некоторые системы программирования, а именно доказыватели теорем типа Coq или Agda имеют ограничения на входную программу. Ограничения, конечно, появляются не на пустом месте. Например, рассматриваются только такие множества программ, о которых доказыватель теорем может хоть-что нибудь (конструктивное) сказать.

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

Coq и Agda могут работать с коданными и корекурсией, только если соответствующие функции являются производительными (productive - отсюда и название статьи).
Является ли функция производительной - задача в общем виде неразрешимая.
Но есть достаточное синтаксическое "условие осмотрительности" (guardedness condition), гарантирующее производительность функций. К сожалению, это синтаксическое ограничение слишком жесткое, и многие "очевидно производительные функции" не распознаются как производительные.

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

В статье показывается, как это может быть сделано с помощью суперкомпиляции на примерах на языке Agda. Детали - в статье.

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

В данном контексте цель суперкомпилятора - привести программу к некоторому синтаксическому виду.

PS. Политико-экономический бэкграунд