This is a notes file which will hopefully evolve towards being a proper blog post. The formalization of some of the concepts below are very much WIP.
Usually for a system to be considered logically consistent, it should avoid paradoxes, in terms of programming languages and theorem provers, those often translate to infinite loops.
I will be talking about type systems, you can figure out how to translate those to languages.
This is the case because in most type systems, there is no term in head normal form with the type of False, meaning the only way to get a term of type False is to have a term that is is not in head normal form.
Systems like the untyped lambda calculus, are known to not be normalizing, not even weak normalizing.
While systems like Gödel System T, a simply typed lambda calculus with natural numbers, are known to be strongly normalizing and logically consistent.
((x) => x(x))((x) => x(x));Often weak normalization is enough.
This is the original problem that inspired Alonzo Church(VERIFY THIS) to add types to the Lambda Lalculus, as in, the purpose of adding a type system to the LC, originally was to achieve logical consistency, which as explained above is mostly about termination.
For the lambda calculus with simple types, Alan Turing provided a proof of weak normalization by redex degree(NOTES HERE), and for the lambda calculus with impredicative polymorphic types(System F), Jean-Yves Girard provided a proof of weak normalization by reducibility candidates. Both can be checked at the book Proof and Types.
The core of the STLC proof relies on the size of the type of a term, such that every beta reductions, decreases the size of the type, even thought it potentially increases the size of the term, eventually the type size will be so small that all the reductions must decrease the size of the term, and eventually reach a normal form.
This in a sense is a type-based termination technique, finite types, implying in finite terms. The iterated approach is the predicative hierarchy of universes, Type(0) : Type(1) : Type(2) : ..., such that effectively the level becomes the external thing decreasing, as in, sometimes the type size does increase, but the level of the type decreases and at Type(0) the type is an STLC type, and thus the term size is finite.
Another form of "mostly" type-based termination is the impredicativity of System F, System Fω and the Calculus of Constructions, where the type size can increase, but somehow(seriously we don't know how), it only happens in such a way that eventually it goes down and there is no more reductions, this is often proven by reducibility candidates, which doesn't provide a great intuition on why it terminates, but it does.
Usually predicativity is better behaved, you can see that extending the STLC to a hierarchy was a "small" change to the proof, this is also true for most common features that you may want to introduce, like decidable subtyping.
Those are also inspired by the set-theory approaches and naively fit in that paradigm.
Sadly, both System U and systems with Type : Type are known to not be terminating, check Hurken's paradox.
Additionally negative recursive types are bad.
A fundamental alternative to this, is term-based / context-based termination, termination where by some restriction to the terms, everything is guaranteed to terminate. The easiest one to visualize is the Untyped Linear Lambda Calculus.
Term, M, N, K ::=
| x | (x) => | M(N)
((x) => K)(N) -> K{x := N} (count(x, K) == 1)Note that this is a strong normalizing system, inspite of the lack of types, as such adding any traditional form of typing to this system, including Type : Type and even negative recursive types, still preserves strong normalization and rejects Hurken's paradox.
The STLC doesn't have polymorphism, that is a huge restriction.
Usually predicativity is better behaved, you can see that extending the STLC to a hierarchy was a "small" change to the proof, this is also true for most common features that you may want to introduce, like decidable subtyping.
But impredicativity is much stronger and includes some terms that are usually never going to have "the proper type" in a predicative setting, as an example the id function id : (A : Type) -> (a : A) -> A in an impredicative setting this would be allowed id(#typeof(id))(id).
On the term-based side, like the Linear Lambda Calculus, it is much weaker and cannot describe a lot of common programs, sure you may be able to do the id(Id)(id) : Id issue above, but it's really not an ergonomic way of writing programs.
A reasonable extension to the Linear LC would be to add grading, a multiplier telling how many times variables can be used, this multiplier is called a Grade(WHY????), but which is honored semantically, as in this function would be using 2 copies of x instead of one (f, x) => f(x $ 2). I'm calling this one for now the Simply Graded Lambda Calculus.
But even the Simply Graded LC, while more ergonomic, it's still quite weak, in terms of common programming issues, those systems cannot do the traditional for loop, aka a fold over any natural.
So traditional systems go with a type-based approach, usually a predicative hierarchy and optionally an impredicative universe, often restricted to mere propositions, like in Rocq and Lean 4.
Introducing some features like universe polymorphism to mitigate the issues related to the limited polymorphism.
Traditionally also systems add inductive types with large elimination, the ability of doing elimination from a universe to a higher one, as an example, if Bool : Type(0) you can then do things like b ? Bool : Nat, which normally would fail, as the inputs cannot have the same size as the "entity" being eliminated, this clearly extends the "power" of the system, but inductive types were historically thought to be needed anyway, as induction was thought to not be derivable otherwise, so killing two birds with one stone.
Eeeeh, not really, there are still many issues, especially around the complexity of such systems, inductive types as an example is a very complex feature when compared to the rest, tracking universes and universe polymorphism is also more work and less ergonomic for users.
In a sense, there is never complete universal quantification in traditional systems, a function that works for all the types, no exceptions, even on impredicative systems.
Additionally the inductive types without large elimination were shown to be derivable by me last year at REPLACE_THIS_BY_LINK in the CoC with Sigma + Identity types and given an impredicative equality, even in the predicative setting, meaning the whole inductive type feature is then limited to be about large elimination.
And large elimination is not even a needed feature in the term-based settings, given that you can have Type : Type and as such, there is only a single universe, meaning (A : Type) -> B means forall types, no exceptions.
In a sense it's weird that large elimination can be added, the termination of the system was previously dependent on the size of the type, but it clearly bypasses the size of the type, but it works, and it's even weirder that it works on impredicative settings, like the original Calculus of Inductive Constructions.
Not quite, in a sense by studying large elimination, it's made clear that something else can be done, this is inspired by some work at Monnier's Impredicative Universe Polymorphism.
Especially if we consider things like elimination of the booleans by using Church Encoding, then b ? (M : A) : (N : A) is the same as b(A)(M)(N), meaning that some functions, can definitely be done in such a way that it would be safe to instantiate them with any universe.
In this specific case, given that the church booleans behavior, the termination is guaranteed, because the boolean is literally just returning one of the two terms, as such, the termination of this expression is strictly dependent on the termination of the two terms.
This pattern works for pretty much all the inductive types, for n(A)(M : A)(N : (a : A) -> A), aka the fold over the naturals, there is a fixed number of iterations encoded in the n and there is nothing preventing the original program to be doing N(N(N(N(...)))), as such, the naturals can only create terms that were already possible before(this is not a proper argument).
In a sense, this feels like term-based, we're allowing this to work, because the set of terms that the inductive types can describe, all include such property, if you allowed this for every type it can have additional terms, "bad" terms, which then would allow to make infinite loops.
Additionally, term-based can get quite fancier. As an example by getting the Linear LC and adding the natural numbers, you're still(NOT PROVED) describing a terminating system, but it can now encode a bunch of other things, including "many copies" of the same term.
Similar to this, is that you can extend the Simply Graded Lambda Calculus to a Polymorphic Graded Lambda Calculus, which is a quite more useful system, but termination is still up to debate.
The Polymorphic Graded LC, suffers from some problems, #(M, 0) still must be a closed term, otherwise there is a straightforward paradox, this is especially annoying when extended with types, making it such that #(M, 0) is not the traditional "erasability" argument, which is very useful for typing purposes.
((x) => #(x(x), 0))((x) => #(x(x), 0))Additionally, two terms that would have the same type, now may have different types, (n : Nat $ 2) => n + n and (n : Nat $ 1) => n, this can be mitigated especifically for inductive types, given the Filinski’s result, as in, you can always do things like n(Nat $ 2)(zero, succ) meaning that Nat $ 2 == Nat $ 1 safely.
Note that even in term-based systems, the inductive types are still special somehow, but here those are not meta-level properties, but instead internal properties of the system.
And the erasability fragment can be improved by tweaking the type formers, effectively a type like (x : A $ 0) -> T instead of the x inside of T being A $ 0 it is just A, potentially even A $ ∞, meaning that even if it's something like a function it could potentially work.
The two types issues can also be further mitigated by existential grading, instead of (a : A) -> B a function can then be represented by [G : Grade, (a : A $ G) -> B], meaning that the caller must be able to provide A for any Grade.
This is also made quite a bit more ergonomic with generalization and the polymorphic grades, mostly top-level definitions get to be always of type (G : Grade) -> T, in a similar way to how universe polymorphism works, the main benefit is that those values are first-class.
A potentially interesting approach, is the one where types are not considered erasable themselves and as such, creating a type will consume a copy of the type, meaning that (A : Type $ 0) => (x : A) -> A doesn't work, as the return is consuming A but there are no copies of A.
You may still be able to do (A : Type $ 0) -> (x : A) -> A, given the special rule of type formers explained above. Additionally Type can be treated as Data like Nat and Type $ 1 == Type $ 2, such that the counter only matters if it's 0 or not.
This produces an interesting result, every type constructor, is still linear and cannot be duplicated, meaning that to produce any potentially infinite type, would require you to have infinite instances of a type constructor, as the f(f) trick is the only way possible here, which is impossible given the grading properties.
That would mean that the type-level is finite, but if the type-level is finite, then the restriction to #(M, G) being closed can be weaken, the paradox above is not a problem anymore, because it would require an infinite type.
Additionally or alternatively, it may be the case that the type former for the many modality, A $ G could itself be consuming G. Which is annoying, but again, both Type and Grade are data, they can be safely duplicated or erased, the only operation that is not permitted is to produce a A $ 1 from a A $ 0.
Sadly such a reliance on the type-level being finite, implies that any recursive types must be restricted, the bright side is that given that we have the naturals already, we're mostly getting the same expressiveness, just an uglier encoding.
For the Simply Graded LC, there is a trivial measure function, but for the Polymorphic Graded LC, I don't know any straightforward measure function.
There is some handwavy intuition that the Polymorphic Graded LC is equivalent to the Linear LC + Naturals, which means if the latter is strong normalizing, so is the former.
I still don't have proofs for the termination of the Linear LC + Naturals in the presentation below, but I'm working on it, in a sense it would be weird if it wasn't strong normalizing, so I'm optimistic.
The further extension where grading is applied to types, is considerably more complex, but the intuition above feels right to me, still it would require quite a bit of work, as this requires term-based and type-based termination, just in different places.
Mostly I would like to imagine a different approach to designing theorem provers, let's call it the Calculus of Graded Constructions.
Two universes, Type the type of all linear types, Data the type of all data types.
Pi, Sigma, Identity, Grade and Many, all other inductive types are derivable, same for induction-induction, as a bonus there is likely additional inductive types, types that would be unsafe, or wouldn't be possible.
For daydreaming, the diagonal argument doesn't close, so a self-interpreter doesn't trivially leads to the second incompleteness theorem and I'm not sure on the status of the first incompleteness theorem.
I think an intuitionistic universe cannot be defined, simply because in terms of ordinal analysis, even the complete system doesn't seems to be above ε₀ and weirdly I don't have any idea how to raise it further.
But it may be possible to extend the system with an intuiotinistic universe to recover the standard intuitionistic logics, such that you endup with a complete theorem prover core, with the additional inductive types and linearity tracking properly supported.
univalence, UIP in the same universe??? While the proof-irrelevant equality is considered a piece of data as it could easily be duplicated, an univalent equality cannot be duplicated, simply because that would imply duplicating an isomorphism, which is made of functions, which cannot be duplicated, as such, this must be reflected in the eliminator and the univalent equality will not be able to transport, through the proof-irrelevant equality, as it would require A $ ∞ in some places.
Grade, G ::=
| 0 | 1 + G
Term, M, N, K ::=
| x | (x) => K | M(N)
| #(M, G) | #x = N; K
((x) => K)(N) -> K{x := N} (count(x, K) == 1)
#x = #(M, G); K -> K{x := M} (count(x, K) == G) & (fv(M) == ∅)
// a measure function
F(x) == 0
F((x) => K) == 1 + F(K)
F(M(N)) == F(M) + F(N)
F(#(M, G)) == 1 + (G * F(M))
F(#x = N; K) == F(N) + F(K)Term, M, N, K, G ::=
| x | (x) => K | M(N)
| 0 | 1 + G
| #(M, G) | #x = N; K
((x) => K)(N) -> K{x := N} (count(x, K) == 1)
#x = #(M, G); K -> K{x := M} (count(x, K) == G) & (fv(M) == ∅)Term, M, N, K ::=
| x | (x) => K | M(N)
| 0 | 1 + M | rec(M, N, K)
((x) => K)(N) |-> K{x := N} (count(x, K) == 1)
// subst doesn't go through N in rec
rec(0, N, K) |-> K
rec(1 + M, N, K) |-> N(rec(M, N, K)) (fv(N) == ∅)Term, M, N, K, G ::=
| Type | Data | x
| Grade | 0 | 1 | M + N | M * N
| A $ G | #(M, G) | #x = N; K
| (a : A) -> B | (x) => K | M(N)
| [a : A, B] | [M, N] | M.0 | M.1
| M == N | refl(M) | M.J(C, K)
Data : Data;
Type : Data;
Grade : Data;
(A : Type) $ (G : Grade) : Type;
(A : Data) $ (G : Grade) : Data;
((a : A) -> B) : Type;
[a : (A : Data), (B : Data)] : Data;
[a : A, B] : Type; // otherwise
M == N : Data;
// such that you still get the eta
M.0 : [a : A, B $ 0]
M.1 : [a : A $ 0, B]
eta(x : [a : A, B]) = [x.0, x.1];
//
Id : Type = (A : Type) -> (a : A) -> A;
(id : Id $ 2) = (A : Type) => (a : A) => a;
id2 = id(Id)(id);
(p : M == N).J(C : (a : A) -> Type $ 0, K : A)