Berechenbarkeitslogik - Computability logic

Nicht zu verwechseln mit Computerlogik .

Computability Logic ( CoL ) ist ein Forschungsprogramm und ein mathematischer Rahmen für die Neuentwicklung von Logik als systematische formale Theorie der Berechenbarkeit im Gegensatz zur klassischen Logik, die eine formale Wahrheitstheorie ist. Es wurde 2003 von Giorgi Japaridze eingeführt und so benannt .

In der klassischen Logik repräsentieren Formeln wahre / falsche Aussagen. In CoL stellen Formeln Rechenprobleme dar . In der klassischen Logik hängt die Gültigkeit einer Formel nur von ihrer Form ab, nicht von ihrer Bedeutung. In CoL bedeutet Gültigkeit, immer berechenbar zu sein. Allgemeiner sagt uns die klassische Logik, wann die Wahrheit einer gegebenen Aussage immer aus der Wahrheit einer gegebenen Menge anderer Aussagen folgt. In ähnlicher Weise sagt uns CoL, wann die Berechenbarkeit eines gegebenen Problems A immer aus der Berechenbarkeit anderer gegebener Probleme B 1 , ..., B n folgt . Darüber hinaus bietet es eine einheitliche Möglichkeit, eine Lösung (einen Algorithmus ) für ein solches A aus bekannten Lösungen von B 1 , ..., B n tatsächlich zu konstruieren .

CoL formuliert Rechenprobleme in ihrem allgemeinsten - interaktiven Sinne. CoL definiert ein Rechenproblem als ein Spiel, das von einer Maschine gegen ihre Umgebung gespielt wird. Ein solches Problem ist berechenbar, wenn es eine Maschine gibt, die das Spiel gegen jedes mögliche Verhalten der Umgebung gewinnt. Eine solche Spielmaschine verallgemeinert die Church-Turing-These auf die interaktive Ebene. Das klassische Konzept der Wahrheit entpuppt sich als ein spezieller Fall von Berechenbarkeit ohne Interaktivitätsgrad. Dies macht die klassische Logik zu einem besonderen Fragment von CoL. Somit ist CoL eine konservative Erweiterung der klassischen Logik. Die Berechenbarkeitslogik ist ausdrucksvoller, konstruktiver und rechnerisch aussagekräftiger als die klassische Logik. Neben der klassischen Logik erweisen sich auch die unabhängige (IF) Logik und bestimmte geeignete Erweiterungen der linearen Logik und der intuitionistischen Logik als natürliche Fragmente von CoL. Daher können aus der Semantik von CoL sinnvolle Konzepte von "intuitionistischer Wahrheit", "linear-logischer Wahrheit" und "IF-logischer Wahrheit" abgeleitet werden.

CoL beantwortet systematisch die grundlegende Frage, was wie berechnet werden kann. Daher hat CoL viele Anwendungen, wie konstruktive angewandte Theorien, Wissensbasissysteme, Planungs- und Handlungssysteme. Von diesen wurden bisher nur Anwendungen in konstruktiv angewandten Theorien eingehend untersucht: Eine Reihe von CoL-basierten Zahlentheorien, die als "Clarithmetik" bezeichnet werden, wurden als rechnerisch und komplexitätstheoretisch bedeutsame Alternativen zum auf klassischer Logik basierenden Peano konstruiert Arithmetik und ihre Variationen wie Systeme der begrenzten Arithmetik .

Herkömmliche Beweissysteme wie natürliche Deduktion und sequentielle Berechnung reichen nicht aus, um nichttriviale Fragmente von CoL zu axiomatisieren. Dies hat die Entwicklung alternativer, allgemeinerer und flexiblerer Beweismethoden wie der Umlaufrechnung erforderlich gemacht .

Sprache

Operatoren der Berechenbarkeitslogik: Namen, Symbole und Messwerte

Die vollständige Sprache von CoL erweitert die Sprache der klassischen Logik erster Ordnung. Sein logisches Vokabular enthält verschiedene Arten von Konjunktionen, Disjunktionen, Quantifizierern, Implikationen, Negationen und sogenannten Wiederholungsoperatoren. Diese Sammlung enthält alle Konnektiva und Quantifizierer der klassischen Logik. Die Sprache hat auch zwei Arten von nichtlogischen Atomen: elementare und allgemeine . Elementare Atome, die nichts anderes als die Atome der klassischen Logik sind, stellen elementare Probleme dar , dh Spiele ohne Züge, die von der Maschine automatisch gewonnen werden, wenn sie wahr sind, und verloren, wenn sie falsch sind. Allgemeine Atome hingegen können als beliebige elementare oder nicht elementare Spiele interpretiert werden. Sowohl semantisch als auch syntaktisch ist die klassische Logik nichts anderes als das Fragment von CoL, das erhalten wird, indem allgemeine Atome in ihrer Sprache verboten werden und alle anderen Operatoren als ¬, ∧, ∨, →, ∀, ∃ verboten werden.

Japaridze hat wiederholt darauf hingewiesen, dass die Sprache von CoL unbefristet ist und möglicherweise weitere Erweiterungen erfahren wird. Aufgrund der Ausdruckskraft dieser Sprache waren Fortschritte in der CoL, wie das Konstruieren von Axiomatisierungen oder das Erstellen von CoL-basierten angewandten Theorien, normalerweise auf das eine oder andere geeignete Fragment der Sprache beschränkt.

Semantik

Die Spiele, die der Semantik von CoL zugrunde liegen, werden als statische Spiele bezeichnet . Solche Spiele haben keine Zugreihenfolge; Ein Spieler kann sich immer bewegen, während die anderen Spieler "nachdenken". Statische Spiele bestrafen einen Spieler jedoch niemals dafür, dass er zu lange "nachgedacht" hat (was seine eigenen Züge verzögert), so dass solche Spiele niemals zu Geschwindigkeitswettbewerben werden. Alle elementaren Spiele sind automatisch statisch, ebenso wie die Spiele Interpretationen allgemeiner Atome sein dürfen.

In statischen Spielen gibt es zwei Spieler: die Maschine und die Umgebung . Die Maschine kann nur algorithmischen Strategien folgen, während das Verhalten der Umgebung nicht eingeschränkt ist. Jeder Lauf (Spiel) wird von einem dieser Spieler gewonnen und vom anderen verloren.

Die logischen Operatoren von CoL werden als Operationen an Spielen verstanden. Hier untersuchen wir informell einige dieser Operationen. Der Einfachheit halber nehmen wir an, dass der Diskursbereich immer die Menge aller natürlichen Zahlen ist: {0,1,2, ...}.

Die Operation ¬ der Negation ("nicht") wechselt die Rollen der beiden Spieler, wobei Bewegungen und Siege der Maschine in die der Umgebung umgewandelt werden und umgekehrt. Wenn zum Beispiel Schach aus der Sicht des weißen Spielers das Schachspiel ist (aber mit Gleichstand ausgeschlossen), dann ist ¬ Schach aus der Sicht des schwarzen Spielers dasselbe Spiel.

Die parallele Konjunktion ∧ ("pand") und die parallele Disjunktion ∨ ("por") kombinieren Spiele auf parallele Weise. Ein Lauf von A ∧ B oder A ∨ B ist ein gleichzeitiges Spiel in den beiden Konjunktionen. Die Maschine gewinnt A ∧ B, wenn sie beide gewinnt. Die Maschine gewinnt A ∨ B, wenn sie mindestens einen von ihnen gewinnt. Zum Beispiel ist Schach ∨¬ Schach ein Spiel auf zwei Brettern, von denen eines weiß und eines schwarz gespielt wird und bei dem die Aufgabe der Maschine darin besteht, auf mindestens einem Brett zu gewinnen. Ein solches Spiel kann leicht gewonnen werden, unabhängig davon, wer der Gegner ist, indem seine Züge von einem Brett auf das andere kopiert werden.

Die parallel Implikation Operator → ( "pimplication") definiert ist durch A → B = ¬ A ∨ B . Die intuitive Bedeutung dieser Operation besteht darin , B auf A zu reduzieren , dh A zu lösen, solange der Gegner B löst .

Die parallelen Quantifizierer ∧ ("pall") und ∨ ("pexists") können definiert werden durch ∧ xA ( x ) = A (0) ∧ A (1) ∧ A (2) ∧ ... und ∨ xA ( x ) = A (0) ∨ A (1) ∨ A (2) ∨ .... Dies sind also gleichzeitige Spiele von A (0), A (1), A (2), ..., jeweils auf einem separaten Brett . Die Maschine gewinnt ∧ xA ( x ), wenn sie alle diese Spiele gewinnt, und ∨ xA ( x ), wenn sie einige gewinnt.

Die blinden Quantifizierer ∀ ("blall") und ∃ ("blexists") erzeugen dagegen Einzelbrettspiele. Ein Lauf von ∀ xA ( x ) oder ∃ xA ( x ) ein Einzeldurchlauf von A . Die Maschine gewinnt ∀ xA ( x ) (bzw. ∃ xA ( x )), wenn ein solcher Lauf ein gewonnener Lauf von A ( x ) für alle (bzw. mindestens einen) möglichen Werte von x ist , und gewinnt ∃ xA ( x) ) wenn dies für mindestens eine gilt.

Alle bisher charakterisierten Operatoren verhalten sich genau wie ihre klassischen Kollegen, wenn sie auf elementare (bewegungslose) Spiele angewendet werden, und validieren dieselben Prinzipien. Aus diesem Grund verwendet CoL für diese Operatoren dieselben Symbole wie die klassische Logik. Wenn solche Operatoren jedoch auf nicht-elementare Spiele angewendet werden, ist ihr Verhalten nicht mehr klassisch. Wenn also beispielsweise p ein Elementaratom und P ein allgemeines Atom ist, ist p → p ∧ p gültig, während P → P ∧ P nicht gültig ist. Das Prinzip des ausgeschlossenen mittleren P ∨¬ P bleibt jedoch gültig. Das gleiche Prinzip ist bei allen drei anderen Arten (Auswahl, sequentielle und Umschaltung) der Disjunktion ungültig.

Die Wahl disjunction ⊔ ( „chor“) von Spielen A und B , geschrieben A ⊔ B , ist ein Spiel , bei dem, um die Maschine zu gewinnen, eine der beiden Disjunktionen zu wählen hat und dann in der gewählten Komponente zu gewinnen. Die sequentielle Disjunktion ("sor") A ᐁ B beginnt als A ; Es endet auch als A, es sei denn, die Maschine macht einen "Schalter" -Zug. In diesem Fall wird A abgebrochen und das Spiel neu gestartet und als B fortgesetzt . Bei der Umschaltdisjunktion ("tor") A ⩛ B kann die Maschine beliebig oft zwischen A und B umschalten . Jeder Disjunktionsoperator hat seine doppelte Konjunktion, die durch Vertauschen der Rollen der beiden Spieler erhalten wird. Die entsprechenden Quantifizierer können ferner auf die gleiche Weise wie im Fall der parallelen Quantifizierer als unendliche Konjunktionen oder Disjunktionen definiert werden. Jede Sortendisjunktion induziert ebenso wie dies bei der parallelen Implikation → eine entsprechende Implikationsoperation. Zum Beispiel kann die Wahl Implikation ( "chimplication") A ⊐ B wird als definiert ¬ A ⊔ B .

Die parallele Wiederholung ("Vorstufe") von A kann als die unendliche parallele Konjunktion A ∧A∧A∧ definiert werden ... Die sequentiellen ("Wiederholung") und umschaltenden ("Wiederholung") Arten von Wiederholungen können ähnlich definiert werden.

Die Kernstromoperatoren können als unendliche Disjunktionen definiert werden. Verzweigungswiederholung ("brecurrence") ⫰ , die stärkste Art der Wiederholung, hat keine entsprechende Konjunktion. ⫰ A ist ein Spiel, das als A beginnt und weitergeht . Die Umgebung kann jedoch jederzeit einen "replikativen" Zug ausführen, der zwei Kopien der damals aktuellen Position von A erstellt und so das Spiel in zwei parallele Fäden mit einer gemeinsamen Vergangenheit, aber möglicherweise unterschiedlichen zukünftigen Entwicklungen aufteilt. Auf die gleiche Weise kann die Umgebung jede Position eines Threads weiter replizieren, wodurch immer mehr Threads von A erzeugt werden . Diese Threads werden parallel gespielt, und die Maschine muss in allen Threads A gewinnen , um der Gewinner in ⫰ A zu sein . Verzweigungskernstrom ("Cobrecurrence") ⫯ wird symmetrisch definiert, indem "Maschine" und "Umgebung" vertauscht werden.

Jede Art von Wiederholung induziert ferner eine entsprechende schwache Version der Implikation und eine schwache Version der Negation. Ersteres soll eine Rimplikation sein , letzteres eine Widerlegung . Die Verzweigungs-Rimplikation ("Brimplikation") A ⟜ B ist nichts anderes als ⫰ A → B , und die Verzweigungs-Widerlegung ("Brefutation") von A ist A ⟜ ⊥, wobei ⊥ das immer verlorene Elementarspiel ist. Ähnliches gilt für alle anderen Arten von Rimplikation und Widerlegung.

Als Problemspezifikationstool

Die Sprache von CoL bietet eine systematische Möglichkeit, eine unendliche Vielfalt von Rechenproblemen mit oder ohne in der Literatur festgelegte Namen zu spezifizieren. Nachfolgend einige Beispiele.

Sei f eine unäre Funktion. Das Problem der Berechnung von f wird als ⊓ x ⊔ y ( y = f ( x )) geschrieben. Nach der Semantik von CoL ist dies ein Spiel, bei dem der erste Zug ("Eingabe") von der Umgebung ausgeht, die einen Wert m für x wählen sollte . Intuitiv bedeutet dies, dass die Maschine aufgefordert wird, den Wert von f ( m ) anzugeben . Das Spiel wird als ⊔ y ( y = f ( m )) fortgesetzt . Nun wird von der Maschine erwartet, dass sie eine Bewegung ausführt ("Ausgabe"), die einen Wert n für y wählen sollte . Dies bedeutet, dass n der Wert von f (m) ist. Das Spiel wird nun auf das Element n = f ( m ) gebracht, das von der Maschine genau dann gewonnen wird, wenn n tatsächlich der Wert von f ( m ) ist.

Sei p ein unäres Prädikat. Dann drückt ⊓ x ( p ( x ) ⊔¬ p ( x )) das Problem der Entscheidung über p aus , ⊓ x ( p ( x ) & ᐁ ¬ p ( x )) drückt das Problem der Halbentscheidung von p aus und ⊓ x ( p () x ) ⩛¬ p ( x )) das Problem der rekursiven Approximation von p .

Sei p und q zwei unäre Prädikate. Dann ⊓ x ( p ( x ) ⊔¬ p ( x )) ⟜ ⊓ x ( q ( x ) ⊔¬ q ( x )) exprimiert , das Problem der Turing mindernde q zu p (in dem Sinne , daß q zu Turing reduzierbaren p , wenn und nur wenn das interaktive Problem ⊓ x ( p ( x ) ⊔¬ p ( x )) ⟜ ⊓ x ( q ( x ) ⊔¬ q ( x )) berechenbar ist). ⊓ x ( p ( x ) ⊔¬ p ( x )) → ⊓ x ( q ( x ) ⊔¬ q ( x )) macht dasselbe, jedoch für die stärkere Version der Turing-Reduktion, bei der das Orakel für p nur einmal abgefragt werden kann . ⊓ x ⊔ y ( q ( x ) ↔ p ( y )) macht dasselbe für das Problem der Mehrfachreduzierung von q auf p . Mit komplexeren Ausdrücken kann man alle Arten von namenlosen, aber möglicherweise bedeutungsvollen Beziehungen und Operationen zu Rechenproblemen erfassen, wie zum Beispiel "Turing-Reduzieren des Problems der Halbentscheidung r auf das Problem der Mehrfachreduzierung von q auf p ". Wenn man der Arbeit der Maschine zeitliche oder räumliche Beschränkungen auferlegt, erhält man ferner komplexitätstheoretische Gegenstücke zu solchen Beziehungen und Operationen.

Als Werkzeug zur Problemlösung

Die bekannten deduktiven Systeme für verschiedene Fragmente von CoL teilen die Eigenschaft, dass eine Lösung (ein Algorithmus) automatisch aus einem Beweis eines Problems im System extrahiert werden kann. Diese Eigenschaft wird weiterhin von allen angewandten Theorien übernommen, die auf diesen Systemen basieren. Um eine Lösung für ein bestimmtes Problem zu finden, reicht es aus, es in der Sprache von CoL auszudrücken und dann einen Beweis für diesen Ausdruck zu finden. Eine andere Möglichkeit, dieses Phänomen zu betrachten, besteht darin, sich eine Formel G von CoL als Programmspezifikation (Ziel) vorzustellen. Dann ist ein Beweis von G - genauer gesagt übersetzt - ein Programm, das dieser Spezifikation entspricht. Es ist nicht erforderlich zu überprüfen, ob die Spezifikation erfüllt ist, da der Beweis selbst tatsächlich eine solche Überprüfung ist.

Beispiele für CoL-basierte angewandte Theorien sind die sogenannten Clarithmetics . Dies sind Zahlentheorien, die auf CoL im gleichen Sinne basieren wie Peano Arithmetic PA auf klassischer Logik. Ein solches System ist normalerweise eine konservative Erweiterung von PA. Es enthält typischerweise alle Peano-Axiome und fügt ihnen ein oder zwei zusätzliche Peano-Axiome hinzu, wie z. B. ⊓ x ⊔ y ( y = x ' ), die die Berechenbarkeit der Nachfolgerfunktion ausdrücken. Typischerweise hat es auch eine oder zwei nicht logische Inferenzregeln, wie konstruktive Versionen der Induktion oder des Verstehens. Durch routinemäßige Variationen solcher Regeln kann man solide und vollständige Systeme erhalten, die die eine oder andere interaktive rechnerische Komplexitätsklasse C charakterisieren . Dies ist in dem Sinne, dass ein Problem genau dann zu C gehört, wenn es einen Beweis in der Theorie hat. Eine solche Theorie kann also verwendet werden, um nicht nur algorithmische, sondern auch effiziente Lösungen bei Bedarf zu finden, beispielsweise Lösungen, die in Polynomzeit oder im logarithmischen Raum ablaufen. Es sollte darauf hingewiesen werden, dass alle klarithmetischen Theorien dieselben logischen Postulate haben und nur ihre nicht logischen Postulate in Abhängigkeit von der Zielkomplexitätsklasse variieren. Ihr bemerkenswertes Unterscheidungsmerkmal von anderen Ansätzen mit ähnlichen Bestrebungen (wie z. B. begrenzte Arithmetik ) besteht darin, dass sie PA eher erweitern als schwächen, wobei die volle deduktive Kraft und Bequemlichkeit der letzteren erhalten bleibt.

Siehe auch

Verweise

Externe Links