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