Game Semantics

Origin. Lorenzen's dialogical logic (1960s). Hintikka's game-theoretic semantics (1970s). Abramsky, Jagadeesan, Malacaria: full abstraction (1990s). Games between Proponent (verifier) and Opponent (falsifier). Foundation for programming language semantics.

Models. Truth as winning strategy. Formula φ is true iff Proponent has winning strategy in game G(φ). Opponent challenges, Proponent defends. ∨: Proponent chooses disjunct. ∧: Opponent chooses conjunct. ∀: Opponent chooses witness. ∃: Proponent chooses witness.

Formalism.

Semantic games (Hintikka): G(φ, M, s): game for φ in model M, assignment s.

G(p): Proponent wins if p true under s.
G(φ ∨ ψ): Proponent chooses φ or ψ, plays that game.
G(φ ∧ ψ): Opponent chooses, Proponent plays.
G(∃x.φ): Proponent picks a, plays G(φ[a/x]).
G(∀x.φ): Opponent picks a, plays G(φ[a/x]).
G(¬φ): roles switch, play G(φ).

Winning: M ⊨ φ iff Proponent has winning strategy in G(φ, M).

Full abstraction (PCF): Arena: set of moves with Player/Opponent labeling. Strategy: set of plays respecting alternation. Composition: strategy composition = function composition. Achieves: two terms equal iff same strategy.

Innocent strategies: Strategy depends only on P-view (justification pointers). Models pure functional computation.

Arena structure: Moves labeled: question/answer, O/P. Bracketing: answers respond to questions. Innocence, well-bracketing, visibility constraints.

Symbols.

Symbol	Unicode	Name	Meaning
P	—	Proponent	Verifier/Player
O	—	Opponent	Falsifier/Environment
σ	U+03C3	Strategy	Winning strategy
⊛	U+229B	Composition	Strategy composition
⟦-⟧	—	Interpretation	Semantic function
q, a	—	Question, Answer	Move types

Metatheory. Game semantics is compositional. Full abstraction for PCF via innocent strategies. Characterizes various effects: state, control, concurrency. Categories of games form models. Decidability via finite-state strategies. Logic completeness: strategy iff proof (cut-free).

Applies to. Programming language semantics. Full abstraction proofs. Program equivalence. Concurrency models. Linear logic semantics. Verification via games. Dialogue systems.

Limitations. Complex mathematical machinery. Many variants for different features. Composition can be intricate. Size explosion for strategies. Not directly implementable. Connection to operational semantics indirect.