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.
The type checker operates over a term syntax comprising:
Universe i
: Type universes with level i ∈ ℕ
.Pi (x, A, B)
: Dependent function, where A : Universe i
and B : Universe j
under x : A
.
Lam (x, A, t)
: Lambda abstraction with totality enforced.
App (f, a)
: Function application.Sigma (x, A, B)
: Dependent pair types.
Pair (a, b)
, Fst p
, Snd p
construction and projections.Id (A, a, b)
: Identity type, with Refl
a and J
eliminator.The typing judgment Γ ⊢ t : T
is defined via infer
and check
functions,
with definitional equality Γ ⊢ t = t'
implemented via equal
.
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 *)
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.
Var x
are equal if names match; universes Universe i
if levels are identical.App (f, arg)
requires equality of function and argument.
Pi (x, a, b)
compares domains and codomains, adjusting for variable renaming via substitution.
Inductive d
checks name, level, and parameters.
Constr
and Elim
compare indices, definitions, and arguments/cases.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.
lookup_var
Retrieve a variable’s type from the context. Context are the objects in the Substitutions categories.
ctx
for (x, ty)
using List.assoc
.Some ty
if found, None
otherwise.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
.
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.
Var
: Replaces x
with s
, leaves others unchanged.Pi/Lam
: Skips substitution if bound variable shadows x
, else recurses on domain and body.App/Constr/Elim
: Recurses on subterms.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_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).
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_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 that t
has type ty
.
Lam
: Ensures the domain is a type, extends the context, and checks the body against the codomain.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.
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.
App (Lam, arg)
: Substitutes arg into the lambda body (β-reduction).App (Pi, arg)
: Substitutes arg into the codomain (type-level β-reduction).App (f, arg)
: Reduces f, then arg if f is unchanged.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
.
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.
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:
Nat
normalizes
to zero
or succ n
[Martin-Löf, 1984]. Per’s normalize achieves strong normalization—every term reduces to a
unique normal form—thanks to CIC’s strict positivity [Coquand & Paulin-Mohring, 1990]. Totality follows: all
well-typed functions terminate, as seen in list_length reducing to succ (succ zero)
.Γ ⊢ t : T
and infer t = t'
, then Γ ⊢ t' : T
;
2) No t
exists such that Γ ⊢ t : Id (Universe 0, Universe 0, Universe 1)
.Γ ⊢ 𝑡 : T
, then infer Δ Γ 𝑡 = T
or check Δ Γ 𝑡 T
holds under suitable Δ
.equal Δ Γ t t'
terminates, reflecting normalize’s partial eta and beta reductions in normnalize
.Inductive d : Universe i
, each Constr (j, d, args)
is total;
2) For t : T
with Ind
or J
, reduce t
terminates;
3) For Lam (x, A, t) : Pi (x, A, B)
, reduce (App (Lam (x, A, t), a))
terminates for all a : A
;
4) normalize Δ Γ t
terminates.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].
infer
and check
terminate with a type or TypeError
.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
>
[9]. Martin-Löf, P. Intuitionistic Type Theory. 1980.
[10]. Thierry Coquand. An Algorithm for Type-Checking Dependent Types. 1996.
[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.
Namdak Tonpa