Статья в сборнике "Математические вопросы кибернетики" №8, Москва, 1999
Авторы:Захаров В.А.
Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ
Аннотация:
В статье исследована проблема эквивалентности для одного класса рекурсивных программ. Программы такого вида применяются в качестве абстрактной вычислительной модели для анализа функциональных программ. Рекурсивная программа состоит из функциональных уравнений. Левой частью каждого уравнения является функциональная переменная (функция, определяемая программой), а правой частью – терм, содержащий функциональные переменные и константы (базовые функции). Рекурсивная программа называется унарной, если все входящие в нее функции одноместны. Рекурсивная программа называется линейной, если правая часть каждого функционального уравнения содержит не более одного вхождения функциональной переменной. Семантика рассматриваемых рекурсивных программ определена посредством интерпретаций (моделей) пропозициональной динамической логики (PDL). В частности, семантика базовых функций задается шкалами PDL. Шкала называется уравновешенной, если для любой пары базовых термов результаты их выполнения будут различными, если эти термы имеют разную длину. В статье представлена новый униформный метод сведения проблемы эквивалентности линейных унарных рекурсивных программ на уравновешенных шкалах к хорошо известной проблеме тождеств в полугруппах. При помощи этого метода сведения удалось показать, что проблема эквивалентности указанных рекурсивных программ с перестановочными операторами разрешима за полиномиальное время.