A Canonical Form for Universe Levels in Impredicative Type Theory

A lot of type theories are based on extensions of Church’s simply-typed $\lambda$-calculus which does not permit expressing terms over arbitrary types (preventing for instance to talk about all the groups). To address this, Martin-Löf introduced a dependent type theory with a type of all types [25], and later, to avoid paradoxes such as Girard’s one [12, 20], introduced a distinction between small types and large types (which are types containing types, and are also called universes) [27].

In the same years, Girard and Reynolds independently invented System F, an extension of Church’s simply-typed $\lambda$-calculus with type polymorphism, and even later, Girard presented System $F_{\omega }$ which adds type operators i.e. the ability to quantify over terms to create types.

The Calculus of Constructions [13] introduced by Coquand in his PhD thesis combined features from both Martin-Löf Type Theory and System $F_{\omega }$. This system allows quantifying on types or terms to build new types and new terms, and it is the pinnacle of the $\lambda$-cube of Barendregt [4], which classifies type systems depending on the quantification possibilities.

The Calculus of Constructions is an elegant system with strong properties such as normalization and logical consistency. However, quantification over Type is not possible since it makes the system incoherent. This led Coquand to generalize the system with a predicative hierarchy of universes [12], in the same way as predicative Martin-Löf type theory [26]. This new system, which we will call ${\text{CC}}^{\mathrm{\infty }}$, contains a countable sequence of universes ${\text{Type}}_0:{\text{Type}}_1:\mathrm{\cdots }$, where ${\text{Type}}_0$ is the universe of the propositions, the indices being referred to as universes levels.

These logical systems are generalized under the name of Pure Type Systems [5, 6].

$𝒜$ describes the sorts typing ($s_1$ has the type $s_2$ when $(s_1,s_2)\in 𝒜$), and $ℛ$ describes the possible quantifications and their typing rules. The terms are the following, where $s\in 𝒮$ and $x$ ranges an infinite set of variables.

Both ${\text{CC}}^{\mathrm{\infty }}$ and predicative Martin-Löf type theory have a set of sorts indexed over the natural numbers, with for all $i\in \mathbb{N}$, ${\text{Type}}_i:{\text{Type}}_{i+1}$. Their difference resides in their set of rules. These rules permit to type products, so we recall the typing rule for products.

With the aim of building a consistent system, paradoxes such as Girard’s one should be avoided. When Coquand analysed it, he found that a product from Type to Type could not live in Type: it should live in a greater type (hence the distinction between small and large types).

With an infinite hierarchy of universes, this principle remains: a product from ${\text{Type}}_i$ to ${\text{Type}}_j$ should live in a greater universe. Therefore, in the predicative Martin-Löf type theory, the set of rules is $\{{\text{Type}}_i,{\text{Type}}_j,{\text{Type}}_{max(i,j)}\}$. The choice of ${\text{CC}}^{\mathrm{\infty }}$ is different (and does not break the consistency either): a product from ${\text{Type}}_i$ to ${\text{Type}}_0$ lives in ${\text{Type}}_0$, so it follows the rules $\{{\text{Type}}_i,{\text{Type}}_j,{\text{Type}}_{\mathrm{imax}(i,j)}\}$ where $\mathrm{imax}:\mathbb{N}\to \mathbb{N}\to \mathbb{N}$ is defined for all $i,j\in \mathbb{N}$ by $\mathrm{imax}(i,0)=0$ and $\mathrm{imax}(i,j+1)=max(i,j+1)$.

This corresponds to the so-called impredicativity of Prop (hence the name $\mathrm{imax}$ for impredicative max) which notably permits to say that we can quantify over all the propositions and still get a new proposition. Accepting or rejecting impredicativity is a philosophical questioning: some consider that $\mathrm{\Pi }P:\text{Prop}\cdot P\to P$ should be a proposition (which is of course true), while others think that a proposition cannot be created by quantifying over all the propositions.

A PTS can be enriched with universe polymorphism which allows the user to quantify over universes [28, 23, 14]. For instance, it permits declaring simultaneously the identity for all the types of any universes with $\lambda s:𝒮\cdot \lambda A:s\cdot \lambda x:A\cdot x$. This feature adds universe variables to the language of a PTS. In the case of ${\text{CC}}^{\mathrm{\infty }}$, it is equivalent to extend the syntax of the levels with level variables.

The universe polymorphic identity of ${\text{CC}}_{\forall }^{\mathrm{\infty }}$ is the term

We can use it by instantiating the level variable. For instance, $\mathrm{id}\mathrm{\hspace{0.17em}1}\text{Prop}$ is the identity of Prop while $\mathrm{id}\mathrm{\hspace{0.17em}2}{\text{Type}}_1$ is ${\text{Type}}_1$’s one. This instantiation is done throughout substitution functions, which replace a level variable by a level, and valuation functions which replace level variables by integers.

This interpretation through the valuations explains why, even if levels are abstract terms, we defined them with the same symbols $0$, $s$, $max$ and $\mathrm{imax}$ that are used for the natural numbers. Indeed, the ground levels can clearly be identified as the natural numbers and the levels’ semantic, through the valuations, justifies to use the same symbol and permits to see the valuations as functions that realise levels, turning them into ground ones.

Besides, two levels can also be compared using these valuations. They are equivalent if they give the same ground levels through any valuation.

This equivalence shows that universes such as ${\text{Type}}_x$ and ${\text{Type}}_{max(x,x)}$ should be identified. However, it is not obvious to check. It is not syntactic, like it was without universe polymorphism, and the $\mathrm{imax}$ function makes it complicated.

The aim of this paper is to address this problem. Since it is a word problem, a direct solution consists in finding a canonical form and an algorithm which computes the canonical form of a given term. The level equivalence is then checked by syntactic comparison of the canonical form. We follow this path. To do this, we study the 0-$\mathrm{imax}$-successor algebra, and we provide a canonical form for its terms. Besides, this equivalence is decidable by a reduction to Presburger arithmetic, and so we provide an additional motivation to our work.

Our main motivation lies in the interoperability between proof systems. Indeed, it became a big challenge in the research on proof-checking, which aims to avoid the redevelopment of the same proof. Instead of developing translators from each system to another one, logical frameworks propose to define theories in a common language, which makes translation easier.

The $\lambda \mathrm{\Pi }$-calculus modulo rewriting ($\lambda \mathrm{\Pi }/\equiv$) [10] is a logical framework that extends $\lambda \mathrm{\Pi }$ (the simply-typed $\lambda$-calculus with dependent types) with higher-order rewrite rules [16, 29] that can be used to define functions, but also types; terms are then identified modulo $\beta$ and these rewrite rules. The computational part of the type theories can then be represented using the expressiveness of rewrite systems.

The Calculus of Constructions and its subtheories can be expressed in $\lambda \mathrm{\Pi }/\equiv$ [8], and, in [15], Cousineau and Dowek showed how to express some PTS. Therefore, several systems have been encoded in $\lambda \mathrm{\Pi }/\equiv$: HOL-Light [30, 1], Agda [19], Matita [1], but also parts of Rocq [18, 9]. Besides, since there exist multiple implementations of $\lambda \mathrm{\Pi }/\equiv$ such as Dedukti [2], Lambdapi [24], or Kontroli [17], these embeddings have been implemented, leading to effective translations [30, 21, 22].

To define ${\text{CC}}_{\forall }^{\mathrm{\infty }}$ in $\lambda \mathrm{\Pi }/\equiv$, we need to define its levels. It can be done with a type nat together with functions max, and imax, and rewrite rules to define them. This permits to express ${\text{CC}}^{\mathrm{\infty }}$ in $\lambda \mathrm{\Pi }/\equiv$, but the equivalence relation that comes with level variables adds some difficulties.

Indeed, for all term $u$ of ${\text{CC}}_{\forall }^{\mathrm{\infty }}$, let us note $\left|u\right|$ its translation in $\lambda \mathrm{\Pi }/\equiv$, and let us consider a function $f:{\text{Type}}_i\to {\text{Type}}_j$ and a term $t:{\text{Type}}_k$ where $k\equiv i$. Since $ft$ is well-typed, then $\left|ft\right|$ should be well-typed in $\lambda \mathrm{\Pi }/\equiv$. Therefore, $\left|t\right|$ should have the type $\left|{\text{Type}}_i\right|$, whereas it has the type $\left|{\text{Type}}_k\right|$. We deduce that $\left|{\text{Type}}_i\right|$ and $\left|{\text{Type}}_k\right|$ should be convertible types, and then that equivalent levels should be convertible terms.

The 0-$max$-successor algebra is well-studied, and so, some solutions exist in the predicative case. In [31], Voevodsky represented each level as $max(n,n_1+x_1,\mathrm{\dots },n_k+x_k)$ where $n⩾max(n_1,\mathrm{\dots },n_k)$. Then, if there exists $i\ne j$ such that $x_j=x_i$, we simplify the term and keep only $max(n_i,n_j)+x_i$. Therefore, we obtain a minimal representation for the 0-$max$-successor algebra.

In [19], Genestier encoded the universe polymorphism of Agda in $\lambda \mathrm{\Pi }/\equiv$ using a similar idea and a representation modulo associativity and commutativity (for the $max$ symbol). Blanqui gave another presentation of this algebra in [7], with an encoding without matching modulo associativity and commutativity.

The 0-$\mathrm{imax}$-successor algebra is less studied. An encoding is proposed in [3], but it does not fully reflect the equalities; for instance, the levels $max(\mathrm{imax}(x,y),x)$ and $max(x,y)$ are not convertible. Besides, Férey also worked on the encoding of universe polymorphism [18].

Finally, an algorithm to check level inequality, and so level equivalence, is presented in [11], but it does not rely on a canonical form.

We use the same idea presented above in the predicative case: find a subset $E$ of levels such that any level can be represented as $maxU$ with $U\subset E$, and such that $maxU$ is a minimal representation that ensures uniqueness property for any other minimal representation $maxV$:

In the predicative case, $E=\mathbb{N}\cup \{n+x|n\in \mathbb{N},x\in 𝐗\}$; and the minimal representation consists in having one term $n$ (the maximum of two integers can be simplified) and for all $x\in 𝐗$ at most one term $n+x$ since $max(n+x,m+x)=max(n,m)+x$. To obtain the canonical representation, we push the successor symbols inside the $max$, and we obtain $maxU$ with $U\subset E$. Then, $U$ can be simplified by removing $u$ if there exists $v\in U$ such that $v\ne u$ and $u⩽v$, leading to the minimal representation.

This gives us the intuition that we need. The elements of the subset should be very basic and simple in the sense that it is not equivalent to a maximum of other levels.

Section 2 studies the algebra and introduces ${𝐒}_{𝐂}$, a set of basic terms, called canonical sublevels. It turns out that these terms do not have the same expressive power than levels, hence we extend $𝐋$ into $𝐄$, the extended levels. But, each level can be represented as a maximum of elements of ${𝐒}_{𝐂}$; such a maximum is a representation, they will form the set of representations $𝐑$.

Then, in Section 3 we introduce ${𝐑}_{𝐂}$, the set of minimal representations which are representations whose elements are incomparable, and we show that any representation has a unique minimal representation.

Moreover, we will see that ${𝐑}_{𝐂}$ is not stable by level substitution, which can generate extended levels. But, in order to have a correct translation of substitution in $\lambda \mathrm{\Pi }/\equiv$, we should be able to identify $\left|u\left\{x≔v\right\}\right|$ with $\left|u\right|\left\{x≔\left|v\right|\right\}$. That is why we generalize the canonical form to the extended levels in Section 4, showing that all extended levels have a minimal representation: its canonical form. Then , we present the canonization algorithm in Appendix A.

Figure 1 summarises this. Besides, the proofs of the results are given in the full version of the paper, as well as a canonization algorithm. Finally, the existence and uniqueness are also proved in Rocq since we formalised the canonization algorithm for the levels ¹¹1https://gitlab.crans.org/geran/level_formalisation.

The very first step to simplify the terms is to express any level as a maximum of levels that do not contain any $max$, that is the principle of our idea. The successor can be distributed over $max$ since for all $u,v\in 𝐋$, $S(max(u,v))\equiv max(S(u),S(v))$, and the next two observations show how to distribute $\mathrm{imax}$ over $max$.

Then, any level can be expressed as a maximum of levels without $max$. Note that for this, we consider that $max$ takes a finite set of levels as argument. We obtain the following theorem.

We can now focus on levels without maximum. The uniqueness property sought for the representation requires the levels to be very basic, and then we search to simplify them.

The main issue in the grammar of Theorem 9 is $\mathrm{imax}$ because it is asymmetric. We aim to restrict the localisation of the $\mathrm{imax}$ symbol to specific parts of the levels in order to understand and control their influence on the levels semantic.

Firstly, we recall some equivalences that are direct consequences of the semantics of $\mathrm{imax}$. They permit to deal with $0$ and the successor.

And we show how to remove $\mathrm{imax}$ symbol in second argument of $\mathrm{imax}$.

Thus, by applying the simplification suggested by observations 10 and 11, we can restrict the second argument of $\mathrm{imax}$ to be a variable. It is more complicated for its first argument. We can simplify the level when it is $0$.

Moreover, we can distribute $S$ over $\mathrm{imax}$, but this cannot be done as directly as we distribute the $S$ over $max$, as shown in the next example.

Besides, we can observe that $S(\mathrm{imax}(u,v)$) is at least $S(v)$, but can also be $S(u)$ when $v$ is active. Therefore, the simplification rule has to take into account the two relevant cases depending on the value of $v$.

Finally, observations 11, 10, 12, and 14 lead to this grammar restriction.

Here, we continue the simplification process in order to find simple enough terms to reach the uniqueness property. Indeed, the terms of the grammar of Theorem 15 are still not simple enough.

The problem is the following: if $\mathrm{imax}(x,y)$ permits to take $x$ into account if $y$ is active, it also takes $y$ into account in all cases. Then, it is redundant with $y$ and lead to the equivalence $\mathrm{imax}(x,y)\equiv max(y,\mathrm{imax}(x,y))$. We would like to obtain $\mathrm{imax}(x,y)=max(y,t)$ with some level $t$, but $\mathrm{imax}(x,y)$ cannot be simplified more.

In fact, the second argument of $\mathrm{imax}$ has too many responsibilities since it should be taken into account, but it is also a condition to take into account the first argument.

The second concern leads us to devise the introduction of a term “$\text{if}y\text{then}x$” such that ${⟦\text{if}y\text{then}x⟧}_{\sigma }$ is $0$ if ${⟦y⟧}_{\sigma }=0$ and ${⟦x⟧}_{\sigma }$ otherwise. This permits us to simplify $\mathrm{imax}(x,y)$ into $max(y,\text{if}y\text{then}x)$, and since $\text{if}y\text{then}x⩽x$, $max(y,\text{if}y\text{then}x,x)$ can be turned into $max(y,x)$.

Since, the $\mathrm{imax}$ functions are nested in the grammar of Theorem 15, we may need to have multiple variables as conditions; we generalize this idea of new terms and extend the level’s grammar with two symbols $𝒱$ and $𝒞$.

The symbols $𝒱$ and $𝒞$ stand for “variable sublevel” and “constant sublevel” in the sense that their semantic consists in taking into account a non-constant or a constant extended level $u$ when a set of extended levels $E$ only contain active ones.

The verification conditions and the parts of a sublevel determine its value and if it is active. Indeed, when $u$ is active, its value is ${⟦\omega \left(u\right)⟧}_{\sigma }+{⟦\nu \left(u\right)⟧}_{\sigma }$. And for $u$ to be active, the verification condition of $u$ should be checked (otherwise the value of $u$ is automatically $0$), and on top of that ${⟦\omega \left(u\right)⟧}_{\sigma }+{⟦\nu \left(u\right)⟧}_{\sigma }$ (which is then the value of $u$) should not be $0$.

Keeping with our idea, we want to show that any level is equivalent to a maximum of sublevels, so we do it for the grammar presented in Theorem 15. Here is the intuition behind the replacement of a nested $\mathrm{imax}$ by a maximum of sublevels. In $[S^k(y),x_1,\mathrm{\dots },x_n]$,

• $\mathrm{■}$

  $x_n$ is always considered, so we take $𝒱(\left\{\right\},x_n,0)$,

• $\mathrm{■}$

  $x_{n-1}$ is considered if $x_n$ is active, so we take $𝒱(\left\{x_n\right\},x_{n-1},0)$,

• $\mathrm{■}$

  $x_{n-2}$ is considered if $x_n$ and $x_{n-1}$ are active, so we take $𝒱(\{x_n,x_{n-1}\},x_{n-2},0)$,

• $\mathrm{■}$

  …

• $\mathrm{■}$

  $S^k(y)$ is considered if all the $x_i$ are active, so we take $𝒱(\{x_n,\mathrm{\dots },x_1\},y,k)$.

The situation is similar in the case $[S^k(0),x_1,\mathrm{\dots },x_n]$, except that the last taken term is $𝒞(\{x_n,\mathrm{\dots },x_1\},k)$.

One could note that since the grammar of $𝐄$ is really permissive, for all $u\in 𝐄$, we have the trivial equivalence $u\equiv 𝒱(\mathrm{\varnothing },u,0)$ to express $u$ as a sublevel. This shows that the sublevels are at least as expressive as the levels, but this equivalence is a nonsense in terms of level simplification. Proposition 21 is a much stronger and useful result since it states that the verification conditions and the variable part of variable sublevels can be restricted to variables to have a complete representation of levels of $𝐋$. However, we made the choice of presenting extended levels without this restriction to facilitate the level instantiation (developed in Section 4). Indeed, a variable will then be replaced by any level, and we want to make this substitution transparent in our level representation.

We have restrained our study to the sublevels whose verification conditions and the variable part (in the case of variable sublevels) are variables. Now, we show that some of them can be obtained as a maximum of other ones. The first restriction is related to the representation of $0$. Indeed, for all $E\subset 𝐗$, $𝒞(E,0)\equiv 0$. Since we already have $0\equiv max\left(\mathrm{\varnothing }\right)$, we can remove all these sublevels. The second restriction is a little more subtle and is illustrated with this example.

The issue here is the fact that the variable part of a variable sublevel does not necessarily appear in its first argument. This is the key of the following equivalence.

If $k=0$, the sublevel $𝒞(E,k)$ obtained with Proposition 23 is removed accordingly to the first restriction. We end up with the following set of sublevels which permits to express any level.

The canonical sublevels correspond to the set of sublevels that we were searching for. We could try to merge the two types of sublevels by introducing a special variable $\mathrm{𝟏}$ such that for all valuation $\sigma$, $\sigma (\mathrm{𝟏})=1$. We can then see $𝒞(E,k+1)$ as $𝒱(E\cup \left\{\mathrm{𝟏}\right\},\mathrm{𝟏},k)$. This simplifies some results but makes the presentation less clear, and the distinction should still be done in a lot of cases.

The sublevels can be easily compared which is quite normal since we chose them to be very basic. To have $u⩽v$, $v$ should be active whenever $u$ is active hence $\mathrm{VC}\left(v\right)\subset \mathrm{VC}\left(u\right)$. And when they are both active, the value of $v$ should be greater than the one of $u$.

With two variable sublevels it means that their variable part is the same or else we can set a very large value to $\nu \left(u\right)$ in order to falsify the inequality. This also explains that we cannot have $𝒱(E,x,l)⩽𝒞(F,k)$. And if $u$ is a constant sublevel and $v$ a variable sublevel, we should remember that when they are active, $\nu \left(v\right)$ is active (because it is included in $\mathrm{VC}\left(v\right)$) and then $\omega \left(u\right)⩽\omega \left(v\right)+1$ suffices.

As a corollary, we get that the sublevel equivalence is a syntactic equality, which is expected to ease uniqueness.

Figure 2 illustrates the comparison of the canonical sublevels on the set of variables $\{x,y\}$ and with $0$ or $1$ as constant part. We see that we get a greater sublevel by increasing the constant part, reducing the set of verification conditions, or moving to a variable sublevel (in that case, the constant part can be reduced by one).

Now, we can show the uniqueness property. We have to show that two equivalent minimal representations $maxU$ and $maxV$ have the same sublevels. Here, we show a slightly different proof. It is more elegant, and it emphasises the property that ensures the uniqueness.

We will show that $u⩽maxV$ implies the existence of $v\in V$ such that $u⩽v$. This statement lead to the uniqueness property. Indeed, if $maxU$ and $maxV$ are two equivalent minimal representation, then for all $u\in U$ there exists a $v\in V$ such that $u⩽v$, and similarly there exists $u^{\prime }\in U$ such that $v⩽u^{\prime }$. Minimality of $maxU$ permits to conclude that $u=u^{\prime }$, and then $u\equiv v$ and finally $u=v$ by comparison of canonical sublevels.

To prove this statement, the idea is to find, for any sublevel $u$, a valuation $\sigma$ such that the only way to have ${⟦u⟧}_{\sigma }⩽{⟦V⟧}_{\sigma }$ is to have $v\in V$ with $u⩽v$. Such a valuation should only activate the verification condition of $u$. Moreover, ${⟦u⟧}_{\sigma }$ should be large enough to overtake the other sublevels of the representation. When $u$ is a variable sublevel, it means to set its variable part to a large number.

This proposition is fundamental for the following theorem.

And we obtain that equivalence of minimal representations is set equality.

Finally, we obtain the main theorem: the existence and uniqueness of a minimal representation for each level, that is to say a canonical form. First, we show the intuitive property that the minimal representation of a maximum of sublevels is formed with some of them.

This theorem states the existence of a canonical form function $c$ for $𝐋$, $c$ being the function that associates any level to its minimal representation.

Moreover, Theorem 34 provides a method to compare two levels, by comparing each sublevel of the minimal representation of the first one to the second one. More generally, two representations are compared in the following way.

In order to define the successor of a canonical sublevel in terms of representation, we define $\mathrm{inc}:{𝐒}_{𝐂}\to {𝐒}_{𝐂}$ such that for all $E\subset 𝐗,k>0$, $\mathrm{inc}\left(𝒞(E,k)\right)=𝒞(E,k+1)$ and for all $E\subset 𝐗,x\in E,k>0$, $\mathrm{inc}\left(𝒱(E,x,k)\right)=𝒱(E,x,k+1)$. This function nearly increments a canonical sublevel but does not fulfil that objective when some elements of $E$ are not active (it will give $0$ instead of $1$). That’s why we take it in combination with $𝒞(\mathrm{\varnothing },1)$ which is $1$.

We immediately deduce the following result.

Following the equivalences $\mathrm{imax}(0,u)\equiv u$ and $\mathrm{imax}(u,0)\equiv 0$, and observations 7 and 8, we have the following equivalence.

Then, it is sufficient to show that for all $u,v\in {𝐒}_{𝐂}$, $\mathrm{imax}(u,v)$ has a representation. We will then obtain a representation of $\mathrm{imax}(maxU,maxV)$ by taking the elements of the ones of $\mathrm{imax}(u,v)$ for all $u\in U$ and $v\in V$.

We now assume that the verification conditions of a sublevel are representations and that its variable part, in the case of a variable sublevel is a representation as well. First, we show how to transform a sublevel $t$ into a maximum of sublevels whose verifications conditions are variable.

For the sublevel to be active, all its verification conditions should be checked. Since these verification conditions are representations, it means that each of them have an active sublevel. Then, we have to consider all the combinations obtained by taking one sublevel for each verification condition of $t$. Moreover, a sublevel is active when its verifications conditions are all checked. Then, we have to consider all the combinations of verification conditions of the verification conditions of $t$.

The term $P(t,u_1,\mathrm{\dots },u_n)$ means that if $u_1,\mathrm{\dots },u_n$ are checked, then we can take into account the value of the sublevel that we want to simplify (which is then $\nu \left(t\right)+\omega \left(t\right)$). Then, we consider such terms when $u_i,\mathrm{\dots },u_n$ are a combination of verification conditions taken from each verification conditions of $t$. This leads to sublevels whose verification conditions are variables.

By Theorem 40 any level has a representation, and therefore a minimal one by Proposition 36.

With Theorem 54, we have shown that ${𝐑}_{𝐂}$ is as expressive as $𝐄$ whereas ${𝐑}_{𝐂}⊊𝐄$. To finish this section, we compare the expressiveness of the different shape of levels.

If $𝐋$ is semantically, and even syntactically, a subset of $𝐄$, one could note that some extended levels are not equivalent to any level. In fact, even some canonical sublevels are not equivalent to any level. For instance, for all $x\in 𝐗$, there is no $u\in 𝐋$ such that $u\equiv 𝒞(\left\{x\right\},1)$.

In the same way we show that some levels are not expressible with just one canonical level. For instance, for all $x,y\in 𝐗$, there is no $u\in {𝐒}_{𝐂}$ such that $u\equiv max(x,y)$.

We end up with the inclusion Hasse diagram displayed in Figure 3.