Корректность задания семантики
Выбери формат для чтения
Загружаем конспект в формате ppt
Это займет всего пару минут! А пока ты можешь прочитать работу в формате Word 👇
Корректность задания семантики
Докажем, что множество ВП, характеризуемое системой уравнений (*),
задано корректно, т.е. решение системы рекурсивных уравнений (*)
существует.
Введем оператор
P1 , P2 ,..., Pn . 1j P1j 1k ^ P1k (Pl ),
jN
kN
... ,
jN
nj
Pnj nk ^ Pnk (Pn )
kN
Запись Ψi(Ø)↓l означает взятие l-ой проекции n-ки, получаемой в
результате i применений оператора Ψ к n-ке <Ø, Ø, ..., Ø>.
Поскольку решение системы рекурсивных уравнений ассоциируется с Р1,
то, очевидно, что последовательность Ø, Ψ(Ø)↓1, Ψ2(Ø)↓1, ....., Ψi(Ø)↓1, ...
ассоциируется с последовательностью аппроксимаций, сопоставляемых
исходной программе в языке L.
Пример 3. Пусть дана система уравнений, полученная ранее в примере 2:
Р1 = T^Р2 + T^Р3 + OUT2,1∘P4
P2 = IN1,2∙∘P5 + OUT2,1∘P6 + γ2,1
P3 = OUT1,2 ∘ P5 + OUT2,1 ∘ P7
Р4 = Т^P6 + Т^P7
Р5 = OUT2,1
P6 = IN1,2
р7 = OUT1,2.
Тогда
Ψ = λ<Р1, Р2, ... Р7>..
Зададим несколько первых аппроксимаций решения этой системы.
Ψ(Ø) = ;
Ψ2(Ø) = ;
Ψ3(Ø) = ;
Ψ4(Ø) = Ψ3(Ø) - фиксированная точка.
P = P1 = Ψ3(Ø)↓1 = T^( IN1,2 ∘ OUT2,1 + OUT2,1 ∘ IN1,2 + γ2,1 ) +
+ T^(OUT1,2 ∘ OUT2,1 + OUT2,1 ∘ OUT1,2 ) + OUT2,1 ∘ (T^IN1,2 + T^OUT1,2 )
ENCH (P) = T^γ2,1 + T^Ø ,
где H = {INi,j, OUTi,j | i = 1, 2, j = 1, 2}.
Данное решение в точности совпадает с полученным ранее результатом.
Для доказательства корректности задания априорной семантики
необходимо показать, что решение системы рекурсивных уравнений (*)
существует, т.е. оператор Ψ имеет наименьшую фиксированную точку
P1, P2, … ,Pn,, такую, что
ΨP1, P2, … ,Pn, = P1, P2, … ,Pn,.
Области, в которых мы будем искать решения систем рекурсивных
уравнений вида (*), есть
S =𝒫(CPath') × …. ×𝒫(CPath') ,
т.е. S является декартовым произведением областей 𝒫(CPath'), где CPath' подмножество множества CPath, содержащее конечные и бесконечные ВП
вида ср = g1 ∘ g2 ∘ ... ∘ gn, либо ср = g1 ∘ g2 ∘ ... ∘ gn ∘ h, либо ср = g1 ∘ g2 ∘ ... ∘ gn
∘ ... ,
g PREF = {A,В,T,IN,OUT, } и h {LOOP,Ø}.
Для ср CPath' будем обозначать через ср[n] префикс, состоящий из
первых n-элементов ср, если длина ср больше или равна n, или само ср в
противном случае. На этом множестве CPath' введем отношение частичного
порядка следующим образом: cp1 ⊑ ср2, если cp1 является префиксом ср2.
Прежде чем определять метрику на области S, приведем ряд определений
и известных результатов из области метрических пространств, используемых
нами в дальнейшем.
Определение 9. Метрика d на множестве CPath' определяется следующим
образом:
2 n , если cp1 [n 1] cp 2 [n 1] и cp1 [n] cp 2 [n]
d (cp1 , cp 2 )
0, в противном случае
Определение 10. Последовательность <хn>n точек метрического
пространства называется фундаментальной, если она удовлетворяет критерию
Каши, т.е. если ∀ε>o ∃N: ∀i,j>N
d(xi, xj) < ε.
Определение 11. Последовательность n точек метрического
пространства сходится к точке х, если ε > 0 ∃ N: i > N d(xi, х) < ε.
Определение 12. Метрическое пространство (M,d) называется полным,
если в нем сходится любая фундаментальная последовательность.
Лемма 6. Метрическое пространство (CPath', d), где d задается в
определении 9, является полным.
Определение 13. (Хаусдорфова мера) Пусть (M,d) - метрическое
пространство.
(а) Метрика между х M и Y M определяется следующим образом:
d(x, Y) = inf d(x, у)
yY
(б) Метрика между X, Y M определяется как:
d(X, Y) = max (sup d(x, Y), sup d(X, у))
xX
yY
Теорема 7.
Если (M, d) - полное метрическое пространство, то
пространство (𝒫(M), d) также является полным. Кроме того, любая
фундаментальная последовательность i в 𝒫(M) имеет предел
lim i = { х | x = lim i, xi X и i - фундаментальная
последовательность в M }.
Следствием этой теоремы является полнота метрического пространства
(𝒫(CPath'), d), где d - Хаусдорфова мера.
Определим теперь метрику на искомой области S.
Определение 14. Пусть s1, s2 S. Тогда:
(s1, s2) =
где
max {d(
)},
l
проекции s1, s2 на l-ый компонент множества S.
Лемма 8. Пространство (S, ) является полным метрическим
пространством, т.е. каждая фундаментальная последовательность k в S
сходится и
lim k = ,
2
n
1
где s k → s1, s k → s2 ,..., s k → sn и i,l:
𝒫(CPath'). ~
s k , si ) ≤ ε
Доказательство. Выберем ε > 0. Определим такое N, что d (lim
k
для всех i > N.
Поскольку k является фундаментальной последовательностью, то ∃N
такое, что i,j > N
(si, sj) <ε.
~
Докажем,
d (lim что
s k , siдля
) выбранного таким образом N утверждение
k
≤ ε справедливо для всех i > N.
Последовательности < >k для l = 1, 2, ..., n являются
фундаментальными последовательностями, ибо, в противном
случае, в силу определения меры
последовательность k
также не являлась бы фундаментальной последовательностью, что
противоречит условию. Для каждой фундаментальной
последовательности
<
>k , 1 ≤ l ≤ n, существует предел
l
lim s k
= sl в пространстве
d), а следовательно, ∃Nl,
k
lims(l𝒫, s(lCPath'),
d(
)
k
i
k
такое что i > Nl
.
max
l {N }. Отсюда, принимая во внимание
Возьмем теперь N =
l
определени
, следует, что i > N
~
d (lim s k , si )
k
max{d (limskl , sil )}
=
l
k
≤ ε , ч.т.д.
Лемма 9. Отображение метрического пространства M = (S, )
в себя является сжимающим отображением.
Доказательство. Пусть x' = < P1' , P2' , , Pn' > и x" = < P1' ' , P2' ' , , Pn' ' > аппроксимации множеств ВП, получаемые в результате применения оператора
к кортежу пустых множеств Ø = < Ø, ... , Ø > некоторое количество раз.
Возьмем для определенности, что x' = m(Ø) и x" = n (Ø) для некоторых m и р.
Требуется показать, что
( (x'), (x"))= ( (m (Ø)), (n (Ø))) ≤ k · ( m (Ø), p (Ø)).
Далее док-во см. в пособии.
Теорема 10 (теорема Банаха). Пусть (M, ) - полное
метрическое пространство и :M → M - сжимающее
отображение, т.е.
( (х'), (х")) ≤ k · (x', x"). Тогда существует x M, такое,
что справедливо:
(1) (х) = x
(x - фиксированная точка ),
(2)y M [ (у)= у y=x]
(x - единственная
фиксированная точка).
Из этой теоремы, учитывая полученные выше результаты,
непосредственно следует искомый результат.
Теорема 11. Оператор :S → S, где S = 𝒫(CPath') × ... × 𝒫(CPath'),
имеет минимальную фиксированную точку.
Таким образом, определенная выше семантика языка
распределенного программирования является корректной.
Упражнения
1. Пусть дана программа pr:
рr ≡ 1::( [b → c1; 2::( c3; [in3 → с4] ) □ out5 → с5] ) ||
3::( [out1 → c6]; in4 ) ||
4::( с7; c8; out3 ) ||
5::in1
Определить среду для подмножеств P1 = {in3, in1}, Р2 = {out5, c7, out3}, Р3 = {c1, c5, c6},
P4 ={in4, out1, c6}, P5 = {[in3 → с4], out5 → с5}.
2. Определить семантическое значение и построить его представление в виде системы
рекурсивных уравнений для следующих программ:
a) 1::[ in2 → c1 □ tt → out2] || 2::[ out1 → с2],
b) 1::*[ in2 → c1] || 2::[out1 → c2],
c) 1::*[tt → skip □ out2 → c1; out2] || 2::*[in1 → с2],
d) 1::*[b → out2; in2; c1] || 2::[in1 → с2; out1],
e) 1::*[out2 → c1 □ out3 → c2] || 2::*[in1 → c4] || 3::*[in1 → c5]
f) 3::*[out4 → in5; c3; out1] || 4::* [in3 → c4] || 5::*[b → out3; c5],
g) 2::[out3 → c2] || 3::*[ in2 → c3 □ out4 → c4] || 4::*[b1 → in3 □ b2 → c5].
3. Для полученных в предыдущем упражнении систем рекурсивных уравнений вычислить
минимальные фиксированные точки, являющиеся решениями этих систем.
