From Rewrite Rules to Axioms in the $\lambda \varPi$-Calculus Modulo Theory

Abstract

The $\lambda \varPi$-calculus modulo theory is an extension of simply typed $\lambda$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $\lambda \varPi$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.

1 Introduction

For Poincaré, the reasoning by which we deduce that $2 + 2 = 4$ is not a meaningful proof, but a simple verification. He concludes that the goal of exact sciences is to “dispense with these direct verifications” [20]. Far from being solely a philosophical issue, this principle impacts the foundations of logical systems and in particular the choice between axioms and rewrite rules. For instance, in systems with axioms $x + \textsf{succ}\ y = \textsf{succ}\ (x + y)$ and $x + 0 = x$, we can prove that $2 + 2 = 4$. On the other hand, in systems with rewrite rules $x + \textsf{succ}\ y \hookrightarrow \textsf{succ}\ (x + y)$ and $x + 0 \hookrightarrow x$, we just need to prove $4 = 4$ as we can compute that $(2 + 2 = 4) \equiv (4 = 4)$. In that respect, logical systems with computation rules are convenient tools for making proofs. That is why rewrite rules have been added to systems such as Agda [5] or Coq [12] and why Dowek [9, 10] developed Deduction modulo theory, an extension of first-order logic that mixes computation and proof. Since logical systems with rewrite rules are more user-friendly, one may ask whether or not the results are the same as in axiomatic logical systems.

Rewrite rules are at the core of the $\lambda \varPi$-calculus modulo theory, an extension of simply typed $\lambda$-calculus with dependent types and user-definable rewrite rules [6]. The combination of $\beta$-reduction and of the rewrite rules of a signature $\varSigma$ forms the conversion $\equiv _{\beta \varSigma }$. If we know that t : A with conversion $A \equiv _{\beta \varSigma } B$, then we can derive that t : B. In this system, a theory is a set of rewrite rules, together with a set of axioms (that are typed constants). The $\lambda \varPi$-calculus modulo theory is a powerful logical framework in which many theories can be expressed, such as Predicate logic, Simple type theory or the Calculus of constructions [3]. It is the theory behind the Dedukti language [2, 16] and the Lambdapi proof assistant.

In this paper, we choose to study the replacement of rewrite rules by axioms in the $\lambda \varPi$-calculus modulo theory. Since it is a logical framework, the result applies to many theories. Moreover, as Dedukti is geared towards the interoperability between proof systems, if we want to exchange proofs between a system with rewrite rules and a system without rewrite rules via Dedukti, we need to replace rewrite rules by axioms in the $\lambda \varPi$-calculus modulo theory. Working in this logical framework rather than in an extension of Martin-Löf type theory [17] is therefore relevant on both theoretical and practical levels, but complicates the task as the $\lambda \varPi$-calculus modulo theory does not feature identity types or an infinite hierarchy of sorts.

One method to replace rewrite rules by axioms is to mimic the behavior of the conversion rule using transports: if we have t : A and $A \equiv _{\beta \varSigma } B$ with p an equality between A and B, then we can deduce that $\textsf{transp}~p ~t : B$, but we do not directly have t : B. However trivial this seems, we face several challenges when trying to demonstrate it fully: the insertion of transports in terms and types is difficult due to the presence of dependent types, and the building of transports is involved as we cannot have inside the $\lambda \varPi$-calculus modulo theory an equality between types.

A similar problem is the elimination of equality reflection from extensional systems. Equality reflection states that $\ell = r$ implies $\ell \equiv r$, just like $\ell \hookrightarrow r$ implies $\ell \equiv r$ in systems with rewrite rules. In extensional systems, typing is eased by a more powerful conversion. Hofmann [14, 15] investigated categorically the problem. Oury [19] developed a translation of proofs from an extensional version of the Calculus of Constructions to the Calculus of Inductive Constructions with equality axioms. Winterhalter, Sozeau and Tabareau [23, 24] built upon this result to reduce the number of axioms needed.

The replacement of rewrite rules by axioms paves the way for the interpretation of a theory into another inside the $\lambda \varPi$-calculus modulo theory. Indeed, when interpreting a theory into another, we represent each constant of the source theory by a term in the target theory, but we cannot generally do the same for rewrite rules. We can however pre-process the source theory to replace its rewrite rules by axioms, and then interpret it. The interpretation of theories allows to prove relative consistency and relative normalization theorems [8].

Contribution. The main contribution of this paper is the translation of a theory with rewrite rules to a theory with equational axioms. To do so, we restrict the theories considered to theories with an encoding of the notions of proposition and proof inside the $\lambda \varPi$-calculus modulo theory. So as to compare objects that possibly do not have the same type, we define a heterogeneous equality—following the one defined by McBride [18]. The restriction considered allows us to build an equality between particular types—called small types. We define a type system with typed conversion for the $\lambda \varPi$-calculus modulo theory, so that the proofs are done by induction on the derivation trees more easily.

Outline of the paper. In Section 2, we present the $\lambda \varPi$-calculus modulo theory, we detail a prelude encoding of the notions of proposition and proof in it, and we identify the assumptions made on the considered theories. The heterogeneous equality and the equality between small types are presented in Section 3. The replacement of rewrite rules by axioms and the translation of terms, judgments and theories are presented in Section 4.

2 Theories in the $\lambda \varPi$-Calculus Modulo Theory

In this section, we give a more detailed overview of the $\lambda \varPi$-calculus modulo theory  [6] and its type system. In particular, we present an encoding of the notions of proposition and proof in the $\lambda \varPi$-calculus modulo theory  [3]. We characterize small types—a subclass of types for which we can define an equality.

2.1 The $\lambda \varPi$-Calculus Modulo Theory

The $\lambda \varPi$-calculus, also known as the Edinburgh Logical Framework [13], is an extension of simply typed $\lambda$-calculus with dependent types. The $\lambda \varPi$-calculus modulo theory ($\lambda \varPi /{\equiv }$) [6] is an extension of the $\lambda \varPi$-calculus, in which user-definable rewrite rules have been added [7]. Its syntax is given by:

where c is a constant and x is a variable (ranging over disjoint sets), C and r are terms, D is a closed term (i.e. a term with no free variables) and $\ell$ is a term such that $\ell = c ~t_1 \ldots t_k$ with c a constant. $\texttt {TYPE}$ and $\texttt {KIND}$ are two sorts: terms of type $\texttt {TYPE}$ are called types, and terms of type $\texttt {KIND}$ are called kinds. $\varPi x : A. ~B$ is a dependent product, $\lambda x : A. ~t$ is an abstraction and t u is an application. $\varPi x : A. ~B$ is simply written $A \rightarrow B$ if x does not appear in B. Signatures and contexts are finite sequences, and are written $\langle \rangle$ when empty. Signatures contain both typed constants and rewrite rules (written $\ell \hookrightarrow r$). $\lambda \varPi /{\equiv }$ is a logical framework, in which $\varSigma$ is fixed by the user depending on the logic they are working in.

The relation $\hookrightarrow _{\beta \varSigma }$ is generated by $\beta$-reduction and by the rules of $\varSigma$. More explicitly, $\hookrightarrow _{\beta \varSigma }$ is the smallest relation, closed by context, such that if t rewrites to u for some rule in $\varSigma$ or by $\beta$-reduction then $t \hookrightarrow _{\beta \varSigma } u$. Conversion $\equiv _{\beta \varSigma }$ is the reflexive, symmetric, and transitive closure of $\hookrightarrow _{\beta \varSigma }$.

2.2 The Type System of the $\lambda \varPi$-Calculus Modulo Theory

We introduce in Figs. 1 and 2 typing rules for $\lambda \varPi /{\equiv }$. Fig. 1 presents the usual typing rules while Fig. 2 focuses on the conversion rules. We write $\vdash \varGamma$ when the context $\varGamma$ is well formed and $\varGamma \vdash t : A$ when t is of type A in the context $\varGamma$. $\langle \rangle \vdash t : A$ is simply written $\vdash t : A$. The notation $(\vdash \varGamma _1) \equiv (\vdash \varGamma _2)$ means that $\varGamma _1$ and $\varGamma _2$ are both well formed, have the same length and have the same variables with convertible types. We write $(\varGamma _1 \vdash t_1 : A_1) \equiv (\varGamma _2 \vdash t_2 : A_2)$ when $t_1$ and $t_2$ are convertible with $\varGamma _1 \vdash t_1 : A_1$ and $\varGamma _2 \vdash t_2 : A_2$. In particular, convertible terms $t_1 \equiv t_2$ are authorized to have different types—provided that both types are convertible—and to be typed in different contexts—provided that both contexts are convertible. In ConvRule, $\vec{x}$ is a vector representing the free variables of $\ell$. The standard weakening rule and substitution lemma can be derived from this type system.

Fig. 1.

Typing rules of the $\lambda \varPi$-calculus modulo theory

Fig. 2.

Convertibility rules of the $\lambda \varPi$-calculus modulo theory

Lemma 1 (Substitution)

[Substitution]

• If we have $\vdash \varGamma , x : A, \varDelta$ and $\varGamma \vdash u : A$, then $\vdash \varGamma , \varDelta [x \mapsto u]$.

• If we have $\varGamma , x : A, \varDelta \vdash t : B$ and $\varGamma \vdash u : A$, then $\varGamma , \varDelta [x \mapsto u] \vdash t[x \mapsto u] : B[x \mapsto u]$.

• If we have $(\vdash \varGamma _1, x : A_1, \varDelta _1) \equiv (\vdash \varGamma _2, x : A_2, \varDelta _2)$ and $\varGamma _1 \vdash u : A_1$, then $(\vdash \varGamma _1, \varDelta _1[x \mapsto u]) \equiv (\vdash \varGamma _2, \varDelta _2[x \mapsto u])$.

• If we have $(\varGamma _1, x : A_1, \varDelta _1 \vdash t_1 : B_1) \equiv (\varGamma _2, x : A_2, \varDelta _2 \vdash t_2 : B_2)$ and $\varGamma _1 \vdash u : A_1$, then $(\varGamma _1, \varDelta _1[x \mapsto u] \vdash t_1[x \mapsto u] : B_1[x \mapsto u]) \equiv (\varGamma _2, \varDelta _2[x \mapsto u] \vdash t_2[x \mapsto u] : B_2[x \mapsto u])$.

Proof

We proceed by induction on the typing derivation.

We chose to present a type system with typed conversion (written $\equiv$)—so as to easily do proofs on the derivations—while the usual type system for $\lambda \varPi /{\equiv }$ features untyped conversion (written $\equiv _{\beta \varSigma }$). The equivalence between type systems with typed conversion and type systems with untyped conversion has been a longstanding question: Geuvers and Werner [11] investigated the case of Pure Type Systems with $\beta \eta$-convertibility, Adams [1] proved the equivalence in the case of functional Pure Type Systems, and Siles [21, 22] later proved the equivalence in the general case of the Pure Type Systems. The case of $\lambda \varPi /{\equiv }$, in which we have $\beta$-convertibility but also user-defined rewrite rules, remains to be investigated.

We write $| \varSigma |$ for the set of constants of $\varSigma$, and $\varLambda (\varSigma )$ for the set of terms t whose constants belong to $| \varSigma |$. We say that $\mathcal {T}= \varSigma$ is a theory when for each rule $\ell \hookrightarrow r \in \varSigma$ we have $\ell$ and r in $\varLambda (\varSigma )$, when $\hookrightarrow _{\beta \varSigma }$ is confluent on $\varLambda (\varSigma )$, and when every rule of $\varSigma$ preserves typing in $\varSigma$ (that is when for all context $\varGamma$ and for all term $A \in \varLambda (\varSigma )$, if $\varGamma \vdash \ell : A$ then $\varGamma \vdash r : A$).

Example 1 (Natural numbers and lists)

[Natural numbers and lists] We can define in $\lambda \varPi /{\equiv }$ a partial theory of natural numbers and indexed lists of natural numbers. $\textsf{nat}$ represents the type of natural numbers and $\textsf{list}$ represents the dependent type of indexed lists of natural numbers. $\textsf{cons}$ adds a new element to a list, $\textsf{concat}$ concatenates two lists, and $\textsf{isRev}$ checks if the first given list is the reverse of the second.

In the context $\ell : \textsf{list}\ (\textsf{succ}\ 0)$, we have $\textsf{concat}\ (\textsf{succ}\ 0)\ 0\ \ell \ \textsf{nil}$ of type $\textsf{list}\ (\textsf{succ}\ 0 + 0)$. If we want to compare $\ell$ and this new list with $\textsf{isRev}$, we cannot directly do it because they do not have the same type. However, we can use the conversion rule with $\textsf{list}\ (\textsf{succ}\ 0 + 0) \equiv _{\beta \varSigma } \textsf{list}\ (\textsf{succ}\ 0)$. This conversion derives from the rewrite rule $x + 0 \hookrightarrow x$ instantiated with $x {:}{=}\textsf{succ}\ 0$.

2.3 A Prelude Encoding for the $\lambda \varPi$-Calculus Modulo Theory

It is possible to introduce in $\lambda \varPi /{\equiv }$ the notions of proposition and proof [3]. In particular, this encoding—called prelude encoding—gives the possibility to quantify on certain propositions through codes, which is not possible inside the standard $\lambda \varPi /{\equiv }$. This encoding is defined by following signature.

Definition 1

The signature $\varSigma _{pre}$ contains the following constants and rewrite rules:

We declare the constant $\textit{Set}$, which represents the universe of types, along with the injection $\textit{El}$ that maps terms of type $\textit{Set}$ into $\texttt {TYPE}$. $o$ is a term of type $\textit{Set}$ such that $\textit{El}~o$ defines the universe of propositions. The injection $\textit{Prf}$ maps propositions into $\texttt {TYPE}$. $\mathbin {\rightsquigarrow _d}$ (respectively $\mathbin {\Rightarrow _d}$) is written infix and is used to represent dependent function types between terms of type $\textit{Set}$ (respectively $\textit{El}~o$). The symbol $\pi$ (respectively $\forall$) is used to represent dependent function types between elements of type $\textit{El}~o$ and $\textit{Set}$ (respectively $\textit{Set}$ and $\textit{El}~o$).

The main advantage of this encoding is that it allows us to quantify on propositions. Indeed, in $\lambda \varPi /{\equiv }$, we cannot quantify on $\texttt {TYPE}$. Instead, we can quantify on objects of type $\textit{El}~o$, and then inject them into $\texttt {TYPE}$ using $\textit{Prf}$.

2.4 Small Types and Small Derivations

As we work in $\lambda \varPi /{\equiv }$ rather than in an extension of Martin-Löf type theory, we do not have a pre-defined equality. Moreover, we cannot define an equality between types since such object would have type $\texttt {TYPE}\rightarrow \texttt {TYPE}\rightarrow \texttt {TYPE}$, which is not allowed in $\lambda \varPi /{\equiv }$.

If we want to compare types $\textit{Prf}~a$ and $\textit{Prf}~b$, we cannot do it directly, but we can compare a and b (that are of type $\textit{El}~o$). We can proceed similarly to compare types $\textit{El}~a$ and $\textit{El}~b$ (with a and b of type $\textit{Set}$). In that respect, we want types to be into a special form—called small type—that takes advantages of the prelude encoding, so as to compare them if necessary. To put types of the prelude encoding into this special form, we use the reverse of the rewrite rules of $\varSigma _{pre}$ to represent dependent types with the symbols $\mathbin {\rightsquigarrow _d}$, $\mathbin {\Rightarrow _d}$, $\pi$ and $\forall$ whenever it is possible. This is achieved by the partial function $\nu$, defined by:

Therefore, when $\nu (A)$ is defined, we have $A \equiv _{\beta \varSigma _{pre}} \nu (A)$. Note that $\nu$ is partial because we do not handle the case where a type is a $\beta$-reducible expression, as in practice we will not have types under $\lambda$-abstraction form.

To continue to characterize a particular form of types, we define the three following grammars:

with $a : \textit{El}~o$ and $b : \textit{Set}$. The notation $A \in \mathcal {S}$ means that A is generated by the grammar $\mathcal {S}$. The grammar $\mathcal {S}$ generates types that only contain $\textit{Set}$. Therefore, if $\nu (A) \in \mathcal {S}$ then $\nu (A) = A$. The grammars $\mathcal {P}$ and $\mathcal {E}$ generate types that contain a central symbol $\textit{Prf}$ or $\textit{El}$.

Definition 2 (Small type, Small context)

[Small type, Small context] A type A is small when $\nu (A)$ is defined and $\nu (A) \in \mathcal {S}\cup \mathcal {P}\cup \mathcal {E}$. In that case, $\nu (A)$ is called the small form of A. A context $\varGamma$ is small when for every $x : A \in \varGamma$ we have that A is a small type.

Example 2

$\textit{Prf}~a \rightarrow \textit{Prf}~b$, with $a, b : \textit{El}~o$, is a small type since its small form $\textit{Prf}~(a \mathbin {\Rightarrow _d}(\lambda z. ~b))$ is generated by the grammar $\mathcal {P}$. The type $\varPi x : \textit{Prf}~b. ~\textit{El}~c$, with $c : \textit{Set}$ depending on x, is a small type since its small form $\textit{El}~(\pi ~b ~(\lambda x : \textit{Prf}~b. ~c))$ is generated by the grammar $\mathcal {E}$. The type $\textit{Prf}~a \rightarrow \textit{Set}\rightarrow \textit{Prf}~b$ is not small, since $\nu (\textit{Prf}~a \rightarrow \textit{Set}\rightarrow \textit{Prf}~b) = \textit{Prf}~a \rightarrow \textit{Set}\rightarrow \textit{Prf}~b \notin \mathcal {S}\cup \mathcal {P}\cup \mathcal {E}$.

We would ideally like all the types to be small, so that we can compare them if necessary. Therefore, if $\varGamma \vdash t : A$, we want A to be a small type, or t to be a small type and $A = \texttt {TYPE}$. However, small types are built using the constants of $\varSigma _{pre}$. In particular, the type of the constants $o$, $\mathbin {\rightsquigarrow _d}$, $\mathbin {\Rightarrow _d}$ and $\forall$ are small, but the types of $\pi$, $\textit{Prf}$ and $\textit{El}$ are not. Note that the type of an application of $\pi$, $\textit{Prf}$ or $\textit{El}$ is small. We thus come up with the following notion.

Definition 3 (Small judgment)

[Small judgment] $\vdash \varGamma$ is a small judgment when $\varGamma$ is a small context. $\varGamma \vdash t : A$ is a small judgment when $\varGamma$ is a small context and when

• $t : A \in \varSigma _{pre}$,

• or t is the type of a constant of $\varSigma _{pre}$,

• or A is a small type,

• or t is a small type.

$(\varGamma _1 \vdash t_1 : A_1) \equiv (\varGamma _2 \vdash t_2 : A_2)$ is a small judgment when $\varGamma _1 \vdash t_1 : A_1$ and $\varGamma _2 \vdash t_2 : A_2$ are small.

Definition 4 (Small derivation)

[Small derivation] A small derivation is a derivation in which all the judgments are small.

2.5 Theories with Prelude Encoding

We define the theories we will consider in the rest of the paper: theories that features the prelude encoding inside $\lambda \varPi /{\equiv }$.

Definition 5 (Theory with prelude encoding)

[Theory with prelude encoding] We say that a theory $\mathcal {T}= \varSigma$ in the $\lambda \varPi /{\equiv }$ is a theory with prelude encoding when:

• there exists $\varSigma _\mathcal {T}$ such that $\varSigma = \varSigma _{pre} \cup \varSigma _\mathcal {T}$ and $\varSigma _{pre} \cap \varSigma _\mathcal {T}= \emptyset$,

• for every $c : A \in \varSigma _\mathcal {T}$, A is small and admits a small derivation $\vdash A : \texttt {TYPE}$,

• for every $\ell \hookrightarrow r \in \varSigma _\mathcal {T}$, we have small derivations $\boldsymbol{x} : \boldsymbol{B} \vdash \ell : A$ and $\boldsymbol{x} : \boldsymbol{B} \vdash r : A$ with A a small type, where $\boldsymbol{x}$ represents the free variables of $\ell$.

A theory with prelude encoding is a theory with the constants and rewrite rules $\varSigma _{pre}$, and additional user-defined constants and rewrite rules. To ensure that $\varSigma _\mathcal {T}$ is encoded inside the prelude encoding, we can only define new constants whose types are small. We do not allow the use of rewrite rules $\ell \hookrightarrow r$ when $\ell$ has $\texttt {TYPE}$ in its type. In particular, we cannot define new rewrite rules on $\textit{Prf}$ or $\textit{El}$ and change the behavior of these constants. It follows that the three grammars $\mathcal {S}$, $\mathcal {P}$ and $\mathcal {E}$ generate disjoint types.

In the following examples, we present three theories with prelude encoding in $\lambda \varPi /{\equiv }$. The examples of predicate logic and set theory illustrate that the restrictions considered are generally respected, even for expressive theories.

Example 3 (Predicate logic)

[Predicate logic] Predicate logic can be encoded in a theory with prelude encoding. We declare constants for tautology and contradiction $\top , \bot : \textit{El}~o$, for negation $\lnot : \textit{El}~o\rightarrow \textit{El}~o$, for conjunction and disjunction $\wedge , \vee : \textit{El}~o\rightarrow \textit{El}~o\rightarrow \textit{El}~o$, and for existential quantification $\exists : \varPi z : \textit{Set}. ~(\textit{El}~z \rightarrow \textit{El}~o) \rightarrow \textit{El}~o$. The semantics of tautology is defined by the rewrite rule $\top \hookrightarrow \forall ~o~(\lambda x : \textit{El}~o. ~x \mathbin {\Rightarrow }x)$, which is equivalent to the more common form $\textit{Prf}~\top \hookrightarrow \varPi z : \textit{El}~o. ~\textit{Prf}~z \rightarrow \textit{Prf}~z$. The rewrite rule $\textit{Prf}~(A \wedge B) \hookrightarrow \varPi P : \textit{El}~o. ~(\textit{Prf}~A \rightarrow \textit{Prf}~B \rightarrow \textit{Prf}~P) \rightarrow \textit{Prf}~P$ can be encoded by $A \wedge B \hookrightarrow \forall ~o~(\lambda P. ~(A \rightarrow B \rightarrow P) \rightarrow P)$. The rule $\textit{Prf}~(\lnot A) \hookrightarrow \textit{Prf}~A \rightarrow \textit{Prf}~\bot$ is forbidden, but $\lnot A \hookrightarrow A \mathbin {\Rightarrow }\bot$ is allowed. We proceed similarly the other rewrite rules.

Example 4 (Natural numbers and lists)

[Natural numbers and lists] We can define our small theory of natural numbers and lists in the prelude encoding, by replacing $\texttt {TYPE}$ by $\textit{Set}$ (in the universe of types) or $\textit{El}~o$ (in the universe of propositions), and by adding $\textit{El}$ and $\textit{Prf}$ at the necessary positions.

Example 5 (Set theory)

[Set theory] The implementation in Dedukti of set theory [4] is a theory with prelude encoding. In this implementation, sets are represented by a more primitive notion of pointed graphs: we have $\textsf{graph}$ and $\textsf{node}$ of type $\textit{Set}$. The predicate $\eta : \textit{El}\ \textsf{graph}\rightarrow \textit{El}\ \textsf{node}\rightarrow \textit{El}\ \textsf{node}\rightarrow \textit{El}\ o$ is such that $\eta \ a\ x\ y$ is the proposition asserting that there is an edge in a from y to x. The operator $\textsf{root}: \textit{El}\ \textsf{graph}\rightarrow \textit{El}\ \textsf{node}$ returns the root of a, which is a node.

In practice, the derivations of small judgments are small derivations. As we consider theories with prelude encoding, the only way of introducing a judgment that is not small is through $\lambda$-abstractions. For instance in Example 4 the judgment $\vdash \textit{El}~(\textsf{list}~((\lambda x : \textit{El}~\textsf{nat}. ~\lambda y : \textit{Set}. ~x) ~0 ~\textsf{nat})) : \texttt {TYPE}$ is small, but in its derivation we have $\vdash \lambda x : \textit{El}~\textsf{nat}. ~\lambda y : \textit{Set}. ~x : \textit{El}~\textsf{nat}\rightarrow \textit{Set}\rightarrow \textit{El}~\textsf{nat}$ which is not a small judgment. However, $\vdash \textit{El}~(\textsf{list}~0) : \texttt {TYPE}$ admits a small derivation. If the derivation is not small, we can in practice apply $\beta$-reduction on the fragments of the derivation that are not small to obtain a small derivation.

3 Equalities

Since we want to replace rewrite rules $\ell \hookrightarrow r$ by equational axioms $\ell = r$, we need to define an equality in the target theory. In this section, we present a heterogeneous equality and a method to compare small types. The heterogeneous equality is necessary to compare objects that do not have the same type. Although we cannot define an equality between types in $\lambda \varPi /{\equiv }$, it is possible to develop an equality between small types, taking advantage of their structure.

3.1 Heterogeneous Equality

In our development, we need to have an equality between two translations of the same term. However, the two translations do not necessarily have the same type, as we may have introduced transports over the course of the translation. To that end, we define a heterogeneous equality inspired by the one of McBride [18]. Our heterogeneous equality is defined by the constant schemas $\textsf{heq}_{A,B} : A \rightarrow B \rightarrow \textit{El}~o$ where A and B are of type $\texttt {TYPE}$. We write $u ~{}_{A}{\approx }_{B} ~v$ for $\textit{Prf}~(\textsf{heq}_{A,B} ~u ~v)$. Heterogeneous equality is reflexive, symmetric, and transitive.

$$ \begin{array}{l} \textsf{refl}_A : \varPi u : A. ~u ~{}_{A}{\approx }_{A} ~u \\ \textsf{sym}_{A,B} : \varPi u : A. ~\varPi v : B. ~u ~{}_{A}{\approx }_{B} ~v \rightarrow v ~{}_{B}{\approx }_{A} ~u \\ \textsf{trans}_{A,B,C} : \varPi u : A. ~\varPi v : B. ~\varPi w : C.\ u ~{}_{A}{\approx }_{B} ~v \rightarrow v ~{}_{B}{\approx }_{C} ~w \rightarrow u ~{}_{A}{\approx }_{C} ~w \end{array} $$

When two objects have the same type, heterogeneous equality acts as Leibniz equality. In particular, we can replace u by v in the universes of propositions and types. The result of a Leibniz substitution on t remains equal to t.

$$ \begin{array}{lcl} \textsf{leib}^\textsf{Prf}_A &{}:&{} \varPi u,v : A. ~\varPi p : u ~{}_{A}{\approx }_{A} ~v. ~\varPi P : A \rightarrow \textit{El}~o. ~\textit{Prf}~(P ~u) \rightarrow \textit{Prf}~(P ~v) \\ \textsf{eqLeib}^\textsf{Prf}_A &{}:&{} \varPi u,v : A. ~\varPi p : u ~{}_{A}{\approx }_{A} ~v. ~\varPi P : A \rightarrow \textit{El}~o. ~\varPi t : \textit{Prf}~(P ~u). \\ &{}&{}\textsf{leib}^\textsf{Prf}_A ~u ~v ~p ~P ~t ~{}_{\textit{Prf}~(P ~v)}{\approx }_{\textit{Prf}~(P ~u)} ~t \end{array} $$

The same axiom schemas exist for the universe of types, with superscript $\textsf{El}$ instead of $\textsf{Prf}$, $\textit{El}$ instead of $\textit{Prf}$, and $\textit{Set}$ instead of $\textit{El}~o$.

Finally, we add axioms for the congruence of each constructor of $\lambda \varPi /{\equiv }$.

Application constructor. For the application, we take:

$$ \begin{array}{ll} \textsf{app}_{A_1,A_2,B_1,B_2} :&{} \varPi t_1 : (\varPi x : A_1. ~B_1). ~\varPi t_2 : (\varPi x : A_2. ~B_2). \\ &{}\varPi u_1 : A_1. ~\varPi u_2 : A_2. ~t_1 ~{}_{}{\approx }_{} ~t_2 \rightarrow u_1 ~{}_{}{\approx }_{} ~u_2 \\ &{}\rightarrow t_1 ~u_1 ~{}_{B_1[x \mapsto u_1]}{\approx }_{B_2[x \mapsto u_2]} ~t_2 ~u_2 \end{array} $$

For the $\lambda$-abstraction and $\varPi$-type constructors, we cannot directly build equality axioms. Indeed, if we want to define an equality between functional terms $t_1$ of type $\varPi x : A_1. ~B_1$ and $t_2$ of type $\varPi x : A_2. ~B_2$, we need to ensure that types $A_1$ and $A_2$ are equal. Therefore, we would like to have

$$ \begin{array}{ll} \textsf{fun}_{A_1,A_2,B_1,B_2} :&{} \varPi t_1 : (\varPi x : A_1. ~B_1). ~\varPi t_2 : (\varPi y : A_2. ~B_2). ~A_1 ~{}_{}{\approx }_{} ~A_2 \\ &{} \rightarrow (\varPi x : A_1. ~\varPi y : A_2. ~x ~{}_{}{\approx }_{} ~y \rightarrow t_1 ~x ~{}_{}{\approx }_{} ~t_2 ~y) \\ &{} \rightarrow t_1 ~{}_{}{\approx }_{} ~t_2 \end{array} $$

but we cannot take such an axiom, since the heterogeneous equality is not defined to compare objects that have type $\texttt {TYPE}$, and $A_1 ~{}_{}{\approx }_{} ~A_2$ is therefore ill typed. This shortcoming is addressed by developing an equality between small types.

3.2 Equality between Small Types

We cannot build an equality between types, since such an equality would have type $\texttt {TYPE}\rightarrow \texttt {TYPE}\rightarrow \texttt {TYPE}$, which is impossible in $\lambda \varPi /{\equiv }$. An option would be to take axiom schemas $A ~{}_{}{\approx }_{} ~B$ for every equality between types A and B. Such an equality would be too far from standard and would require additional axioms to build transports. An alternative is to define an equality between small types. By construction, if $\nu (A) \in \mathcal {P}$, then $\nu (A)$ is generated from $\textit{Prf}~a$ for some $a : \textit{El}~o$, and if $\nu (A) \in \mathcal {E}$, then $\nu (A)$ is generated from $\textit{El}~a$ for some $a : \textit{Set}$. If the small form of A contains $\textit{Prf}~a$ and the small form of B contains $\textit{Prf}~b$, then we want an equality between a and b. We define the partial function $\kappa$ on small forms by

where $\textsf{True}{:}{=}\varPi P : \textit{El}~o. ~\textit{Prf}~P \rightarrow \textit{Prf}~P$, so we can always give a witness of $\kappa (S,S)$ if $S \in \mathcal {S}$. By convention, we simply write $\kappa (A,B)$ for the result of $\kappa (\nu (A),\nu (B))$.

Example 6

$\kappa (\varPi x : \textit{Set}. ~\textit{Prf}~P \rightarrow \textit{Prf}~Q,\varPi x : \textit{Set}. ~\textit{Prf}~R) = \varPi x : \textit{Set}. ~(P \mathbin {\Rightarrow _d}\lambda z : P. ~Q) ~{}_{}{\approx }_{} ~R$ since $\nu (\varPi x : \textit{Set}. ~\textit{Prf}~P \rightarrow \textit{Prf}~Q) = \varPi x : \textit{Set}. ~\textit{Prf}~(P \mathbin {\Rightarrow _d}(\lambda z : P. ~Q))$.

We can now go back to the definition of equality axioms for the constructors of $\lambda \varPi /{\equiv }$.

Function constructor. If $A_1$ and $A_2$ are small types, we can take $\kappa (A_1,A_2)$. We do not compare objects of type $\texttt {TYPE}$ anymore, but objects that have either type $\textit{El}~o$ or type $\textit{Set}$. The axiom schema for the function constructor is thus:

$$ \begin{array}{ll} \textsf{fun}_{A_1,A_2,B_1,B_2} :&{} \varPi t_1 : (\varPi x : A_1. ~B_1). ~\varPi t_2 : (\varPi y : A_2. ~B_2). ~\kappa (A_1,A_2) \\ &{} \rightarrow (\varPi x : A_1. ~\varPi y : A_2. ~x ~{}_{}{\approx }_{} ~y \rightarrow t_1 ~x ~{}_{}{\approx }_{} ~t_2 ~y) \\ &{}\rightarrow t_1 ~{}_{}{\approx }_{} ~t_2 \end{array} $$

This axiom schema is a generalization of the functional extensionality principle with distinct domains $A_1$ and $A_2$ in the case of heterogeneous equality. Functional extensionality states that two pointwise-equal functions are equal. If the domains $A_1$ and $A_2$ are generated by $\mathcal {S}$, then they are syntactically equal and we can derive a simpler axiom schema:

$$ \begin{array}{ll} \textsf{fun}_{A,B_1,B_2} :&{} \varPi t_1 : (\varPi x : A. ~B_1). ~\varPi t_2 : (\varPi x : A. ~B_2). ~(\varPi x : A. ~t_1 ~x ~{}_{}{\approx }_{} ~t_2 ~x) \\ &{} \rightarrow t_1 ~{}_{}{\approx }_{} ~t_2 \end{array} $$

$\varPi$-type constructor. The congruence axiom for dependent types aims at building $\kappa (\varPi x : A_1. ~B_1,\varPi x : A_2 ~B_2)$. There are different cases depending on the grammars generating $\nu (A_1)$, $\nu (A_2)$, $\nu (B_1)$ and $\nu (B_2)$. If $\nu (A_1)$, $\nu (A_2)$, $\nu (B_1)$, $\nu (B_2) \in \mathcal {S}$, then $\varPi x : A_1. ~B_1$ and $\varPi x : A_2. ~B_2$ are syntactically equal and we can build an object of type $\textsf{True}$. If $\nu (A_1)$, $\nu (A_2) \in \mathcal {S}$ and $\nu (B_1)$, $\nu (B_2) \in \mathcal {P}\cup \mathcal {E}$, then $A_1 = A_2$ and $\kappa (\varPi x : A_1. ~B_1,\varPi x : A_2 ~B_2) = \varPi x : A_1. ~\kappa (B_1,B_2)$. If $\nu (A_1)$, $\nu (A_2) \in \mathcal {P}\cup \mathcal {E}$ and $\nu (B_1)$, $\nu (B_2) \in \mathcal {S}$, then $B_1 = B_2$ and $\kappa (\varPi x : A_1. ~B_1,\varPi x : A_2 ~B_2) = \kappa (A_1,A_2)$. If $\nu (A_1)$, $\nu (A_2)$, $\nu (B_1)$, $\nu (B_2) \in \mathcal {P}\cup \mathcal {E}$, then there are four cases, corresponding to $\mathbin {\rightsquigarrow _d}$, $\mathbin {\Rightarrow _d}$, $\pi$ and $\forall$. For instance, if $\nu (A_1)$, $\nu (A_2)$, $\nu (B_1)$ and $\nu (B_2)$ are all generated by $\mathcal {E}$, then necessarily we have $\nu (A_1) = \textit{El}~a_1$, $\nu (A_2) = \textit{El}~a_2$, $\nu (B_1) = \textit{El}~b_1$ and $\nu (B_2) = \textit{El}~b_2$. Therefore $\kappa (\varPi x : A_1. ~B_1,\varPi x : A_2. ~B_2) {:}{=}(a_1 \mathbin {\rightsquigarrow _d}(\lambda x : \textit{El}~a_1. ~b_1)) ~{}_{}{\approx }_{} ~(a_2 \mathbin {\rightsquigarrow _d}(\lambda y : \textit{El}~a_2. ~b_2))$. The axiom is:

$$ \begin{array}{ll} \textsf{prod}_{\mathbin {\rightsquigarrow _d}} :&{} \varPi a_1, a_2 : \textit{Set}. ~\varPi b_1 : (\textit{El}~a_1 \rightarrow \textit{Set}). ~\varPi b_2 : (\textit{El}~a_2 \rightarrow \textit{Set}). ~a_1 ~{}_{}{\approx }_{} ~a_2\\ &{} \rightarrow (\varPi x : \textit{El}~a_1. ~\varPi y : \textit{El}~a_2. ~x ~{}_{}{\approx }_{} ~y \rightarrow b_1 ~x ~{}_{}{\approx }_{} ~b_2 ~y) \\ &{} \rightarrow (a_1 \mathbin {\rightsquigarrow _d}b_1) ~{}_{}{\approx }_{} ~(a_2 \mathbin {\rightsquigarrow _d}b_2) \end{array} $$

Note that this axiom is derivable from the previous axioms. We proceed similarly for the cases $\mathbin {\Rightarrow _d}$, $\pi$ and $\forall$.

We write $\varSigma _{eq}$ for the signature formed by the axiom schemas defining the heterogeneous equality. Reflexivity, symmetry, and transitivity are standard axioms of equality. We have also added axioms stating that a heterogeneous equality comparing two objects of the same type acts like Leibniz equality. Finally, we have an axiom for the application constructor and one axiom for the abstraction constructor—that is functional extensionality. Both axioms are used by Oury [19], who also assumes the uniqueness of identity proofs principle that entails the Leibniz principle we use.

4 Replacing Rewrite Rules

When working in theories with prelude encoding, rewriting originates from the rewrite rules of $\varSigma _{pre}$ (which are generic rewrite rules), from the rewrite rules $\varSigma _\mathcal {T}$ (which are defined by the user) and from $\beta$-reduction. The goal of this work is to replace the user-defined rewrite rules $\varSigma _\mathcal {T}$ by equational axioms. In the rest of the paper, we write $\vdash _{\mathcal {R}}$ for a derivation inside the source theory—the theory with user-defined rewrite rules—and $\vdash$ for a derivation inside the target theory—the theory with axioms instead of user-defined rewrite rules.

We now have all the tools to replace rewrite rules by equational axioms. To do so, we build suitable transports, such that if $\varGamma \vdash t : A$ and $\varGamma \vdash p : \kappa (A,B)$, then $\varGamma \vdash \textsf{transp}~p ~t : B$. The goal is to insert such transports into the terms instead of using conversion with the rules of $\varSigma _\mathcal {T}$. In the signature, each rewrite rule $\ell \hookrightarrow r$ is replaced by the equational axiom $\overline{\ell }~{}_{}{\approx }_{} ~\overline{r}$.

4.1 Transports

If we have $\varGamma \vdash t : A$ and $\varGamma \vdash p : \kappa (A,B)$, we want to transport t from A to B, that is to build a term $\textsf{transp}~p ~t$ such that $\varGamma \vdash \textsf{transp}~p ~t : B$. A paramount result is that t and $\textsf{transp}~p ~t$ are heterogeneously equal.

Lemma 2 (Transport)

[Transport] Given $\varGamma \vdash t : A$ and $\varGamma \vdash p : \kappa (A,B)$ with A and B small types, there exists $\textsf{transp}~p ~t$, called transport of t along p, such that:

• $\varGamma \vdash \textsf{transp}~p ~t : B$,

• there exists $\textsf{eqTransp}$ such that $\varGamma \vdash \textsf{eqTransp}~p ~t : \textsf{transp}~p ~t ~{}_{B}{\approx }_{A} ~t$.

Proof

A and B are small types and we have an equality $\kappa (A,B)$. If $A,B \in \mathcal {S}$ then $\nu (A) = \nu (B) = A = B$ and we take $\textsf{transp}~p ~t {:}{=}t$ and $\textsf{eqTransp}~p ~t {:}{=}\textsf{refl}_A ~t$. Otherwise, by construction of $\kappa$, we know that $\nu (A), \nu (B) \in \mathcal {P}$, or $\nu (A), \nu (B) \in \mathcal {E}$, and that $\nu (A)$ and $\nu (B)$ have the same structure. Moreover, using $A \equiv _{\beta \varSigma _{pre}} \nu (A)$, we have $\varGamma \vdash t : \nu (A)$. We proceed by induction on the grammar $\mathcal {P}$ (we proceed similarly for the grammar $\mathcal {E}$).

• If $\nu (A) = \textit{Prf}~a$ and $\nu (B) = \textit{Prf}~b$, then we have $\varGamma \vdash p : a ~{}_{}{\approx }_{} ~b$. We take $\textsf{transp}~p ~t {:}{=}\textsf{leib}^\textsf{Prf}_{\textit{El}~o} ~a ~b ~p ~(\lambda w : \textit{El}~o. ~w) ~t$. We conclude using $\textsf{eqLeib}^\textsf{Prf}_{\textit{El}~o}$.

• If $\nu (A) = A' \rightarrow S$ and $\nu (B) = B' \rightarrow S$, with $A', B' \in \mathcal {P}$ and $S \in \mathcal {S}$, then we have $\kappa (A',B') = \kappa (A,B)$. From $\varGamma \vdash p : \kappa (A',B')$ we can build some $p'$ such that $\varGamma \vdash p' : \kappa (B',A')$ (using $\textsf{sym}$). By weakening, we also have $p' : \kappa (B',A')$ in the context $\varGamma , m_b : B'$. By induction, we have $\textsf{transp}~p' ~m_b : A'$ and $\textsf{eqTransp}~p' ~m_b : \textsf{transp}~p' ~m_b ~{}_{}{\approx }_{} ~m_b$ in the context $\varGamma , m_b : B'$. We take $\textsf{transp}~p ~t {:}{=}\lambda m_b : B'. ~t ~(\textsf{transp}~p' ~m_b)$. Using $\textsf{trans}$ and $\textsf{app}$ we obtain an equality $t ~(\textsf{transp}~p' ~m_b) ~{}_{}{\approx }_{} ~t ~m_a$ in the context $\varGamma , m_a : A', m_b : B', p_m : m_a ~{}_{}{\approx }_{} ~m_b$. Using $\textsf{fun}$ and $\equiv _{\beta \varSigma _{pre}}$, we have $\lambda m_b : B'.\ t\ (\textsf{transp}\ p'\ m_b) ~{}_{}{\approx }_{} ~t$ in the context $\varGamma$.

• If $\nu (A) = \varPi z : S. ~A'$ and $\nu (B) = \varPi z : S. ~B'$ with $A', B' \in \mathcal {P}$ and $S \in \mathcal {S}$, then we have $\kappa (A,B) = \varPi z : S. ~\kappa (A',B')$. By weakening and application, we have $\varGamma , z : S \vdash p ~z : \kappa (A',B')$. By induction we have $\textsf{transp}~(p ~z) ~(t ~z) : B'$ and $\textsf{eqTransp}~(p ~z) ~(t ~z) : \textsf{transp}~(p ~z) ~(t ~z) ~{}_{}{\approx }_{} ~t ~z$ in the context $\varGamma , z : S$. We take $\textsf{transp}~p ~t {:}{=}\lambda z : S. ~\textsf{transp}~(p ~z) ~(t ~z)$. We obtain $\lambda z : S. ~\textsf{transp}~(p ~z) ~(t ~z) ~{}_{}{\approx }_{} ~t$ using $\textsf{fun}$ and $\equiv _{\beta \varSigma _{pre}}$.    $\square$

The transport of t from A to B depends on the small form of A and B. In that respect, there exists a different transport for each possible family of small form, and such transport is indexed over an equality of a small type.

4.2 Translation of Terms

To translate a theory with rewrite rules into a theory with equational axioms, we add transports at the proper locations in the terms and types. If we have $\varGamma \vdash _{\mathcal {R}}t : A$ in the source theory, we want to find $\overline{\varGamma }$, $\overline{t}$ and $\overline{A}$ that are translations of $\varGamma$, t and A, and such that $\overline{\varGamma }\vdash \overline{t}: \overline{A}$ in the target theory.

We add transports in a term by induction on a typing derivation—which is not unique—so we may have different translations for a same term. As such, we define a relation $\triangleleft$ where $\overline{t}\triangleleft t$ states that $\overline{t}$ is a translation of t. The relation is defined by induction on the terms of $\lambda \varPi /{\equiv }$. Variables, constants, $\texttt {TYPE}$ and $\texttt {KIND}$ are translations of themselves. The translations of $\lambda$-abstractions $\lambda x : A. ~t$, dependent types $\varPi x : A. ~B$ and applications t u rely on the translations of t, u, A and B. The most important part of the definition is that the translation is stable by transports: if $\overline{t}$ is a translation of t, then $\textsf{transp}~p ~\overline{t}$ is also a translation of t, with p typically an equality. This relation captures all possible translations, but some are not correct as they may not be well typed. For instance, $\lambda x : \overline{A}. ~\overline{t}$ is not a valid translation of $\lambda x : A. ~t$ when the variable x used in $\overline{t}$ does not expect type $\overline{A}$ but another translation $\overline{A}'$.

Definition 6

The translation relation $\triangleleft$ is defined by:

where p is an arbitrary term.

Due to the typing rules of $\lambda \varPi /{\equiv }$, transports for objects that have $\texttt {TYPE}$ in their type do not exist. Therefore, the only well-typed translations of $\texttt {TYPE}$, $\texttt {KIND}$, $\textit{Set}$, $\textit{Prf}$ and $\textit{El}$ are themselves, and the well-typed translations of $\varPi x : A. ~B$ are of the form $\varPi x : \overline{A}. ~\overline{B}$ with $\overline{A}~\triangleleft ~A$ and $\overline{B}~\triangleleft ~B$. It follows that a well-typed translation of a small type is still a small type. In particular, if $A \in \mathcal {S}$ then for any $\overline{A}$ we have $\overline{A}{:}{=}A$; if $\nu (A) \in \mathcal {P}$ then $\nu (\overline{A}) \in \mathcal {P}$; and if $\nu (A) \in \mathcal {E}$ then $\nu (\overline{A}) \in \mathcal {E}$.

We extend the relation to contexts and signatures. For each rewrite rule $\ell \hookrightarrow r$ of a signature, we have $\boldsymbol{x} : \boldsymbol{B} \vdash _{\mathcal {R}}\ell : A$ and $\boldsymbol{x} : \boldsymbol{B} \vdash _{\mathcal {R}}r : A$, for some $\boldsymbol{B}$ and A, and some $\boldsymbol{x}$ representing the free variables of $\ell$. The translation of the rewrite rule $\ell \hookrightarrow r$ is given by the equational axiom $\textsf{eq}_{\ell r} : \varPi \boldsymbol{x} : \overline{\boldsymbol{B}}. ~\overline{\ell }~{}_{\overline{A}}{\approx }_{\overline{A}} ~\overline{r}$. Since the type of a term is not unique in $\lambda \varPi /{\equiv }$, we have made a choice of $\boldsymbol{B}$ and A, which is not a problem as we will see in the proof of Theorem 1.

Definition 7

$\triangleleft$ is defined on contexts and signatures by:

Lemma 3

If $\overline{t}~\triangleleft ~t$ and $\overline{u}~\triangleleft ~u$ then $\overline{t}[x \mapsto \overline{u}] ~\triangleleft ~t[x \mapsto u]$.

Proof

By induction on the derivation of $\overline{t}~\triangleleft ~t$. For the case with the transport, we can prove that $(\textsf{transp}~p ~t)[x \mapsto u] = \textsf{transp}~p[x \mapsto u] ~t[x \mapsto u]$.    $\square$

Definition 8

(Relation $\sim$). We say that $t_1 \sim t_2$ when there exists some t such that $t_1 ~\triangleleft ~t$ and $t_2 ~\triangleleft ~t$.

Lemma 4

$\sim$ is an equivalence relation.

Proof

$\sim$ is reflexive, symmetric and transitive. When proving transitivity we exploit the fact that whenever $t ~\triangleleft ~u_1$ and $t ~\triangleleft ~u_2$, we have $u_1 = u_2$. Reflexivity is proved by induction on the term.    $\square$

An important result we need to prove is that two well-typed translations $t_1$ and $t_2$ of the same term t are heterogeneously equal. By construction, both terms do not necessarily have the same type or the same context. We will always consider $\varGamma _1 \vdash t_1 : A_1$ and $\varGamma _2 \vdash t_2 : A_2$, where $\varGamma _1$ and $\varGamma _2$ have the same length and the same variables (with possibly different types). The equality between $t_1$ and $t_2$ must be typed in some context, but $\varGamma _1$ and $\varGamma _2$ are not sufficient. That is why we define a common context $\varGamma _1 \star \varGamma _2$ (written $\textsf{Pack} ~\varGamma _1 ~\varGamma _2$ in the work of Winterhalter et al.  [23]) by duplicating each variable and by assuming a witness of heterogeneous equality between these two duplicates. More precisely, we partially define $\star$ by induction on small contexts:

$$\begin{aligned} \langle \rangle \star \langle \rangle {:}{=}\langle \rangle \end{aligned}$$

$$\begin{aligned} (\varGamma _1, x : A_1) \star (\varGamma _2, x : A_2) {:}{=}\varGamma _1 \star \varGamma _2, x_1 : A_1[\gamma _1], x_2 : A_2[\gamma _2], p_x : x_1 ~{}_{}{\approx }_{} ~x_2 \end{aligned}$$

where $\gamma _1$ substitutes variables z by $z_1$ and $\gamma _2$ substitutes variables z by $z_2$. We write $\gamma _{12}$ for the substitution that replaces the variables $z_1$ and $z_2$ by z and the variable $p_z$ by $\textsf{refl}~z$.

Lemma 5

If $\varGamma \star \varGamma \vdash t : A$, then we can derive $\varGamma \vdash t[\gamma _{12}] : A[\gamma _{12}]$.

Proof

We proceed by induction on the length of $\varGamma$. If we have $\langle \rangle \star \langle \rangle \vdash t : A$ then by definition we have $\langle \rangle \vdash t : A$. Suppose that we have $(\varGamma , x : B) \star (\varGamma , x : B) \vdash t : A$. We apply successively Lemma 1 to replace $x_2$ and $x_1$ by x and then $p_x$ by $\textsf{refl}~x$.    $\square$

The following lemma states that two translations of a same term are heterogeneously equal.

Lemma 6 (Equal translations)

[Equal translations] Let $t_1 \sim t_2$ such that $\varGamma _1 \vdash t_1 : A_1$ and $\varGamma _2 \vdash t_2 : A_2$ with $\varGamma _1$ and $\varGamma _2$ small contexts.

• 1. If $\varGamma _1 \vdash A_1 : \texttt {TYPE}$ and $\varGamma _2 \vdash A_2 : \texttt {TYPE}$, then there exists some p such that $\varGamma _1 \star \varGamma _2 \vdash p : t_1[\gamma _1] ~{}_{A_1[\gamma _1]}{\approx }_{A_2[\gamma _2]} ~t_2[\gamma _2]$.

• 2. If $t_1$ and $t_2$ are small types, then there exists some p such that $\varGamma _1 \star \varGamma _2 \vdash p : \kappa (t_1[\gamma _1],t_2[\gamma _2])$.

Proof

We proceed by induction on the derivation of $t_1 \sim t_2$. We show two interesting cases.

• Transport $(\textsf{transp}~p ~t_1) \sim t_2$

  We have $\varGamma _1 \vdash \textsf{transp}~p ~t_1 : A_1$ and $\varGamma _2 \vdash t_2 : A_2$. By inversion of typing, we have $\varGamma _1 \vdash t_1 : A_1'$ and $\varGamma _1 \vdash p : \kappa (A_1',A_1)$. By induction there exists some $p_t$ such that $\varGamma _1 \star \varGamma _2 \vdash p_t : t_1[\gamma _1] ~{}_{}{\approx }_{} ~t_2[\gamma _2]$. We also have $\varGamma _1 \vdash \textsf{eqTransp}~p ~t_1 : \textsf{transp}~p ~t_1 ~{}_{}{\approx }_{} ~t_1$. We derive that $\varGamma _1 \star \varGamma _2 \vdash (\textsf{eqTransp}~p ~t_1)[\gamma _1] : (\textsf{transp}~p ~t_1)[\gamma _1] ~{}_{}{\approx }_{} ~t_1[\gamma _1]$. We conclude using transitivity.

• Application $(t_1 ~u_1) \sim (t_2 ~u_2)$

  Suppose that $t_1 ~u_1$ and $t_2 ~u_2$ are small types. Then the only possible cases are $t_1 = t_2 = \textit{Prf}$ or $t_1 = t_2 = \textit{El}$. If $t_1 = t_2 = \textit{Prf}$, then we have $\varGamma _1 \vdash \textit{Prf}~u_1 : \texttt {TYPE}$ and $\varGamma _2 \vdash \textit{Prf}~u_2 : \texttt {TYPE}$. Since $\kappa (\textit{Prf}~u_1,\textit{Prf}~u_2) = u_1 ~{}_{}{\approx }_{} ~u_2$, the result is simply the induction hypothesis $\varGamma _1 \star \varGamma _2 \vdash p : u_1[\gamma _1] ~{}_{}{\approx }_{} ~u_2[\gamma _2]$. We proceed similarly for $\textit{El}~u_1 \sim \textit{El}~u_2$.

  Suppose that we have $\varGamma _1 \vdash t_1 ~u_1 : T_1$ and $\varGamma _2 \vdash t_2 ~u_2 : T_2$ with $\varGamma \vdash T_1 : \texttt {TYPE}$ and $\varGamma \vdash T_2 : \texttt {TYPE}$. Then by inversion of typing we have $\varGamma _1 \vdash u_1 : B_1$ and $\varGamma _2 \vdash u_2 : B_2$ and $\varGamma _1 \vdash t_1 : \varPi x : A_1. ~B_1$ and $\varGamma _2 \vdash t_2 : \varPi x : A_2. ~B_2$, with $T_1 \equiv _{\beta \varSigma _{pre}} B_1[x \mapsto u_1]$ and $T_2 \equiv _{\beta \varSigma _{pre}} B_2[x \mapsto u_2]$. By induction hypotheses, we have $\varGamma _1 \star \varGamma _2 \vdash p_t : t_1[\gamma _1] ~{}_{}{\approx }_{} ~t_2[\gamma _2]$ and $\varGamma _1 \star \varGamma _2 \vdash p_u : u_1[\gamma _1] ~{}_{}{\approx }_{} ~u_2[\gamma _2]$. We conclude using $\textsf{app}$.    $\square$

4.3 Translation of Judgments

In Section 4.2 we have seen all the possible translations for terms. However, the only translations that matter are the translations of judgments: context formation judgments and typing judgments.

Definition 9

For any $\vdash _{\mathcal {R}}\varGamma$ we define a set $[\![\vdash _{\mathcal {R}}\varGamma ]\!]$ of valid judgments such that $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$ if and only if $\overline{\varGamma }~\triangleleft ~\varGamma$. For any $\varGamma \vdash _{\mathcal {R}}t : A$ we define a set $[\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$ of valid judgments such that $\overline{\varGamma }\vdash \overline{t}: \overline{A}\in [\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$ if and only if $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$, $\overline{t}~\triangleleft ~t$ and $\overline{A}~\triangleleft ~A$.

We are now able to prove that it is possible to switch between two translations of a small type.

Lemma 7 (Switching translations)

[Switching translations] Suppose that we have A a small type, $\overline{\varGamma }\vdash \overline{t}: \overline{A}\in [\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$ and $\overline{\varGamma }\vdash \overline{A}' : \texttt {TYPE} \in [\![\varGamma \vdash _{\mathcal {R}}A : \texttt {TYPE} ]\!]$ with $\overline{\varGamma }$ a small context. Then there exists $\overline{t}'$ such that $\overline{\varGamma }\vdash \overline{t}' : \overline{A}' \in [\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$.

Proof

If $\nu (A) \in \mathcal {S}$, then $\overline{A}{:}{=}A$ and $\overline{A}' {:}{=}A$, and we take $\overline{t}' {:}{=}\overline{t}$. If $\nu (A) \in \mathcal {P}$, then $\nu (\overline{A}), \nu (\overline{A}') \in \mathcal {P}$ (this is similar for $\mathcal {E}$). As $\overline{A}$ and $\overline{A}'$ are two translations of A, we have $\overline{A}\sim \overline{A}'$. From Lemma 6, we have $\overline{\varGamma }\star \overline{\varGamma }\vdash p : \kappa (\overline{A}[\gamma _1],\overline{A}'[\gamma _2])$. Using Lemma 5 we obtain $\overline{\varGamma }\vdash p[\gamma _{12}] : \kappa (\overline{A},\overline{A}')$. Using Lemma 2, there exists some $\textsf{transp}~p[\gamma _{12}] ~\overline{t}~\triangleleft ~t$ (since $\overline{t}~\triangleleft ~t$) such that $\overline{\varGamma }\vdash \textsf{transp}~p[\gamma _{12}] ~\overline{t}: \overline{A}'$.    $\square$

4.4 Translation of Theories

Now that we have translated terms and judgments, we want to translate theories, so that the translation of every provable judgment in the source theory is provable in the target theory. The target theory $\mathcal {T}^{ax} = \varSigma _{pre} \cup \varSigma _{eq} \cup \overline{\varSigma }_{\mathcal {T}}$ is obtained by adding the axioms of equality to the signature, and by translating $\varSigma _{\mathcal {T}}$. To do so, we translate each typed constant and rewrite rule one by one. At the end, the rewrite rules of $\varSigma _{\mathcal {T}}$ have been replaced by equational axioms.

The paramount result of this paper is the following theorem. The first item concerns context formation. The second item is about the translation of typing judgments. The third item focuses on convertible contexts. The fourth and fifth items are about the conversion rules. It is worth noting that in the second item we use the universal quantifier on $\overline{\varGamma }$ instead of using the existential quantifier. We have opted for the universal quantifier so we can obtain the induction hypotheses for a common context.

Theorem 1 (Elimination of the rewrite rules)

[Elimination of the rewrite rules] Let a theory $\mathcal {T}= \varSigma$ in $\lambda \varPi /{\equiv }$ such that $\mathcal {T}$ is a theory with prelude encoding and such that all the derivations considered are small derivations. There exists a signature $\overline{\varSigma }_{\mathcal {T}} ~\triangleleft ~\varSigma _{\mathcal {T}}$ such that the theory $\mathcal {T}^{ax} = \varSigma _{pre} \cup \varSigma _{eq} \cup \overline{\varSigma }_{\mathcal {T}}$ satisfies:

• 1. If $\vdash _{\mathcal {R}}\varGamma$, then there exists $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$.

• 2. If $\varGamma \vdash _{\mathcal {R}}t : A$, then for every $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$ there exist $\overline{t}$ and $\overline{A}$ such that $\overline{\varGamma }\vdash \overline{t}: \overline{A}\in [\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$.

• 3. If $(\vdash _{\mathcal {R}}\varGamma _1) \equiv (\vdash _{\mathcal {R}}\varGamma _2)$, then for every $\vdash \overline{\varGamma }_1 \in [\![\vdash _{\mathcal {R}}\varGamma _1 ]\!]$ and $\vdash \overline{\varGamma }_2 \in [\![\vdash _{\mathcal {R}}\varGamma _2 ]\!]$, we have $\vdash \overline{\varGamma }_1 \star \overline{\varGamma }_2$.

• 4. If $(\varGamma _1 \vdash _{\mathcal {R}}u_1 : A_1) \equiv (\varGamma _2 \vdash _{\mathcal {R}}u_2 : A_2)$ with $\varGamma _1 \vdash _{\mathcal {R}}A_1 : \texttt {TYPE}$ and $\varGamma _2 \vdash _{\mathcal {R}}A_2 : \texttt {TYPE}$, then for every $\vdash \overline{\varGamma }_1 \in [\![\vdash _{\mathcal {R}}\varGamma _1 ]\!]$ and $\vdash \overline{\varGamma }_2 \in [\![\vdash _{\mathcal {R}}\varGamma _2 ]\!]$, we have $\overline{\varGamma }_1 \vdash \overline{u}_1 : \overline{A}_1 \in [\![\varGamma _1 \vdash _{\mathcal {R}}u_1 : A_1 ]\!]$ and $\overline{\varGamma }_2 \vdash \overline{u}_2 : \overline{A}_2 \in [\![\varGamma _2 \vdash _{\mathcal {R}}u_2 : A_2 ]\!]$ and there exists some p such that $\overline{\varGamma }_1 \star \overline{\varGamma }_2 \vdash p : \overline{u}_1[\gamma _1] ~{}_{\overline{A}_1[\gamma _1]}{\approx }_{\overline{A}_2[\gamma _2]} ~\overline{u}_2[\gamma _2]$.

• 5. If $(\varGamma _1 \vdash _{\mathcal {R}}u_1 : \texttt {TYPE}) \equiv (\varGamma _2 \vdash _{\mathcal {R}}u_2 : \texttt {TYPE})$, then for every $\vdash \overline{\varGamma }_1 \in [\![\vdash _{\mathcal {R}}\varGamma _1 ]\!]$ and $\vdash \overline{\varGamma }_2 \in [\![\vdash _{\mathcal {R}}\varGamma _2 ]\!]$, we have $\overline{\varGamma }_1 \vdash \overline{u}_1 : \texttt {TYPE} \in [\![\varGamma _1 \vdash _{\mathcal {R}}u_1 : \texttt {TYPE} ]\!]$ and $\overline{\varGamma }_2 \vdash \overline{u}_2 : \texttt {TYPE} \in [\![\varGamma _2 \vdash _{\mathcal {R}}u_2 : \texttt {TYPE} ]\!]$ and there exists some p such that $\overline{\varGamma }_1 \star \overline{\varGamma }_2 \vdash p : \kappa (\overline{u}_1[\gamma _1],\overline{u}_2[\gamma _2])$.

Proof

The proof of the five items is done by induction on the typing derivations, assuming the existence of $\overline{\varSigma }_{\mathcal {T}}$. We show three relevant cases.

• Prod:

  

  Take $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$. By induction hypothesis, we have $\overline{\varGamma }\vdash \overline{A}: \texttt {TYPE} \in [\![\varGamma \vdash _{\mathcal {R}}A : \texttt {TYPE} ]\!]$. We have $(\overline{\varGamma }, x : \overline{A}) ~\triangleleft ~(\varGamma , x : A)$ and we know that the only translation of sort s is itself, therefore by induction hypothesis we have $\overline{\varGamma }, x : \overline{A}\vdash \overline{B}: s \in [\![\varGamma , x : A \vdash _{\mathcal {R}}B : s ]\!]$. We conclude that $\overline{\varGamma }\vdash \varPi x : \overline{A}. ~\overline{B}: s$ using the Prod rule.

• Conv:

  

  Take $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$. As we consider small derivations, either A is a small type or A and B are the same type.

  If A is a small type, then by induction hypothesis we have $\overline{\varGamma }\star \overline{\varGamma }\vdash p : \kappa (\overline{A}[\gamma _1],\overline{B}[\gamma _2])$. By Lemma 5 we obtain $\overline{\varGamma }\vdash p[\gamma _{12}] : \kappa (\overline{A},\overline{B})$. By Lemma 7 and induction hypothesis we have $\overline{\varGamma }\vdash \overline{t}: \overline{A}\in [\![\varGamma \vdash _{\mathcal {R}}t : A ]\!]$. Thanks to Lemma 2, there exists some $\overline{t}'$ such that $\overline{\varGamma }\vdash \overline{t}' : \overline{B}\in [\![\varGamma \vdash _{\mathcal {R}}t : B ]\!]$.

  If A and B are the same type, then no conversion is needed and the result is simply given the induction hypothesis $\overline{\varGamma }\vdash \overline{t}: \overline{A}$.

• ConvRefl:

  

  Take $\vdash \overline{\varGamma }\in [\![\vdash _{\mathcal {R}}\varGamma ]\!]$. By induction hypothesis, we have $\overline{\varGamma }\vdash \overline{u}: \overline{A}\in [\![\varGamma \vdash _{\mathcal {R}}u : A ]\!]$.

  If $\varGamma \vdash _{\mathcal {R}}A : \texttt {TYPE}$, then we build $\overline{\varGamma }\star \overline{\varGamma }\vdash p : \overline{u}[\gamma _1] ~{}_{}{\approx }_{} ~\overline{u}[\gamma _2]$ using all the congruence rules of $\approx$.

  We proceed similarly for the case $A = \texttt {TYPE}$.

The existence of $\overline{\varSigma }_{\mathcal {T}}$ is proved by induction on the length of $\varSigma _{\mathcal {T}}$, using the previous five items and $\langle \rangle ~\triangleleft ~\langle \rangle$.    $\square$

Corollary 1 (Preservation)

[Preservation] If $\vdash _{\mathcal {R}}t : A$ and $\vdash A : s \in [\![ \vdash _{\mathcal {R}}A : s ]\!]$, then there exists $\overline{t}$ such that $\vdash \overline{t}: A$.

Proof

By Theorem 1 we have $\vdash \overline{t}' : \overline{A}' \in [\![ \vdash _{\mathcal {R}}t : A ]\!]$. Using Lemma 7 with $\overline{A}{:}{=}A$, we have some $\overline{t}$ such that $\vdash \overline{t}: A \in [\![ \vdash _{\mathcal {R}}t : A ]\!]$.    $\square$

We directly derive the two following conservativity and consistency results. We say that a theory $\mathcal {T}_2$ is conservative over a theory $\mathcal {T}_1$ when every formula in the common language of $\mathcal {T}_1$ and $\mathcal {T}_2$ that is provable in $\mathcal {T}_2$ is also provable in $\mathcal {T}_1$.

Corollary 2 (Conservativity)

[Conservativity] $\mathcal {T}$ is a conservative extension of $\mathcal {T}^{ax}$.

Corollary 3 (Relative consistency)

[Relative consistency] If $\mathcal {T}^{ax}$ is consistent then $\mathcal {T}$ is also consistent.

5 Conclusion

Discussion. In this paper, we showed that it is possible to replace user-defined rewrite rules by equational axioms, in the case of the $\lambda \varPi$-calculus modulo theory. This result works for theories with prelude encoding—which is satisfied by expressive theories such as predicate logic and set theory—and for small derivations—which is in practice the case. So as to replace rewrite rules by equational axioms, we have defined a heterogeneous equality with standard axioms—reflexivity, symmetry, transitivity, Leibniz principle—and congruences for each constructor. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.

Related work. The similar problem of the translation from an extensional system to an intensional system has been investigated by Oury [19]. He proposed a translation from the Extensional Calculus of Constructions to the Calculus of Inductive Constructions with additional axioms that define a heterogeneous equality. Winterhalter, Sozeau and Tabareau provided a translation from extensional type theory to intensional type theory [23, 24]. They took advantage of the presence of dependent pairs to encode a heterogeneous equality, unlike Oury who defined it with axioms.

In this paper, we have shown the existence of a translation from a theory with rewrite rules to a theory with equational axioms. Technical challenges appear as we are not in an extensional type system. In particular, Oury and Winterhalter et al. had a homogeneous equality in their source theory and introduce a heterogeneous equality in the target theory. In this work, the source theory does not contain a homogeneous equality, and the target theory only contains a heterogeneous equality.

The major difference with previous works is that we are in a logical framework without an infinite hierarchy of sorts $s_i : s_{i+1}$ for $i \in \mathbb {N}$. In $\lambda \varPi /{\equiv }$, we only have $\texttt {TYPE}: \texttt {KIND}$, which is the reason why we cannot define an equality between types. As such an equality is of paramount importance in the transports, we have considered a subclass of types—called small types—for which we can define an equality. However, it is worth noting that the sorts of $\lambda \varPi /{\equiv }$ allowed a simplification: by construction, there is no transports on types, so the translation of a dependent function type is directly a dependent function type.