Logika obliczalności

Nie mylić z logiką obliczeniową .

Logika obliczalności ( CoL ) to program badawczy i ramy matematyczne do ponownego opracowania logiki jako systematycznej formalnej teorii obliczalności , w przeciwieństwie do logiki klasycznej , która jest formalną teorią prawdy. Został wprowadzony i tak nazwany przez Giorgi Japaridze w 2003 roku.

W logice klasycznej formuły reprezentują zdania prawda/fałsz. W CoL formuły reprezentują problemy obliczeniowe . W logice klasycznej ważność formuły zależy tylko od jej formy, a nie od jej znaczenia. W CoL ważność oznacza bycie zawsze obliczalnym. Mówiąc bardziej ogólnie, logika klasyczna mówi nam, kiedy prawdziwość danego zdania zawsze wynika z prawdziwości danego zestawu innych zdań. Podobnie CoL mówi nam, kiedy obliczalność danego problemu A zawsze wynika z obliczalności innych danych problemów B 1 ,..., Bn . Ponadto zapewnia jednolity sposób faktycznego skonstruowania rozwiązania ( algorytmu ) dla takiego A z dowolnych znanych rozwiązań B 1 ,..., Bn .

CoL formułuje problemy obliczeniowe w ich najbardziej ogólnym – interaktywnym znaczeniu. CoL definiuje problem obliczeniowy jako grę rozgrywaną przez maszynę przeciwko jej otoczeniu. Taki problem jest obliczalny , jeśli istnieje maszyna, która wygrywa grę z każdym możliwym zachowaniem otoczenia. Taka maszyna do gry uogólnia tezę Churcha-Turinga na poziom interaktywny. Klasyczne pojęcie prawdy okazuje się szczególnym przypadkiem obliczalności o zerowym stopniu interaktywności. To czyni logikę klasyczną szczególnym fragmentem CoL. Zatem CoL jest konserwatywnym rozszerzeniem logiki klasycznej. Logika obliczalności jest bardziej wyrazista, konstruktywna i znacząca obliczeniowo niż logika klasyczna. Poza logiką klasyczną naturalnymi fragmentami CoL okazują się również logika niezależna (IF) oraz pewne właściwe rozszerzenia logiki liniowej i logiki intuicjonistycznej . Stąd znaczące pojęcia „prawdy intuicjonistycznej”, „prawdy logiki liniowej” i „prawdy logiki IF” można wyprowadzić z semantyki CoL.

CoL systematycznie odpowiada na fundamentalne pytanie, co można obliczyć i jak; zatem CoL ma wiele zastosowań, takich jak konstruktywne teorie stosowane, systemy baz wiedzy, systemy planowania i działania. Spośród nich tylko zastosowania w konstruktywnych teoriach stosowanych zostały jak dotąd szeroko zbadane: seria teorii liczb opartych na CoL, zwanych „klarymetyką”, została skonstruowana jako alternatywy o znaczeniu obliczeniowym i złożoności teoretycznej dla opartej na logice klasycznej Peano arytmetyka i jej odmiany, np. układy arytmetyki ograniczonej .

Tradycyjne systemy dowodowe, takie jak dedukcja naturalna i rachunek sekwencyjny, są niewystarczające do aksjomatyzacji nietrywialnych fragmentów CoL. Wymagało to opracowania alternatywnych, bardziej ogólnych i elastycznych metod dowodzenia, takich jak rachunek różniczkowy .

Język

Operatory logiki obliczalności: nazwy, symbole i odczyty

Pełny język CoL rozszerza język klasycznej logiki pierwszego rzędu. Jego słownictwo logiczne zawiera kilka rodzajów koniunkcji, dysjunkcji, kwantyfikatorów, implikacji, negacji i tak zwanych operatorów rekurencyjnych. Ta kolekcja zawiera wszystkie spójniki i kwantyfikatory logiki klasycznej. Język ma również dwa rodzaje atomów nielogicznych: elementarny i ogólny . Atomy elementarne, które nie są niczym innym jak atomami logiki klasycznej, reprezentują elementarne problemy , tj. gry bez ruchów, które maszyna automatycznie wygrywa, gdy jest prawdziwa, i przegrywa, gdy jest fałszywa. Natomiast atomy ogólne można interpretować jako dowolne gry, elementarne lub nieelementarne. Zarówno pod względem semantycznym, jak i składniowym, logika klasyczna jest niczym innym jak fragmentem CoL uzyskanym przez zakazanie ogólnych atomów w swoim języku i zakazanie wszystkich operatorów innych niż ¬, ∧, ∨, →, ∀, ∃.

Japaridze wielokrotnie zwracał uwagę, że język CoL jest otwarty i może podlegać dalszym rozszerzeniom. Ze względu na ekspresyjność tego języka postępy w CoL, takie jak konstruowanie aksjomatyzacji lub budowanie teorii stosowanych opartych na CoL, były zwykle ograniczone do jednego lub drugiego właściwego fragmentu języka.

Semantyka

Gry leżące u podstaw semantyki CoL nazywane są grami statycznymi . W takich grach nie ma kolejności tur; gracz zawsze może się poruszać, podczas gdy inni gracze „myślą”. Jednak gry statyczne nigdy nie karzą gracza za zbyt długie „myślenie” (opóźnianie własnych ruchów), więc takie gry nigdy nie stają się konkursami szybkości. Wszystkie gry elementarne są automatycznie statyczne, podobnie jak gry mogą być interpretacjami ogólnych atomów.

W grach statycznych bierze udział dwóch graczy: maszyna i środowisko . Maszyna może podążać tylko za strategiami algorytmicznymi, podczas gdy nie ma ograniczeń co do zachowania środowiska. Każdy bieg (zagrywka) jest wygrywany przez jednego z tych graczy, a przegrywany przez drugiego.

Operatory logiczne CoL są rozumiane jako operacje na grach. Tutaj nieformalnie badamy niektóre z tych operacji. Dla uproszczenia przyjmujemy, że dziedziną dyskursu jest zawsze zbiór wszystkich liczb naturalnych: {0,1,2,...}.

Operacja ¬ negacji („nie”) zmienia role dwóch graczy, zamieniając ruchy i wygrane maszyny na te wykonywane przez otoczenie i odwrotnie. Na przykład, jeśli szachy są grą w szachy (ale z wykluczonymi remisami) z perspektywy białego gracza, to ¬ Szachy są tą samą grą z perspektywy czarnego gracza.

Koniunkcja równoległa ∧ („pand”) i równoległa dysjunkcja ∨ („por”) łączą gry w sposób równoległy. Przebieg A ∧ B lub A ∨ B to jednoczesna gra w dwóch koniunkcjach. Maszyna wygrywa A ∧ B , jeśli wygrywa oba z nich. Maszyna wygrywa A ∨ B , jeśli wygrywa przynajmniej jedną z nich. Na przykład Szachy ∨¬ Szachy to gra na dwóch planszach, na jednej gra się białymi, a na drugiej czarnych, a zadaniem maszyny jest wygranie przynajmniej na jednej szachownicy. Taką grę można łatwo wygrać niezależnie od tego, kto jest przeciwnikiem, kopiując jego ruchy z jednej planszy na drugą.

Operator implikacji równoległej → („pimplikacja”) jest zdefiniowany przez A → B = ¬ A ∨ B . Intuicyjne znaczenie tej operacji polega na sprowadzeniu B do A , czyli rozwiązywaniu A tak długo, jak długo przeciwnik rozwiązuje B .

Równoległe kwantyfikatory ∧ („pall”) i ∨ („pexists”) można zdefiniować jako ∧ xA ( x ) = A (0) ∧ A (1) ∧ A (2) ∧... i ∨ xA ( x ) = A (0)∨ A (1)∨ A (2)∨.... Są to więc równoczesne zagrania A (0), A (1), A (2),..., każda na osobnej planszy . Maszyna wygrywa ∧ xA ( x ), jeśli wygrywa wszystkie te gry, i ∨ xA ( x ), jeśli wygrywa niektóre.

ślepe kwantyfikatory ∀ („blall”) i ∃ („bleksyści”) generują gry jednoplanszowe. Przebieg ∀ xA ( x ) lub ∃ xA ( x ) to pojedynczy przebieg A . Maszyna wygrywa ∀ xA ( x ) (odp. ∃ xA ( x )), jeśli taki przebieg jest wygranym przebiegiem A ( x ) dla wszystkich (odp. co najmniej jednej) możliwych wartości x , i wygrywa ∃ xA ( x ) ), jeśli jest to prawdą dla co najmniej jednego.

Wszystkie dotychczas scharakteryzowane operatory zachowują się dokładnie tak, jak ich klasyczne odpowiedniki, gdy są stosowane w elementarnych (bez ruchu) grach i potwierdzają te same zasady. Dlatego CoL używa tych samych symboli dla tych operatorów, co logika klasyczna. Kiedy jednak takie operatory są stosowane do gier nieelementarnych, ich zachowanie nie jest już klasyczne. Na przykład, jeśli p jest atomem elementarnym, a P atomem ogólnym, p → p ∧ p jest ważne, podczas gdy P → P ∧ P nie. Zasada wyłączonego środka P ∨¬ P pozostaje jednak aktualna. Ta sama zasada jest nieważna w przypadku wszystkich trzech innych rodzajów dysjunkcji (wybór, sekwencja i przełączanie).

Dysjunkcja wyboru ⊔ („chor”) gier A i B , zapisana A ⊔ B , to gra, w której aby wygrać, maszyna musi wybrać jedną z dwóch dysjunkcji, a następnie wygrać w wybranym elemencie. Sekwencyjna dysjunkcja („sor”) A ᐁ B zaczyna się jako A ; kończy się również jako A , chyba że maszyna wykona ruch „przełączenia”, w którym to przypadku A zostaje przerwane, a gra uruchamia się ponownie i kontynuuje jako B . W alternatywie przełączającej („tor”) A ⩛ B , maszyna może przełączać się między A i B dowolną skończoną liczbę razy. Każdy operator dysjunkcji ma swoją podwójną koniunkcję, uzyskaną przez zamianę ról dwóch graczy. Odpowiednie kwantyfikatory można dalej zdefiniować jako nieskończone koniunkcje lub dysjunkcje w taki sam sposób, jak w przypadku kwantyfikatorów równoległych. Każda dysjunkcja sortowania indukuje również odpowiednią operację implikacji w taki sam sposób, jak to miało miejsce w przypadku implikacji równoległej →. Na przykład implikacja wyboru („szymplikacja”) A ⊐ B jest zdefiniowana jako ¬ A ⊔ B .

Powtarzanie równoległe („prekursywność”) A można zdefiniować jako nieskończoną koniunkcję równoległą A ∧A∧A∧… W podobny sposób można zdefiniować sekwencyjne („powtórzenie”) i przełączające („powtórzenie”) rodzaje nawrotów.

Operatory współbieżności można zdefiniować jako nieskończone dysjunkcje. Powtarzanie rozgałęzione („brecurrence”) ⫰ , które jest najsilniejszym rodzajem powtarzania, nie ma odpowiadającego mu koniunkcji. ⫰ A to gra, która rozpoczyna się i przebiega jako A . Jednak w dowolnym momencie otoczenie może wykonać ruch „replikacyjny”, który tworzy dwie kopie aktualnej wówczas pozycji A , dzieląc w ten sposób grę na dwa równoległe wątki ze wspólną przeszłością, ale prawdopodobnie różnymi przyszłymi wydarzeniami. W ten sam sposób środowisko może dalej replikować dowolną pozycję dowolnego wątku, tworząc w ten sposób coraz więcej wątków A . Te wątki są rozgrywane równolegle, a maszyna musi wygrać A we wszystkich wątkach, aby być zwycięzcą w ⫰ A . Rozgałęziona współbieżność („współbieżność”) ⫯ jest definiowana symetrycznie przez zamianę „maszyny” i „środowiska”.

Każdy rodzaj powtórzenia wywołuje dodatkowo odpowiednią słabą wersję implikacji i słabą wersję negacji. O pierwszym mówi się, że jest implikacją , a o drugim obaleniu . Rozgałęziona Rimplikacja („brimplikacja”) A ⟜ B to nic innego jak ⫰ A → B , a rozgałęzione zaprzeczenie („brefutacja”) A to A ⟜ ⊥, gdzie ⊥ jest zawsze przegrywaną grą elementarną. Podobnie dla wszystkich innych rodzajów implikacji i obaleń.

Jako narzędzie do specyfikacji problemu

Język CoL oferuje systematyczny sposób określania nieskończonej różnorodności problemów obliczeniowych, z nazwami ustalonymi w literaturze lub bez. Poniżej znajduje się kilka przykładów.

Niech f będzie funkcją jednoargumentową. Problem obliczenia f zostanie zapisany jako ⊓ x ⊔ y( y = f ( x )). Zgodnie z semantyką CoL jest to gra, w której pierwszy ruch („wejście”) jest wykonywane przez otoczenie, które powinno wybrać wartość m dla x . Intuicyjnie sprowadza się to do poproszenia maszyny o podanie wartości f ( m ). Gra toczy się dalej jako ⊔ y( y = f ( m )). Teraz oczekuje się, że maszyna wykona ruch („wyjście”), którym powinno być wybranie wartości n dla y . Sprowadza się to do stwierdzenia, że ​​n jest wartością f (m). Gra sprowadza się teraz do elementarnego n = f ( m ), w którym wygrywa maszyna wtedy i tylko wtedy, gdy n jest rzeczywiście wartością f ( m ).

Niech p będzie predykatem jednoargumentowym. Wtedy ⊓ x ( p ( x )⊔¬ p ( x )) wyraża problem decydowania p , ⊓ x ( p ( x )& ᐁ ¬ p ( x )) wyraża problem półdecydowania p , a ⊓ x ( p ( x )⩛¬ p ( x )) problem rekurencyjnego przybliżania p .

Niech p i q będą dwoma predykatami jednoargumentowymi. Wtedy ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) wyraża problem Turinga-redukcji q do p (w tym sensie, że q jest Turinga redukowalne do p wtedy i tylko wtedy, gdy problem interaktywny ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) jest obliczalny). ⊓ x ( p ( x )⊔¬ p ( x )) → ⊓ x ( q ( x )⊔¬ q ( x )) robi to samo, ale dla silniejszej wersji redukcji Turinga, gdzie wyrocznię dla p można sprawdzić tylko raz . ⊓ x ⊔ y ( q ( x )↔ p ( y )) robi to samo dla problemu redukcji wielu-jednego q do p . Za pomocą bardziej złożonych wyrażeń można uchwycić wszelkiego rodzaju bezimienne, ale potencjalnie znaczące relacje i operacje na problemach obliczeniowych, takie jak na przykład „Turing-redukcja problemu półdecydowania r do problemu wielu-jedności redukcji q do p ”. Nakładając ograniczenia czasowe lub przestrzenne na pracę maszyny, otrzymuje się dodatkowo teoretyczne odpowiedniki takich relacji i operacji w teorii złożoności.

Jako narzędzie do rozwiązywania problemów

Znane systemy dedukcyjne dla różnych fragmentów CoL mają wspólną właściwość polegającą na tym, że rozwiązanie (algorytm) może być automatycznie wyodrębnione z dowodu problemu w systemie. Ta właściwość jest dalej dziedziczona przez wszystkie stosowane teorie oparte na tych systemach. Aby więc znaleźć rozwiązanie danego problemu, wystarczy wyrazić je w języku CoL, a następnie znaleźć dowód tego wyrażenia. Innym sposobem spojrzenia na to zjawisko jest myślenie o formule G CoL jako specyfikacji programu (celu). Wtedy dowód G jest – dokładniej przekłada się na – program spełniający tę specyfikację. Nie ma potrzeby weryfikowania, czy specyfikacja jest spełniona, bo sam dowód jest właśnie taką weryfikacją.

Przykładami teorii stosowanych opartych na CoL są tak zwane klarytmetyki . Są to teorie liczbowe oparte na CoL w tym samym sensie, w jakim arytmetyka Peano PA oparta jest na logice klasycznej. Taki system jest zwykle konserwatywnym rozszerzeniem PA. Zwykle zawiera wszystkie aksjomaty Peano i dodaje do nich jeden lub dwa dodatkowe aksjomaty Peano, takie jak ⊓ x ⊔ y ( y = x' ) wyrażające obliczalność funkcji następcy. Zwykle ma również jedną lub dwie nielogiczne reguły wnioskowania, takie jak konstruktywne wersje indukcji lub rozumienia. Dzięki rutynowym zmianom takich reguł można uzyskać solidne i kompletne systemy charakteryzujące taką lub inną interaktywną klasę złożoności obliczeniowej C. Jest to w tym sensie, że problem należy do C wtedy i tylko wtedy, gdy ma dowód w teorii. Tak więc taką teorię można wykorzystać do znajdowania nie tylko rozwiązań algorytmicznych, ale także efektywnych na żądanie, takich jak rozwiązania działające w czasie wielomianowym lub w przestrzeni logarytmicznej. Należy zaznaczyć, że wszystkie teorie klarytmetyczne mają te same postulaty logiczne, a jedynie ich postulaty nielogiczne różnią się w zależności od docelowej klasy złożoności. Ich zauważalną cechą odróżniającą od innych podejść o podobnych aspiracjach (takich jak arytmetyka ograniczona ) jest to, że raczej rozszerzają niż osłabiają PA, zachowując pełną moc dedukcyjną i wygodę tego drugiego.

Zobacz też

Linki zewnętrzne

Pobrano z „ https://en.wikipedia.org/w/index.php?title=Computability_logic&oldid=1018752096 ”