graded_mltt.md

Graded MLTT

The system below is a candidate for a novel approach to strong normalization, it is effectively a graded version of MLTT with Type : Type, such that every variable can be used G times, this is also true for usage while constructing types.

The arguments for termination are:

• every beta in the non-erasable fragment consumes a lambda
• constructing types is in the non-erasable fragment
• an infinite type would require infinite lambdas
• no infinite type, implies in termination of the erasable fragment

Definitions

Term, M, N, K, A, B, G, H ::=
  | 0 | 1 | G + H | G * H
  | Grade | Type | Π(a : A $ G) -> B
  | x | λ(a : A $ G) => K | M(N)

// context operations
(Γ, a : A $ G) + (Δ, a : A $ H) == (Γ + Δ), a : A $ (G + H)
(Γ, a : A $ G) * H == (Γ * H), a : A $ (G * H)

// inference rules
------------------------
(Γ * 0) |- Grade : Type

-----------------------
(Γ * 0) |- Type : Type

-------------------
Γ * 0 |- 0 : Grade

-------------------
Γ * 0 |- 1 : Grade

Γ |- G : Grade  Δ |- H : Grade
--------------------------------
Γ + Δ |- G + H : Grade

Γ |- G : Grade  Δ |- H : Grade
------------------------------
Γ + Δ |- G * H : Grade

---------------------------
(Γ * 0), x : A $ 1 |- x : A

// H is the usages in the subject-type
Γ |- A : Type  Δ |- G : Grade  Φ, a : A $ H |- B : Type
-------------------------------------------------------
Γ + Δ + Φ |- Π(a : A $ G) -> B : Type

Γ |- A : Type  Δ |- G : Grade  Φ, a : A $ G |- K : B
--------------------------------------------------------------
(Γ * 0) + (Δ * 0) + Φ |- λ(a : A $ G) => K : Π(a : A $ G) -> B

Γ |- M : Π(a : A $ G) -> B  Δ |- N : A
--------------------------------------
Γ + (Δ * G) |- M(N) : B{a := N}