Содержание к диссертации
Введение
1. Задача проверки эквивалентности программ 4
1.1. Модели программ и задача проверки эквивалентности в рамках этих моделей 7
1.2. Логико-термальная эквивалентность стандартных схем программ 2. Задача выделения метода 13
3. Задачи унификации и антиунификации 17
4. Цели исследования. 20
5. Результаты исследования
5.1. Формулировка основных результатов 21
5.2. Методика получения результатов 24
5.3. Новизна и значимость 27
5.4. Структура работы 29
Глава 1. Основные понятия 30
1.1. Алгебра подстановок 30
1.2. Стандартные схемы программ 42
1.3. Логико-термальная эквивалентность программ 48
Глава 2. Задача проверки логико-термальной эквивалентности программ 51
2.1. Граф совместных вычислений 51
2.2. Процедура разметки графа совместных вычислений 57
2.3. Редуцированные подстановки и алгоритм редукции 64
2.4. Редуцированная антиунификация подстановок 71
2.5. Модифицированный алгоритм проверки логико-термальной эк
вивалентности, его корректность и сложность 76
Глава 3. Логико-термальная унифицируемость программ 79
3.1. Задача унификации программ 79
3.2. Алгоритм проверки логико-термальной унифицируемости программ 83
3.3. Полиномиальный алгоритм проверки логико-термальной унифицируемости программ и его корректность 90
Глава 4. Двусторонняя унификация программ 97
4.1. Задача двусторонней унификации подстановок 98
4.2. Задача ограниченного домино 101
4.3. Обоснование полноты задачи двусторонней унификации подстановок 105
4.4. Задача проверки двусторонней унифицируемости программ 113
Заключение 117
Список литературы
- Стандартные схемы программ
- Процедура разметки графа совместных вычислений
- Алгоритм проверки логико-термальной унифицируемости программ
- Обоснование полноты задачи двусторонней унификации подстановок
Введение к работе
Актуальность и степень разработанности темы исследования. При проектировании программного обеспечения часто возникают ситуации, когда различные фрагменты программы выполняют схожие действия с поступающими в них данными. Такое поведение отдельных фрагментов программ приводит не только к трудности понимания логики программы, но и к увеличению затрат на ее дальнейшую разработку и сопровождение. Поиск таких фрагментов — клонов — даже в небольших программах является очень трудным делом, осуществление же его вручную на промышленных проектах фактически невозможно. В связи с этим возникает потребность в автоматическом средстве обнаружения клонов, которое также позволило бы осуществить проверку того, можно ли путем подстановки вместо входных переменных одного фрагмента программы некоторых инициализирующих выражений сделать его эквивалентным другому фрагменту программы. В этом случае несколько разных фрагментов можно заменить вызовом одной и той же процедуры с разными значениями ее входных параметров. Такой подход к трансформации программ широко используется в рефакторинге — изменении структуры программы, не затрагивающем ее внешнего поведения. Этот метод рефакторинга называется выделением процедуры.
Кроме задач рефакторинга, необходимость проверки эквивалентности фрагментов кода возникает при решении задач оптимизации, построения суперкомпиляторов, построения обфускирующих преобразований, поиска вредоносного кода и многих других.
Для того чтобы создать средство автоматического поиска клонов, необходимо в первую очередь выбрать подходящую математическую модель программ, в рамках которой можно было бы не только адекватно формализовать отношение подобия (“похожести”) программ, но также иметь возможность эффективно распознавать это отношение.
Наиболее естественным для задач такого типа является отношение функциональной эквивалентности программ, при котором каждая программа рассматривается как описание функции, преобразующей набор входных данных в набор выходных данных, а эквивалентность двух заданных программ определяется как совпадение реализуемых ими функций. Однако из теоремы Райса-Успенского следует, что функциональная эквивалентность неразрешима в любой модели вычислений, в которой реализуемы все вычислимые по Тьюрингу функции. Это означает, что для анализа программ необходимо выбирать более строгие, но разрешимые виды эквивалентности, которые аппроксимировали бы функциональную эквивалентность.
Было разработано большое количество моделей программ, многие из них были введены в работах А. А. Ляпунова, Ю. И. Янова, В. М. Глушкова, А. А. Летичевского, М. Патерсона, Д. Скотта, А. П. Ершова, Р. И. Подловчен-ко, В. А. Захарова, Ч. Хоара и других авторов. При этом данные модели имели разные выразительные возможности и, соответственно, разную сложность задачи проверки эквивалентности в них. В данной работе рассматривается модель стандартных схем программ, предложенная М. Патерсоном в 1970 году и изученная А. П. Ершовым. В качестве отношения эквивалентности выбрано отношение логико-термальной эквивалентности стандартных схем программ, впервые предложенное В. Э. Иткиным в 1972 году.
Модель стандартных схем программ представляет собой развитие концепции схем программ Ляпунова-Янова посредством использования языка первого порядка для описания операторов и логических условий, что делает эту модель близкой к тому, каким именно образом описываются программы на большинстве современных языков программирования. Выбор логико-термальной эквивалентности обусловлен тем, что она аппроксимирует функциональную эквивалентность и при этом разрешима за полиномиальное время.
Логико-термальная эквивалентность не использует в своем определении интерпретации функций и предикатов программы и поэтому на нее не распро-2
страняется результат о неразрешимости невырожденных интерпретационных отношений эквивалентности на стандартных схемах программ. Фактически эта разновидность эквивалентности требует изучения лишь синтаксических свойств программы. Данная особенность логико-термальной эквивалентности стандартных схем программ делает это отношение привлекательным для использования при решении некоторых задач статического анализа программ. Первый алгоритм распознавания логико-термальной эквивалентности был представлен В.Э. Иткиным в той же работе, где она была введена. Однако этот алгоритм был достаточно сложным. Позже А. О. Будой был предложен алгоритм, который сводил задачу распознавания логико-термальной эквивалентности к ранее изученной задаче распознавания эквивалентности в классе двухленточных автоматов. Этот алгоритм имел экспоненциальную сложность по времени выполнения. Первый полиномиальный алгоритм был предложен В. К. Сабельфельдом в 1979 году и имел оценку сложности (7), где — суммарный размер анализируемых схем программ.
Важную роль в исследовании, представленном в данной работе, играет алгебра подстановок. Э. Эдером было показано, что множество подстановок с введенными на нем отношениями эквивалентности и частичного порядка представляет собой решетку, на которой могут быть введены операции взятия точной верхней (унификация) и точной нижней (антиунификация) граней.
Задача синтаксической унификации термов возникла при разработке метода резолюций для систем автоматического доказательства теорем, и алгоритмы унификации стали одним из базовых механизмов при вычислении логических программ. Задача антиунификации выражений впервые была рассмотрена независимо в работах Г. Д. Плоткина и Дж. Рейнольдса в 1970 году. В связи с изучением этих задач были построены специальные структуры данных для представления подстановок.
В данной работе для решения задачи проверки логико-термальной эквивалентности стандартных схем программ используется алгебра подстановок. Это
связано с тем, что подстановки представляют собой удобный механизм описания вычислительного эффекта операторов присваивания в программах. Ранее такой подход к решению указанной задачи не исследовался. Как оказалось, использование аппарата подстановок не только упростило решение задачи проверки логико-термальной эквивалентности схем программ, но также позволило решить несколько других смежных задач анализа программ.
Целью диссертационной работы является исследование возможности применения математических моделей и методов теории схем программ для решения задач, возникающих при рефакторинге программ и связанных с проблемой проверки эквивалентности программ, оценка сложности этих задач и разработка алгоритмов их решения.
Для этого были поставлены следующие задачи.
-
Разработать новый алгоритм проверки логико-термальной эквивалентности стандартных схем программ, который опирался бы на свойства решетки подстановок и превосходил бы по эффективности ранее известные алгоритмы решения этой задачи.
-
Разработать алгоритм, осуществляющий за полиномиальное время проверку того, могут ли две заданные стандартные схемы программ стать логико-термально эквивалентными в результате применения некоторой подстановки к их входным переменным. В случае положительного ответа алгоритм должен строить такую унифицирующую подстановку.
-
Изучить задачу, которая заключается в проверке того, могут ли две заданные стандартные схемы программ стать логико-термально эквивалентными в результате применения к входным и выходным переменным одной из них некоторой пары подстановок. Определить, к какому классу сложности относится эта задача. Разработать алгоритм, разрешающий эту задачу и конструирующий указанную пару подстановок, если это возможно.
Основные результаты работы
-
Разработан полиномиальный алгоритм проверки логико-термальной эквивалентности стандартных схем программ, использующий метод совместных вычислений и свойства решетки подстановок. Для данного алгоритма строго обоснована его корректность. Доказано, что сложность этого алгоритма составляет (6), где — суммарный размер исходных стандартных схем программ.
-
Разработан полиномиальный алгоритм проверки логико-термальной унифицируемости стандартных схем программ, который позволяет строить унифицирующие исходные программы подстановки. Для этого алгоритма приведено строгое обоснование его корректности. С использованием этого алгоритма показано, что задача проверки логико-термальной унифицируемости может быть решена за время (11), где — суммарный размер исходных схем программ.
-
Для задачи проверки двусторонней унифицируемости подстановок показана ее -полнота с помощью сведения к ней задачи ограниченного домино, а также разработан недетерминированный алгоритм решения этой задачи, работающий за полиномиальное время. На основании этого результата показана -полнота задачи проверки двусторонней унифицируемости программ, для которой также построен недетерминированный алгоритм, строящий двусторонний унификатор схем программ за полиномиальное относительно их суммарных размеров время. Корректность всех указанных алгоритмов обоснована.
При получении основных результатов использовались методы теории автоматов, алгебры, теории графов, теории сложности алгоритмов.
Научная новизна. Ранее задача проверки логико-термальной эквивалентности стандартных последовательных схем программ уже была решена,
построенный для ее решения алгоритм был полиномиальным и работал за время, равное (7), где — суммарный размер исходных программ. В основе этого алгоритма лежала особого вида структура данных — функциональные сети. В данной диссертационной работе построен алгоритм проверки логико-термальной эквивалентности стандартных схем программ, который использует механизм подстановок и имеет сложность (6).
Задача логико-термальной унификации стандартных схем программ ранее не исследовалась. В данной работе построен полиномиальный по времени алгоритм, разрешающий проверку унифицируемости двух схем программ путем подачи на их вход измененных состояний данных и работающий за (11). Данная задача имеет важное прикладное значение при поиске и изъятии программных клонов.
Другими видами задач семантической унификации, которые рассматривались в данной работе, являются двусторонняя унификация схем программ и двусторонняя унификация подстановок. Ни одна из этих задач ранее не исследовалась. Обе задачи оказались -полны, что свидетельствует о том, что к ним необходимо применять специальные методы решения задач, принадлежащих этому классу сложности.
Теоретическая и практическая значимость. Алгоритм проверки эквивалентности, полученный в данной работе, может быть применен не только при проведении рефакторинга программ, но и для решения многих задач статического анализа, таких как обфускация, верификация, тестирование, поиск вредоносного кода. Полученная для этого алгоритма полиномиальная оценка времени выполнения позволяет судить о возможности его эффективного применения при решении подобных задач.
Задача унификации схем программ, впервые сформулированная и исследованная в данной работе, позволяет осуществлять построение контекста для изымаемого фрагмента. При этом существование разрешающего эту задачу полиномиального по времени алгоритма позволяет судить о возможности приме-6
нения подобного подхода на практике при решении задач рефакторинга.
Показанная в работе сложность задачи проверки двусторонней унифицируемости, напротив, свидетельствует о том, что для решения этой задачи целесообразно применять методы и эвристики, подходящие для решения -полных задач.
Степень достоверности, апробация, список публикаций. Все результаты, представленные в диссертации, сформулированы в виде теорем и снабжены строгими доказательствами.
Результаты представлены на конференции “Проблемы теоретической кибернетики” (2011 год, Нижний Новгород), семинаре “Дискретная математика и её приложения” (2012 год, Москва), конференции “Проблемы теоретической кибернетики” (2014 год, Казань), на семинарах “UNIF-2013” (2013 год, Эйнд-ховен), “UNIF-2014” (2014 год, Вена), а также на конференциях “Ломоносов” (2012, 2014 годы, Астана) и опубликованы в работах [–], четыре из них — в журналах из перечня ВАК [3,6,,]. В работах [3,6,,] научному руководителю В. А. Захарову принадлежат постановки задач.
Структура и объём диссертации. Диссертация состоит из четырех глав, введения, заключения и следующего за заключением списка литературы. Общий объём рукописи составляет 135 страниц и включает 8 рисунков. Список литературы содержит 154 наименования.
Стандартные схемы программ
Назовем /с-местной атомарной формулой (или просто атомом) всякое выражение вида Р к {t\,..., tk), где Р(к — предикатный символ, а t\,..., tk — термы. Множество атомарных формул обозначим записью Atom(Var, F). Записи Vart и VafA будут обозначать множества переменных, входящих в состав терма t и атома А соответственно.
Пусть X и Y — два конечных множества переменных, X С Var, Y С Var. X — Y-подстановкой назовем всякое отображение в : X — Term(Y, F), сопоставляющее каждой переменной из X некоторый терм во множестве Term(Y,F), при этом само множество Term(Y,F) будем называть областью значений подстановки. Множество Dome = {х Є X : 6(х) ф х} будем называть областью подстановки. Множество подстановок с конечной областью X и областью значений Term(Y,F) обозначим Subst(X,Y, F). Если в є Subst(X,Y, F), Dome = { 1, 2,..., xn} и 6(ХІ) = j, 1 г n, то подстановка в однозначно определяется множеством пар {x\lt\,x ilt i, ,xn/tn}. Эти пары также будем называть связками подстановки в. Запись Varo будет использоваться для обозначения множества переменных (Jf=1 Уаг\ , входящих в состав всех термов подстановки. Результатом применения подстановки в к терму t Є Term(X, F) называется терм t0, который получается одновременной заменой в t каждой переменной ХІ термом 6(ХІ). Аналогично определяется результат применения подстановки к атому: Ав есть атом, который получается одновременной заменой каждого вхождения переменной ХІ в атом А термом 9{ХІ). Пусть Е — атом или терм, тогда выражение Ев, полученное в результате применения к выражению Е подстановки в, будем называть примером выражения Е, специализированным подстановкой в.
Композицию 9г] подстановок в Є Subst(X, У, F) и ц є Subst(Y, Z, F) определим следующим образом: (6rf){x) = (0(х))г) для каждой переменной х Є X, при этом для подстановки /І = Qr\ верно /І Є Subst(X, Z,F). Поскольку для любого терма t,t Є Term(Var,F) справедливо равенство t{9r]) = (t$)r), опера 32 ция композиции подстановок является ассоциативной. Подстановка р, которая является биекцией Y на У, называется переименованием.
На множестве Subst(X, У, F) введем отношение предпорядка и отношение эквивалентности : для пары подстановок #i,#2 условимся считать, что #1 #2 выполняется, если существует такая подстановка ц Є Subst(Y,Y, F), что #2 = #і?7. В этом случае подстановку 0\ будем называть прототипом или шаблоном подстановки #2, подстановку 02 — примером подстановки 0\. Подстановку г] будем называть пополнением прототипа 0\ до примера 02- В случае, если для некоторого переименования р верно, что 02 = 9\р, будем говорить, что подстановки 0\ и 02 эквивалентны: 0\ 02 Как было показано в работе [25], отношение предпорядка - индуцирует на множестве классов эквивалентности Subst (X,Y,F) отношение частичного порядка Частично упорядоченное множество (Subst (X,Y,F), ) образует решетку, наименьшим элементом которой является класс эквивалентности, порожденный так называемой пустой подстановкой є = {хі/уі,... ,жп/уп}. Данное частично упорядоченное множество было также подробно изучено в работах [52,65]. Введем на множестве подстановок специальную максимальную подстановку т, удовлетворяющую равенству т0 = 0т = г для любой подстановки 0.
Операция взятия точной верхней грани в этой решетке называется унификацией подстановок и обозначается символом "f, операция взятия точной нижней грани называется антиунификацией подстановок и обозначается символом -І. В работе [25] было установлено, что решетка (Subst (X,Y,F), ) обладает свойством обрыва убывающих цепей: для всякой подстановки 0 длина любой цепи между классами 0 и є конечна.
В дальнейшем запись 0\ \. 02 будем использовать для обозначения произвольной подстановки из класса эквивалентности 0 \. 0 . Также для любой пары подстановок в , в є Subst(X , У, F) и 0"\0" є Subst(X", У, F) в том случае, если X П X" = 0, мы будем использовать запись 0 U 0" для обозначения подстановки ту, которая представляет собой теоретико-множественное объединение связок подстановок в и в".
Задача антиунификации (построения наименее общих шаблонов) подстановок рассматривалась в ряде работ [63,65,70,72,83,92,114]; в этих работах были предложены различные алгоритмы антиунификации подстановок и термов, а также исследованы свойства этой операции.
Для представления термов в дальнейшем будут использоваться ациклические ориентированные графы (АОГ).
Рассмотрим произвольный конечный ациклический ориентированный граф G = (V, Е), где через V обозначено множество вершин, а через Е — множество дуг графа. Размером графа будем называть суммарное количество его вершин и дуг, то есть \G\ = \V\ + \Е\. Разметкой ациклического ориентированного графа назовем отображение, которое ставит в соответствие каждой вершине графа v символ sV, где sv Є {F,Var}, а каждой дуге графа ставится в соответствие некоторое натуральное число.
Разметка АОГ называется правильной, если она удовлетворяет следующим двум требованиям: если вершина v является листовой, то есть не имеет исходящих дуг, то она помечена либо константой, либо переменной; если из вершины v исходят п дуг, где п 0, то эта вершина помечена функциональным символом местности п, а пометки всех исходящих дуг соответствуют попарно различным числам из множества {1,2,..., п}. Если в правильно размеченном АОГ G из вершины v\ в вершину V2 ведет дуга, помеченная числом т, то вершину V2 будем называть т-наследником вершины V\. Каждой вершине v правильно размеченного АОГ G с приписанным ей символом sv можно однозначным образом поставить в соответствие терм tV, который строится согласно следующим правилам:
Процедура разметки графа совместных вычислений
Поскольку для подстановки ц и любых подстановок в\, 02 выполняются отношения г] г]9\ и г] 77 2, в силу свойств операции антиунификации верно и отношение г] г]9\ \. г]02- Последнее неравенство означает, что существует такая подстановка , Є Subst(Y, У, F), для которой верно равенство r]6i -J, 77 2 = vC-Следовательно, существуют такие подстановки pi,p2, РьР2 Є Subst(Y,Y, F), что Г]6і = iJ Pi И 1 2 = 11 Р2- Рассмотрим произвольную переменную у из множества Y. Предположим, что у Є Varti: где ti - терм, соответствующий паре {xi/ti(yi,... ,Ут)} из подстановки 77. Тогда для указанных выше подстановок и терма ti верны две цепочки равенств Из совпадения левых частей этих равенств следует, что у0\ = у рі для переменной у. Поскольку переменная у — произвольная переменная из множества У, это последнее равенство справедливо для всех у Є Y. Аналогично можно показать, что у02 = У Р2. Таким образом справедливы неравенства \у 0\\у и ,\У $2Іу, и как их следствие неравенство \у 0\\у -J, 0 і\у
Из определения операции антиунификации следует, что для проекций двух подстановок на одну и ту же переменную выполнено равенство 0\ \у \. 02\у [0\ \. Оо)\у. Таким образом, мы приходим к заключению о том, что \у [0\ \. 02)\у
Рассмотрим проекции подстановок на все множество Y. C учетом соотношения г]9\ \. 7#2 = т] получаем следующую цепочку соотношений Г]9і .J, Г]02 = = Vi W) ?(($1 -i 2)\Y) = г]{0\ і 2)- которая и служит обоснованием неравенства т\0\ \- Ц02 77 П
Введем понятие стандартной схемы программы. Рассмотрим два заданных конечных множества переменных X = {хі,... ,хп} и Y = {г/і,... ,уто}. Параметрами или входными переменными программы назовем переменные множества X, а внутренними или локальными переменными программы — переменные множества Y.
Стандартной схемой императивной программы со множеством входных переменных X будем называть конечную систему переходов (размеченный ориентированный граф) тт(Х). Каждой вершине v этого графа приписан некоторый оператор ветвления, соответствующий логическому переходу в программе по условному оператору (предикату). Из каждой вершины исходят две дуги, одна из которых помечена символом 0, а другая — символом 1. Переходы между вершинами этого графа соответствуют линейным участкам в программе — последовательностям операторов присваивания. Каждому оператору присваивания вида х := t(...) в программе соответствует подстановка {#/(...)}; при этом линейному участку операторов присваивания вида Х\ := t\(...); Х2 := хп := tn(...) в соответствие может быть поставлена композиция подстановок в = {xn/tn}{xn-i/tn-i} ... {x\/t\}. Указанная подстановка в призвана корректно отображать вычислительный эффект линейного участка операторов присваивания в программе в терминах алгебры подстановок.
Введем формальное определение программы. При этом в дальнейшем будем опускать указание множества входных переменных программы, если оно понятно из контекста.
Программой над множеством входных переменных X = {xi,... ,хп} и множеством внутренних переменных Y = {г/і,..., ут} назовем размеченную систему переходов (размеченный ориентированный граф) 7Г = (X, У, У, Vin, Vout, -В, — -, Ао), где: функция переходов. Каждой невыходной вершине v, v Є V \ {iw}, программы 7Г в зависимости от истинностного значения приписанного ей предиката функция указывает подстановку, описывающую результат выполнения линейного участка программы, следующего за вершиной v в программе, а также вершину, на которую переходит управление программы после выполнения этого линейного участка; Ло Є Subst(X,Y,F) — подстановка, инициализирующая внутренние переменные программы.
Введем несколько обозначений. Договоримся, что если заданная подстановка соответствует линейному участку программы между вершинами и, г , то для краткости такую подстановку будем обозначать 9 vy Кроме того, в дальнейшем при обращении к функции переходов вместо записи —и, 5) = (v,0UyV) бу 5,9 дем использовать запись и — v, опуская у подстановки индекс u,v, если он понятен из контекста. Мы также будем использовать запись Vj = succ(7r, Vi, 5) для обозначения того факта, что в графе программы 7Г из вершины Vi исходит дуга с пометкой 6 Є А в вершину Vj, и для удобства в этой записи опускать соответствующую подстановку 9VuV . При этом вершина Vj называется А-наследником
Алгоритм проверки логико-термальной унифицируемости программ
Как уже было сказано во введении, задача проверки логико-термальной эквивалентности программ непосредственно связана с задачами рефакторин-га программного кода. В частности, задача выделения метода подразумевает, что изъятый фрагмент кода действительно является эквивалентным коду той функции, вызовом которой заменяется его вхождение. При этом, однако, каждый фрагмент программного кода подразумевает наличие “предыстории”: перед входом во фрагмент каждая переменная имеет некоторую термальную историю. В связи с этим оправданным является подход, когда происходит не просто изъятие фрагмента и замена его на вызов некоторой процедуры, не делающей никаких предположений о значении переменных, а замена фрагмента вызовом процедуры, принимающей на вход переменные в их текущем состоянии.
В данной главе вводится понятие логико-термальной унификации программ. Предложенный алгоритм проверки унифицируемости программ позволяет проверить, может ли один фрагмент кода быть логико-термально эквивалентен другому фрагменту при условии, что перед входом в каждый из них осуществляется некоторая инициализация переменных. Данный алгоритм позволяет также в случае, если программы являются унифицируемыми, получать унифицирующую подстановку.
Полученные в данной главе результаты были изложены в статьях [104], [149] и частично в статье [146].
Для того, чтобы формально поставить задачу проверки логико-термальной унифицируемости программ и задачу нахождения унификатора, введем предварительно операцию применения подстановки к программе. Пусть заданы программа тт(Х) = (X, У, У, Vin vout В, — -, Ло) и подстановка а, а Є Subst(X, X, F). Тогда результатом применения подстановки а к программе 7Г назовем программу а; 7Г, полученную в результате следующих действий: в программе 7Г переименовывается входная вершина: вершина Vin становится вершиной г о; в программу вносится новая вершина -и, исходящие из нее дуги направляются в вершину VQ. Вершине v приписывается нульместный атом А$. В программу вводятся две дуги, ведущие из вершины v в вершину г о, одна из которых помечается 0, а другая — 1. Каждой из этих дуг приписывается подстановка а; введенная вершина v становится входной в новой программе.
Семантически таким образом определенное применение подстановки к программе соответствует задаче, возникающий при выделении метода в рефакто-ринге. Подстановка а играет роль набора подготовительных присваиваний перед передачей управления в тело функции, представляемой программой 7Г. Это позволяет изымать из программы не только логико-термально эквивалентные фрагменты кода, но, как будет показано дальше, некоторые виды фрагментов, которые эквивалентными не являются, но тем не менее имеют сходное поведение. Для формальной постановки указанной задачи введем понятие логико-термально унифицируемых программ.
Пусть конечное множество переменных X разбито на два непересекающихся подмножества X и X" . Подстановку а, а Є Subst(X, X, F), назовем логико-термальным унификатором программ тт (Х ) и ІЇ (Х"), если программы а; 7г и а; ті" логико-термально эквивалентны. Далее для краткости будем называть логико-термальный унификатор просто унификатором. Две программы тт (Х ) и ті"{Х") назовем логико-термально унифицируемыми, если для них существует унификатор.
Унификатор а программ тт (Х ) и тт"(Х") назовем наиболее общим унификатором этих программ, если для любого унификатора этих программ а выполнено а а . Наиболее общий унификатор двух программ ТТ (Х ) и тт"(Х") будем обозначать MGU(7r (X ),7r"(X")). Для унификатора программ тт (Х ) и ті"{Х") справедливо следующее свойство. Теорема 12. Подстановка а, а Є Subst{X U Х",Х U X F) является унификатором программ ТІ = (X ,Y , У [п)у ои1) , -V, Х0) и ТІ" = (X", У", V",v"n,v"ut, В" -V , X0) в том и только в том случае, когда граф их совместных вычислений IV // корректен и для любого маршрута где $i = {9[ U 6"}, в нем выполнено равенство В (v n+1)0a = В"(у +1)ва, где 9 = 0n0n_1...00. Доказательство.
Пусть программы 7г и -к" логико-термально унифицируемы, при этом унифицирующая их подстановка есть а. Тогда по определению унифицируемых программ из теоремы 2 следует, что каждый путь в графе совместных вычислений Га;7Г/;а;7Г// программ а] 7г и а; ті" удовлетворяет указанному в теореме равенству. Рассмотрим граф совместных вычислений Т / п программ ті и ті". Выберем в нем произвольный путь path. Ему соответствует единственный путь path! в графе Га;7Г/;а;7Г//, который, как показано выше, удовлетворяет равенству в условии теоремы. Отсюда получаем справедливость утверждения теоремы для пути path.
Обратное утверждение доказывается схожим образом. Пусть для каждого пути графа совместных вычислений Т " выполнено приведенное в теореме ра венство. Рассмотрим произвольный путь этого графа path. В графе совместных вычислений Га;7Г/;а;7Г// существует единственный путь path , соответствующий пу ти path, для которого выполнено равенство B (v n+l)9a = B"(v"+1)0a, где 9 — соответствующая пути path подстановка. Тогда из определения унификатора программ, произвольного выбора пути path и из теоремы 2 следует, что для каждого пути path графа Га;7Г/;а;7Г// выполнено равенство из условия теоремы, а значит, программы 7г и тт" логико-термально унифицируемы и а — их унифи катор. Пусть T i n = (V,it -, Ао) — граф совместных вычислений программ 7г и тт". Рассмотрим для каждой вершины w = (u,v) графа IV // путь path, ведущий из вершины wo в вершину w, а также подстановку этого пути, 9path. Обозначим через Н и множество пар {B {u)9path-,B"{v)9path). Для введенного таким образом множества справедлива следующая теорема.
Обоснование -полноты задачи двусторонней унификации подстановок
Эта подстановка вместо каждой переменной, ассоциированной с парой смежных сторон квадратов (ii,ji), ( 2?J2) области Area, подставляет нумерал, дополняющий исходный цвет пары сторон c(ii,Ji,i2?J2) ДО максимального цвета ІІГ. Фактически, данная подстановка осуществляет синхронное перекрашивание пар смежных сторон. Принимая во внимание, что исходное покрытие является -правильным, подобное синхронное перекрашивание приводит к построению монохромно окрашенной области, которую как раз и описывает подстановка 02-( =). Пусть существует пара подстановок (г) ,г)"): таких, что v[Q\v[ = 62-Для того, чтобы выяснить состав подстановок т/, г)" , рассмотрим устройство подстановок в\ и $2. Каждая нелистовая вершина каждого размеченного дерева леса, представляющего геометрическую реализацию подстановки 9\, помечена одним из символов f(l или ЬУ\ причем в каждом пути единственный функциональный символ Ьл& предшествует функциональным символам f l . В то же время, размеченные деревья, представляющие подстановку #2, по каждому пути от корня к листу содержат сначала вершины, помеченные функциональным символом д 2\ затем единственную вершину, помеченную символом ЬУ\ затем вершины, помеченные символом f l\ после чего по каждой ветви следует листовая вершина. Кроме того, каждое дерево терма подстановки в\ для каждого квадрата (i,j) области Area содержит единственное поддерево, начинающееся с функционального символа Ьл&\ и такое, что его терм имеет вид h(fi(yo),fj(yo),---)- Из приведенных фактов следует, что подстановка п имеет следующий вид:
Рассмотрим покрытие Т области Area, в котором для каждого квадрата (i,j) выполнено равенство T(i,j) = Uj тогда и только тогда, когда в некотором терме подстановке п содержится переменная Xijjir Покажем, что такое покрытие является -правильным.
Предположим, что это не так. Это означает, что существуют два соседних квадрата (i,j), (і -,] ) таких, что окраска сторон домино, примыкающих к их общей границе, разная, то есть выполнено одно из неравенств: T(i,j)[i — i ,j — j ] Ф T(i , j )[i — і, j — j], если (і, j), (і , j ) є Interior, или T(і, j)[і — і , j — j ] ф B(i ,j ): если (i,j) Є Interior, a (i ,j ) Є Border.
Рассмотрим сначала первый вариант. Не ограничивая общности, будем считать, что і i, j j . Поскольку глубина вхождения переменной yij j в термы tij (ij) и ti ,j ,T(i ,j ) определяется показателем нумерала /п, входящего в состав терма, а показатель нумерала в свою очередь является номером цвета соответствующей стороны домино, то глубина вхождения этой переменной в термы tij (ij) и ti ,j ,T(i ,j ) будет разной. Но из устройства подстановок т/ и в\ следует, что в разных связках композиции г] 9\ вхождения переменной yij j также будут иметь разную глубину. Рассмотрим композицию r[Q\r[ . В ней ну-мералы, соответствующие подтермам tijj4 и ti j j., ., будут разными. Но терм подстановки 02 моделирует монохромную окраску, то есть показатели всех нуме-ралов, связанных с окраской домино, должны быть в нем одинаковы. Получаем противоречие с тем, что 02 = Г] 9іГ]".
Второй вариант, когда отличается цвет соседних сторон домино в квадратах, один из которых расположен на границе, опровергается аналогично.
Доказательство. Рассмотрим описанный в этом разделе процесс построения пары подстановок (#i,#2), ассоциированных с примером задачи ограниченного домино ВТ = (n, m, Tiles, В). Этот процесс является детерминированным алго ритмом, который строит термы tij, tij, tijjij и tijjir Для построения древесного представление каждого из таких термов алгоритму необходим объем рабочей памяти размера O(logN), где N — размер исходной задачи. Таким образом, пара подстановок (#i,#2) требует объема рабочей памяти, пропорционального логарифму размера описания примера задачи ограниченного домино. Таким образом, из лемм 27 и 28, а также из результатов, полученных в работе [54], следует справедливость следующей теоремы.
Задача проверки двусторонней унифицируемости программ фактически является обобщением задачи двусторонней унификации подстановок. Рассмотрим эту задачу для введенной в первой главе модели последовательных императивных программ и для введенного над этой моделью отношения логико-термальной эквивалентности программ. Для этого необходимо описать операцию применения подстановок к программе. Отметим, что описание этой операции хоть и повторяет частично описание применения подстановки ко входам программы, описанное в предыдущей главе, но является более широким: в данном случае подстановки применяются не только ко входным переменным программы, но и к переменным, поданным на выход.