Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report

Joris Ceulemans, Andreas Nuyts, Dominique Devriese

TL;DR

This report contains a full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2, including many rules for $\sigma$-equivalence and a description of all rules that have been omitted.

Abstract

This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2, including many rules for $σ$-equivalence and a description of all rules that have been omitted. Furthermore, we present completeness and soundness proofs of the substitution algorithm in full detail. These can be found in Sections 4 and 5 respectively. In order to make this document relatively self-contained, we also include a description of Substitution-Free Multimode Type Theory (SFMTT) in Section 3.

A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report

TL;DR

This report contains a full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2, including many rules for -equivalence and a description of all rules that have been omitted.

Abstract

This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2, including many rules for -equivalence and a description of all rules that have been omitted. Furthermore, we present completeness and soundness proofs of the substitution algorithm in full detail. These can be found in Sections 4 and 5 respectively. In order to make this document relatively self-contained, we also include a description of Substitution-Free Multimode Type Theory (SFMTT) in Section 3.
Paper Structure (23 sections, 32 theorems, 14 equations, 11 figures)

This paper contains 23 sections, 32 theorems, 14 equations, 11 figures.

Table of Contents

  1. Introduction
  2. WSMTT: Full Description & σ-equivalence
  3. Extrinsically typed syntax
  4. σ-equivalence
  5. SFMTT: Full Description
  6. Intrinsically Scoped Syntax for SFMTT
  7. Applying SFMTT Substitutions
  8. Relating WSMTT and SFMTT
  9. Completeness
  10. Observational Equivalence of SFMTT Substitutions
  11. Definition & Proof Technique (Part 1)
  12. Mixed Sequences of Atomic Rensubs
  13. Action of Lifted Atomic Rensubs on Variables
  14. Lifted Atomic Rensubs and π
  15. Proof Technique (Part 2)
  16. ...and 8 more sections

Key Result

Theorem 1

If we can deduce $\hat{\Gamma} \vdash_{\!\mathsf{ws}{}} t\equiv^\upsigma s \ \mathsf{expr} \, \textcolor{gray}{@ \, m}$, then we have that $\left\llbracket t \right \rrbracket = \left\llbracket s \right \rrbracket$.

Figures (11)

  • Figure 1: Definition of scoping contexts and lock telescopes. This figure is identical to Figure 3 in the paper.
  • Figure 2: Definition of WSMTT expressions (partial) and substitutions (full). This figure is identical to Figure 4 in the paper.
  • Figure 3: Remaining constructors for WSMTT expressions, not covered in the paper
  • Figure 4: Definition of $\upsigma$-equivalence for WSMTT expressions and substitutions (see the overview for which rules are omitted, figure continues on the next page).
  • Figure 5: Definition of $\upsigma$-equivalence for WSMTT expressions and substitutions (continued).
  • ...and 6 more figures

Theorems & Definitions (35)

  • Theorem 1
  • Definition 2: Observational equivalence
  • Proposition 3
  • Proposition 4
  • Lemma 5
  • Lemma 6
  • Lemma 7
  • Corollary 8
  • Lemma 9
  • Lemma 10
  • ...and 25 more