Корректность задания семантики

👀 251 просмотр
📌 188 загрузок

Выбери формат для чтения

Конспект лекции по дисциплине «Корректность задания семантики», ppt

Загружаем конспект в формате ppt

Это займет всего пару минут! А пока ты можешь прочитать работу в формате Word 👇

Конспект лекции по дисциплине «Корректность задания семантики», Word формат

Корректность задания семантики Докажем, что множество ВП, характеризуемое системой уравнений (*), задано корректно, т.е. решение системы рекурсивных уравнений (*) существует. Введем оператор    P1 , P2 ,..., Pn  .   1j  P1j   1k ^ P1k   (Pl ), jN kN ... ,  jN nj  Pnj   nk ^ Pnk   (Pn )  kN Запись Ψ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, у) yY (б) Метрика между X, Y  M определяется как: d(X, Y) = max (sup d(x, Y), sup d(X, у)) xX yY Теорема 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. Для полученных в предыдущем упражнении систем рекурсивных уравнений вычислить минимальные фиксированные точки, являющиеся решениями этих систем.