A program specialization relation based on supercompilation and its properties

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