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

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

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

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

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

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

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

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

Примеры цепочек схемы S₁ (рисунок 1.3,а): (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, …, l₂, l₃,…) - последовательность меток инструкций S, выписанных в том порядке, в котором эти метки входят в конфигурации протокола выполнения программы (S, I). Ясно, что эта последовательность – цепочка схемы S. Считают, что интерпретация I подтверждает (порождает) эту цепочку.

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

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

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

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

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

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

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

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

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

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

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

в) для любого функционального символа f ⁽ⁿ⁾ из базиса В, I_h(f ⁽ⁿ⁾) = F⁽ⁿ⁾: Tⁿ T, где F⁽ⁿ⁾ - словарная функция такая, что F⁽ⁿ⁾(t₁, t₂, ..., t_n) = f ⁽ⁿ⁾ (t₁, t₂, ..., t_n), n ³ 1, т. е. функция 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.3, а), и в этой интерпретации предикат Р = I_h(р) задан так: P(t) = 1, если число функциональных символов в t больше двух; P(t) = 0, в противном случае.

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

Табл. 1.3.

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

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

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

A*B+C =>AB*C+;A*B+C*D =>AB*CD*+.

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

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

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

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

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

Не нашли, что искали? Воспользуйтесь поиском по сайту: