Wnioskowanie o działaniach z wykorzystaniem semantyki Dijkstry dla

j_{}ezyków programowania: podejście imperatywne

Ewa Madalińska

na podstawie pracy:

W. Łukaszewicz, E. Madalińska-Bugaj. Reasoning about Action and Change Using Dijkstra’s Semantics for Programming Languages: Preliminary Report. Proceedings of 14th International Joint Conference on Artificial Intelligence, 1995, p. 1950-1955.

Wnioskowanie o scenariuszach

Definicja 1 Scenariuszem nazywamy wyrażenie

SC = ⟨α_{0}⟩ A_{1}; ⟨α_{1}⟩ A_{2}; …; ⟨α_{n−1}⟩ A_{n} ⟨α_{n}⟩ (1)

gdzie A_{1}, …, A_{n} s _{}a symbolami akcji, a α_{0}, …, α_{n} s _{}a obserwacjami.

Intuicyjna interpretacja scenariusza jest nast_{}epuj _{}aca: α_{0} zachodzi w stanie pocz _{}atkowym, nast_{}epnie zostaj _{}a wykonane sekwencyjnie akcje A_{1}, …, A_{n} oraz dla każdego 0 < i ≤ n, po wykonaniu akcji A_{i} zaobserwowano, że zachodzi α_{i}.

Opis działania:

{warunek wst_{}epny_{1}} Nazwa {efekt_{1}} ⋮ {warunek wst_{}epny_{n}} Nazwa {efekt_{n}} Zadanie wnioskowania o scenariuszach: “Dla danego scenariusza (1), zdania γ i liczby całkowitej k określ, czy γ zachodzi po wykonaniu akcji A_{1}, …, A_{k}”.

Realizacja procesu wnioskowania o scenariuszach wymaga:

1. zdefiniowania j_{}ezyka, który umożliwiałby formalny opis zarówno dopuszczalnych działań, jak i stanów systemu.

2. skonstruowania mechanizmu wnioskowania o efektach działań.

3. zapewnienia pełności i poprawności skonstruowanego mechanizmu.

Przyjmujemy:

1. Jako baz_{}e logiczn _{}a – logik_{}e zdań. Stałe zdaniowe wyst_{}epuj _{}ace w j_{}ezyku logiki b_{}edziemy nazywać fluentami.

2. J_{}ezyk opisu działań – j_{}ezyk programowania Dijkstry.

3. Semantyk_{}e działań b_{}edziemy wyrażać za pomoc _{}a transformatorów formuł Dijkstry dla instrukcji reprezentuj _{}acej działanie.

Przykład 1 (Yale Shooting Scenario)

Y SS = ⟨a ∧ ¬l⟩load; wait; shoot⟨T ⟩,

gdzie:

1. Fluenty: a – oznacza, że indyk żyje; l – strzelba jest naładowana.

2. Działania: load: strzelba zostaje naładowana; wait: nic si_{}e nie dzieje; shoot: jeśli strzelba jest naładowana, to indyk zostaje zabity, w pp. brak działania.

J_{}ezyk definiowania działań i semantyka Dijkstry

Założenia: tylko jeden typ zmiennych – zmienne logiczne (Boolean).

V – zbiór zmiennych logicznych.

Stan nad zbiorem V – funkcja σ określona na zbiorze V o wartościach w zbiorze {0, 1}

σ : V → {0, 1}

J_{}ezyk asercji L(V) nad zbiorem zmiennych logicznych V – zbiór formuł skonstruowanych w zwykły sposób z elementów zbioru V, spójników logicznych (¬, ⇒, ∧, ∨, ≡) i stałych logicznych T (prawda) i F (fałsz). β – formuła, α_{1}, …, α_{n} – wyrażenia boolowskie, x_{1}, …, x_{n} – zmienne

β[x_{1} ← α_{1}, …, x_{n} ← α_{n}] oznacza formuł_{}e otrzyman _{}a z β w wyniku jednoczesnego zast _{}apienia wszystkich wolnych wyst _{}apień x_{1}, …, x_{n} odpowiednio przez α_{1}, …, α_{n}.

Kwantyfikatory (∀, ∃)^{∗}:

∀x.α =^{def} α[x ← T] ∧ α[x ← F],

∃x.α =^{def} α[x ← T] ∨ α[x ← F].

∗Zauważmy, że kwantyfikatory mog _{}a być zastosowane jedynie do zmiennych logicznych.

Wartość formuły α ∈ L(V) w stanie σ, ∥ α ∥_{σ} jest to element zbioru {0, 1} wyznaczony według reguł klasycznej logiki zdań.

Stan σ spełnia formuł_{}e α wtw ∥ α ∥_{σ}= 1 . Jeżeli σ spełnia α, to σ nazywamy modelem α. Mówi _{}ac, że σ spełnia α, b_{}edziemy zawsze zakładać, że σ określa interpretacj_{}e dla wszystkich zmiennych boolowskich wyst_{}epuj _{}acych w α.

Transformatory formuł:

Rozważamy 3 transformatory formuł: najsłabszy warunek wst_{}epny – wp, najsłabszy liberalny warunek wst_{}epny – wlp oraz najmocniejszy warunek końcowy – sp.

Dla dowolnej instrukcji S i formuły α:

• wp(S, α) jest formuł _{}a, której modelami s _{}a dokładnie wszystkie stany takie, że wykonanie S rozpocz_{}ete w którymkolwiek z nich zakończy si_{}e w stanie spełniaj _{}acym warunek α.

• wlp(S, α) jest formuł _{}a, której modelami s _{}a dokładnie wszystkie stany takie, że jeśli wykonanie S rozpocznie si_{}e w którymkolwiek z nich i zakończy, to stan końcowy spełnia warunek α.

• sp(S, α) jest formuł _{}a, której modelami s _{}a dokładnie te stany, które s _{}a osi _{}agalne w wyniku wykonania S, jeśli S si_{}e skończy, gdy S rozpocznie si_{}e w stanie spełniaj _{}acym warunek α.

{α}S{β}
{wlp(β)}S{β} i α ⇒ wlp(β)
{wp(β}S{β} i α ⇒ wp(β)
{α}S{sp(α)} i sp(β) ⇒ α

Semantyka instrukcji

Lista instrukcji:

skip, przypisanie, sekwencyjne złożenie, alternatywa (niedeterministyczna).

1. Instrukcja skip. Jest to instrukcja “pusta”, tzn. jej wykonanie nie zmienia stanu obliczeń.

wlp(skip, α) = sp(skip, α) = α.

2. Instrukcja przypisania. Jest postaci x := e, gdzie x jest zmienn _{}a boolowsk _{}a, a e jest wyrażeniem boolowskim. W wyniku wykonania instrukcji wartość x zostaje zast _{}apiona przez wartość wyrażenia e.

wlp(x := e, α) = α[x ← e]. sp(x := e, α) =

∃y.((x ≡ e[x ← y]) ∧ α[x ← y]),  (2)

gdzie y jest now _{}a zmienn _{}a.

Jeśli zmienna x nie wyst_{}epuje w wyrażeniu e, równanie (2) można uprościć do postaci

sp(x := e, α) = (x ≡ e) ∧ ∃x.α

a bior _{}ac pod uwag_{}e, że zmienne s _{}a tylko typu boolowskiego, jest to równoważne

sp(x := e, α) =

(x ≡ e) ∧ (α[x ← T] ∨ α[x ← F]). (3)

W przykładach cz_{}esto b_{}edziemy mieć do czynienia z przypisaniami x := e, gdzie e jest T lub F.

Wtedy (3) można zast _{}apić przez

sp(x := T, α) = x ∧ (α[x ← T] ∨ α[x ← F])
sp(x := F, α) = ¬x ∧ (α[x ← T] ∨ α[x ← F])

3. Instrukcja sekwencyjnego złożenia. Jest ona postaci S_{1}; S_{2}, gdzie S_{1} i S_{2} s _{}a dowolnymi instrukcjami. Wykonanie jej polega na wykonaniu najpierw S_{1}, a nast_{}epnie S_{2}.

wlp(S_{1}; S_{2}, α) = wlp(S_{1}, wlp(S_{2}, α));

sp(S_{1}; S_{2}, α) = sp(S_{2}, sp(S_{1}, α)).

4. Instrukcja alternatywy. Jest ona postaci

if B_{1} → S_{1} []⋯ [] B_{n} → S_{n} fi  (4)

gdzie B_{1}, …, B_{n} s _{}a wyrażeniami boolowskimi, a S_{1}, …, S_{n} dowolnymi instrukcjami.

B_{1}, …, B_{n} nazywaj _{}a si_{}e dozorami, a wyrażenia B_{i} → S_{i} instrukcjami dozorowanymi.

Instrukcj_{}e alternatywy (4) b_{}edziemy oznaczać if□_{i=1}^{n} B_{i} → S_{i} fi lub w skrócie jako IF.

Wykonanie instrukcji przebiega nast_{}epuj _{}aco: jeśli wszystkie dozory s _{}a fałszywe, wykonanie si_{}e kończy, w przeciwnym przypadku spośród tych instrukcji dozorowanych B_{i} → S_{i} , dla których B_{i} jest prawdziwe zostaje losowo wybrana jedna i S_{i} zostaje wykonane.

wlp(IF, α) = ⋀_{i=1}^{n} (B_{i} ⇒ wlp(S_{i}, α))
∧((⋀_{i=1}^{n} ¬B_{i}) ⇒ α)
sp(IF, α) = (⋁_{i=1}^{n} sp(S_{i}, B_{i} ∧ α))
∨((⋀_{i=1}^{n} ¬B_{i}) ∧ α).

Uwaga 1 W wersji oryginalnej j_{}ezyka Dijkstry przypadek, gdy wszystkie dozory s _{}a fałszywe sprowadza si_{}e do instrukcji abort, której nie wł _{}aczyliśmy do naszego repertuaru. Podana tutaj wersja IF jest specjalnym przypadkiem IF Dijkstry, tj.: if B_{1} → S_{1}[]⋯ []B_{n} → S_{n}[]¬B_{1} ∧ … ∧ ¬B_{n} → skip fi.

Uwaga 2 Zauważmy, że jeśli wi_{}ecej niż jeden dozór jest prawdziwy, wybór instrukcji dozorowanej jest niedeterministyczny.

Klasa obliczeń reprezentowana przez scenariusz SC = ⟨α_{0}⟩ A_{1}; ⟨α_{1}⟩ A_{2}; …; ⟨α_{n−1}⟩ A_{n} ⟨α_{n}⟩ jest to wyrażenie oznaczone jako

[A_{1}; …; A_{n}](α_{0}, …, α_{n}). (5)

Stany scenariusza Niech ST^{SC}(i), 0 ≤ i ≤ n, b_{}edzie zbiorem wszystkich stanów spełniaj _{}acych nast_{}epuj _{}acy warunek: dla każdego σ ∈ ST^{SC}(i), istnieje obliczenie c ∈ [A_{1}; …; A_{n}](α_{0}, …, α_{n}) takie, że σ jest osi _{}agany przez c po wykonaniu A_{1}; …; A_{i}. Elementy ST^{SC}(i) b_{}edziemy nazywać i-stanami SC.

0-stany – stany pocz _{}atkowe n-stany – stany końcowe.

Opis i-stanów

Niech W LP_{i}^{SC} i SP_{i}^{SC} b_{}ed _{}a formułami zdefiniowanymi indukcyjnie w sposób nast_{}epuj _{}acy:

SP_{0}^{SC} = α_{0}; W LP_{n}^{SC} = ¬α_{n} i dla 0 < k ≤ n SP_{k}^{SC} = α_{k} ∧ sp(A_{k}, SP_{k−1}^{SC}); W LP_{n−k}^{SC} = ¬α_{n−k} ∨ wlp(A_{n−k+1} , W LP_{n−k+1}^{SC} ).

Twierdzenie 2 Niech SC = ⟨α_{0}⟩ A_{1}; ⟨α_{1}⟩ A_{2}; …; ⟨α_{n−1}⟩ A_{n} ⟨α_{n}⟩. Zbiór stanów pocz _{}atkowych scenariusza SC opisuje formuła

D_{0}^{SC} = ¬W LP_{0}^{SC} ∧ α_{0}.  (6)

Formuł_{}e D_{0}^{SC} b_{}edziemy nazywać opisem stanu pocz _{}atkowego scenariusza SC.

Twierdzenie 3 Niech SC = ⟨α_{0}⟩ A_{1}; ⟨α_{1}⟩ A_{2}; …; ⟨α_{n−1}⟩ A_{n} ⟨α_{n}⟩. Zbiór stanów końcowych scenariusza SC opisuje formuła

D_{n}^{SC} = SP_{n}^{SC}.  (7)

Twierdzenie 4 Zbiór i−stanów scenariusza SC opisuje formuła

D_{i}^{SC} = SP_{i}^{SC} ∧ ¬W LP_{i}^{SC}  (8)

Przykłady

1. Fluenty: a – indyk żyje; l – strzelba jest naładowana

2. Działania: load: l := T;

• wlp(load, α) = α[l ← T];

• sp(load, α) = l ∧ (α[l ← T] ∨ α[l ← F]);

shoot: if l → a := F; l := F [] ¬l → skip fi;

• wlp(shoot, α) = (l ⇒ α[a ← F, l ← F]) ∧ (¬l ⇒ α);

• sp(shoot, α) = (¬a ∧ ¬l ∧ α[a←T, l←T]) ∨ (¬a ∧ ¬l ∧ α[a←F, l←T]) ∨ (¬l ∧ α); wait: skip;

• wlp(wait, α) = sp(wait, α) = α;

spin: if T → l := T [] T → l := F fi;

• wlp(spin, α) = α[l ← T] ∧ α[l ← F];

• sp(spin, α) = α[l ← T] ∨ α[l ← F]; Przykład 2 (Yale Shooting Scenario)

Y SS = ⟨a ∧ ¬l⟩load; wait; shoot⟨T ⟩.

Oczekiwan _{}a konkluzj _{}a jest, że po wykonaniu działań load; wait; shoot indyk nie żyje i strzelba jest nienaładowana. Obliczamy D_{3}^{Y SS}.

\begin{aligned}D_{3}^{Y SS} & = & sp(load; wait; shoot, a ∧ ¬l) \\ & = & ¬a ∧ ¬l. \end{aligned}

Ponieważ D_{3}^{Y SS} ⊢ ¬a∧¬l, wi_{}ec w stanie końcowym indyk jest nieżywy i strzelba rozładowana.

Przykład 3 (Russian Turkey Scenario) (RTS) jest przykładem problemu predykcji, w którym wyst_{}epuj _{}a działania niedeterministycze.

RT S = ⟨a ∧ ¬l⟩ load; spin; shoot ⟨T ⟩.

Oczekiwan _{}a konkluzj _{}a jest, że nie możemy stwierdzić czy w stanie końcowym indyk żyje czy nie.

Obliczamy D_{3}^{RT S}.

\begin{aligned}D_{3}^{RT S} & = & sp(load; spin; shoot, a ∧ ¬l) \\ & = & ¬l. \end{aligned}

Ponieważ zarówno D_{3}^{RT S} ⊬ a jak i D_{3}^{RT S} ⊬ ¬a, nie można wywnioskować czy w stanie końcowym indyk żyje, czy nie.