- •Вопрос №9(Система аксиом ив, Полнота и независимость системы аксиом)
- •Аксиомы ив
- •1.6. Операции над протоколами
- •1.6.1. Конкатенация
- •1.6.2. Сужение
- •1.6.3. Голова и хвост
- •1.6.4. Звездочка
- •1.6.5. Порядок
- •1.6.6. Длина
- •1.7. Реализация протоколов
- •1.8. Протоколы процесса
- •1.8.1. Законы
- •1.8.2. Реализация
- •1.8.3. После
- •1.9. Дальнейшие операции над протоколами
- •1.9.1. Замена символа
- •1.9.2. Конкатенация
- •1.9.3. Чередование
- •1.9.4. Индекс
- •1.9.5. Обратный порядок
- •1.9.6. Выборка
- •1.9.7. Композиция
- •2.2. Взаимодействие
- •2.2.1. Законы
- •2.2.2. Реализация
- •2.2.3. Протоколы
- •2.3. Параллелизм
- •2.3.1. Законы
- •2.3.2. Реализация
- •2.3.3. Протоколы
- •1.10.1. Соответствие спецификации
- •1.10.2. Доказательства
1.6.4. Звездочка
Множество A*–это набор всех конечных протоколов (включая <>), составленных из элементов множества A. После сужения на A такие протоколы остаются неизменными, Отсюда следует простое определение:
A* = {s | s ↾ A = s}
Приведенные ниже законы являются следствиями этого определения:
L1. <> ∈ A*
L2. <x> ∈ A* ≡ x ∈ A
L3. (s^t) ∈ A* ≡ s ∈ A* & t ∈ A*
Они обладают достаточной мощностью, чтобы определить, принадлежит ли протокол множеству A*. Например, если
x ∈ A, а у ∉ A, то
<x, y> ∈ A* ≡ (<x>^<y>) ∈ A*
≡ (<x> ∈ A*) & (<y> ∈ A*) по L3
≡ истина & ложь по L2
≡ ложь
Еще один полезный закон может служить рекурсивным определением A*:
L4. A* = {t | t = <> ∨ (t0 ∈ A & t’ ∈ A*)}
1.6.5. Порядок
Если s – копия некоторого начального отрезка t, то можно найти такое продолжение u последовательности s, что s^u = t Поэтому мы определим отношение порядка
s ≤ t = (∃u.s^ = t)
и будем говорить, что s является префиксом t. Например:
<x, y> ≤ <x, y, x, w>
<x, y> ≤ <z, x, y> ≡ x = z
Отношение ≤ является частичным упорядочением и имеет своим наименьшим элементом <>. Об этом говорят законы L1–L4:
L1. <> ≤ s наименьший элемент
L2. s ≤ s рефлексивность
L3. s ≤ t & t s ⇒s = t антисимметричность
L4. s ≤ t & t ≤ u ⇒ s ≤ u транзитивность
Следующий закон вместе с L1 позволяет определить, является ли справедливым отношение s ≤ t:
L5. (<x>^s) ≤ t ≡ t ≠ <> & x = t0 & s ≤ t’
Множество префиксов данной последовательности вполне упорядочено:
L6. s ≤ u & t ≤ u ⇒ s ≤ t ∨ t ≤ s
Если s является подпоследовательностью t (не обязательно начальной), мы говорим, что s находится в t; это можно определить так:
s в t = (∃u, v.t = u^s^v)
Это отношение также задает частичный порядок в том смысле, что оно удовлетворяет законам L1–L4, Кроме того, для него справедливо следующее утверждение:
L7. (<x>^s) в t = t ≡ t ≠ <> & ((t0 = х & s ≤ t) ∨ (<x>^s) в t’)
Будем говорить, что функция f из множества протоколов во множество протоколов монотонна, если она сохраняет отношение порядка ≤ т. е.
f(s) ≤ f(t) всякий раз, когда s≤t
Все дистрибутивные функции монотонны, например;
L8. s ≤ t ⇒ (s ↾ A) ≤ (t ↾ A)
Двуместная функция может быть монотонной по каждому из аргументов. Например, конкатенация монотонна по второму (но не по первому) аргументу:
L9. t ≤ u ⇒ (s^t) ≤ (s^u)
Функция, монотонная по всем аргументам, называется просто монотонной.
1.6.6. Длина
Длину протокола t будем обозначать #t, Например, #<x, y, x> = 3 Следующие законы определяют операцию #;
L1. #<> = 0
L2. #<x> = 1
L3. #(s^t) = (#s) + (#t)
Число вхождений в t символов из A вычисляется выражением # (t ↾ A).
L4. #(t ↾ (A ∪ B)) = #(t ↾ A) + #(t ↾ В) – #(t ↾ (A ∩ B))
L5. s ≤ t ⇒ #s ≤ #t
L6. #(tn) = n(#t)
Число вхождений символа х в протокол s определяется как
s ↓ x = #(s ↾ {x})
1.7. Реализация протоколов
Для машинного представления протоколов и реализации операций над ними нам потребуется язык высокого уровня с развитыми средствами работы со списками, К счастью, ЛИСП как нельзя лучше подходит для этой цели. Протоколы в нем очевидным образом представляются списками атомов, соответствующих его событиям:
<> = NIL
<мон>= cons("MOН, NIL)
<мон, шок> = "(МОН, ШОК)
что означает cons("МОН, cons("ШОК, NIL)).
Операции над протоколами легко реализовать как функции над списками. Так, например, голова и хвост непустого списка задаются примитивами car и cdr:
t0 = car(t)
t’ = cdr(t)
<x>^s = cons(x,s)
Конкатенация в общем виде реализуется с помощью известной функции append, которая задается рекурсивно:
s^t = append(s, t)
где append(s, t) = if s = NIL then t
else cons(car(s),append(cdr(s, t))
Корректность этого определения вытекает из законов
<>^t = t
s^t = <s0>^(s’^t) когда s ≠ <>.
Завершение ЛИСП–функции append гарантируется тем, что при каждом рекурсивном вызове список, подставляемый в качестве первого аргумента, короче, чем на предыдущем уровне рекурсии. Подобное рассуждение позволяет установить корректность и других, приведенных ниже, реализаций. Для реализации сужения представим конечное множество списком его элементов. Проверка (x ∈ B) выполняется вызовом функции
принадлежит(х, В) = if В = NIL then ложь
else if х = саr(В) then истина
else принадлежит(x, cdr(В))
после чего сужение (s ↾В) может быть реализовано функцией
сужение (s, B) = if s = NIL then NIL
else if принадлежит(car(s), B) then cons(car(s), сужение(cdr(s), В))
else сужение(cdr(s),В)
Проверка (s ≤ t) реализуется функцией, дающей ответ истина или ложь; реализация основана на законах 1.6.5 L1 и L5:
префикс_ли(s, t) = if s = NIL then истина
else if t = NIL then ложь
else car(s) = car(t) & префикс_ли (cdr(s), cdr(t))