Normalization for multimodal type theory

This paper establishes the normalization of Multimodal Type Theory (MTT) by extending synthetic Tait computability to handle modalities, thereby providing a unified type-checking algorithm for various modal systems like guarded recursion and internalized parametricity.

The Gist

The Big Picture: The Universal Translator

Imagine you are building a massive, futuristic library. This library doesn't just store books; it stores the rules for writing books. Some books are about magic (modalities), some are about logic, and some are about time travel.

For a long time, librarians (computer scientists) could only write rules for one specific type of book at a time. If you wanted to add a new rule for "time travel," you had to rebuild the entire library from scratch, often making mistakes or creating contradictions.

The Problem:
There was a specific library design called MTT (Multimodal Type Theory). It was brilliant because it was a "universal translator." You could plug in different "modalities" (like time travel, secrecy, or parallel universes) and it would instantly generate a working system for them.

However, there was a catch. No one could prove that this library was safe to use. Specifically, they couldn't prove that if you wrote a sentence in this library, the computer could always simplify it down to its most basic, undeniable form (a process called Normalization). Without this proof, the library was theoretically beautiful but practically dangerous—you couldn't be sure if two different-looking sentences actually meant the same thing.

The Solution:
This paper, by Daniel Gratzer, finally proves that MTT is safe. It shows that no matter how complex the "magic" you plug into the system, the computer can always simplify the results and decide if two things are equal.

---

The Analogy: The "Gluing" Workshop

To understand how the author solved this, we need to look at the method used, which is called Normalization-by-Gluing.

1. The Old Way: The "Free-Hand" Sculptor

Traditionally, proving these systems work was like a sculptor trying to carve a statue by hand, chipping away at the stone bit by bit. They had to check every single rule to make sure the statue didn't collapse.

• The issue: As the statue got more complex (adding more "modalities" or magic rules), the sculptor got overwhelmed. The stone kept cracking in weird places.

2. The New Way: The "Glued" Factory

The author uses a technique called Gluing. Imagine you have two factories:

• Factory A (The Real World): Where the messy, complicated code lives.
• Factory B (The Ideal World): A perfect, simplified world where everything is already sorted and clean.

The author builds a Bridge (The Glue) between these two factories.

• This bridge doesn't just connect them; it creates a hybrid factory.
• In this hybrid factory, every object has two parts:
  1. Its messy, real-world form.
  2. Its perfect, ideal form (the "normal form").

The Magic Trick:
The author proves that you can build this hybrid factory using a special set of tools called Synthetic Tait Computability (STC).

• Think of STC as a universal instruction manual. Instead of building the bridge brick-by-brick (which is hard), the manual tells you exactly how to assemble the bridge using pre-fabricated, modular parts.
• The author extends this manual to handle "multimodal" situations (multiple types of magic). They show that the bridge works even when the factories are connected by complex, twisting tunnels (modalities).

---

Key Concepts Simplified

What is "Normalization"?

Imagine you have a sentence: "The cat that is sleeping on the mat that is red is actually a dog."
It's grammatically correct, but it's messy.
Normalization is the process of simplifying that sentence to its core truth: "The dog is red."
In computer science, if a system can always do this, it means the system is decidable. You can always ask, "Are these two sentences the same?" and get a "Yes" or "No" answer instantly.

What are "Modalities"?

Think of modalities as filters or lenses.

• Standard Logic: "It is raining."
• Modal Logic (Time): "It will rain."
• Modal Logic (Secrecy): "It is secretly raining."
  MTT allows you to mix and match these lenses. The paper proves that even if you stack five different lenses on top of each other, the system can still simplify the result.

What is "Synthetic Tait Computability"?

This is the author's secret weapon.

• Old Way: You had to prove the bridge was strong by testing every single beam.
• STC Way: You build the bridge inside a simulation (a computer model). Because the simulation is built with perfect rules, if you can build the bridge there, you know it will work in the real world.
• The author upgraded this simulation to handle the "multimodal" complexity, proving that the bridge holds up even under heavy traffic.

---

Why Does This Matter?

1. Safety First: Before this paper, using MTT was like driving a car with no brakes. You hoped it worked, but you couldn't prove it. Now, we have the "brakes" (the normalization algorithm).
2. One Tool for All Jobs: Because MTT is a general framework, this proof automatically fixes the safety issues for dozens of specific systems used in cryptography, programming languages, and AI. You don't have to prove it for each one individually anymore.
3. The "Universal" Algorithm: The paper provides a recipe. If you give the computer the rules of your specific "magic" (the mode theory), the computer can automatically generate a tool that checks if your code is correct.

The Bottom Line

Daniel Gratzer took a complex, flexible, but unproven system (MTT) and built a universal safety net around it. He did this by creating a "hybrid factory" (Gluing) and using a high-tech instruction manual (Synthetic Tait Computability) to ensure that no matter how you twist and turn the rules, the system can always simplify itself and tell you the truth.

It's the difference between having a map of a maze that might have dead ends, and having a map that guarantees you can always find the exit.

Technical Summary

1. Problem Statement

The paper addresses the lack of a normalization algorithm for Multimodal Type Theory (MTT), a general framework for dependent type theories with modalities.

• Context: MTT allows for the internalization of various modal type theories (e.g., guarded recursion, internalized parametricity) by instantiating it with a "mode theory" (a strict 2-category).
• The Challenge: While MTT had previously been proven sound and canonical (for closed terms), it remained an open question whether it admitted a normalization algorithm. Without normalization, type checking (deciding if two terms are definitionally equal) is undecidable.
• Specific Obstacles:
  • MTT has a complex substitution structure inherited from its underlying 2-categorical mode theory.
  • Standard normalization-by-evaluation (NbE) proofs are notoriously difficult for modal theories because they require intricate logical relations and struggle with the "strict equations" imposed by the 2-categorical structure.
  • Previous attempts to prove metatheoretic properties for MTT often required restricting the theory (e.g., adding specific equalities like $1.{\mu} = 1$) to make proofs tractable.

2. Methodology: Multimodal Synthetic Tait Computability (MSTC)

The author develops a novel proof technique combining Artin gluing with Synthetic Tait Computability (STC), extended to handle multiple modes.

A. From Gluing to Synthetic Gluing

Instead of defining a normalization algorithm explicitly and proving its properties (soundness, completeness, idempotence) separately, the paper constructs a gluing model of MTT.

• Artin Gluing: The proof constructs a category $\text{Gl}(F)$ by gluing a category of syntactic contexts to a category of semantic predicates. Objects in this category are triples $(C, D, f)$ representing a context $C$ equipped with a proof-relevant predicate $f$.
• Synthetic Tait Computability (STC): Following Sterling and Harper, the author works internally within the language of the glued topos. This avoids the "strict equations" that plague external gluing proofs.
  • The internal language includes lex idempotent monads ($\#$ and $\flat$) that allow the separation of "computable" (syntactic) and "semantic" parts of the model.
  • A realignment axiom is used to adjust isomorphic structures to satisfy strict equality requirements, allowing the construction of the model using general categorical theorems rather than explicit, tedious calculations.

B. Extension to Multimodal Settings (MSTC)

Standard STC works for a single topos. MTT, however, involves a network of categories (modes) connected by adjoints.

• The Innovation: The author generalizes STC to Multimodal Synthetic Tait Computability (MSTC).
• Mechanism: The proof constructs a glued cosmos (a network of locally cartesian closed categories) where each mode is equipped with STC structure ($\#$, $\flat$, realignment).
• Key Insight: The modalities of MTT commute with the STC monads ($\#$ and $\flat$). This ensures that the "computational" structure required for normalization is preserved across mode transitions.

C. The Normalization Cosmos

The core of the proof is the construction of a specific model called the Normalization Cosmos ($\mathcal{G}$):

1. Base: It is built by gluing the category of renamings (substitutions up to definitional equality) to the syntactic model of MTT.
2. Structure: $\mathcal{G}$ is equipped with a projection $\pi_0: \mathcal{G} \to \mathcal{S}$ (where $\mathcal{S}$ is the syntactic model).
3. Internal Logic: Inside $\mathcal{G}$, types are defined as pairs consisting of a syntactic type code and a proof-relevant predicate (the "Tait computability" predicate) that tracks which terms have normal forms.
4. Reification: The proof defines a reify operation that maps elements of the model (terms with predicates) back to syntactic normal forms.

3. Key Contributions

1. First Normalization Algorithm for MTT: The paper provides the first proof that MTT admits a normalization algorithm for the full suite of connectives (dependent sums, products, identity types, universes, and modal types).
2. Decidability of Type Checking: It establishes that type checking in MTT is decidable, provided that equality in the underlying mode theory (modes, modalities, and 2-cells) is decidable.
3. Generalization of STC: It successfully extends Synthetic Tait Computability to a multimodal setting, demonstrating that MTT itself is a suitable metalanguage for proving metatheorems about MTT.
4. Handling Crisp Induction: The proof is shown to be modular; it can be extended to support crisp induction principles (a modal induction rule) without collapsing, provided the underlying modal extensionality holds.

4. Main Results

• Theorem 6.4 (Normalization): There exists a function $nf_\Gamma(M, A)$ that maps any well-typed term to a normal form such that:
  • Soundness: The decoded normal form is definitionally equal to the original term.
  • Completeness: If two terms are definitionally equal, their normal forms are syntactically identical.
• Corollary 6.10 (Decidability): If the mode theory is decidable, then type checking in MTT is decidable.
• Corollary 6.9 (Injectivity): Type constructors in MTT are injective (e.g., if $A \to B = C \to D$, then $A=C$ and $B=D$).
• Corollary 6.11 (Canonicity): The proof implies canonicity for closed terms (e.g., closed terms of type bool reduce to tt or ff) without requiring the artificial equality $1.{\mu} = 1$ used in previous work.

5. Significance

• Theoretical Foundation: This work resolves a major open problem in modal type theory, providing a rigorous foundation for MTT as a general framework. It confirms that the flexibility of MTT does not come at the cost of losing fundamental metatheoretic properties like normalization.
• Practical Implementation: By reducing type checking to the decidability of the mode theory, the paper paves the way for implementing generic MTT proof assistants. Any specific modal calculus (like guarded recursion) instantiated via MTT automatically inherits a type-checking algorithm.
• Methodological Advancement: The shift from "free-hand" NbE proofs to Synthetic Tait Computability represents a significant simplification in proving metatheorems for complex type theories. It demonstrates that working internally within a glued topos can handle the intricate substitution structures of multimodal theories more elegantly than external logical relations.
• Modularity: The proof's ability to accommodate crisp induction principles suggests that MSTC is a robust framework for future extensions of modal type theories, including those involving higher-dimensional structures or more complex modal logics.

In summary, Gratzer proves that MTT is not just a syntactic framework but a fully computable system, using a sophisticated blend of category theory (gluing) and type theory (synthetic methods) to tame the complexity of multimodal substitutions.