2022/03/24 by Norihiro Yamada, Yamada, Norihiro
Computer Science · #Artificial Intelligence in Games #Combinatorics (math.CO) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2203.13069
openalex publication_date 2022/03/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This work extends the present author's computational game semantics of Martin-Löf type theory to the cumulative hierarchy of universes. This extension completes game semantics of all standard types of Martin-Lö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.