Двусторонняя унификация программ и ее применение для задач рефакторинга

Труды Института системного программирования РАН. 2014. Т. 26. № 2. С. 245–268.

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

Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи унификации. В этой статье мы вводим понятие двусторонней унификации как процесса преобразования одной заданной подстановки θ_1 к другой заданной подстановке θ_2 при помощи композиции, применяемой как справа, так и слева к подстановке θ_1. Иначе говоря, задача двусторонней унификации состоит в решении уравнений вида Xθ_1 Y=θ_2. Двусторонняя унификация подстановок может быть использована при решении одной из задач реорганизации (рефакторинга) программ – выделения в заданном фрагменте кода тела библиотечной процедуры с целью последующей замены выделенного участка кода на вызов этой процедуры. В статье исследован вопрос о сложности задачи двусторонней унификации подстановок. Установлено, что эта задача является NP-полной. Доказательство NP-трудности задачи двусторонней унификации проводится путем сведения к ней NP-полной задачи правильного расположения домино в прямоугольной области плоскости. В статье также сформулирована и исследована задача двусторонней унификации программ в модели программ первого порядка с отношением логико-термальной эквивалентности. Доказано, что сформулированная задача двусторонней унификации программ также является NP-полной.

Ключевые слова: программа, эквивалентность, complexity, NP-Completeness, equivalence, алгоритмическая сложность, substitution, program, tiling problem, подстановка, проблема домино, NP-полнота