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

программа, семантика, пропозициональная динамическая логика, шкала, проблема эквивалентности, полугруппа, разрешающий алгоритм

Математические вопросы и теория численных методов