Game semantics
From Free net encyclopedia
Game semantics (German: dialogische Logik) is an approach to the semantics of logic that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player. Paul Lorenzen was the first to introduce a game semantics for logic, doing so in the late 1950s. Since then, a number of different game semantics have been studied in logic. Game semantics has also been applied to the formal semantics of programming languages.
Contents |
Intuitionistic logic, denotational semantics, linear logic
The primary motivation for Lorenzen and Kuno Lorenz was to find a game-theoretic (their term was "dialogical" Dialogische Logik) semantics for intuitionistic logic. Blass was the first to point out connections between game semantics and linear logic. This line was further developed by Samson Abramsky, Radhakrishnan Jagadeesan, Pasquale Malacaria and independently Martin Hyland and Luke Ong, who placed special emphasis on compositionality, i.e. the definition of strategies inductively on the syntax. Using game semantics, the authors mentioned above have solved the long-standing problem of defining a fully abstract model for the programming language PCF. Consequently, game semantics has led to fully abstract semantic models for a variety of programming languages and, to new semantic-directed methods of software verification by software model checking.
Quantifiers
Foundational considerations of game semantics have been more emphasised by Jaakko Hintikka and Gabriel Sandu, especially for Independence-friendly logic (IF logic, more recently Information-friendly logic), a logic with branching quantifiers. It was thought that the principle of compositionality fails for these logics, so that a Tarskian truth definition could not provide a suitable semantics. To get around this problem, the quantifiers were given a game-theoretic meaning. Specifically, a universal quantifier and existential quantifier represent a choice by a player from the domain. In the universal case, a natural name for the player is "Falsifier"; in the existential, "Verifier". Note that a single counterexample falsifies a universally quantified statement, and a single example suffices to verify an existentially quantified one. Wilfred Hodges has proposed a compositional semantics and proved it equivalent to game semantics for IF-logics. Foundational considerations have motivated the works of others, such as Japaridze's computability logic.
See also
- Independence-friendly logic
- Intuitionistic logic
- Linear logic
- Computability logic
- Interactive computation
Articles
- Krabbe, E. C. W., 2001. "Dialogue Foundations: Dialogue Logic Revisited," Supplement to the Proceedings of The Aristotelian Society 75: 33-49.
Books
- K. Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978
- P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Stuttgart 2000 ISBN 3-476-01784-2
- R. Inhetveen: Logik. Eine dialog-orientierte Einführung., Leipzig 2003 ISBN 3-937219-02-1