Dynamic logic

Co z logiką dynamiczną? Słyszałem, że teraz nie logika algorytmiczna lecz logika dynamiczna się liczy.

1. Autorzy książki Dynamic Logic uważają, że logika algorytmiczna jest logiką dynamiczną.

2. Vaughan Pratt, wynalazca logiki dynamicznej(1976), był zaskoczony gdy studenci pokazali mu prace z logiki algorytmicznej datujące się parę lat wcześniej. Podobno powiedział, że nie zapoczątkowałby logiki dynamicznej gdyby wcześniej znał logikę algorytmiczną. Napewno od 1980 roku nie publikuje prac dotyczących logiki dynamicznej.

3. Logika dynamiczna kładzie nacisk na niedeterminizm.

a) Oprócz zwykłych instrukcji przypisania postaci {x:=e}, język LD zawiera instrukcje niedeterministycznego wyboru {x:=?}. Odpowiednie aksjomaty mają postać

[x:=?]φ ≡ ∀x φ

<x:=?>φ ≡ ∃x φ

Intuicjoniści sprzeciwiają się gorąco temu, by twierdzić, że w ten sposób można definiować operacje, nie podając przy tym algorytmu. Nasz nieżyjący już kolega profesor Antoni Kreczmar, usłyszał kiedyś na seminarium zdanie: "aksjomat wyboru gwarantuje istnienie algorytmu obliczającego rozwiązanie problemu ...". Tak na pewno nie powinno się mówić. Wielu matematyków przyjmuje dowód istnienia pewnej funkcji oparty na aksjomacie wyboru, ale stwierdzanie, że aksjomat wyboru gwarantuje istnienie algorytmu nie jest poprawne.

b) Instrukcja iteracji ma postać α* gdzie α jest programem.

c) Zauważ, że programy {x:=?} i {x:=0; (x:=x+1)*} są równoważne w tym sensie, że oba realizują niedeterministyczny wybór liczby naturalnej.

Obie te konstrukcje mogą być przydatne, w pewnym stopniu, do modelowania zjawisk zachodzących podczas obliczeń. Nie są jednak tożsame z programami. Dlaczego? Ponieważ nie istnieje żaden efektywny mechanizm, który gwarantowałby spełnienie jednocześnie dwu warunków: (i) nieograniczony wybór, i (ii) kończenie obliczeń. Argument ten podał E.W. Dijkstra w książce Umiejętność programowania, WNT, Warszawa,1985, str. 77-79.

Dla ciekawych: Intuicjonizm -- sposób uprawiania matematyki zapoczatkowany przez Brouwera -- nie zezwala na niekonstruktywne dowody zdań egzystencjalnych.

Podsumowując:

a) Język logiki dynamicznej dopuszcza jako programy pewne konstrukcje nieefektywne,

b) System logiki algorytmicznej cieszy się własnością pełności. Logika dynamiczna przez pewien czas zadowalała się twierdzeniem o tzw. arytmetycznej pełności. Dopiero po naszej krytyce w książce Dynamic Logic znalazł się system wzorowany na systemie aksjomatów i reguł wnioskowania G. Mirkowskiej [GM1].

c) Logika dynamiczna nie zajmuje się strukturami danych innymi niż standardowy system liczb naturalnych. Logika algorytmiczna jest systemem dedukcyjnym stosowanym w teoriach podstawowych struktur: algorytmiczna teoria stosów, algorytmiczna teoria kolejek FIFO, algorytmiczna teoria s łowników, algorytmiczna teoria kolejek priorytetowych, algorytmiczna teoria drzew binarnych, algorytmiczna teoria dzew BST binarnych poszukiwań, ...

d)