Co wynika ze współczesnej logiki formalnej?
2.3. L OGIKA MODALNA I JEJ ROZSZERZENIA
2.3.0.UWAGI WSTĘPNE
Logika modalna uprawiana była już przez Arystotelesa jako sylogistyka zdań modalnych (porównaj 2.0.1). Współczesną postacią logiki modalnej jest modalny rachunek zdań. Cechą charakterystyczną modalnych rachunków zdań jest występowanie w nich: funktora możliwości, oznaczanego <> oraz funktora konieczności, oznaczanego przez □. Twórcą pierwszych systemów modalnego rachunku zdań (nazwanych później S1 i S2) jest C. I. Lewis. Następnie powstało jeszcze kilka innych systemów – Lewisa (zwanych odpowiednio S3, S4, S5). Intencją Lewisa było stworzenie takiej logiki, która lepiej niż implikacja materialna w klasycznym rachunku zdań oddawałaby implikację występującą w języku naturalnym. Lewis nie uświadamiał sobie jeszcze w pełni różnicy między wynikaniem a implikacją ścisłą, współcześnie jednak logiki Lewisa interpretuje się powszechnie jako logiki zdań modalnych, na których gruncie właśnie implikację ścisłą zdefiniować można następująco:
2.3.0.10 𝑝 → 𝑞 =Df ¬<>(𝑝 ∧ ¬𝑞).
Dalsze rozszerzenia logiki modalnej prowadzą między innymi do logik temporalnych, w szczególności logik temporalnych dotyczących czasu dyskretnego (nie ciągłego). Wyobraźmy sobie graf stanów dwu zmiennych zdaniowych, którego
Rysunek 2.3.0.00. Graf stanów zmiennych zdaniowych p oraz q.
wierzchołki służą do przechowywania stanów prawda (lub true) i fałsz (lub false). Stany grafu znajdują się w węzłach (patrz rys. 2.3.0.00):
2.3.0.20 s0(p) = ┬, s0(q) = ┴, s1(p) = ┬, s1(q) = ┬, s2(p) = ┴, s2(q) = ┬, s3(p) = ┴, s3(q) = ┴.
Funkcjonalność przejście (transition) ○ - pomiędzy węzłami grafu (patrz rys. 2.3.0.00) opisują zbiory dopuszczalnych przejść:
2.3.0.30 ○(s0) ∈ {s1, s2}, ○(s1) ∈ {s1, s2, s3}, ○(s2) ∈ {s1}, ○(s3) ∈ {s2, s3}.
2.3.0.40 Wyjaśnienie. Funktor możliwości <>p = ┬ - w przypadku grafu stanów możemy interpretować, iż wśród stanów węzłów grafu, wystąpi co najmniej jeden raz wartość p = ┬;
natomiast ¬<>p = ┬ – możemy interpretować, iż wśród stanów węzłów grafu, nie wystąpi co najmniej jeden raz wartość p = ┴. Natomiast funktor konieczności □p = ┬ - w przypadku grafu stanów możemy interpretować, iż we węzłach grafu mamy stan p = ┬; natomiast ¬□p = ┬ - możemy interpretować, iż żadnym węźle grafu stanów, niema stanu p = ┬.
Piśmiennictwo: Ben-Ari M. B.2.1., Chellas B. C.1.1. Harel D. H.1.1., Tiuryn J. T.4.1.
2.3.1.SYSTEM MODALNY S5
System S5 należy do najszerzej znanych i najprostszych systemów modalnego rachunku zdań.
Występujące w nim funktory zdaniotwórcze możliwości <> i konieczności □, odróżniające go od klasycznego rachunku zdań, można rozumieć intuicyjnie odwołując się do Leibnizowskiej koncepcji światów możliwych: zdanie konieczne jest prawdziwe we wszystkich możliwych światach, zdanie możliwe jest prawdziwe w niektórych możliwych światach. Funktory możliwości <> i konieczności □ są przy tym wzajemnie definiowalne w następujący sposób:
2.3.1.11 <>𝑋 ↔ ¬□¬𝑋;
2.3.1.12 𝑋 ↔ ¬<>¬𝑋;
gdzie 𝑋 jest formułą zdaniową.
Piśmiennictwo: Ben-Ari M. B.2.1., Chellas B. C.1.1. Harel D. H.1.1., Tiuryn J. T.4.1.
2.3.2.JĘZYK SYSTEMU MODALNEGO S5
2.3.2.10 Wyjaśnienie. Słownik języka logiki modalnej systemu S5 jest językiem klasycznego dwuwartościowego rachunku zdań rozszerzonym o funktory zdaniotwórcze możliwość <> oraz konieczność □.
2.3.2.20 Wyjaśnienie. Na język składają się następujące elementy:
1. zmienne zdaniowe w ilości nieograniczonej, oznaczane przez p, q, r, s...
2. stałe logiczne stanowią funktory zdaniotwórcze: zero-argumentowe – stała verum ┴ oraz stała falsum ┬ ; spójniki jednoargumentowe: negacji ¬ , możliwości <> i konieczności □;
spójniki dwuargumentowe koniunkcji ∧, alternatywy ∨, implikacji → oraz równoważności ↔.
2.3.2.30 Wyjaśnienie. Do zbioru formuł zdaniowych należą natomiast:
1. wszystkie zmienne zdaniowe, 2. wyrażenia ┬ i ┴,
3. wyrażenia ¬𝑋, □𝑋, <>𝑋 , gdzie 𝑋 jest formułą zdaniową,
4. wyrażenia 𝑋 ∧ 𝑌, 𝑋 ∨ 𝑌, 𝑋 → 𝑌, 𝑋 ↔ 𝑌, gdzie X i Y są formułami zdaniowymi
5. wyrażenia powstające przez zastosowanie reguł 3 i 4 w skończonej liczbie kroków.
Piśmiennictwo: Ben-Ari M. B.2.1., Chellas B. C.1.1. Harel D. H.1.1., Tiuryn J. T.4.1.
2.3.3.AKSJOMATYKA SYSTEMU MODALNEGO S5
Na gruncie systemu S5 przyjmuje się następujące aksjomaty i definicje (uzupełniające aksjomatykę klasycznego dwuwartościowego rachunku zdań):
2.3.3.10. Aksjomat □𝑋 → 𝑋.
2.3.3.20. Aksjomat <>𝑋 → □<>𝑋.
2.3.3.30. Aksjomat □(𝑋 → 𝑌) → (𝑋 → 𝑌).
2.3.3.40. Aksjomat możliwości <>𝑋 ↔ ¬□¬𝑋.
Na gruncie systemu S5 przyjmuje się następujące dwie reguły dowodzenia:
2.3.3.50. Reguła wnioskowania 1 𝑋
□𝑋 2.3.3.60. Reguła wnioskowania 2 𝑋→𝑌,𝑋
𝑌
Piśmiennictwo: Ben-Ari M. B.2.1., Chellas B. C.1.1. Harel D. H.1.1., Tiuryn J. T.4.1.
2.3.4.WYBRANE PRAWA SYSTEMU MODALNEGO S5
Poniżej podajemy przykłady praw systemu S5, rozszerzające zestaw praw klasycznego dwu-wartościowego rachunku zdań. A mianowicie:
2.3.4.11. Prawo. Jeśli X jest konieczne, to X zachodzi rzeczywiście: □𝑋 → 𝑋.
2.3.4.12. Prawo. Jeśli X jest możliwe, to jest konieczne, że X jest możliwe: <>𝑋 → □<>𝑋.
2.3.4.21. Prawo rozdzielności konieczności względem implikacji mówi, że jeśli konieczna jest zarazem implikacja i jej poprzednik, konieczny jest też jej następnik: □(𝑋 → 𝑌) → (□𝑋 → □𝑌).
2.3.4.22. Prawo rozdzielności konieczności względem koniunkcji: □(𝑋 ∧ 𝑌) → (□𝑋 ∧ □𝑌).
2.3.4.31. Prawo niniejsza mówi, że co jest prawdziwe, jest zarazem możliwe: 𝑋 → <>𝑋.
2.3.4.32. Prawo niniejsza mówi, że co jest konieczne, jest też możliwe: 𝑋 →<>𝑋.
2.3.4.33. Prawo. Jeśli zachodzi X, to jest konieczne, że X jest możliwe: 𝑋 → □<>𝑋.
2.3.4.41. Prawo. Co może być konieczne, zachodzi rzeczywiście: <>□𝑋 → 𝑋.
2.3.4.42. Prawo. Jeśli coś jest konieczne, to jest konieczne, że jest to konieczne: □𝑋 → □□𝑋.
2.3.4.43. Prawo. Jeśli jest możliwe, że coś jest możliwe, to jest to możliwe: <><>𝑋 →<>𝑋.
Piśmiennictwo: Ben-Ari M. B.2.1., Chellas B. C.1.1. Harel D. H.1.1., Tiuryn J. T.5.1.
2.3.5.LOGIKI TEMPORALNE JAKO ROZWINIĘCIE IDEI MODALNYCH
2.3.5.10. Wyjaśnienie. Dopiero w drugiej połowie XX wieku, pojawiły się rozwiązania pozwalające na wykorzystaniu modalności dla rozszerzenia logiki zadań o funktory czasu i stworzenie narzędzi do dowodzenia twierdzeń, nazwanych logiką temporalną. Obecnie pojęciem
„logika temporalna” określanych jest wiele różnych logik, jedynym czynnikiem łączącym te różnorodne logiki, jest zależność od czasu.
2.3.5.20. Wyjaśnienie. Wzmiankowane logiki różnią się pomiędzy sobą, między innymi, przyjętymi definicjami funktorów czasu. Punktem wyjścia do logiki temporalnej, a ściślej mówiąc do temporalnego rachunku zdań, podobnie jak do trójwartościowego rachunku zdań Łukasiewicza, są wyrażenia modalne i ich interpretacja ze względu na czas. Funktory modalne można interpretować względem czasu na trzy sposoby, co prowadzi do trzech różnych logik czasu:
1. Logiki czasu gramatycznego;
2. Logiki czasu liniowego fizycznego i technicznego;
3. Logiki czasu relatywnego i rozgałęzionego.
2.3.5.30. Wyjaśnienie.. Logiki czasu gramatycznego - określają jedynie czasy, jako przeszłe, teraźniejsze oraz przyszłe, natomiast nie dają możliwości precyzyjniejszego określenia danej chwili czasu.
2.3.5.40. Wyjaśnienie. Logiki czasu liniowego - dotyczą zarówno czasu ciągłego, jak i dyskretnego. W zasadzie czas liniowy nie ma początku ani końca (podobnie jak prosta w geometrii euklidesowej), natomiast zdarzenia są uporządkowane w czasie, czyli jeśli mamy parę zdarzeń o określonym czasie rozpoczęcia – to potrafimy powiedzieć, które z nich rozpoczęło się wcześniej, a które rozpoczęło się później (chyba, że rozpoczęło się jednocześnie). Z takim czasem mamy do czynienia w wielu eksperymentach fizycznych i w wielu urządzeniach technicznych, jak również w stosunkowo prostych (precyzyjnie mówiąc – jednowątkowych) programach komputerowych.
2.3.5.50. Wyjaśnienie. Logika czasu relatywnego i rozgałęzionego – dotyczy zdarzeń fizyki relatywistycznej, jak również rozproszonych (w tym również wieloprocesorowych) systemów informatycznych, a wersja rozgałęziania czasu dotyczy złożonych – wielowątkowych programów komputerowych, w szczególności wykonywanych na wieloprocesorowych komputerach lub w sieciach.
Ze względu na tematykę niniejszej książki, interesować nas będzie jedynie czas dyskretny, w wersji liniowej.
Piśmiennictwo: Ben-Ari M. B.2.1., Kazanecka A. K.6.1., Pnueli A. P.3.1., Prior A. P.4.1.
2.3.6.LOGIKA CZASU LINEARNEGO
2.3.6.10. Wyjaśnienie. Logika czasów gramatycznych wywodzi się z logiki modalnej. Jej twórcą był w 1947 roku – brytyjski logik Arthur N. Prior – wprowadzając cztery funktory zależności czasowych:
2.3.6.11. Funktor H p - było w przeszłości zawsze tak, że p - w skrócie: „dotąd zawsze”.
2.3.6.12. Funktor P p – było w przeszłości kiedyś tak, że p - w skrócie: „nastąpiło”.
2.3.6.13. Funktor G p - będzie w przyszłości zawsze tak, że p - w skrócie: „odtąd zawsze”.
2.3.6.14. Funktor F p - będzie w przyszłości kiedyś tak, że p - w skrócie: „nastąpi”.
Rachunek zdań rozszerzony przez Priora, oznaczono symbolem PL, jest to system czasu linearnego – dyskretnego, w którym relacja poprzedzania "<" jest przechodnia, obustronnie liniowa, bez momentu początkowego i końcowego (tak jak prosta w geometrii euklidesowej).
Funktory G i F oraz H i P są wzajemnie zależne. Zależności te mają odpowiednio postać:
2.3.6.21. G p ≡ [¬F (¬p)].
2.3.6.22. H p ≡ [¬P (¬p)].
2.3.6.30. Wyjaśnienie. Rachunek ten z pewnymi rozszerzeniami pozwala na prowadzenie szeregu formalnych rozważań dotyczących gramatycznych zależności czasowych, np. w językach naturalnych. Natomiast z punktu widzenia nauk ścisłych, w tym informatyki – jest mało przydatny.
2.3.6.40. Wyjaśnienie. W odniesieniu do czasu używanego przez fizykę newtonowską i technikę – potrzebne są dodatkowe funkcjonalności:
• Liniowość czasu, który może być dyskretny lub ciągły;
• Warunkowe spełnianie zdania - p, w zależności od prawdziwości albo fałszywości drugiego ze zdań - q.
W tym celu - Kamp w 1968 roku wprowadziła dwa binarne operatory S - “since” czyli “od tego momentu” oraz U “until” czyli “aż do momentu”. Oba wzmiankowane operatory są definiowane, jak niżej:
2.3.6.41 Funktor S(p, q) - “p ma wartość prawda, tak długo jak q ma wartość prawda”.
2.3.6.42 Funktor U(p, q) - “p będzie miało wartość prawda, gdy q przyjmie wartość prawda”.
2.3.6.50. Wyjaśnienie. Dodatkowo wprowadzono operator ○ następstwa czasu („the next time”
operator ○), który w przypadku czasu dyskretnego mówi o następnej jednostce (chronie) czasu.
Dla czasu dyskretnego - operator ○ daje się wyrazić z pomocą operatora U.
Piśmiennictwo: Ben-Ari M. B.2.1., Kazanecka A. K.6.1., Pnueli A. P.3.1., Prior A. P.4.1., Trzęsicki K. T.3.1.
2.3.7.UWAGI O TEMPORALNOŚCI W INFORMATYCE
2.3.7.10. Wyjaśnienie. Poprawność działania systemu informatycznego zależy od poprawności programu i od poprawnej konstrukcji urządzeń informatycznych składających się na ten system.
Do opisu oraz analizy działania systemów informatycznych stosowane są metody logiczne, w szczególności metody logiki temporalnej. We współczesnej informatyce logiki temporalne mają dwa rodzaje zastosowań:
1. W tzw. układach sekwencyjnych, na razie ograniczymy się do najprostszego przypadku układu sekwencyjnego dwustanowego (tzw. przerzutnika, który przyjmuje jeden z dwóch możliwych stanów „set” oraz „unset”), którego działanie zależy od czasu dyskretnego (synchronicznego lub asynchronicznego) reprezentowanego przez impulsy zegarowe (przypadek synchroniczny) lub zdarzenia (przypadek asynchroniczny). Opisane w 2.6.2, operatory binarne S, U oraz O – są przydatne do opisania działania układów sekwencyjnych.
Obszernej o układach sekwencyjnych będzie mowa w części 4 (patrz podrozdział 4.2.2.).
2. W analizie poprawności i niezawodności działania procesów tworzonych przez system programów komputerowych. Temu przypadkowi przyjrzymy się obecnie bliżej.
2.3.7.20. Wyjaśnienie. W ogólnej metodologii nauk termin „weryfikacja” lub „walidacja” oznacza stwierdzenie poprawności. Termin „falsyfikacja” jest używany w znaczeniu: wykrycia błędu. W informatyce termin „weryfikacja” jest używany odnośnie zgodności projektu z wymaganiami, zaś
„walidacja” odnosi do procesu określenia, czy program lub system programów - działa poprawnie czyli jest lub może być zwalidowany, czyli zgodnie z podaną specyfikacją; czy też działa błędnie, czyli niezgodnie ze specyfikacją, a tym samym nie może być zwalidowany.
Oczywiście, że przy założeniu braku sprzeczności w specyfikacji danego programu lub systemu programów.
2.3.7.30. Wyjaśnienie. Dość powszechnie uważa się, że poprawność działania programu można zapewnić używając techniki testowania, na zgodność ze specyfikacją oprogramowania.
Rzeczywistość wygląda jednak inaczej. Testowanie umożliwia jedynie stwierdzenie, czy uwzględnione w opracowaniu testu kombinacje występujących sytuacji, dają poprawne albo błędne działanie testowanego programu. Innymi słowy, jeśli jakaś kombinacja danych
wejściowych – przy zadanym stanie wewnętrznym programu, nie została sprawdzona w przeprowadzonym teście, to nic nie wiemy o tym, jak program zachowa się w przypadku wystąpienia takiej kombinacji danych. Testowanie dotyczy jedynie tych kombinacji danych oraz stanów, które zostały objęte zakresem testu. Jak z tego widać, na ogół technika testowania nie jest wystarczająca, aby stwierdzić poprawność działania, złożonych systemów programów z procesami współbieżnymi sterowanymi zdarzeniami zewnętrznymi i wewnętrznymi stanami tegoż systemu.
2.3.7.40. Wyjaśnienie. Znacznie doskonalszym podejściem od testowania dla zapewnienia poprawnego działania, jest dowiedzenie poprawności działania programu lub systemu programów, czyli walidacja. Posługując się terminologią logiki formalnej, dowiedzenie poprawności oznacza, że dla każdego możliwego zdarzenia: reaktywne - działanie systemu na to zdarzenie, jest tautologią. Realizację takiego zadania można powierzyć narzędziom oferowanym przez logikę temporalną. Operatory temporalne okazały się użyteczne do opisu działania systemów informatycznych. Struktura stanów (sekwencja lub drzewo) i zdarzeń zewnętrznych, są kluczowymi pojęciami, dzięki którym logika temporalna nadaje się zarówno do opisywania specyfikacji systemu informatycznego, jak i sprawdzania poprawności działania systemu informatycznego opracowanego na podstawie tej specyfikacji, czyli sprawdzenie czy niema miejsca falsyfikacja systemu.
2.3.7.50. Wyjaśnienie. Język logiki temporalnej adaptowany przez izraelskiego informatyka Amira Pnueli, dla potrzeb systemów informatycznych, spełnia trzy ważne warunki:
•
Zdolność opisania wszystkich rodzajów specyfikacji niezależnie od języka programowania użytego w implementacji (ekspresywność);•
Sprawdzenie czy każdy przypadek działania implementowanego systemu - spełnia reguły określone w specyfikacji czyli jest tautologią (złożoność);• Dzięki podobieństwu do języka naturalnego jest łatwy do nauczenia się (pragmatyka).
Szczegółowe wyłożenie wariantu logiki temporalne Pnueli – wykracza poza ramy niniejszej książki. Język logiki temporalnej może być zastosowany do specyfikacji szerokiego spektrum systemów informatycznych. W wypadku systemów reaktywnych, logika temporalna jest bardziej użyteczna niż logika Floyd-Hoare’a, która jest właściwym narzędziem dla programów sekwencyjnych, czyli typu „wejście-wyjście”. Język logiki temporalnej tworzy ogólne lingwistyczne ramy dedukcyjne dla systemu stanów w taki sam sposób, jak logika formalna- dla systemów matematycznych.
Piśmiennictwo: Ben-Ari M. B.2.1., Kazanecka A. K.6.1., Pnueli A. P.3.1., Prior A. P.4.1., Trzęsicki K. T.3.1.