Свойства и виды стандартных схем программ

1.3.1. Эквивалентность, тотальность, пустота, свобода

ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливается).

Стандартные схемы S₁ и S₂ в базисе В функционально эквивалентны (S₁ ~ S₂), если либо обе зацикливаются, либо обе останавливаются с одинаковым результатом, т. е. val (S₁, I)» val (S₂, I).

Примеры тотальных, пустых и эквивалентных схем S₂, S₃, S₄, S₅ приведены на рисунке 1.3.

Рисунок 1.3

Цепочкой стандартной схемы (ЦСС) называют:

1. конечный путь по вершинам схемы, ведущий от начальной вершины к заключительной;

2. бесконечный путь по вершинам, начинающийся начальной вершиной схемы.

В случае, когда вершина-распознаватель (v), то дополнительно указывается верхний индекс (1 или 0), определяющий 1-дугу или 0-дугу, исходящую из вершины.

Примеры цепочек схемы S₁ (рисунок 1.2,а):

(0, 1, 2¹, 5); (0, 1, 2⁰, 3, 4, 2⁰,3,4,2¹,5) и т. д.

Цепочкой операторов (ЦО) называется последовательность операторов, метящих вершины некоторой цепочки схемы.

Например для S₁: (start (х), у:=a, р¹(x), stop (у)) или (start (х), у:=a, р⁰(x), y:=g(x, y), x:=h(x), р⁰(x), y:=g(x, y), x:=h(x), р⁰(x), y:=g(x, y), x:=h(x), …)) и т. д.

Предикатные символы ЦО обозначаются так же, как вершины распознавателей в ЦСС.

Пусть S - ССП в базисе В, I - некоторая его интерпретация, (0, 1, к₂, к₃,…) - последовательность меток инструкций S, выписанных в том порядке, в котором эти метки входят в конфигурации протокола выполнения программы (S, I). Ясно, что эта последовательность – цепочка схемы S. Считают, что интерпретация I подтверждает (порождает) эту цепочку.

ЦСС в базисе В называют допустимой, если она подтверждается хотя бы одной интерпретацией этого базиса.

Не всякая ЦСС является допустимой. В схеме S₂ (рисунок 1.3,а) цепочки (0, 1, 2⁰, 5, 6¹, 7), (0, 1, 2¹, 3, 4⁰, 7) и все другие конечные цепочки не подтверждаются ни одной интерпретацией.

Свойство допустимости цепочек играет чрезвычайно важную роль в анализе ССП. В частности оно определяет те случаи, когда стандартная схема свободна.

ССП свободна, если все ее цепочки допустимы.

Допустимая цепочка операторов - это цепочка операторов, соответствующая допустимой цепочке схемы. В тотальной схеме все допустимые цепочки (и допустимые цепочки операторов) конечны. В пустой схеме - бесконечны.

Рассмотренные свойства распространяются на все другие классы стандартных схем и образуют опорные пункты схематологии программирования.

1.3.2. Свободные интерпретации

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

Все СИ базиса В имеют одну и ту же область интерпретации, которая совпадает со множеством Т всех термов базиса В. Все СИ одинаково интерпретируют переменные и функциональные символы, а именно:

а) для любой переменной х из базиса В и для любой СИ I_h этого базиса I_h(x)=x;

б) для любой константы a из базиса В I_h(a)=a;

в) для любого функционального символа f⁽ⁿ⁾ из базиса В, где n³1, I_h(f⁽ⁿ⁾)=F⁽ⁿ⁾: Tⁿ®T, где F⁽ⁿ⁾ - словарная функция такая, что

F⁽ⁿ⁾(t₁, t₂,..., t_n)= f⁽ⁿ⁾ (t₁, t₂,... t_n),

т. е. функция F⁽ⁿ⁾ по термам t₁, t₂,...t_n из Т строит новый терм, используя функциональный смысл символа f⁽ⁿ⁾.

Что касается интерпретации предикатных символов, то она полностью свободна, т.е. разные СИ различаются лишь интерпретаций предикатных символов.

Таким образом, после введения СИ термы используются в двух разных качествах, как функциональные выражения в схемах и как значения переменных и выражений. В дальнейшем термы-значения будем заключать в апострофы. Например, если где t₁=`f(x,a)` - терм-значение переменной x, а где t₂ = `g(y)` - терм-значение переменной y, то значение свободно интерпретированного терма t₃=f(x, h(y)) равно терму-значению `f(f(x,a), h(g(y)))`.

Пример 1.1. Пусть I_h -СИ базиса, в котором определена схема S₁ (рисунок 1.2, а), и в этой интерпретации предикат Р=I_h(р) задан так: P(t) = 1, если число функциональных символов в t больше двух; P(t) = 0, в противном случае.

Тогда ПВП (S₁,I_h) можно представить таблицей 1.3.

Таблица 1.3

Конфигурация	Метка	Значения
		X	у
U0		`x`	`y`
U1		`x`	`a`
U2		`x`	`a`
U3		`x`	`g(x,a)`
U4		`h(x)`	`g(x,a)`
U5		`h(x)`	`g(x,a)`
U6		`h(x)`	`g(h(x),g(x,a))`
U7		`h(h(x))`	`g(h(x),g(x,a))`
U8		`h(h(x))`	`g(h(x),g(x,a))`
U9		`h(h(x))`	`g(h(h(x)),g(h(x),g(x,a)))`
U10		`h(h(h(x)))`	`g(h(h(x)),g(h(x),g(x,a)))`
U11		`h(h(h(x)))`	`g(h(h(x)),g(h(x),g(x,a)))`
U12		`h(h(h(x)))`	`g(h(h(x)),g(h(x),g(x,a)))`

Обратим внимание на следующую особенность термов. Если из терма удалить все скобки и запятые, то получим слово (назовем его бесскобочным термом), по которому можно однозначно восстановить первоначальный вид терма (при условии, что отмечена или известна местность функциональных символов). Например, терму g⁽²⁾(h⁽¹⁾(x), g⁽²⁾(x,y)) соответствует бесскобочный терм ghxgxy. Правила восстановления терма по бесскобочной записи аналогичны правилам восстановления арифметических по их прямой польской записи, которая просто и точно указывает порядок выполнения операций.

В этой записи, впервые примененной польским логиком Я. Лукашевичем, операторы следуют непосредственно за операндами. Поэтому ее иногда называют постфиксной записью. Классическая форма записи, как мы обычно пишем, называется инфиксной. Например:

A*B => AB* A*B+C =>AB*C+ A*(B+C/D) =>ABCD/+* A*B+C*D =>AB*CD*+

Правила представления в польской записи:

1) Идентификаторы следуют в том же порядке, что и в инфиксной записи

2) Операторы следуют в том же порядке, в каком они должны вычисляться (слева направо)

3) 3) Операторы располагаются непосредственно за своими операндами.

Бесскобочная запись термов короче и она будет использоваться далее наряду с обычной записью.

1.3.3. Согласованные свободные интерпретации

Полагают, что интерпретация I и СИ I_h (того же базиса В) согласованы, если для любого логического выражения p справедливо I_h(p)=I(p).

Пусть, например, t=`g(h(h(x)), g(h(x), g(x,a)))`, а интерпретация I₃ совпадает с интерпретацией I₁ из п. 1.2.4 за исключением лишь того, что I(x)=3. Так как I₃(a) = 1; I₃(g) - функция умножения; I₃(h) - функция вычитания 1; получаем I₃(t) = ((3-1)-1)*((3-1)*(3*1)) = 6.

В этом случае I_h примера из п. 1.3.2. согласована с только что рассмотренной интерпретацией I₃, а так же с I₂ (рисунок 1.2, в), но не согласована с I₁ (рисунок 1.2, б).

Справедливы прямое и обратное утверждения, что для каждой интерпретации I базиса В существует согласованная с ней СИ этого базиса.

Так, например, выше было сказано, что I_h рассмотренного примера не согласована с I₁. Что бы сделать I_h согласованной, необходимо условие Р(t) видоизменить: P(t) = 1, если число функциональных символов в t больше трех; P(t) = 0, в противном случае.

Можно поступить и по другому. Оставить I_h без изменения и согласовать с ней I₁. Для этого необходимо будет заменить I₁(x) = 4, на I₁(x) = 3.

Введем важное вспомогательное понятие подстановки термов, используемое в дальнейшем. Если x₁, …, x_n (n ≥ 0) – попарно различные переменные, t₁,..., t_n – термы из Т, а p - функциональное или логическое выражение, то через p[t₁/x₁,..., t_n/x_n] будем обозначать выражение, получающееся из выражения p одновременной заменой каждого из вхождений переменной x_i на терм t_I (i = 1, …, n). Например: a[y/x]=a, f(x, y)[y/x, x/y]=f(y, x), g(x)[g(x)/x]=g(g(x)), p(x)[a/x]=p(a).

Приведем без доказательства несколько важных утверждений:

Если интерпретация I и свободная интерпретация I_h согласованы, то программы (S, I) и (S, I_h) либо зацикливаются, либо обе останавливаются и I(val(S,I_h))= val(S,I), т.е. каждой конкретной программе можно поставить во взаимно-однозначное соответствие свободно интерпретированную (стандартную) согласованную программу.

Если интерпретация и свободная интерпретация согласованы, они порождают одну и ту же цепочку операторов схемы.

Теорема Лакхэма – Парка – Паттерсона. Стандартные схемы S₁ и S₂ в базисе В функционально эквивалентны тогда и только тогда, когда они функционально эквивалентны на множестве всех свободных интерпретаций базиса В, т.е. когда для любой свободной интерпретации I_h программы (S₁,I_h) и (S₂,I_h) либо обе зацикливаются, либо обе останавливаются и val(S₁,I) = {I(val(S₁ I_h)) = I(val(S₂ I_h))} = val(S₂,I).

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

Стандартная схема S в базисе В свободна тогда и только тогда, когда она свободна на множестве всех свободных интерпретаций этого базиса, т. е. когда каждая цепочка схемы подтверждается хотя бы одной свободной интерпретацией.

1.3.4. Логико-термальная эквивалентность

Отношение эквивалентности Е, заданное на парах стандартных схем, называют корректным, если для любой пары схем S₁ и S₂ из S₁ ~Е~ S₂ следует, что S₁~ S₂, т. е. S₁ и S₂ функционально эквивалентны.

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

Идея построения таких (корректных и разрешимых) отношений связанна с введением понятия истории цепочки схем. В истории с той или иной степенью детальности фиксируются промежуточные результаты выполнения операторов рассматриваемой цепочки. Эквивалентными объявляются схемы, у которых совпадают множества историй всех конечных цепочек.

Одним из отношений эквивалентности является логико-термальная эквивалентность (ЛТЭ).

Определим термальное значение переменной х для конечного пути ω схемы S как терм t(ω, x), который строится следующим образом.

1. Если путь ω содержит только один оператор А, то: t(ω, x) = t, если А – оператор присваивания, t(ω, x) = х, в остальных случаях.

2. Если ω = ω’Ае, где А – оператор, е – выходящая из него дуга, ω’ – непустой путь, ведущий к А, а x₁, …, x_n – все переменные терма t(Ае, x), то t(ω, x) = t(Ае, x)[ t(ω’, x₁)/x₁, …, t(ω’, x_n)/x_n].

Понятие термального значения распространим на произвольные термы t: t(ω, x) = t [ t(ω, x₁)/x₁, …, t(ω, x_n)/x_n].

Например, пути

start (х); y:=x; p¹(x); x:=f(x); p⁰(y); y:=x; p¹(x); x:=f(x) в схеме на рисунке 1.4, а соответствует термальное значение f(f(x)) переменной х.

Рисунок 1.4.

Для пути ω в стандартной схеме S определим ее логико-термальную историю (ЛТИ) lt(S, ω) как слово, которое строится следующим образом.

1. Если путь ω не содержит распознавателей и заключительной вершины, то lt(S, ω) – пустое слово.

2. Если ω = ω’vе, где v – распознаватель с тестом p(t₁,..., t_k), а е – выходящая из него Δ-дуга, Δ Î{0,1}, то lt(S, ω) = lt(S, ω’) p^Δ(t(ω’, t₁), …, t(ω’, t_k)).

3. Если ω = ω’v, где v – заключительная вершина с оператором stop (t₁,..., t_k), то

lt(S, ω) = lt(S, ω’) t(ω’, t₁) … t(ω’, t_k).

Например, логико-термальной историей пути, упомянутого в приведенном выше примере, будет p¹(x) p⁰(x) p¹(f(x)).

Детерминантом (обозначение: det(S)) стандартной схемы S называют множество ЛТИ всех ее цепочек, завершающихся заключительным оператором.

Схемы S₁ и S₂ называют ЛТЭ (лт - эквивалентными) S₁ ~ЛТ~ S₂, если их детерминанты совпадают.

Приведем без доказательства следующие утверждение:

Логико-терминальная эквивалентность корректна, т. е. из ЛТЭ следует функциональная эквивалентность (S₁ ~ЛТ~ S₂ Þ S₁ ~ S₂). Обратное утверждение как видно из рисунка 1.4 не верно.

ЛТ–эквивалентность допускает меньше сохраняющих ее преобразований, чем функциональная эквивалентность.

Дата добавления: 2014-01-07