| Game Semantics |
Article Index for Game |
Website Links For Game Semantics |
Information AboutGame Semantics |
| CATEGORIES ABOUT GAME SEMANTICS | |
| logic | |
| mathematical logic | |
| philosophical logic | |
| logic in computer science | |
| semantics | |
| quantification | |
|
CLASSICAL LOGIC The simplest application of game semantics is to Propositional Logic . Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the Disjunction s in the formula, and the Falsifier is likewise given ownership of all the Conjunction s. Each move of the game consists of allowing the owner of the dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant connective making the next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a Winning Strategy , while it will be false whenever the Falsifier has the winning strategy. If the formula contains negations or implications, other, more complicated, techniques may be used. For example, a Negation should be true if the thing negated is false, so it must have the effect of interchanging the roles of the two players. More generally, game semantics may be applied to Predicate Logic ; the new rules allow a dominant Quantifier to be removed by its "owner" (the Verifier for Existential Quantifier s and the Falsifier for Universal Quantifier s) and its Bound Variable replaced at all occurrences by an object of the owner's choosing, drawn from the Domain Of Quantification . Note that a single counterexample falsifies a universally quantified statement, and a single example suffices to verify an existentially quantified one. All of these games are of Perfect Information ; the two players always know the Truth Value s of each primitive, and are aware of all preceding moves in the game. 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 . 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 . SEE ALSO
REFERENCES Articles
Books
EXTERNAL LINKS
|
|
|