sestini2023-inductive-inductive-thesis

Title: Bootstrapping Extensionality

Outline

Overview

Martin-Löf Type Theory

Definition

Martin-Löf Type Theory (MLTT) is an Intuitionism, predicative dependent type theory introduced by Per Martin-Löf.

Abstract

MLTT designates the family of type theories derived from the foundational work of Per Martin-Löf. It integrates logic and computation through the propositions-as-types correspondence, functioning as the basis for modern dependently typed languages and proof assistants.

The Logical Framework

The presentation of MLTT is frequently mediated by a core Logical Framework. The base framework contains dependent function types ($\Pi$-types) and a few structural constructs. We formulate extensions to the base system by introducing new type formers as constants reflecting into a Tarski universe $\mathcal{U}$. This isolates the generic machinery of binding and substitution from the specific rules of individual type formers.

Inductive Types and Pattern Matching

Implementations utilizing the Logical Framework, notably the Alf system, permit the definition of types within a universe simply by declaring their constructors. We then construct functions over these inductive types via dependent pattern matching on the constructors, rather than relying exclusively on primitive recursors or elimination constants.

References

• martin-lof1975-intuitionistic-predicative
• martin-lof1984-mltt
• nordstrom-petersson-smith1990-mltt
• magnusson1994-alf-mltt
• hoffmann1997-dependent-types

Link to original

Definition

The identity type (aka path type or propositional equality) represents the concept of equality between two terms of the same type. For a type $A$ and terms $a,b:A$, the type is denoted $a{=}_{A}b$ or ${\mathsf{Id}}_A(a,b)$. Unlike definitional equality, which is a judgement, the identity type is a type within the theory whose terms represent witnesses of equality.

Link to original

Definitional Equality

Definition

In type theory, definitional equality (or judgmental equality) is a metatheoretic relation between terms of the same type, denoted by the metatheoretic judgment $\Gamma ⊢a\equiv b:A$. It represents equality by definition or computational reduction. If two terms are definitionally equal, they are treated as identical by the type checker.

Equivalence Relation

Definitional equality forms an equivalence relation on well typed terms, satisfying reflexivity, symmetry, and transitivity.

$$\frac{\Gamma ⊢a:A}{\Gamma ⊢a\equiv a:A}\frac{\Gamma ⊢a\equiv b:A}{\Gamma ⊢b\equiv a:A}\frac{\Gamma ⊢a\equiv b:A\Gamma ⊢b\equiv c:A}{\Gamma ⊢a\equiv c:A}$$

Congruence

It satisfies congruence, meaning equality is preserved under all type formers and term formers. Applying definitionally equal functions to definitionally equal arguments yields definitionally equal results.

Computational Rules

Definitional equality is generated by structural rules and computational rules, primarily beta reduction and eta conversion.

Beta Reduction

Beta reduction specifies the computational behavior of an eliminator applied to a constructor. For function types, applying a lambda abstraction to an argument definitionally reduces to substitution.

$(\lambda x.t)u\equiv t[u/x]$

Eta Conversion

Eta conversion enforces uniqueness principles for elements of a type. For function types, it asserts a function is definitionally equal to its pointwise application.

$f\equiv \lambda x.fx$

Relation to Propositional Equality

Definitional equality is a metatheoretic property of the deductive system. Propositional equality is represented internally by the identity type.

By the reflection rule, definitional equality implies propositional equality. If $\Gamma ⊢a\equiv b:A$, we can construct a term of type $a{=}_{A}b$ using the reflexivity constructor.

The converse holds in extensional type theory but fails in intensional type theory and homotopy type theory.

Decidability

In standard intensional type theory, definitional equality is designed to be strongly normalizing and decidable, guaranteeing algorithmic type checking. In extensional systems, definitional equality is undecidable because it collapses with propositional equality.

References

hott2013-book

References

hott2013-book

In Higher Observational Type Theory, definitional equality is where syntactically one term can be replaced by another simply by substituting definitions.

Link to original

Document