О логико-термальной эквивалентности стандартных схем программ.

Авторы

Захаров В.А., Новикова Т.А.

Аннотация

Широко известную в теории схем программ модель вычислений стандартных схем программ с отношением логико-термальной эквивалентности можно рассматривать как вариант обобщенного конечного автомата, который получает на входе двоичную последовательность и вычисляет на выходе последовательность атомарных формул. Ранее нами был предложен полиномиальный по времени алгоритм проверки логико-термальной эквивалентности стандартных схем программ. На основе этого алгоритма было получено решение более общей задачи – проблемы логико-термальной эквивалентности стандартных схем программ. Задача унификации программ возникает при решении многих проблем программирования; она является обобщением широко известной задачи синтаксической унификации термов, исследованной в алгебре и логике. Для ее решения в настоящей статье был предложен алгоритм вычисления наиболее общего логико-термального унификатора стандартных схем программ за полиномиальное время относительно суммарного размера анализируемых программ.

Ключевые слова

стандартная модель программ, логико-термальная эквивалентность

Издание

Материалы XI Международного семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О.Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), 2014, Изд-во механико-математического ф-та МГУ Москва, с. 147-149.

Научная группа

Теоретическая информатика

Все публикации за 2012 год

Все публикации