Hypergames and full completeness for system F (rough draft)

TL;DR

This paper revisits the hypergames model of system F, highlighting its full completeness and the innovative way it models type instantiation and uniformity through game semantics, based on a decade of prior work.

Contribution

It provides a comprehensive review of the hypergames model of system F, emphasizing its full completeness and the novel game-theoretic approach to type variables.

Findings

Hypergames model achieves full completeness for system F.

Type variables are modeled as games, with instantiation via copycat expansion.

The approach offers a uniform semantics for polymorphic types.

Abstract

This paper reviews the fully complete hypergames model of system $F$, presented a decade ago in the author's thesis. Instantiating type variables is modelled by allowing ``games as moves''. The uniformity of a quantified type variable $\forall X$ is modelled by copycat expansion: $X$ represents an unknown game, a kind of black box, so all the player can do is copy moves between a positive occurrence and a negative occurrence of $X$. This presentation is based on slides for a talk entitled ``Hypergame semantics: ten years later'' given at `Games for Logic and Programming Languages', Seattle, August 2006.