Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Normalization for multimodal type theory

Daniel Gratzer

TL;DR

This work addresses the problem of normalizing a broad, multimodal dependent type theory ($MTT$) and establishing decidability for type checking by reducing it to modality equality in the underlying mode theory. It introduces multimodal synthetic Tait computability (MSTC) and a normalization cosmos to implement normalization-by-gluing across many modal instantiations, including guarded recursion and parametricity calculi. The main contributions are a complete normalization algorithm for $MTT$, proofs of decidability, injectivity of type formers, and canonicity, along with extensions to crisp induction; the framework scales to arbitrary mode theories. The approach is semantically grounded in presheaf cosmoi and the internal language of gluing, enabling a modular, implementable path to generic modal type theories and their metatheory with a unified method for normalization and type checking. This work thus provides a practical, general engine for reasoning about and implementing a broad class of modal type theories with robust metatheoretic guarantees.

Abstract

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof uses a generalization of synthetic Tait computability -- an abstract approach to gluing proofs -- to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.

Normalization for multimodal type theory

TL;DR

This work addresses the problem of normalizing a broad, multimodal dependent type theory () and establishing decidability for type checking by reducing it to modality equality in the underlying mode theory. It introduces multimodal synthetic Tait computability (MSTC) and a normalization cosmos to implement normalization-by-gluing across many modal instantiations, including guarded recursion and parametricity calculi. The main contributions are a complete normalization algorithm for , proofs of decidability, injectivity of type formers, and canonicity, along with extensions to crisp induction; the framework scales to arbitrary mode theories. The approach is semantically grounded in presheaf cosmoi and the internal language of gluing, enabling a modular, implementable path to generic modal type theories and their metatheory with a unified method for normalization and type checking. This work thus provides a practical, general engine for reasoning about and implementing a broad class of modal type theories with robust metatheoretic guarantees.

Abstract

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof uses a generalization of synthetic Tait computability -- an abstract approach to gluing proofs -- to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.
Paper Structure (36 sections, 31 theorems, 74 equations, 5 figures)

This paper contains 36 sections, 31 theorems, 74 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Multimodal type theory
  3. Normalization-by-evaluation
  4. Normalization-by-gluing
  5. Synthetic Tait computability
  6. Synthetic Tait computability for
  7. Contributions
  8. A primer on
  9. Mode-local connectives in
  10. Modalities in
  11. Standard combinators within
  12. Normal and neutral forms in
  13. Renamings
  14. Models and cosmoi
  15. Natural models of
  16. ...and 21 more sections

Key Result

Lemma 2.3

The decoding of renamings to substitutions gives a 2-natural transformation $\Mor[\EmbRen[-]]{\Ren{-}}{\Cx{-}}$.

Figures (5)

  • Figure 1: Key rules for contexts and substitutions in
  • Figure 2: Complete definition of renamings
  • Figure 3: Definition of selected normals, neutrals, and normal types
  • Figure 4: Internal presentation of an cosmos
  • Figure 5: Neutral and normal forms, internally

Theorems & Definitions (75)

  • Example 1.1
  • Remark 2.1
  • Remark 2.2
  • Lemma 2.3
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3: Definition 18 awodey:2018
  • Theorem 3.4
  • Definition 3.5
  • Example 3.6
  • ...and 65 more