# Encoding Agda Programs Using Rewriting

Guillaume Genestier

► To cite this version:

Guillaume Genestier. Encoding Agda Programs Using Rewriting. FSCD - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. 10.4230/LIPIcs.FSCD.2020.31 . hal-03838613

HAL Id: hal-03838613

https://inria.hal.science/hal-03838613

Submitted on 3 Nov 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Encoding Agda Programs Using Rewriting

## Guillaume Genestier

Université Paris-Saclay, ENS Paris-Saclay, Inria, CNRS, LSV, France

MINES ParisTech, PSL University, France

### Abstract

We present in this paper an encoding in an extension with rewriting of the Edinburgh Logical Framework (LF) [13] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between AGDA and DEDUKTI developed by the author.

**2012 ACM Subject Classification** Theory of computation → Equational logic and rewriting; Theory of computation → Type theory

**Keywords and phrases** Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2020.31

**Supplementary Material** The translator is available at https://github.com/Deducteam/Agda2Dedukti, the directory theory/ contains the encoding presented in Sections 3 and 4. It is able to translate and type-check 162 files of AGDA's standard library [9].

**Funding** Part of this work was carried out during a stay at Chalmers University of Technology, Sweden, funded by the Cost Action CA15123: EUTypes.

**Acknowledgements** I am grateful to Jesper Cockx and Andreas Abel, who received me in Chalmers and helped me to find my way in the hostile jungle the Agda implementation would have been without their help. Then I would like to thank Frédéric Blanqui, Olivier Hermant, Kostia Chardonnet and the anonymous reviewers for their thorough comments, both on the form and content of this article, which greatly improved its quality.

## 1 Introduction

With the multiplication of proof assistants, interoperability has become a main obstacle preventing the dissemination of formally verified software among industrial companies.

Indeed, a lot of mathematical results have been formalized, using many different proof assistants. Hence, if one want to use two already proved theorems in her development, there is a high risk that these two proofs are in different systems.

To avoid the community the burden of redevelopping the same proofs in each system, the LOGIPEDIA project aims at building an encyclopedia of formal proofs, agnostic in the system they were developed in. To do so, the logics of the proof assistants can be encoded in the same *Logical Framework: DEDUKTI*, which is based of the λΠ-calculus modulo rewriting. Once all the logics are encoded in the same framework, it becomes easier to compare them, and so to export to a target system proofs originally made in another system.

In this article, we present an encoding of two common features, shared by many proof assistants.

The first one is universe polymorphism. Introduced by Harper and Pollack [14], this allows the user to declare a symbol only once for all universe levels, and then to instantiate it several times with concrete levels.

The second one is equality modulo $\eta$. In set theory, a function is identified with its graph, hence two functions outputing the same result when fed with the same data are equal. In type theory, it is not the case. $\eta$-conversion is a weak form of this principle of extensionality, which just states that $f$ is equal to the function associating to any $x$ the result of $f$ applied to $x$.

<figure><img src="image_2.png" /></figure>

© Guillaume Genestier;

licensed under Creative Commons License CC-BY

5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020).

Editor: Zena M. Ariola; Article No. 31; pp. 31:1–31:17

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 31:2 Encoding Agda Programs Using Rewriting

Developped for twenty years, AGDA is a dependently-typed functional programming language based on an extension Martin-Löf's type theory. Thanks to Curry-Howard correspondence, it is often used as a proof assistant. Furthermore, it features the two ingredients this article focuses on. Hence, the author developed, in collaboration with Jesper Cockx, an automatic translator from a fragment of AGDA to DEDUKTI.

### Outline

After a brief presentation of the λΠ-calculus modulo rewriting, Section 2 introduces the Cousineau-Dowek's encoding of *Pure Type Systems*. Section 3 presents a general encoding of universe polymorphism and an instantiation of this encoding in the special case of the predicative two-ladder universe system behind AGDA. The main theorem of this section is the preservation of typability of this encoding. Then, Section 4 explains how to encode η-conversion using rewriting. Preservation of the conversion is the main result of this section. Finally, after a presentation of the implementation in Section 5, Section 6 summarizes our result and provides hints on future extensions.

## 2 Encoding Pure Type Systems in λΠ-modulo Rewriting

In [3], Barendregt presents the λ-cube, a classification of eight widely used type systems, distinguishing themselves from each other by the possibility they offer (or not) to quantify on a type, a term to construct a type, or a term.

Those constructions of systems in the λ-cube were generalized by Terlouw and Berardi [5], giving birth to what they called “generalized type system”, nowadays more often called *Pure Type Systems* (PTS).

Every PTS shares the same typing rules. The only difference between them are the relations $\mathcal{A}$ and $\mathcal{R}$. $\mathcal{A}$, called axioms, states inhabitation between sorts and $\mathcal{R}$, called rules, controls on which sort one can quantify.

**► Definition 1 (Syntax and typing of PTS).** Let $\mathcal{X}$ be an infinite set of variables and $S$ be the set of sorts.

$$ t, u ::= s \mid x \mid (x : t) \to u \mid \lambda x^t . u \mid tu \qquad \text{with } s \in \mathcal{S} \text{ and } x \in \mathcal{X} $$

The typing rules include 5 introduction rules related to the syntax, and 2 structural rules.

$$ (var) \qquad \frac{\Gamma \vdash A : s}{\Gamma, x : A \vdash x : A} x \notin \text{dom}(\Gamma) $$

$$ (ax) \qquad \frac{\vdash_{s_1 : s_2} (s_1, s_2) \in \mathcal{A}}{\text{prod}} \qquad \frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash (x : A) \to B : s_3} (s_1, s_2, s_3) \in \mathcal{R} $$

$$ (app) \qquad \frac{\Gamma \vdash t : (x : A) \to B \quad \Gamma \vdash u : A}{\Gamma \vdash t u : B [u/x]} \qquad \frac{\Gamma \vdash (x : A) \to B : s \quad \Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda x^{A.t} : (x : A) \to B} $$

$$ (conv) \qquad \frac{\Gamma \vdash t : A \quad \Gamma \vdash B : s}{\Gamma \vdash t : B} A \rightsquigarrow_{\beta} B \qquad \text{weak} \qquad \frac{\Gamma \vdash A : s \quad \Gamma \vdash t : B}{\Gamma, x : A \vdash t : B} x \notin \text{dom}(\Gamma) $$

**► Definition 2 (Functional Pure Type System).** A PTS is called functional if axioms and rules are functional relations, respectively from $S$ and $S \times S$ to $S$.

One can be even more restrictive on the class of PTS's considered, by defining a special case of *functional PTS*, the *full PTS*.
**► Definition 3 (Full Pure Type System).** A PTS is called full if axioms and rules are total functions, respectively from $S$ and $S \times S$ to $S$.

**► Example 4 ($\mathcal{P}^\infty$ and $\mathcal{C}^\infty$).** The predicative and impredicative infinite hierarchies, are two full PTS: $\mathcal{P}^\infty$ is $S = \{*_i | i \in \mathbb{N}\}$; $\mathcal{A} = \{(*_i,*_j,*_k)\}$; $\mathcal{R} = \{(*_i,*_j,*_k) | k = \max(i, j)\}$ whereas $\mathcal{C}^\infty$ is $S = \{*_i | i \in \mathbb{N}\}$; $\mathcal{A} = \{(*_i,*_i+1)\}$; $\mathcal{R} = \{(*_i,*_j,*_k) | j \ge 1 \text{ and } k = \max(i, j)\} \cup \{(*_i,*_0,*_0)\}$.

**► Definition 5 (Embedding of PTS).** Given $P_1 = (S_1; \mathcal{A}_1; \mathcal{R}_1)$ and $P_2 = (S_2; \mathcal{A}_2; \mathcal{R}_2)$ two PTS, $f: S_1 \to S_2$ is an embedding of $P_1$ in $P_2$ if for all $(s, s') \in \mathcal{A}_1$, we have $(f(s), f(s')) \in \mathcal{A}_2$ and for all $(s, s', s'') \in \mathcal{R}_1$, we have $(f(s), f(s'), f(s'')) \in \mathcal{R}_2$.

f is extended to terms of $P_1$, by:
$$f(x) = x, \text{ if } x \in \mathcal{X}; \qquad f(\lambda x^A.t) = \lambda x^{f(A)}.f(t);$$
$$f(tu) = f(t)f(u); \qquad f((x: A) \to B) = (x: f(A)) \to f(B).$$

**► Proposition 6 (Soundness of the Embedding).** If $f$ is an embedding from a PTS $P_1$ to $P_2$, if $\Gamma \vdash_{P_1} t : A$, then $f(\Gamma) \vdash_{P_2} f(t) : f(A)$.

*Proof.* By induction on the proof tree. Since $f$ preserves $\mathcal{A}$ and $\mathcal{R}$, the $(ax)$ and $(prod)$ cases are satisfied. All the other cases are direct, since $f$ does not act on the shape of terms. ◀

The Edinburgh Logical Framework [13] (LF), denoted $\lambda P$ in Barendregt's $\lambda$-cube is the minimal PTS including dependent types. It has two sorts $S = \{\star, \Box\}$, with the axioms $\mathcal{A} = \{(\star, \Box)\}$ and the rules $\mathcal{R} = \{(\star, \star, \star), (\star, \Box, \Box)\}$. It is well-known to be “a framework for defining logics”, since it allows to encode most of the proof systems. One can note, LF is not a Full PTS, since $\Box$ is the left-hand side of no axioms.

The logic behind the *Logical Framework DEDUKTI* is the $\lambda\Pi$-calculus modulo rewriting [2, 6], an extension of the Edinburgh Logical Framework with user-defined rewrite rules used not only to define functions, but also types, allowing for shallow embedding of various type systems. Indeed, even if one can encode many logics in LF, those encodings are deep, meaning that applications, $\lambda$-abstractions and variables of the encoded system are not translated directly by their equivalent in LF, but by using explicit symbols App, Lam and Var. Using rewriting, the introduction of those extra symbols can be avoided, allowing for more reasonable size translations.

**► Definition 7 (Signature in $\lambda\Pi$-modulo rewriting).** A signature in $\lambda\Pi$-modulo rewriting is $(\Sigma, \Theta, \mathbb{R})$ where $\Sigma$ is a set of symbols, disjoint of $\mathcal{X}$, $\Theta$ is a function from $\Sigma$ to terms and $\mathbb{R}$ is a set of rewriting rules, i.e. a set of pair of terms of the form $f \vec{l} \leftrightarrow r$, with $f \in \Sigma$ and all $l_i$'s are Miller's pattern [16].

We say that $t$ rewrites to $u$, denoted $t \rightsquigarrow u$ if there is a rule $f \vec{l} \leftrightarrow r$, a substitution $\sigma$ and a “term with a hole” $C[]$, such that $t = C[(f \vec{l})\sigma]$ and $u = C[r\sigma]$. $\rightsquigarrow$ is the smallest relation containing $\leftrightarrow$ and stable by substitution and context. We denote by $\rightsquigarrow^*$ the reflexive transitive closure of $\rightsquigarrow$ and by $\leftrightarrow^*$ the convertibility relation, which is the reflexive symmetric and transitive closure of $\rightsquigarrow$.

**► Definition 8 (Typing rules of $\lambda\Pi$-modulo rewriting).** They are the one of LF (those of Def. 1, instantiated with $S = \{\star, \Box\}$, $\mathcal{A} = \{(\star, \Box)\}$ and $\mathcal{R} = \{(\star, \star, \star), (\star, \Box, \Box)\}$), but with a rule to introduce symbols of $\Sigma$ and enrichment of the conversion, to include both $\beta$-reduction and the user-defined rewriting rules.

$$ (\mathit{sig}) \quad \frac{\Gamma \vdash \Theta(f) : s \quad f \in \Sigma}{\Gamma \vdash f : \Theta(f)} \qquad (\mathit{conv}) \quad \frac{\Gamma \vdash t : A \quad \Gamma \vdash B : s}{\Gamma \vdash t : B} \quad A \rightsquigarrow^* \beta \cup \mathbb{R} \ B $$
31:4 Encoding Agda Programs Using Rewriting

In 2007, Cousineau and Dowek [8] proposed an encoding of any functional PTS in DEDUKTI. Their encoding contained two symbols for each sort, and one symbol for each axiom or rule. However, having an infinite number of symbols and rules is not well-suited for implementations. Hence, to encode *Pure Type Systems* with an infinite number of sorts, one prefers to have a type *Sort* for sorts and only one symbol for products [1]. For *full Pure Type Systems*, this extension is quite straightforward. The general encoding of full PTS is:

First the PTS specification: a type of sorts and two functions for $\mathcal{A}$ and $\mathcal{R}$.

constant Sort : TYPE.
symbol axiom : Sort ⇒ Sort.      symbol rule : Sort ⇒ Sort ⇒ Sort.

For each sort $s$, a type $Univ s$ containing the codes of its elements. Indeed, since the $\lambda\Pi$-calculus, does not allow to quantify over types, one needs to declare the type of the logic we are encoding, not directly as a type, but as a code, which can be decoded to a type using rewriting rules.

constant Univ : (s : Sort) ⇒ TYPE.

Then a symbol to decode the elements of $Univ s$ as type of $\lambda\Pi$-modulo rewriting.

symbol Term : (s : Sort) ⇒ Univ s ⇒ TYPE.

The encoding of sorts and the rewrite rule to decode it. (Simulates the rule $(ax)$ of a PTS).

constant code : (s : Sort) ⇒ Univ (axiom s).
Term _ (code s) → Univ s.

The encoding of products and its decoding rewrite rule. (Simulates the rule $(prod)$ of a PTS).

constant prod : (s1 : Sort) ⇒ (s2 : Sort) ⇒
(A : Univ s1) ⇒ (Term s1 A ⇒ Univ s2) ⇒ Univ (rule s1 s2).
Term _ (prod a b A B) → (x : Term a A) ⇒ Term b (B x).

Then the peculiarity of each PTS is reflected in the encoding of the elements of $S$ as terms of *Sort*, and in the implementation of *axiom* and *rule* to encode $\mathcal{A}$ and $\mathcal{R}$ respectively.

3 Universe Polymorphism and its Encoding

It is quite common to enrich PTS with *Universe Polymorphism* [14], which consists in
allowing the user to quantify over *universe levels*, allowing to declare simultaneously a symbol
for several sorts. For instance, if the sorts are { Set<ι> | ι ∈ N }, then one want to declare *List*
in ∀ι, (A : Set<ι>) → Set<ι>. Indeed, just like polymorphism was used to avoid declaring a type
of lists for each type of elements, one want to avoid one declaration of a new type of lists for
each universe level.

We present here a definition of *universe polymorphism* inspired by the one given by Sozeau and Tabareau [19] for the proof assistant COQ. In this setting, the context contains three lists: a list $\Sigma$ called signature, a list $\Theta$ of level variables, and a list $\Gamma$ called local context. Both $\Sigma$ and $\Gamma$ contain pairs of a variable name and a type, but the variables in $\Gamma$ can contain free level variables (those occuring in $\Theta$), whereas all the level variables are bound by a prenex quantifier $\forall$ in the signature $\Sigma$. Unlike [19], we do not need to store constraints between universe levels, since those constraints are related to cumulativity, a feature we are not trying to encode here.
**► Definition 9 (Uniform Universe Polymorphic Full PTS).** We consider a set $\mathbb{L}$ of levels and a finite set $\mathcal{H}$ of sort constructors. Then the sorts are $\{s_\ell\}_{\ell \in \mathcal{H}, \ell \in \mathbb{L}}$.

In addition to functionality and totality of $\mathcal{A}$ and $\mathcal{R}$, we assume a uniformity in the hierarchy. Meaning that for all $s \in \mathcal{H}$, there is a $s' \in \mathcal{H}$, such that for all $\ell \in \mathbb{L}$, there is a $\ell' \in \mathbb{L}$, such that $(s_\ell, s'_{\ell'}) \in \mathcal{A}$ and for all $s^{(1)}, s^{(2)} \in \mathcal{H}$, there is a $s^{(3)} \in \mathcal{H}$, such that for all $\ell_1, \ell_2 \in \mathbb{L}$, there is $\ell_3 \in \mathbb{L}$ such that $(s_{\ell_1}^{(1)}, s_{\ell_2}^{(2)}, s_{\ell_3}^{(3)}) \in \mathcal{R}$.

We denote by $\bar{\mathcal{A}}$ the function $\{(s, s') \in \mathcal{H}^2 | \exists \ell, \ell', (s_\ell, s'_{\ell'}) \in \mathcal{A}\}$ and for all $s$ by $\mathcal{A}_s$ the function $\{(\ell, \ell') \in \mathbb{L}^2 | \exists s', (s_\ell, s'_{\ell'}) \in \mathcal{A}\}$.

Analogously $\bar{\mathcal{R}}$ is the function $\{(s^{(1)}, s^{(2)}, s') \in \mathcal{H}^3 | \exists \ell_1, \ell_2, \ell', (s_{\ell_1}^{(1)}, s_{\ell_2}^{(2)}, s_{\ell'}) \in \mathcal{R}\}$ and for all $(s^{(1)}, s^{(2)})$, $\mathcal{R}_{s^{(1)},s^{(2)}}$ is the function $\{(\ell_1, \ell_2, \ell') \in \mathbb{L}^3 | \exists s', (s_{\ell_1}^{(1)}, s_{\ell_2}^{(2)}, s_{\ell'}) \in \mathcal{R}\}$.

The typing rules are:

$$ (\mathit{lvl}) \qquad \overline{\Theta \vdash \ell \ \mathit{isLvl}} \ \ell \in \mathbb{L} \qquad (\mathit{ax}) \qquad \frac{\Theta \vdash \gamma \ \mathit{isLvl}}{[\quad; \Theta; [\quad \vdash s_\gamma : s'_{\mathcal{A}_s(\gamma)} \quad \quad (s, s') \in \bar{\mathcal{A}}]} $$

$$ (\mathbb{Lvar}) \qquad \overline{\Theta \vdash i \ \mathit{isLvl}} \ i \in \Theta \qquad (\mathit{abs}) \qquad \frac{\Sigma; \Theta, \Gamma \vdash (x : A) \to B : s_\gamma \quad \Sigma; \Theta, \Gamma : x : A \vdash t : B}{\Sigma; \Theta; \Gamma \vdash \lambda(x : A).t : (x : A) \to B} $$

$$ (\mathbb{L}A) \qquad \frac{\Theta \vdash \ell \ \mathit{isLvl}}{\Theta \vdash \mathcal{A}_s(\ell) \ \mathit{isLvl}} \qquad (\mathit{app}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash t : (x : A) \to B \quad \Sigma; \Theta; \Gamma \vdash u : A}{\Theta; \Gamma \vdash t u : B [u/x]} $$

$$ (\mathbb{L}\mathcal{R}) \qquad \frac{\Theta \vdash \ell_1 \ \mathit{isLvl}}{\Theta \vdash \mathcal{R}_{s s'}(\ell_1, \ell_2) \ \mathit{isLvl}} \qquad (\mathit{conv}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash t : A \quad \Sigma; \Theta; \Gamma \vdash B : s_\gamma}{\Sigma; \Theta; \Gamma \vdash t : B} \quad A \rightsquigarrow_B^* B $$

$$ (\mathit{var}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash A : s_\gamma}{\Sigma; \Theta; \Gamma, x : A \vdash x : A} x \notin \Sigma, \Gamma \qquad (\mathit{sig}) \qquad \frac{\Sigma; \Theta; [\quad \vdash A : s_\gamma}{\Sigma, x : \forall \Theta.A; \Theta'; [\quad \vdash x : \forall \Theta.A} x \notin \Sigma, \Gamma $$

$$ (\mathit{inst}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash t : \forall [i_1, \dots, i_n], A \quad \Theta \vdash \gamma_1 \ \mathit{isLvl} \quad \dots \quad \Theta \vdash \gamma_n \ \mathit{isLvl}}{\Sigma; \Theta; \Gamma \vdash t[\gamma_1, \dots, \gamma_n] : A [\gamma_k/i_k]_k} $$

$$ (\mathit{prod}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash A : s_\gamma \quad \Sigma; \Theta; \Gamma : x : A \vdash B : s'_{\gamma'}(s, s', s'') \in \bar{\mathcal{R}}}{\Sigma; \Theta; \Gamma \vdash (x : A) \to B : s''_{\mathcal{R}_{s,s'}(\gamma, \gamma')}} $$

$$ (\mathit{ctx-weak}) \qquad \frac{\Sigma; \Theta; \Gamma \vdash A : s_\gamma \quad \Sigma; \Theta; \Gamma \vdash t : B}{\Sigma; \Theta; \Gamma, x : A \vdash t : B} x \notin \Sigma, \Gamma $$

$$ (\mathit{sig-weak}) \qquad \frac{\Sigma; \Theta; [\quad \vdash A : s_\gamma \quad \Sigma; \Theta' ; [\quad \vdash t : B]}{\Sigma, x : \forall \Theta.A; \Theta'; \Gamma \vdash t : B} x \notin \Sigma, \Gamma $$

In all those typing rules, $s, s' \in \mathcal{H}$ and $i, x \in \mathcal{X}$. Furthermore, we allowed ourselves to simply write $x \notin \Sigma, \Gamma$, rather than “for all $A$, $x : A$ is not in $\Sigma, \Gamma$”.

One typical case of use, is to have only one hierarchy: $\mathcal{H} = \{\text{Set}\}$ and to use natural numbers for levels: $\mathbb{L} = \mathbb{N}$. But we do not want to restrict ourselves to have only one hierarchy, since some proof assistants feature several. For instance, in AGDA and COQ, there are 2, called Set and Prop, and Type and SProp respectively.

The two rules modifying the signature $\Sigma$, allows to completely change the set $\Theta$ of names of local variables. Changing this set during the proof is not necessary, however, without this renewal of $\Theta$, all the symbols in the signature would have been quantified over the same set $\Theta$, no matter which variables occur really in it.

The universe polymorphism we are interested in is purely prenex. Furthermore, universally quantified types are not typed themselves and are only inhabited by variables. This form of universe polymorphism only provides ease of use, but it does not allow to prove more, meaning that it does not compromise the consistency of the logic.
31:6 Encoding Agda Programs Using Rewriting

To prove this, one can construct a new PTS ($S^\Theta$, $A^\Theta$, $R^\Theta$) simply by adding a brand new sort for every expression containing a level variable (such expressions are in $\mathbb{L}_\Theta^+$). Then embedding this newly-constructed PTS in the original one is defined just by interpreting level variables. Then using this interpretation of the variables, one can mimic the proofs done using universe polymorphism in the original PTS.

**Proposition 10 (Conservativity of the universe polymorphism).** Let $P = (\mathbb{L}, \mathcal{H}, A, R)$ be a uniform universe polymorphic full PTS and $\Theta$ be a subset of $\mathcal{X}$.

Let $\mathbb{L}_\Theta^+$ be the smallest subset such that:

$$ \mathbb{L}_\Theta^+ = \Theta \cup \{ \mathcal{A}_s(l) \mid s \in \mathcal{H}, l \in \mathbb{L}_\Theta^+ \} \cup \{ \mathcal{R}_{ss'}(l_1, l_2) \mid s, s' \in \mathcal{H}, (l_1, l_2) \in (\mathbb{L} \cup \mathbb{L}^+)^2 \setminus \mathbb{L}^2 \}. $$

Let $\mathcal{X}^+ = \mathcal{X} \cup \{y[l_1, \dots, l_n] \mid y \in \mathcal{X}, n \in \mathbb{N}, (l_1, \dots, l_n) \in (\mathbb{L} \cup \mathbb{L}_\Theta^+)^n\}$ and $P^\Theta$ be the PTS:

$$ S^\Theta = \{ s_l \mid s \in \mathcal{H}, l \in \mathbb{L} \cup \mathbb{L}_\Theta^+ \}; \quad A^\Theta = A \cup \left\{ \left( s_l, s'_{A_s(l)} \right) \mid (s, s') \in \bar{A}, l \in \mathbb{L}_\Theta^+ \right\} $$

$$ R^\Theta = R \cup \left\{ \left( s_{l_1}, s'_{l_2}, s''_{R_{ss'}(l_1, l_2)} \right) \mid (s, s', s'') \in \bar{R}, (l_1, l_2) \in (\mathbb{L} \cup \mathbb{L}^+)^2 \setminus \mathbb{L}^2 \right\} $$

a. There is an embedding from $P^\Theta$ to the underlying PTS of P.

b. If $\Sigma; \Theta; \Gamma \vdash t : A$ in P and A is not a universal quantification, then there is a

$$ \bar{\Sigma} \subset \left\{ x[l_1, \dots, l_n] : A' \mid x : \forall [y_1, \dots, y_n]. A \in \Sigma, A' = A \left[ \frac{l_i}{y_i} \right]_{i=1 \dots n} \text{ and all } l_i \in \mathbb{L} \cup \mathbb{L}_\Theta^+ \right\} $$

such that $\bar{\Sigma}, \Gamma \vdash_{P^\Theta} t : A$ using the enriched set of variables $\mathcal{X}^+$.

**Proof sketch.** a. The embedding consists in just choosing a level for each variable in $\Theta$.

b. Since A is not a universal quantification, in the proof of $\Sigma; \Theta; \Gamma \vdash t : A$, all the (sig) are followed directly by an arbitrary number of weakenings and a (inst). The weakenings can be anticipated and to create a proof in $P^\Theta$, the (sig) and (inst) are compressed in a single introduction of a variable of $\bar{\Sigma}$. $\blacksquare$

In a PTS, if $\Gamma \vdash t : A$, then there is a sort $s$ such that $A = s$ or $\Gamma \vdash A : s$. In a full PTS, $A$ is a total function, hence, all sorts inhabit a sort, allowing us to refer to $s$ as the sort of a $A$. However, in the presentation of universe polymorphism of Def. 9, this property is lost because universally quantified types have no type. To overcome this issue, we assign artificially a type to those quantified types, using a brand new sort $\text{Sort}_\omega$, which is not typable, is the type of no sort and over which one cannot quantify. Its only purpose is to make “the sort of $A$” well-defined whenever $A$ is inhabited. It must be noted that Sort is not in $\mathcal{H}$ and $\omega$ is not a level.

To encode Universe Polymorphic Full PTS, one introduce a symbol `sortOmega` and a quantification symbol $\forall_{\mathbb{L}}$ which takes as first argument the sort in which the term will live once instanciated. The definition of the decoding function `Term` is enriched with a new rule, specifying its behaviour when applied to a $\forall_{\mathbb{L}}$.

**Definition 11 (Encoding).**

constant `sortOmega` : Sort.

constant $\forall_{\mathbb{L}}$ : (f:(\mathbb{L}⇒Sort)) ⇒ ((1:\mathbb{L}) ⇒ Univ (f 1)) ⇒ Univ `sortOmega`.

Term _ ($\forall_{\mathbb{L}}$ f t) → (1 : \mathbb{L}) ⇒ Term (f 1) (t 1).

For instance, the encoding of $\forall \ell$, Set$_\ell$ is $\forall_{\mathbb{L}}$ ($\lambda 1$, axiom (set 1)) ($\lambda 1$, code (set 1)), if `set` is a sort constructor in the encoding. And its decoding (when applying `Term sortOmega`) is, as expected, $(1:\mathbb{L}) \Rightarrow Univ (set 1)$.
**► Example 12.** Consider the system $\mathcal{H} = \{s, \sigma\}$, $\mathcal{A} = \{(A_i, s_{ax_A(i)}) | A \in \mathcal{H}\}$ and $\mathcal{R} = \{(A_i, B_j, B_{ru(i,j)}) | A, B \in \mathcal{H}\}$, with $ax_s$, $ax_\sigma$ and $ru$ three functions remaining abstract here. $ru$ could be indexed by two sorts, for ease of readability, we have chosen not present such a general case.

(; one symbol for each sort constructor ;)

constant s : L ⇒ Sort.          constant σ : L ⇒ Sort.

(; Function axiom ;)

symbol axiom : Sort ⇒ Sort.

symbol ax_s : L ⇒ L.          symbol ax_σ : L ⇒ L.

axiom (s i) → s (ax_s i).      axiom (σ i) → s (ax_σ i).

(; Function rule ;)

symbol rule : Sort ⇒ Sort ⇒ Sort.  symbol ru : L ⇒ L ⇒ L.

rule (s i) (s j) → s (ru i j).    rule (s i) (σ j) → σ (ru i j).

rule (σ i) (s j) → s (ru i j).    rule (σ i) (σ j) → σ (ru i j).

**► Definition 13 (Translation).** We translate well-typed terms in a Universe Polymorphic Full Pure Type System by: $\|x\| = x$; $\|s_\ell\| = \text{code } |s_\ell|_S$; $\|t u\| = \|t\| \|u\|$;

$$ \|\lambda x^A.t\| = \lambda(x : \text{Term } |s_A|_S \|A\|) \cdot \|t\|; $$

$$ \|(x : A) \to B\| = \text{prod } |s_A|_S |s_B|_S \|A\| \quad (\lambda x : \text{Term } |s_1|_S \|A\| \cdot \|B\|); $$

$$ \|\forall [\ell_1, \dots, \ell_n], A\| = \forall_L (\lambda \ell_1 : \mathbb{L}. \ \text{sortOmega}) \quad (\lambda \ell_1 \dots \forall_L (\lambda \ell_n : \mathbb{L} \cdot |s_A|_S) \quad (\lambda \ell_n : \mathbb{L} \cdot \|A\|) \dots); $$

$$ \|A[\gamma_1, \dots, \gamma_n]\| = \|A\| \cdot |\gamma_1|_L \cdots |\gamma_n|_L. $$

The translation of sorts is $|\text{Sort}_\omega|_S = \text{sortOmega}$, $|s_\gamma|_S = s$ $|\gamma|_L$.

And the translation of levels is $|i|_L = i$ if $i \in \mathcal{X}$;

$$ |\mathcal{A}_s(\ell)|_L = \text{ax\_s} \cdot |\ell|_L \quad \text{and} \quad |\mathcal{R}_{ss'}(\ell_1, \ell_2)|_L = \text{ru\_ss'} \cdot |\ell_1|_L |\ell_2|_L. $$

Wherever they are used, $s_A$ and $s_B$ are respectively the sorts of A and B.

It can be noted that the translation $|\ell|_L$ for $\ell \in \mathbb{L}$ is not given, since in general the number of level is infinite, hence, we do not want to introduce one new symbol per level. Furthermore, with universe polymorphism, universe levels are open terms, hence, convertibility between universe levels is now an issue. Fortunately, it is the last one, since once this issue is overcome, the encoding has one of the expected properties: we type check at least as much terms as in the original system.

To state this, we start with two useful lemmas:

**► Lemma 14 (Substitution and conversion).**

a. If $x$ is a free variable in $t$ such that $t$ and $t[u/x]$ are well-typed, $\|t[u/x]\| = \|t\| \cdot \|u/x\|$;

b. If $\ell$ is a level variable in $t$ such that $t$ and $t[u/\ell]$ are well-typed, $\|t[u/x]\| = \|t\| \cdot \|u_L/x\|$;

c. If $t \leadsto \beta u$, then $\|t\| \leadsto \beta \|u\|$.

**Proof.** a and b are proved by induction on the term $t$. c is because a $\beta$-redex is translated as a $\beta$-redex. ◀

The proof of this property is only sketched, since Section 4 will contain detailed proofs on the conversion specifically.

**► Lemma 15 (Shape-preservation of type).**

a. If $s$ is a sort, $\text{Term} \cdot |\mathcal{A}(s)|_S \|s\| \leadsto^* \text{Univ} \cdot |s|_S$,

b. If $(x: A) \to B$ is of sort $s$, $\text{Term} \cdot |s|_S \|(x: A) \to B\| \leadsto^* (x: \text{Term} \cdot |s_A|_S \|A\|) \Rightarrow \text{Term} \cdot |s_B|_S \|B\|$;

c. If $\ell_1 < \dots < \ell_n$, $\text{Term} \cdot \text{sortOmega} \quad \|\forall \{\ell_i\}_i, A\| \leadsto^* (\ell_1 : \mathbb{L}) \Rightarrow \dots \Rightarrow (\ell_n : \mathbb{L}) \Rightarrow \|A\|$.

**Proof.** The three rules on Term are crafted to ensure those properties. ◀
31:8 Encoding Agda Programs Using Rewriting

To state properly the Correctness Theorem, one first has to define the translation of contexts:

► **Definition 16 (Context Translation).** If $\Sigma = x_1 : T_1, \dots, x_l : T_l, \Theta = i_1, \dots, i_m$ and $\Gamma = y_1 : A_1, \dots, y_n : A_n$, then the translation is $\|\Sigma; \Theta; \Gamma\| = x_1 : \mathbf{Term} \ \mathbf{sortOmega} \ \|T_1\|, \dots, x_l : \mathbf{Term} \ \mathbf{sortOmega} \ \|T_l\|, i_1 : \mathbb{L}, \dots, i_m : \mathbb{L}, y_1 : \mathbf{Term} \ |s_{A_1}|_S \ |A_1|, \dots, y_n : \mathbf{Term} \ |s_{A_n}|_S \ |A_n|.$

► **Theorem 17 (Correctness).** Given a correct criterion for equality of levels (i.e. if two levels $\ell_1$ and $\ell_2$ are equals, their translations $|\ell_i|_L$ are convertible), for a Universe Polymorphic Full Pure Type System P, if $\Sigma; \Theta; \Gamma \vdash t : A$, then $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \|t\| : \mathbf{Term} \ |s|_S \ |A|$, where $s$ is the sort of $A$.

**Proof.** By induction on the derivation. We assume that if $\Theta \vdash \gamma$ is Lvl, then $\|\|\|; \Theta; \|\|\|$ $\vdash_{\lambda\Pi/P} |\gamma|_L : \mathbb{L}$, a property which can be proved by induction on the derivation, with the assumption that for all $\ell \in \mathbb{L}$, $\vdash_{\lambda\Pi/P} |\ell|_L : \mathbb{L}$. We then consider the 10 remaining cases:

(var) By induction hypothesis, $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \|A\| : \mathbf{Univ} \ |s_\gamma|_S$. Hence $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \mathbf{Term} \ |s_\gamma|_S \ |A\| : \mathbf{TYPE}$, so one can introduce a variable of this type.

(ax) The translation of $s_\gamma$ is code ($s|_{\gamma|_L}$) which lives in Univ ($s'$ ($\mathbf{ax\_s}|_{\gamma|_L}$)), which is the reduct of the translation as type of $s'_A$ ($\gamma$).

(abs) By induction hypothesis, $\|\Sigma; \Theta; \Gamma\|, x : \mathbf{Term} \ |s|_S \ |A\| \vdash_{\lambda\Pi/P} \|t\| : \mathbf{Term} \ |s'|_S \ |B\|$, hence, one has that $\lambda(x : \mathbf{Term} \ |s|_S \ |A\|).t$ inhabits $(x : \mathbf{Term} \ |s|_S \ |A\|) \to \mathbf{Term} \ |s'|_S \ |B\|$, which is the reduct of the translation as type of $(x : A) \to B$. The other induction hypothesis $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \|(x : A) \to B\| : \mathbf{Univ} \ |s_\gamma|_S$ ensures us that $\mathbf{Term} \ |s|_S \ |A\|$ lives in TYPE.

(app) By the induction hypothesis and the Lem. 15, one can apply the translation of $t$ to the translation of $u$. The result lives in the translation of $B[u/x]$ thanks to Lem. 14.

(conv) This is a direct consequence of Lem. 14 and the induction hypotheses.

(sig) By induction hypothesis, $\|\Sigma; \Theta; \|\|\|$ $\vdash_{\lambda\Pi/P} \|A\| : \mathbf{Univ} \ |s_\gamma|_S$. Hence, one can use the (prod) rule of $\lambda\Pi$-modulo rewriting to move all the $i : \mathbb{L}$ from the context to the term. By Lem. 15, the product obtained is convertible with $\|\forall\Theta.A\|$, hence one can introduce a variable of this type. One must then use the weakening, to Re-invent the variables of type $\mathbb{L}$ corresponding to the $\Theta'$.

(inst) Lem. 15 tells us that, after conversion, the induction hypothesis is $\|\Sigma; \Theta; \Gamma\| \vdash \|A\| : (\ell_1 : \mathbb{L}) \to \dots \to (\ell_n : \mathbb{L}) \to \|X\|$, hence, we can apply the $\gamma_i$'s without type issues.

(prod) By induction hypothesis, we have $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \|A\| : \mathbf{Univ} \ |s_\gamma\|$ and also $\|\Sigma; \Theta; \Gamma, x : A\| \vdash_{\lambda\Pi/P} \|B\| : \mathbf{Univ} \ |s'_\gamma\|$, so $\|\Sigma; \Theta; \Gamma\|, x : \mathbf{Term} \ |s_\gamma|_S \ |A\| \vdash_{\lambda\Pi/P} \|B\| : \mathbf{Univ} \ |s'_\gamma\|$ and we can conclude by introducing the lambda and applying prod.

(ctx-weak) As before, we have $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \|A\| : \mathbf{Univ} \ |s_\gamma\|$, so $\|\Sigma; \Theta; \Gamma\| \vdash_{\lambda\Pi/P} \mathbf{Term} \ |s_\gamma|_S \ |A\| : \mathbf{TYPE}$, so one can weaken with a variable of this type.

(\textbf{\textit{weak}}) Like for the (sig) rule, one can empty the context of the variables of type $\mathbb{L}$ by applying the rule (prod) of $\lambda\Pi$-modulo rewriting. Then, one can weaken with a variable of this type and variables of type $\mathbb{L}$ to translate the $\Theta'$.

Now, we will more specifically focus on a specific hierarchy of levels, where $\mathbb{L} = \mathbb{N}$ and all the $A_s$ are the successor function and all $R_{ss'}$ are the maximum function. This is the predictive hierarchy of $P^\infty$ (Expl. 4), used in AGDA for instance.

The grammar of universe level we are interested in is: $t, u \in \mathcal{L} ::= x \in \mathcal{X} \mid 0 \mid st \mid \max tu:$

constant $\mathbb{L}$ : TYPE.

symbol $s$ : $\mathbb{L} \Rightarrow \mathbb{L}$.

symbol 0 : $\mathbb{L}$.

symbol $\max$ : $\mathbb{L} \Rightarrow \mathbb{L} \Rightarrow \mathbb{L}$.
31:10 Encoding Agda Programs Using Rewriting

<figure><img src="image_4.png" /></figure>

And finally we give rewrite rules for the symbols of the syntax:

<figure><img src="image_5.png" /></figure>

This encoding is not confluent, as the following example illustrates:

<figure><img src="image_6.png" /></figure>

But this is not an issue, since we are only interested in reducts of elements of the syntax,
meaning that all the variables are of type $\mathbb{L}$.

**Proposition 18.** The absence of variable of type $\mathbb{N}$ or $\mathbb{LvlSet}$ ensures the uniqueness of normal form (modulo AC) property.

**Proof.** Since there are no variables of type $\mathbb{N}$ and $\mathbb{LSet}$, the function $\max_N$, $+_N$ and $\text{mapPlus}$ are fully defined and cannot occur in the normal forms.

Hence, normal forms contain only $0_\mathbb{N}$, $s_\mathbb{N}$, $\text{Max}$, $\emptyset$, $\oplus$ and $\cup$. Among it, the only constructor of a $\mathbb{L}$ is $\text{Max}$, hence every level is either a variable or headed by $\text{Max}$.

If it contains a $\text{Max}$, there is one at the head. Hence the terms are of the form $\text{Max n s}$ with n a closed natural and s a $\mathbb{LSet}$. If there are more than one $\text{Max}$, it means that the $\mathbb{LSet}$ contains a level which is not a variable. This one, is headed by $\text{Max}$, so one of the rewrite rule regarding the interaction between $\text{Max}$ and $\oplus$ can be applied.

Hence all normal forms are either a variable or of the form $\text{Max n s}$, with n closed natural and s a $\mathbb{LSet}$ where all levels are variable. The non-linear rule ensures us that the variables are all distinct.

One can check that the invariant that every natural which is the first argument of a $\oplus$ is smaller or equal to the first argument of the $\text{Max}$ directly above the $\oplus$ is preserved by every rule and verified by the reducts of the syntax.

So, we can conclude that the normal forms have the shape announced.

To check that a term cannot have two distinct normal forms, the definition of the
interpretation is extended to the symbols we introduced and one can verify that all the rules
preserve the interpretation and that all the terms of the shape we described have a different
interpretation.

◀

4 **Eta-conversion**

Many proof assistants implement, among other conversion rules, the $\eta$ rule, which state that if $f$ is a function, $f \equiv_{\eta} \lambda x.f x$.
At first sight, this conversion might look quite harmless, and one can hope to just add the corresponding rewrite rule. However, this conversion is an important issue for translation of systems in DEDUKTI. Indeed, the contraction rule cannot be stated, since $\lambda x.f x$ is not a Miller pattern: It requires to match on the fact that $f x$ is an application, which would be “meta-matching” and is not in the definition of $\lambda\Pi$-modulo rewriting. Furthermore, we could replace it by $\lambda x.f[x]$, but $f$ is not a valid right-hand side anymore, since it is of arity one. On the other hand, to preserve typing, the expansion rule has to match on the type of a variable, and is not syntax-directed anymore.

Another natural solution could be to define $\lambda\Pi$-modulo rewriting as a logical framework with $\eta$ hard-coded in the conversion (just like $\beta$ is). But this is a path *logical frameworks* want to avoid. Indeed, if $\eta$ is hard-coded, it is impossible to have a shallow encoding of the $\lambda$-calculus without $\eta$-conversion.

One could expect that $\eta$-expanding every term during the translation phase, could allow us to completely ignore $\eta$-conversion in the $\lambda\Pi$-calculus modulo rewriting. Indeed, with dependent types it might happen than an $\eta$-long term has a non-$\eta$-long type. A situation that often breaks the *type preservation of the translation*.

**► Example 19.** To illustrate this, we start by defining a type, whose number of arrows depends on a natural number, with a constructor for this type.

```
symbol D : (x : N) ⇒ TYPE.
D O → N.

constant d : (x : N) ⇒ D x.
D (s x) → N ⇒ D x.
```

We then define a new type depending on the first one and its constructor.

```
symbol E : (x : N) ⇒ D x ⇒ TYPE.
symbol e : (x : N) ⇒ E x (d x).
```

Now, the term `e 1` is $\eta$-long and has type `E 1` (`d 1`), but not `E 1` (`\lambda x, d 1 x`) which is the $\eta$-long form of the type.

To overcome this issue, we propose to postpone $\eta$-expansion, until the type is fully instantiated. For this, we introduce in the translation a symbol $\eta E$, which purpose is to tag with their types the subterms which may become $\eta$-expandable. Then some rewrite rules pattern match on this type annotation to decide when and how the expansion can be performed.

**► Definition 20 (Eta-expansion rewrite rules).** $\eta E$ annotates terms with their types, to do so, it takes as arguments a sort, a code of type in this sort and the term to annotate. The rules state that $\eta$-expansion is the identity for inhabitant of sorts ($\eta S$), and generates $\lambda$'s for inhabitants of products ($\eta P$). Furthermore, a rule state that $\eta$-expansion is an idempotent operation ($\eta I$).

```
symbol ηE : (s : Sort) ⇒ (A : Univ s) ⇒ Term s A ⇒ Term s A.
"ηS" ηE _ (code _ ) t —→ t.
"ηP" ηE _ (prod a b A B) t —→
       λ (x : Term a A), ηE b (B (ηE a A x)) (t (ηE a A x)).
"ηI" ηE _ _ (ηE a A t) —→ ηE a A t.
```

To prove that adding those annotations in the encoding enriches enough the conversion to simulate $\eta$-equality, we will also add those annotations in the system we are translating, just like what is done in [12, 11].

For sake of readibility, we will study in this section, terms typed in a full PTS embeddable in $C^\infty$, like $P^\infty$ and $C^\infty$ defined in Expl. 4, in order to directly reuse the induction principle defined in [4].
31:12 Encoding Agda Programs Using Rewriting

Performing $\eta$-expansion can be required for variables or if an application instantiated a type, allowing it to reduce to a product. Hence, we will add those tags on the variable and application rules. Hence, one could imagine having the rules:

$$ (\text{var}') \qquad \frac{\Gamma \vdash A : s_i}{\Gamma, x : A \vdash x^A : A} \qquad x \notin \text{dom}(\Gamma) \qquad (\text{app}') \qquad \frac{\Gamma \vdash t : (x : A) \to B \quad \Gamma \vdash u : A}{\Gamma \vdash (tu)^B[u/x] : B[u/x]} $$

But those rules, do not have the property that if a term is well-type, its subterms are well-typed with a smaller tree, because of the substitution performed on B. Fortunately, the induction principle defined by Barthe, Hatcliff and Sørensen [4] ensures us that, if we annotate the applications with normal form, this property is verified, leading to:

$$ (\text{app''}) \qquad \frac{\Gamma \vdash t : (x : A) \to B \quad \Gamma \vdash u : A}{\Gamma \vdash (tu)^B[u/x] \downarrow : B[u/x]} $$

One must note here that the same tags can be added to the universe polymorph version of the full PTS considered. Indeed, Prop. 10 ensures us that the set of typable terms are the same in both systems. However, it would require to annotate the $x[l_1, \dots, l_n]$, generating an overweight in the proof, without introducing technicality.

**► Definition 21 (Translation).** Given an annotated well-typed term $t$ in a Full Pure Type System, with the rules (var') and (app'') and the conversion enriched with $\eta$, we translate $t$ by: $||x^A|| = \eta E |s_A|_S ||A|| \mathbf{x}$; $||s|| = \text{code} |s|_S$; $||(tu)^A|| = \eta E |s_A|_S ||A|| (||t|| ||u||)$; $||\lambda x^A.t|| = \lambda(x : \text{Term} |s_A|_S ||A||) . ||t||$; $||(x : A) \to B|| = \text{prod} |s_A|_S |s_B|_S ||A|| (\lambda x : \text{Term} |s_1|_S ||A|| . ||B||)$; $s_A$ and $s_B$ are respectively the sorts of A and B, and $|\cdot|_S$ is the translation of sorts.

The correctness of our translation relies on the preservation of conversion. This result comes from the three following lemmas:

**► Lemma 22 (No $\eta E$ on translation).** If $\Gamma \vdash t : A$, then $\eta E |s_A|_S ||A\downarrow|| ||t|| \rightsquigarrow^* ||t||$.

**► Lemma 23 (Substitution).** If $t$ is well-typed in the context $\Gamma, x_1 : A_1, \dots, x_n : A_n, \Gamma'$ and if $\Gamma \vdash u_1 : A_1, \dots, \Gamma \vdash u_n : A_n$ then $||t|| \left[ ||u_i||/x_i \right]_{i \in \{1, \dots, n\}} \rightsquigarrow^* ||t|| \left[ u_i/x_i \right]_{i \in \{1, \dots, n\}}$.

**► Lemma 24 (Reduction).** If $\Gamma \vdash t : A$ and $t \rightsquigarrow u$, then $||t|| \rightsquigarrow^* ||u||$.

We prove those three lemmas, in this order, by a mutual induction on the combination of the subterm ordering and reduction on a multiset of terms (this multiset is of size at most 2), called “measure” in the proofs.

**Proof of Lem. 22.** We use $||t||$ as the measure. If the normal form of A is a sort, then one can conclude using the rule $\eta S$. We proceed by case on $t$ for the remaining cases:

- If $t = x^B$, then $\eta E |s_A|_S ||A\downarrow|| ||t|| = \eta E |s_A|_S ||A\downarrow|| (\eta E |s_B|_S ||B|| \mathbf{x}) \rightsquigarrow^{\eta I} ||t||$.

- If $t = (uv)^B$, then it is again a direct consequence of the rule $\eta I$.

- If $t = \lambda x_1^{B_1} \dots \lambda x_n^{B_n} .u$, with $u$ not a $\lambda$-abstraction.

There is a C such that: $A\downarrow = (x_1 : B_1\downarrow) \to \dots \to (x_n : B_n\downarrow) \to C$. We denote by $s_i$ the sort of $(x_i : B_i\downarrow) \to \dots \to (x_n : B_n\downarrow) \to C$. We have:
$$
\begin{align*}
& \eta E |s_A|_S \|A\downarrow\| \|t\| \\
&= \eta E |s_A|_S (\mathbf{prod} |s_{B_1}|_S |s_2|_S \|B_1\downarrow\| (\lambda(x_1 : \mathbf{Term} |s_{B_1}|_S \|B_1\downarrow\|). \\
& \qquad \mathbf{prod} \dots |s_{B_n}|_S |s_C|_S \|B_n\downarrow\| (\lambda(x_n : \mathbf{Term} |s_{B_n}|_S \|B_n\downarrow\|). \|C\|) \dots)) \\
& \qquad (\lambda(x_1 : \mathbf{Term} |s_{B_1}|_S \|B_1\|) \dots \lambda(x_n : \mathbf{Term} |s_{B_n}|_S \|B_n\|). \|u\|) \\
&\rightsquigarrow \eta P \quad \lambda(x_1 : \mathbf{Term} |s_1|_S \|B_1\downarrow\|). \eta E |s_2|_S ((\lambda \dots \|C\|)(\eta E |s_1|_S \|B_1\downarrow\| x_1)) \\
& \qquad ((\lambda x_1 \dots \|u\|)(\eta E |s_1|_S \|B_1\downarrow\| x_1)) \\
&\rightsquigarrow^2 \beta \quad \lambda(x_1 : \mathbf{Term} |s_1|_S \|B_1\downarrow\|). \eta E |s_2|_S (\mathbf{prod} |s_{B_2}|_S |s_3|_S \|B_2\downarrow\| \dots \|C\|) \sigma (\lambda x_2 \dots \|u\|) \sigma \\
&\text{with } \sigma = [\eta E |s_1|_S \|B_1\downarrow\| x_1/x_1] \\
& (\rightsquigarrow \eta P \rightsquigarrow^2 \beta)^{n-1} \lambda(x_1 : \mathbf{Term} |s_1|_S \|B_1\downarrow\|) \dots \lambda(x_n : \mathbf{Term} |s_n|_S \|B_n\downarrow\|). \eta E |s_C|_S \|C\| \tau \|u\| \tau \\
&\text{with } \tau = [\eta E |s_i|_S \|B_i\downarrow\| x_i/x_i]_{i \in \{1, \dots, n\}} \\
&\rightsquigarrow^*_{\text{Lem.23}} \lambda(x_1 : \mathbf{Term} |s_1|_S \|B_1\downarrow\|) \dots \lambda(x_n : \mathbf{Term} |s_n|_S \|B_n\downarrow\|). \eta E |s_C|_S \|C\tau'\| \|u\tau'\| \\
&\text{with } \tau' = [x_i^{B_i \downarrow} / x_i]_{i \in \{1, \dots, n\}} \\
&\rightsquigarrow^*_{\text{IH}} \lambda \left\| \lambda x_1^{B_1} \dots \lambda x_n^{B_n} \cdot u \right\| \quad \blacksquare
\end{align*}
$$

**Proof of Lem. 23.** There, the measure is $\|t, t[u_i/x_i]_{i \in \{1, \dots, n\}}\|$. Depending on the shape of $t$, we have:

- If $t$ is a sort, the substitution does not have any impact.

- If $t = x_i^{A_i}$, $\|t\| = \eta E |s_{A_i}|_S \|A_i\| x_i$, so $\|t\| \left[ \|u_i\|/x_i \right]_i = \eta E |s_{A_i}|_S \|A_i\| \|u_i\|$. By Lem. 24, $\|A_i\| \rightsquigarrow^* \|A_i\downarrow\|$ and one can conclude by Lem. 22 that $\|t\| \left[ \|u_i\|/x_i \right]_i \rightsquigarrow^* \|u_i\|$.

- If $t = y^B$ with $y \notin \{x_i\}_i$, then $\|t\| = \eta E |s_B|_S \|B\| y$, so

$$ \|t\| \left[ \|u_i\|/x_i \right]_i = \eta E |s_B|_S \|B\| \left[ \|u_i\|/x_i \right]_i y \rightsquigarrow^*_{\text{IH}} \left\| y^B [u_i/x_i]_i \right\| = \left\| t \left[ u_i/x_i \right]_i \right\|. $$

- If $t = \lambda y^B \cdot v$, then $\|t\| = \lambda(y : \mathbf{Term} |s_B|_S \|B\|) \cdot \|v\|$, so

$$ \begin{align*}
\|t\| \left[ \|u_i\|/x_i \right]_i &= \lambda(y : \mathbf{Term} |s_B|_S \|B\| \left[ \|u_i\|/x_i \right]_i) \cdot \|v\| \left[ \|u_i\|/x_i \right]_i \\
&\rightsquigarrow^*_{\text{IH}} \lambda(y : \mathbf{Term} |s_B|_S \|B\| [u_i/x_i]_i) \cdot \|v\| [u_i/x_i]_i = \|(\lambda y^B \cdot v) [u_i/x_i]_i\|
\end{align*} $$

The other cases are straightforward, just like the previous two.

**Proof of Lem. 24.** We use $\|t\|$ as the measure. If the reduction is not at the head of $t$, then the result follows by the induction hypothesis.

Otherwise, the reduction occurs at the head of the term. It can be either $\eta$ or $\beta$ reduction.

(η) Then $t = \lambda x^A \cdot (u x^A)^B$ and $u$ is either a variable, an application or a $\lambda$-abstraction. In every case $\|t\| = \lambda(x : \mathbf{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| (\|u\| (\eta E |s_A|_S \|A\| x))$.

- If $u = y^C$, then $C \downarrow = (x : A \downarrow) \to B$.

$$
\begin{align*}
\|u\| &= \eta E |s_C|_S \|C\| y \rightsquigarrow^*_{\text{IH}} \eta E |s_C|_S \|(x : A \downarrow) \to B\| y \\
&= \eta E |s_C|_S (\mathbf{prod} |s_A|_S |s_B|_S \|A \downarrow\| (\lambda(x : \mathbf{Term} |s_A|_S \|A \downarrow\|). \|B\|)) y \\
&\rightsquigarrow \eta P \quad \lambda(x : \mathbf{Term} |s_A|_S \|A \downarrow\|). \eta E |s_B|_S \|B\| (y (\eta E |s_A|_S \|A \downarrow\| x))
\end{align*}
$$

When we instantiate $\|t\|$ in this case, we get:
31:14 Encoding Agda Programs Using Rewriting

$$
\begin{align*}
\|t\| &\rightsquigarrow_{\beta} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| \\
&\quad (\eta E |s_B|_S \|B\| [\eta E |s_A|_S \|A\| \|x/x\|] (y (\eta E |s_A|_S \|A\| \|x\|))) \\
&\rightsquigarrow_{\eta I} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| (y (\eta E |s_A|_S \|A\| \|x\|)) \rightsquigarrow_{IH}^* \|u\|
\end{align*}
$$

- If $u = (v w)^{(x:A) \to B}$.

$$
\begin{align*}
\|u\| &= \eta E |C|_S \|(x : A \downarrow) \to B\| (\|v\| \|w\|) \\
&\rightsquigarrow_{\eta P} \lambda(x : \text{Term} |s_A|_S \|A \downarrow\|) \cdot \eta E |s_B|_S \|B\| (\|v\| \|w\| (\eta E |s_A|_S \|A \downarrow\| x))
\end{align*}
$$

Instantiating $\|t\|$ in this case give:

$$
\begin{align*}
\|t\| &\rightsquigarrow_{\beta} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| (\eta E |s_B|_S \|B\| [\eta E |s_A|_S \|A\| \|x/x\|]) \\
&\qquad (\|v\| \|w\| (\eta E |s_A|_S \|A\| \|x\|))
\end{align*}
$$

Since $v$ and $w$ do not contain $x$ free.

$$
\rightsquigarrow_{\eta I} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| (\|v\| \|w\| (\eta E |s_A|_S \|A\| \|x\|)) \rightsquigarrow_{IH}^* \|u\|
$$

- If $u = \lambda y^C.v$, then $C \downarrow = A \downarrow$, then $\|u\| = \lambda(y : \text{Term} |s_C|_S \|C\|). \|v\|$. Then,

$$
\begin{align*}
\|t\| &\rightsquigarrow_{\beta} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| \|v\| \left[ \frac{(\eta E |s_A|_S \|A\| \|x\|)}{y} \right] \\
&\rightsquigarrow_{\text{Lem.23}}^{*} \lambda(x : \text{Term} |s_A|_S \|A\|) \cdot \eta E |s_B|_S \|B\| \left\| v \left[ \frac{x}{y} \right] \right\| \\
(\lambda y.v) x \text{ is a subterm of } t.
\end{align*}
$$

$$
\rightsquigarrow_{\text{Lem.22}}^{*} \lambda(x : \text{Term} |s_A|_S \|A\|). \left\| v \left[ x/y \right] \right\| =_{\alpha} \|u\|
$$

(β) Then $t = ((\lambda x^A.v) w)^B$ and $u = v[w/x]$. We have :

$$
\begin{align*}
\|t\| &= \eta E |s_B|_S \|B\| ((\lambda(x : \text{Term} |s_A|_S \|A\|). \|v\|) \|w\|) \\
&\rightsquigarrow_{\beta} \eta E |s_B|_S \|B\| \|v\| \left[ \|w\|/x \right]
\end{align*}
$$

$$
\begin{align*}
& \rightsquigarrow_{\text{Lem.23}}^{*} \eta E |s_B|_S \|B\| \|v[w/x]\| \rightsquigarrow_{\text{Lem.22}}^{*} \|v[w/x]\| \\
& v \text{ and } v[w/x] \text{ are respectively subterm and reduct of } t, \text{ hence Lem. 23 applies. } \quad \blacksquare
\end{align*}
$$

From those three lemmas, one can conclude that

► **Theorem 25** (Correctness of the translation). If $\Gamma \vdash t : A$ and $t \rightsquigarrow^* u$, then $\|t\| \rightsquigarrow^* \|u\|$.

5 Implementation

AGDA [18, 17] is a dependently-typed programming languages, based on an extension of Martin-Löf type theory, Luo's Unifying Theory of dependent Types [15, Chapter 9], which features both universe polymorphism and η-conversion. DEDUKTI [10, 2] is an implementation of the λΠ-calculus modulo rewriting, which was recently enriched with conversion modulo associativity and commutativity.

Developing a prototypical translator [7] from AGDA to DEDUKTI allowed the author to give a concrete application to the ideas presented in Sections 3 and 4.

However, AGDA offers its users a logic much richer than a universe polymorphic pure type
system with η-conversion. First of all, AGDA permits to declare inductive types and then to
define functions using dependent pattern-matching on the constructors of this type. This
behaviour can easily be replicated in DEDUKTI, by declaring new symbols for inductive types,
constructors and functions and rewrite rules for each case of the dependent pattern-matching.
Just like sorts and products have an encoded and a decoded version, linked by the application
of the function Term, the type has two translation, one as code and one decoded, linked by a
rewrite rule enriching the definition of Term. Analogously, one rewrite rule is added to enrich
the definition of ηE.

► **Example 26.** The AGDA declaration of the addition of natural numbers:

```
data Nat : Set where
zero : Nat
suc : (n : Nat) → Nat
```

```
_ + _ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
```

is translated in DEDUKTI by:

```
constant TYPE Nat : TYPE.
Term _ Nat → TYPE Nat.
constant Nat zero : Term (set 0) Nat.
constant Nat suc : Term (set 0) (prod (set 0) (set 0) Nat (λ n, Nat)).
symbol {|_ + _|} : Term (set 0) (prod (set 0) (set 0) Nat (λ _0, prod (set 0) (set 0) Nat (λ _1, Nat))).
{|_ + _|} Nat zero m → m.
{|_ + _|} (Nat suc n) m → Nat suc ({|_ + _|} n m).
```

We can observe, that Nat in AGDA became TYPE\_Nat and Nat in DEDUKTI, and two rules
have been added: one to state that TYPE\_Nat is the decoding of Nat and the other to extend
the definition of ηE.

Each declaration of a new type consists in adding a new constructor to the type Univ s.
The new rules on ηE and Term are here to ensure that the pattern-matching on this type
remains exhaustive, in order to completely get rid of administrative encoding operators on
the normal forms of values.

One can note, that the enrichment of the functions Term and ηE are left to the will of
the author of the translation. This proves to be a good feature, since the η-conversion of
AGDA does not restrict to product types, but also concerns records (η-conversion of records
is also sometimes called “surjective pairing” and means that if t lives in Σ<sub>x:A</sub> B, then t
and (fst t, snd t) are convertible). This does not require to introduce a new symbol for this
enrichment of the conversion, but just to define adequate rules on ηE.

► **Example 27.** The declaration of this record:

```
record r : Set1 where
    field A : Set
```

is translated by:

```
constant TYPE r : TYPE.
Term _ r → TYPE r.
ηE _ r y → r cons (r A y) (ηE 0 (r A y) (r b y)).
constant r cons : Term (set (s 0)) (prod (set (s 0)) (set (s 0)) (code (set 0)) (λ A, prod (set 0) (set (s 0)) A (λ b, r))).
symbol r A : Term (set (s 0)) (prod (set (s 0)) (set (s 0)) r (λ r, code (set 0))).
symbol r b : Term (set (s 0)) (prod (set (s 0)) (set 0) r (λ r, r A r)).
r A (r cons A b) → A.      r b (r cons A b) → ηE 0 A b.
```
The rule to define the $\eta$-expansion of an element of $\mathbf{r}$ states that if $y$ is of type $\mathbf{r}$, then
$y \equiv \{a = y.a; b = y.b\}$.

This translator is available at https://github.com/Deducteam/Agda2Dedukti, the directory `theory/` contains the encoding presented in Sections 3 and 4. It is able to translate and type-check 162 files of AGDA's standard library [9].

# 6 Conclusion and Future Work

We presented in this article a correct encoding of universe polymorphism in $\lambda\Pi$-modulo rewriting, meaning that every term typable in the original system is translated to a typable term. We also presented a rewrite system to decide equality in the max-plus algebra, which is a common universe algebra.

Furthermore, we proposed an operator $\eta E$ to encode shallowly a type-directed rule, like $\eta$-conversion, since the translation of an application really involves the application of the translation of a term to the other one, reducing the interleaving between the computation steps coming from the original system and the steps related to the encoding.

Finally, we applied those results to the practical case of the translation of the proof system AGDA, which offers, among others, the features we targeted, allowing us to provide DEDUKTI users with more than 500 declarations of types, constructors or functions, originating from AGDA's standard library.

We proved that translation of well-typed terms remain typable in our encoding. However, it could be that our encoding is over-permissive and type-checks much more terms than the original system. Hence, one could envision a conservativity theorem, stating that if the translation of a type is inhabited, then the type is also inhabited in the original system. For implementability purposes, we have chosen an encoding with finitely many symbols. Such a theorem has only been proved [8, 1], for encodings of PTS with as many symbols as sorts, axioms and rules. Extending those theorems to our setting is a short-term goal.

Regarding the implementation, making the translator more complete is naturally an objective, however, it involves more theoretical problems, which are long run research programs. For instance, how size types or co-inductive types can be encoded in the $\lambda\Pi$-calculus modulo rewriting is not known yet.

Now that proofs have been translated to the logical framework DEDUKTI, they can be analysed, and (when it is possible) exported to other proof assistants, like what was done with proofs originating from the arithmetic library of MATITA [20].

# References

1. Ali Assaf. *A Framework for Defining Computational Higher-Order Logics*. PhD thesis, École polytechnique, France, 2015.

2. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a logical framework based on the $\lambda\pi$-calculus modulo theory, 2019. URL: http://www.lsv.fr/~dowek/Publi/expressing.pdf.

3. Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, *Handbook of Logic in Computer Science (Vol. 2)*, pages 117–309. Oxford University Press, Inc., New York, NY, USA, 1992.

4. Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. An induction principle for pure type systems. *Theoretical Computer Science*, 266(1-2):773–818, 2001.
5 Stefano Berardi. *Type Dependence and Constructive Mathematics*. Phd, Carnegie Mellon University, Dept. Comp. Sci., Pittsburgh, Pennsylvania, USA and Torino University, Dipartimento di Informatica, Torino, Italy, 1990.

6 Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The λΠ-calculus Modulo as a Universal Proof Language. *PxTP*, page 16, 2012.

7 Jesper Cockx and Guillaume Genestier. Agda2dedukti. https://github.com/Deducteam/Agda2Dedukti, 2019.

8 Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In *Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications*, Lecture Notes in Computer Science 4583, 2007.

9 Nils Anders Danielsson, Matthew Daggitt, and Guillaume Allais. Agda standard library. https://github.com/agda/agda-stdlib, 2010.

10 Deducteam. Dedukti. https://deducteam.github.io/, 2011.

11 Gilles Dowek, Gérard Huet, and Benjamin Werner. On the Definition of the Eta-long Normal Form in Type Systems of the Cube. In *Informal Proceedings of the Workshop on Types for Proofs and Programs*, pages 115–130, 1993.

12 Herman Geuvers and Mark-Jan Nederhof. Modular proof of strong normalization for the calculus of constructions. *Journal of Functional Programming*, 1(2):155–189, 1991.

13 Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. *Journal of the ACM*, 40(1):143–184, January 1993.

14 Robert Harper and Randy Pollack. Type Checking with Universes. *Theoretical Computer Science*, 89:107–136, 1991.

15 Zhaohui Luo. *Computation and reasoning - a type theory for computer science*, volume 11 of *International series of monographs on computer science*. Oxford University Press, 1994.

16 Dale Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. *J. Log. Comput.*, 1(4):497–536, 1991.

17 Ulf Norell. *Towards a practical programming language based on dependent type theory*. Phd, Chalmers University of Technology, Gothenburg, Sweden, 2007.

18 Ulf Norell, Andreas Abel, Niels Anders Danielsson, Makoto Takeyama, and Catarina Coquand. Agda. https://github.com/agda/agda, v1.0 : 1999.

19 Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Gerwin Klein and Ruben Gamboa, editors, *Interactive Theorem Proving*, pages 499–514. Springer, 2014.

20 François Thiré. Sharing a Library between Proof Assistants: Reaching out to the HOL Family. In *Logical Frameworks and Meta-Languages: Theory and Practice*, LFMTP, pages 57–71, 2018.