Spielsemantik - Game semantics

Semantik
Computer
Typen
Theorie
Analyse
Anwendungen

Spiel Semantik ( Deutsch : Dialogische Logik , übersetzt als dialogische Logik ) ist ein Ansatz zur formalen Semantik , dass Gründe , die Konzepte der Wahrheit oder Gültigkeit auf spieltheoretische Konzepte, wie die Existenz einer Gewinnstrategie für einen Spieler, etwas ähnlich sokratischen Dialoge oder mittelalterliche Theorie der Obligationen .

Geschichte

Ende der 1950er Jahre führte Paul Lorenzen als erster eine Spielsemantik für die Logik ein , die von Kuno Lorenz weiterentwickelt wurde . Fast zeitgleich mit Lorenzen entwickelte Jaakko Hintikka einen modelltheoretischen Ansatz, der in der Literatur als GTS (spieltheoretische Semantik) bekannt ist. Seitdem wurden eine Reihe verschiedener Spielsemantiken in der Logik untersucht.

Shahid Rahman (Lille) und seine Mitarbeiter entwickelten die dialogische Logik zu einem allgemeinen Rahmen für das Studium logischer und philosophischer Fragen im Zusammenhang mit dem logischen Pluralismus. Dies löste ab 1994 eine Art Renaissance mit nachhaltigen Folgen aus. Dieser neue philosophische Impuls erfuhr eine parallele Erneuerung auf den Gebieten der theoretischen Informatik , der Computerlinguistik , der künstlichen Intelligenz und der formalen Semantik von Programmiersprachen , beispielsweise durch die Arbeit von Johan van Benthem und Mitarbeitern in Amsterdam, die sich eingehend mit der Schnittstelle zwischen Logik beschäftigten und Spiele, und Hanno Nickau, der das Problem der vollständigen Abstraktion in Programmiersprachen mit Hilfe von Spielen ansprach. Neue Ergebnisse zur linearen Logik von Jean-Yves Girard in den Schnittstellen zwischen mathematischer Spieltheorie und Logik einerseits und Argumentationstheorie und Logik andererseits führten zu den Arbeiten vieler anderer, darunter S. Abramsky , J. van Benthem, A Blass , D. Gabbay , M. Hyland , W. Hodges , R. Jagadeesan, G. Japaridze , E. Krabbe, L. Ong, H. Prakken, G. Sandu, D. Walton und J. Woods, die platzierten Spielsemantik im Zentrum eines neuen Konzepts der Logik, in dem Logik als dynamisches Inferenzinstrument verstanden wird. Es gab auch eine alternative Perspektive auf die Beweistheorie und die Bedeutungstheorie, die befürwortet, dass Wittgensteins "Bedeutung als Verwendung"-Paradigma im Kontext der Beweistheorie verstanden wird, wo die sogenannten Reduktionsregeln (die die Wirkung von Eliminationsregeln auf das Ergebnis von Einführungsregeln) sollten als angemessen angesehen werden, um die Erklärung der (unmittelbaren) Konsequenzen zu formalisieren, die man aus einem Satz ziehen kann, und so die Funktion/Zweck/Nützlichkeit seines Hauptkonnektivs in der Sprachkalküle aufzuzeigen . ( de Queiroz (1988) , de Queiroz (1991) , de Queiroz (1994) , de Queiroz (2001) , de Queiroz (2008) )

Klassische Logik

Die einfachste Anwendung der Spielsemantik ist die Aussagenlogik . Jede Formel dieser Sprache wird als Spiel zwischen zwei Spielern interpretiert, bekannt als "Verifier" und "Falsifier". Dem Verifizierer wird "Eigentum" aller Disjunktionen in der Formel gegeben, und dem Falsifizierer wird ebenfalls das Eigentum an allen Konjunktionen gegeben . Jeder Zug des Spiels besteht darin, dem Besitzer des dominanten Bindeglieds zu erlauben, einen seiner Zweige auszuwählen; Das Spiel wird dann in dieser Unterformel fortgesetzt, wobei der Spieler, der sein dominantes Konnektiv kontrolliert, den nächsten Zug macht. Das Spiel endet, wenn ein primitiver Vorschlag von den beiden Spielern so gewählt wurde; zu diesem Zeitpunkt gilt der Verifizierer als Gewinner, wenn der resultierende Vorschlag wahr ist, und der Verifizierer gilt als Gewinner, wenn er falsch ist. Die ursprüngliche Formel wird genau dann als wahr angesehen, wenn der Verifizierer eine Gewinnstrategie hat , während sie falsch ist, wenn der Verifizierer die Gewinnstrategie hat.

Wenn die Formel Negationen oder Implikationen enthält, können andere, kompliziertere Techniken verwendet werden. Zum Beispiel sollte eine Negation wahr sein, wenn das Negierte falsch ist, also muss sie den Effekt haben, dass die Rollen der beiden Spieler vertauscht werden.

Allgemeiner kann die Spielsemantik auf die Prädikatenlogik angewendet werden ; die neuen Regeln erlauben es, einen dominanten Quantor von seinem "Eigentümer" (den Verifier für existenzielle Quantoren und den Falsifier für universelle Quantoren ) zu entfernen und seine gebundene Variable bei allen Vorkommen durch ein Objekt der Wahl des Eigentümers aus dem Bereich der Quantifizierung zu ersetzen . Beachten Sie, dass ein einziges Gegenbeispiel eine universell quantifizierte Aussage verfälscht und ein einziges Beispiel ausreicht, um eine existentiell quantifizierte zu verifizieren. Unter der Annahme des Auswahlaxioms stimmt die spieltheoretische Semantik für die klassische Logik erster Ordnung mit der üblichen modellbasierten (Tarskischen) Semantik überein . Für die klassische Logik erster Ordnung besteht die Gewinnstrategie für den Verifier im Wesentlichen darin, geeignete Skolem-Funktionen und Zeugen zu finden . Wenn zum Beispiel S bezeichnet eine dann equisatisfiable Anweisung für S ist . Die Skolem-Funktion f (sofern sie existiert) kodifiziert tatsächlich eine Gewinnstrategie für den Verifizierer von S, indem sie für jede Wahl von x, die der Falsifizierer treffen könnte, einen Zeugen für die existenzielle Unterformel zurückgibt.

Die obige Definition wurde zuerst von Jaakko Hintikka im Rahmen seiner GTS-Interpretation formuliert. Die ursprüngliche Version der Spielsemantik für die klassische (und intuitionistische) Logik nach Paul Lorenzen und Kuno Lorenz wurde nicht in Modellen, sondern in Gewinnstrategien gegenüber formalen Dialogen definiert (P. Lorenzen, K. Lorenz 1978, S. Rahman und L. Keiff 2005). Shahid Rahman und Tero Tulenheimo entwickelten einen Algorithmus, um GTS-Gewinnstrategien für die klassische Logik in die dialogischen Gewinnstrategien umzuwandeln und umgekehrt.

Für die meisten gängigen Logiken, einschließlich der oben genannten, haben die daraus resultierenden Spiele perfekte Informationen – das heißt, die beiden Spieler kennen immer die Wahrheitswerte jedes Primitiven und sind sich aller vorhergehenden Züge im Spiel bewusst. Mit dem Aufkommen der Spielsemantik wurden jedoch Logiken, wie die unabhängigkeitsfreundliche Logik von Hintikka und Sandu, mit einer natürlichen Semantik in Bezug auf Spiele mit unvollkommener Information vorgeschlagen.

Intuitionistische Logik, denotationale Semantik, lineare Logik, logischer Pluralismus

Die primäre Motivation für Lorenzen und Kuno Lorenz war eine spieltheoretische (ihr Begriff war zu finden dialogisch , in deutscher Sprache Dialogische Logik  [ de ] ) Semantik für intuitionismus . Andreas Blass hat als Erster Zusammenhänge zwischen Spielesemantik und linearer Logik aufgezeigt . Diese Linie wurde von Samson Abramsky , Radhakrishnan Jagadeesan , Pasquale Malacaria und unabhängig davon Martin Hyland und Luke Ong weiterentwickelt , die besonderen Wert auf Kompositionalität legten, also die Definition von Strategien induktiv über die Syntax. Mit Hilfe von Spielesemantik haben die oben genannten Autoren das seit langem bestehende Problem gelöst, ein vollständig abstraktes Modell für die Programmiersprache PCF zu definieren . Folglich wird vollständig abstrakte semantische Modelle für eine Vielzahl von Programmiersprachen führte Semantik Spiel, und auf neue semantische gerichteten Methoden der Software - Verifikation von Software Model Checking .

Shahid Rahman  [ fr ] und Helge Rückert erweiterten den dialogischen Ansatz auf das Studium mehrerer nichtklassischer Logiken wie Modallogik , Relevanzlogik , freie Logik und konnexive Logik . Kürzlich haben Rahman und seine Mitarbeiter den dialogischen Ansatz zu einem allgemeinen Rahmen entwickelt, der auf die Diskussion des logischen Pluralismus abzielt.

Quantifizierer

Grundlegende Überlegungen zur Spielsemantik wurden von Jaakko Hintikka und Gabriel Sandu stärker betont , insbesondere für die unabhängigkeitsfreundliche Logik (IF-Logik, neuerdings informationsfreundliche Logik), eine Logik mit verzweigten Quantoren . Es wurde angenommen, dass das Prinzip der Kompositionalität für diese Logiken versagt, so dass eine Tarskische Wahrheitsdefinition keine geeignete Semantik liefern könnte. Um dieses Problem zu umgehen, erhielten die Quantoren eine spieltheoretische Bedeutung. Genauer gesagt ist der Ansatz derselbe wie in der klassischen Aussagenlogik, außer dass die Spieler nicht immer perfekte Informationen über vorherige Züge des anderen Spielers haben. Wilfrid Hodges hat eine Kompositionssemantik vorgeschlagen und bewiesen, dass sie der Spielsemantik für IF-Logiken entspricht.

In jüngerer Zeit implementierten Shahid Rahman  [ fr ] und das Team der dialogischen Logik in Lille Abhängigkeiten und Unabhängigkeiten innerhalb eines dialogischen Rahmens mittels eines dialogischen Ansatzes zur intuitionistischen Typentheorie , dem immanenten Denken .

Berechenbarkeitslogik

Die Berechenbarkeitslogik von Japaridze ist ein spielsemantischer Zugang zur Logik im extremen Sinne, der Spiele als Ziele behandelt, die von der Logik bedient werden sollen, und nicht als technisches oder grundlegendes Mittel zum Studium oder zur Rechtfertigung von Logik. Ihr philosophischer Ausgangspunkt ist, dass Logik als universelles, allgemein verwendbares intellektuelles Werkzeug zum "Navigieren in der realen Welt" gedacht ist und als solches eher semantisch als syntaktisch ausgelegt werden sollte, da es die Semantik ist, die als Brücke zwischen reale Welt und ansonsten bedeutungslose formale Systeme (Syntax). Syntax ist somit sekundär und nur insofern interessant, als sie der zugrunde liegenden Semantik dient. Von diesem Standpunkt aus hat Japaridze wiederholt die oft verfolgte Praxis kritisiert, die Semantik an einige bereits vorhandene syntaktische Zielkonstruktionen anzupassen, wobei Lorenzens Ansatz zur intuitionistischen Logik ein Beispiel ist. Dieser Gedankengang geht dann davon aus, dass die Semantik wiederum eine Spielsemantik sein sollte, weil Spiele „die umfassendsten, kohärentsten, natürlichsten, angemessensten und bequemsten mathematischen Modelle für das Wesen aller ‚Navigations‘-Aktivitäten von Agenten bieten : ihre Interaktionen mit der umgebenden Welt“. Dementsprechend besteht das von der Berechenbarkeitslogik übernommene Logikerstellungsparadigma darin, die natürlichsten und grundlegendsten Operationen in Spielen zu identifizieren, diese Operatoren als logische Operationen zu behandeln und dann nach soliden und vollständigen Axiomatisierungen der Sätze spielsemantisch gültiger Formeln zu suchen. Auf diesem Weg ist eine Vielzahl bekannter oder unbekannter logischer Operatoren in der offenen Sprache der Berechenbarkeitslogik entstanden, mit verschiedenen Arten von Negationen, Konjunktionen, Disjunktionen, Implikationen, Quantoren und Modalitäten.

Spiele werden zwischen zwei Agenten gespielt: einer Maschine und ihrer Umgebung, wobei die Maschine nur effektive Strategien verfolgen muss. Auf diese Weise werden Spiele als interaktive Rechenprobleme und die Gewinnstrategien der Maschine für sie als Lösungen für diese Probleme angesehen. Es wurde festgestellt, dass die Berechenbarkeitslogik robust gegenüber vernünftigen Variationen in der Komplexität erlaubter Strategien ist, die auf den logarithmischen Raum und die polynomiale Zeit (das eine impliziert das andere bei interaktiven Berechnungen nicht) reduziert werden kann, ohne die Logik zu beeinflussen. All dies erklärt den Namen „Berechenbarkeitslogik“ und bestimmt die Anwendbarkeit in verschiedenen Bereichen der Informatik. Klassische Logik , unabhängigkeitsfreundliche Logik und gewisse Erweiterungen der linearen und intuitionistischen Logik erweisen sich als spezielle Fragmente der Berechenbarkeitslogik, die lediglich durch das Verbieten bestimmter Gruppen von Operatoren oder Atomen erhalten werden.

Siehe auch

Verweise

Literaturverzeichnis

Bücher

  • T. Aho und AV. Pietarinen (Hrsg.) Wahrheit und Spiele. Essays zu Ehren von Gabriel Sandu . Societas Philosophica Fennica (2006). ISBN  951-9264-57-4 .
  • J. van Benthem, G. Heinzmann, M. Rebuschi und H. Visser (Hrsg.) The Age of Alternative Logics . Springer (2006). ISBN  978-1-4020-5011-4 .
  • R. Inhetveen: Logik. Eine dialogorientierte Einführung. , Leipzig 2003 ISBN  3-937219-02-1
  • L. Keiff Le Pluralisme Dialogique . Dissertation Université de Lille 3 (2007).
  • K. Lorenz, P. Lorenzen: Dialogische Logik , Darmstadt 1978
  • P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie , Stuttgart 2000 ISBN  3-476-01784-2
  • O. Majer, A.-V. Pietarinen und T. Tulenheimo (Herausgeber). Spiele: Logik, Sprache und Philosophie vereinen . Springer (2009).
  • S. Rahman, Über Dialogue protologische Kategorien und andere Seltenheiten . Frankfurt 1993 ISBN  3-631-46583-1
  • S. Rahman und H. Rückert (Hrsg.), Neue Perspektiven in der Dialogischen Logik . Synthese 127 (2001) ISSN  0039-7857 .
  • S. Rahman und N. Clerbout: Linking Games and Constructive Type Theory: Dialogische Strategien, CTT-Demonstrationen und das Axiom der Wahl. Springer-Briefs (2015). https://www.springer.com/gp/book/9783319190624 .
  • S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: Immanentes Denken oder Gleichheit in Aktion. Ein Plaidoyer für das Play levell . Springer (2018). https://www.springer.com/gp/book/9783319911489 .
  • J. Redmond & M. Fontaine, Wie man Dialoge spielt. Eine Einführung in die Dialogische Logik. London, College Publications (Col. Dialogues and the Games of Logic. A Philosophical Perspective N° 1). ( ISBN  978-1-84890-046-2 )

Artikel

Externe Links