
TL;DR
This paper extends game semantics to include the cumulative hierarchy of universes in Martin-Löf type theory, enabling combinatorial reasoning for universes and addressing key challenges with identity types.
Contribution
It provides the first comprehensive game semantics for all standard types in Martin-Löf type theory, including universes, overcoming previous conflicts with identity types.
Findings
Successfully models universes within game semantics
Addresses and resolves the conflict between identity types and universes
Enables new combinatorial reasoning methods for type theory
Abstract
This work extends the present author's computational game semantics of Martin-L\"{o}f type theory to the cumulative hierarchy of universes. This extension completes game semantics of all standard types of Martin-L\"{o}f type theory for the first time in the 30 years history of modern game semantics. As a result, the powerful combinatorial reasoning of game semantics becomes available for the study of universes and types generated by them. A main challenge in achieving game semantics of universes comes from a conflict between identity types and universes: Naive game semantics of the encoding of an identity type by a universe induces a decision procedure on the equality between functions, a contradiction to a well-known fact in recursion theory. We overcome this problem by novel games for universes that encode games for identity types without deciding the equality.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsArtificial Intelligence in Games · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
