Game semantics of Martin-L?f type theory

摘要

This work presents game semantics of Martin-L?f type theory (MLTT) equipped with the One, the Zero,the N, Pi, Sigma and Id types. Game semantics interprets a wide range of logic and computation, even thepolymorphic λ-calculus; however, it has remained a well-known challenge in the past 25 years to achievegame semantics of dependent type theories such as MLTT, and past attempts lack directness or generality.For instance, the approach taken by Abramsky et al. interprets Sigma types indirectly by formal lists, notby games, making an interpretation of universes hopeless, and it is limited to a very specific class of dependenttypes. The difficulty of this challenge comes from a conflict between the extensionality of dependenttypes and the intensionality of game semantics. We overcome the challenge by inventing a novel variantof games, while we keep strategies unchanged, in such a way that this variant inherits the strong pointsof conventional game semantics. Also, our method enables an interpretation of subtyping on dependenttypes for the first time as game semantics. We finally give a new, game-semantic proof of the independenceof Markov’s principle from MLTT. This proof illustrates an advantage of our intensional model overextensional ones such as Hyland’s effective topos.