per

Per Martin-Löf: Intuitionistic Type Theory

Abstract

Per is a theorem prover implemented in OCaml, constitutes a MLTT-80 core for a dependently-typed lambda calculus, constrained to exclude pattern matching, let-bindings, implicit arguments. It encompasses universes, dependent products Pi, dependent pairs Sigma, identity types Id, and 0, 1, 2, W types for well-founded definitions. Its mathematical properties, focusing on correctness, soundness, totality, canonicity, decidability and related attributes relevant to formal mathematics are being analyzed.

Introduction

The type checker operates over a term syntax comprising:

The typing judgment Γ ⊢ t : T is defined via infer and check functions, with definitional equality Γ ⊢ t = t' implemented via equal.

Syntax

type term =
  | Var of name | Universe of level
  | Pi of name * term * term | Lam of name * term * term | App of term * term
  | Sigma of name * term * term | Pair of term * term | Fst of term | Snd of term
  | Id of term * term * term | Refl of term
  | J of term * term * term * term * term * term  (* J A a b C d p *)

Semantics

Syntactic Equality equal

Structural equality of terms under an environment and context.

The function implements judgmental equality with substitution to handle bound variables, avoiding explicit α-conversion by assuming fresh names (a simplification over full de Bruijn indices [3]). The recursive descent ensures congruence, but lacks normalization, making it weaker than CIC’s definitional equality, which includes β-reduction.

Theorem. Equality is reflexive, symmetric, and transitive modulo α-equivalence (cf. [1], Section 2). For Pi (x, a, b) and Pi (y, a', b'), equality holds if a = a' and b[x := Var x] = b'[y := Var x], ensuring capture-avoiding substitution preserves meaning.

Context Variables Lookup lookup_var

Retrieve a variable’s type from the context. Context are the objects in the Substitutions categories.

Theorem: Context lookup is well-defined under uniqueness of names (cf. [1], Section 3). If ctx = Γ, x : A, Δ, then lookup_var ctx x = Some A.

Substitution Calculus subst

Substitute term s for variable x in term t. Substitutions are morphisms in Substitution categorties.

The capture-avoiding check if x = y prevents variable capture but assumes distinct bound names, a simplification over full renaming or de Bruijn indices. For Elim, substituting in the motive and cases ensures recursive definitions remain sound, aligning with CIC’s eliminator semantics.

Theorem. Substitution preserves typing (cf. [13], Lemma 2.1). If Γ ⊢ t : T and Γ ⊢ s : A, then Γ ⊢ t[x := s] : T[x := s] under suitable conditions on x.

Infer Equality Induction infer_J

Ensuring J (ty, a, b, c, d, p) has type c a b p by validating the motive, base case, and path against CIC’s equality elimination rule.

The infer_J function implements the dependent elimination rule for identity types in the Calculus of Inductive Constructions (CIC), enabling proofs and computations over equality (e.g., symmetry : Π a b : ty, Π p : Id (ty, a, b), Id(ty, b, a)). It type-checks the term J (ty, a, b, c, d, p) by ensuring ty : Universe 0 is the underlying type, a : ty and b : ty are endpoints, c : Π (x:ty), Π (y:ty), Π (p: Id(ty, x, y)), Type0 is a motive over all paths, d : Π (x:ty), c x x (Refl x) handles the reflexive case, and p : Id(ty, a, b) is the path being eliminated. The function constructs fresh variables to define the motive and base case types, checks each component, and returns c a b p (normalized), reflecting the result of applying the motive to the specific path.

Theorem. For an environment env and context ctx, given a type A : Type_i, terms a : A, b : A, a motive C : Π (x:A), Π (y:A), Π(p:Id(A, x, y)),Type_j, a base case d : Π(x:A), C x x (Refl x), and a path p : Id(A, a, b), the term J (A, a, b, C, d, p) is well-typed with type C a b p. (Reference: CIC [1], Section 4.5; Identity Type Elimination Rule).

Type Inference infer

Infer the type of term t in context ctx and environment env.

For Pi and Lam, universe levels ensure consistency (e.g., Type i : Type (i + 1)), while Elim handles induction, critical for dependent elimination. Note that lambda agrument should be typed for easier type synthesis [13].

Check Universes check_universe

Ensure t is a universe, returning its level. Infers type of t, expects Universe i.

This auxiliary enforces universe hierarchy, preventing paradoxes (e.g., Type : Type). It relies on infer, assuming its correctness, and throws errors for non-universe types, aligning with ITT’s stratification.

Theorem: Universe checking is decidable (cf. [13]). If ctx ⊢ t : Universe i, then check_universe env ctx t = i.

Check check

Check that t has type ty.

The function leverages bidirectional typing: specific cases (e.g., Lam) check directly, while the default case synthesizes via infer and compares with a normalized ty, ensuring definitional equality (β-reduction). Completeness hinges on normalize terminating (ITT’s strong normalization) and equal capturing judgmental equality.

Theorem. Type checking is complete (cf. [1], Normalization). If ctx ⊢ t : T in the type theory, then check env ctx t T succeeds, assuming normalization and sound inference.

One-step β-reductor reduce

Perform one-step β-reduction or inductive elimination.

The function implements a one-step reduction strategy combining ITT’s β-reduction with CIC’s ι-reduction for inductives. The App (Lam, arg) case directly applies substitution, while Elim (Constr) uses apply_case to handle induction, ensuring recursive calls preserve typing via the motive p. The Pi case, though unconventional, supports type-level computation, consistent with CIC’s flexibility.

Theorem. Reduction preserves typing (cf. [8], Normalization Lemma, Subject Reduction). If ctx ⊢ t : T and t → t' via β-reduction or inductive elimination, then ctx ⊢ t' : T.

Normalization normalize

This function fully reduces a term t to its normal form by iteratively applying one-step reductions via reduce until no further changes occur, ensuring termination for well-typed terms.

This function implements strong normalization, a cornerstone of MLTT [9] and CIC [1], where all reduction sequences terminate. The fixpoint iteration relies on reduce’s one-step reductions (β for lambdas, ι for inductives), with equal acting as the termination oracle. For plus 2 2, it steps to succ succ succ succ zero, terminating at a constructor form.

Theorem. Normalization terminates (cf. [1]. Strong Normalization via CIC). Every well-typed term in the system has a ormal form under β- and ι-reductions.

Conclusion

Per’s elegance rests on firm theoretical ground. Here, we reflect on key meta-theorems for Classical MLTT with General Inductive Types, drawing from CIC’s lineage:

Soundness

Completeness

Canonicity

Totality

Consistency

The system is logically consistent, meaning no term t exists such that Γ ⊢ t : ⊥. This is upheld by normalization and the absence of paradoxes such as Girard’s [Girard, 1972].

Decidability

Artefact

https://per.groupoid.space/

  🧊 MLTT Theorem Prover version 0.5 (c) 2025 Groupoїd Infinity

For help type `help`.

Starting proof for: Π(n : Nat).Nat
Goal 1:
Context: []
⊢ Π(n : Nat).Nat

1 goals remaining
>

MLTT

[9]. Martin-Löf, P. Intuitionistic Type Theory. 1980.
[10]. Thierry Coquand. An Algorithm for Type-Checking Dependent Types. 1996.

PTS

[11]. N. G. de Bruijn. Lambda Calculus Notation with Nameless Dummies. 1972.
[12]. J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures. 1972.
[13]. Thierry Coquand, Gerard Huet. The Calculus of Constructions. 1988.

Author

Namdak Tonpa