Guillaume Genestier

Encoding Agda Programs Using Rewriting

Keywords: 2012 ACM Subject Classification Theory of computation → Equational logic and rewriting; Theory of computation → Type theory Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion Digital Object Identifier 10.4230/LIPIcs.FSCD.2020.31

 of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.

Introduction

With the multiplication of proof assistants, interoperability has became 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 developped 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 [START_REF] Harper | Type Checking with Universes[END_REF], 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 η. 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. η-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. Definition 1 (Syntax and typing of PTS). Let X be an infinite set of variables and S be the set of sorts.

t, u

::= s | x | (x : t) → u | λx t .u | t u
with s ∈ S and x ∈ X

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

(var) Definition 3 (Full Pure Type System). A PTS is called full if axioms and rules are total functions, respectively from S and S × S to S.

Γ A : s Γ, x : A x : A x / ∈ dom(Γ) (ax) s1 : s2 (s1, s2) ∈ A (prod) Γ A : s1 Γ, x : A B : s2 Γ (x : A) → B : s3 (s1, s2, s3) ∈ R (app) Γ t : (x : A) → B Γ u : A Γ t u : B [ u / x ] (
Example 4 (P ∞ and C ∞ ). The predicative and impredicative infinite hierarchies, are two full PTS:

P ∞ is S = { * i | i ∈ N} ; A = {( * i , * i+1 )} ; R = { ( * i , * j , * k )| k = max(i, j)} whereas C ∞ is S = { * i | i ∈ N} ; A = {( * i , * i+1 )} ; R = { ( * i , * j , * k )| j 1 and k = max(i, j)} ∪ {( * i , * 0 , * 0 )}.
Definition 5 (Embedding of PTS). Given P 1 = (S 1 ; A 1 ; R 1 ) and P 2 = (S 2 ; A 2 ; R 2 ) two PTS, f : S 1 → S 2 is an embedding of P 1 in P 2 if for all (s, s ) ∈ A 1 , we have (f (s), f (s )) ∈ A 2 and for all (s, s , s

) ∈ R 1 , we have (f (s), f (s ), f (s )) ∈ R 2 .
f is extended to terms of P 1 , by:

f (x) = x, if x ∈ X ; f (λx A .t) = λx f (A) .f (t); f (t u) = f (t) f (u); f ((x : A) → B) = (x : f (A)) → f (B).
Proposition 6 (Soundness of the Embedding). If f is an embedding from a PTS P

1 to P 2 , if Γ P1 t : A, then f (Γ) P2 f (t) : f (A).
Proof. By induction on the proof tree. Since f preserves A and 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 Edimburgh Logical Framework [START_REF] Harper | A Framework for Defining Logics[END_REF] (LF), denoted λP in Barendregt's λ-cube is the minimal PTS including dependent types. It has two sorts S = { , }, with the axioms A = {( , )} and the rules R = {( , , ), ( , , )}. 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 is the left-hand side of no axioms.

The logic behind the Logical Framework Dedukti is the λΠ-calculus modulo rewriting [START_REF] Assaf | Dedukti: a logical framework based on the λπ-calculus modulo theory[END_REF][START_REF] Boespflug | The λΠ-calculus Modulo as a Universal Proof Language[END_REF], an extension of the Edimburg 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, λ-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 λΠ-modulo rewriting). A signature in λΠ-modulo rewriting is (Σ, Θ, R) where Σ is a set of symbols, disjoint of X , Θ is a function from Σ to terms and R is a set of rewriting rules, i.e. a set of pair of terms of the form f l → r, with f ∈ Σ and all l i 's are Miller's pattern [START_REF] Miller | A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification[END_REF].

We say that t rewrites to u, denoted t u if there is a rule f l → r, a substitution σ and a "term with a hole"

C[], such that t = C[(f l)σ] and u = C[rσ].
is the smallest relation containing → and stable by substitution and context. We denote by * the reflexive transitive closure of and by * the convertibility relation, which is the reflexive symmetric and transitive closure of . Definition 8 (Typing rules of λΠ-modulo rewriting). They are the one of LF (those of Def. 1, instantiated with S = { , }, A = {( , )} and R = {( , , ), ( , , )}.), but with a rule to introduce symbols of Σ and enrichment of the conversion, to include both β-reduction and the user-defined rewriting rules.

(sig) Γ Θ(f ) : s f ∈ Σ Γ f : Θ(f ) (conv) Γ t : A Γ B : s Γ t : B A * β∪R B
F S C D 2 0 2 0 31:4

Encoding Agda Programs Using Rewriting

In 2007, Cousineau and Dowek [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF] 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 [START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF]. For full Pure Type Systems, this extension is quite straightforward. The general encoding of full PTS is:

First the PTS specificification: a type of sorts and two functions for A and 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 λΠ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 λΠ-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). 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 A and R respectively.

Universe Polymorphism and its Encoding

It is quite common to enrich PTS with Universe Polymorphism [START_REF] Harper | Type Checking with Universes[END_REF], 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 i | i ∈ 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 [START_REF] Sozeau | Universe Polymorphism in Coq[END_REF] for the proof assistant Coq. In this setting, the context contains three lists: a list Σ called signature, a list Θ of level variables, and a list Γ called local context. Both Σ and Γ contain pairs of a variable name and a type, but the variables in Γ can contain free level variables (those occuring in Θ), whereas all the level variables are bound by a prenex quantifier ∀ in the signature Σ. Unlike [START_REF] Sozeau | Universe Polymorphism in Coq[END_REF], 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 L of levels and a finite set H of sort constructors. Then the sorts are {s } s∈H, ∈L .

In addition to functionality and totality of A and R, we assume a uniformity in the hierarchy. Meaning that for all s ∈ H, there is a s ∈ H, such that for all ∈ L, there is a ∈ L, such that (s , s ) ∈ A and for all s (1) , s (2) ∈ H, there is a s (3) ∈ H, such that for all

1 , 2 , ∈ L, there is 3 ∈ L such that (s (1)
1 , s

(2)

2 , s (3)
3 ) ∈ R. We denote by Ā the function (s, s ) ∈ H 2 ∃ , , (s , s ) ∈ A and for all s by A s the function ( , ) ∈ L 2 ∃s , (s , s ) ∈ A .

Analogously R is the function (s (1) , s (2) , s

) ∈ H 3 ∃ 1 , 2 , , (s (1) 1 , s (2)
2 , s ) ∈ R and for all (s (1) , s (2)

), R s (1) ,s (2) is the function ( 1 , 2 , ) ∈ L 3 ∃s , (s (1) 1 , s (2) 2 , s ) ∈ R .
The typing rules are: In all those typing rules, s, s ∈ H and i, x ∈ X . Furthermore, we allowed ourselves to simply write x / ∈ Σ, Γ, rather than "for all A, x : A is not in Σ, Γ".

(lvl) Θ isLvl ∈ L (ax) Θ γ isLvl []; Θ; [] sγ : s As(γ) (s, s ) ∈ Ā (Lvar) Θ i isLvl i ∈ Θ (abs) Σ; Θ, Γ (x : A) → B : sγ Σ; Θ; Γ, x : A t : B Σ; Θ; Γ λ(x : A).t : (x : A) → B (LA) Θ isLvl Θ As( ) isLvl (app) Σ; Θ; Γ t : (x : A) → B Σ; Θ; Γ u : A Θ; Γ t u : B [ u / x ] (LR) Θ 1 isLvl Θ 2 isLvl Θ R ss ( 1, 2) isLvl (conv) Σ; Θ; Γ t : A Σ; Θ; Γ B : sγ Σ; Θ; Γ t : B A * β B (var) Σ; Θ; Γ A : sγ Σ; Θ; Γ, x : A x : A x / ∈ Σ, Γ (sig) Σ; Θ; [] A : sγ Σ, x : ∀Θ.A; Θ ; [] x : ∀Θ.A x / ∈ Σ, Γ (
One typical case of use, is to have only one hierarchy: H = {Set} and to use natural numbers for levels: L = 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 Σ, allows to completely change the set Θ of names of local variables. Changing this set during the proof is not necessary, however, without this renewal of Θ, all the symbols in the signature would have been quantified over the same set Θ, 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.

Encoding Agda Programs Using Rewriting

To prove this, one can construct a new PTS (S Θ , A Θ , R Θ ) simply by adding a brand new sort for every expression containing a level variable (such expressions are in L + Θ ). 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 = (L, H, A, R) be a uniform universe polymorphic full PTS and Θ be a subset of X .

Let L + Θ be the smallest subset such that:

L + Θ = Θ ∪ A s (l) s ∈ H, l ∈ L + Θ ∪ R ss (l 1 , l 2 ) s, s ∈ H, (l 1 , l 2 ) ∈ (L ∪ L + ) 2 \ L 2 . Let X + = X ∪ y[l 1 , . . . , l n ] y ∈ X , n ∈ N, (l 1 , . . . , l n ) ∈ (L ∪ L + X )
n and P Θ be the PTS:

S Θ = s l s ∈ H, l ∈ L ∪ L + Θ ; A Θ = A ∪ s l , s As(l)) (s, s ) ∈ Ā, l ∈ L + Θ R Θ = R ∪ s l1 , s l2 , s R ss (l1,l2)) (s, s , s ) ∈ R, (l 1 , l 2 ) ∈ (L ∪ L + ) 2 \ L 2
a. There is an embedding from P Θ to the underlying PTS of P . b. If Σ; Θ; Γ t : A in P and A is not a universal quantification, then there is a

Σ ⊂ x[l 1 , . . . , l n ] : A x : ∀[y 1 , . . . , y n ].A ∈ Σ, A = A l i/ y i i=1...n and all l i ∈ L ∪ L + Θ such that Σ, Γ P Θ t : A using the enriched set of variables X + .
Proof sketch. a. The embedding consists in just chosing a level for each variable in Θ. b. Since A is not a universal quantification, in the proof of Σ; Θ; Γ 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 Θ , the (sig) and (inst) are compressed in a single introduction of a variable of Σ.

In a PTS, if Γ t : A, then there is a sort s such that A = s or Γ 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 Sort ω , 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 H and ω is not a level.

To encode Universe Polymorphic Full PTS, one introduce a symbol sortOmega and a quantification symbol ∀ 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 ∀ L .

Definition 11 (Encoding).

constant sortOmega : Sort . constant

∀ L : ( f: (L⇒Sort )) ⇒ (( l:L) ⇒ Univ ( f l )) ⇒ Univ sortOmega . Term _ (∀ L f t ) -→ ( l : L) ⇒ Term ( f l ) ( t l ).
For instance, the encoding of ∀ , Set is ∀ L (λ l, axiom (set l)) (λ l, code (set l)), if set is a sort constructor in the encoding. And its decoding (when applying Term sortOmega) is, as expected, (l:L) ⇒ Univ (set l).

Example 12. Consider the system H = {s, σ}, A = (A i , s ax A (i) ) A ∈ H and R = (A i , B j , B ru(i,j) ) A, B ∈ H , with ax s , ax σ and ru three functions remaining abstract here. ru could be indexed by two sorts, for ease of readibility, 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 = code |s | S ; t u = t u ; λx A .t = λ(x : Term |sA| S A ). t ; (x : A) → B = prod |sA| S |sB| S A (λx : Term |s1| S A . B ); ∀[ 1, . . . , n], A = ∀ L (λ 1 : L. sortOmega) (λ 1 . . . ∀ L (λ n : L.|sA| S ) (λ n : L. A ). . . ); A[γ 1 , . . . , γ n ] = A |γ 1 | L . . . |γ n | L . The translation of sorts is |Sort ω | S = sortOmega, |s γ | S = s |γ| L .

And the translation of levels is |i|

L = i if i ∈ X ; |A s ( )| L = ax_s | | L and |R ss ( 1 , 2 )| L = ru_ss' | 1 | L | 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 | | L for ∈ 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: Proof. a and b are proved by induction on the the term t. c is because a β-redex is translated as a β-redex.

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

Lemma 15 (Shape-preservation of type

). a. If s is a sort, Term |A(s)| S s * Univ |s| S , b. If (x : A) → B is of sort s, Term |s| S (x : A) → B * (x :Term |s A | S A )⇒Term |s B | S B ; c. If 1 < • • • < n , Term sortOmega ∀ { i } i , A * ( 1 : L)⇒ . . . ⇒( n : L)⇒ A .
Proof. The three rules on Term are crafted to ensure those properties. By Lem. 15, the product obtained is convertible with ∀Θ.A , hence one can introduce a variable of this type. One must then use the weakening, to Re-invent the variables of type L corresponding to the Θ . (inst) Lem. 15 tells us that, after conversion, the induction hypothesis is Σ; Θ; Γ A :

( 1 : L) → • • • → ( n : L) → X ,
hence, we can apply the γ i 's without type issues. (prod) By induction hypothesis, we have Σ; Θ; Γ λΠ/P A : Univ s γ and also Σ; Θ; Γ, x : A λΠ/P B : Univ s γ , so Σ; Θ; Γ , x : Term |s γ | S A λΠ/P B : Univ s γ and we can conclude by introducing the lambda and applying prod. (ctx-weak) As before, we have Σ; Θ; Γ λΠ/P A : Univ s γ , so Σ; Θ; Γ λΠ/P Term |s γ | S A : TYPE, so one can weaken with a variable of this type. (∀weak) Like for the (sig) rule, one can empty the context of the variables of type L by applying the rule (prod) of λΠ-modulo rewriting. Then, one can weaken with a variable of this type and variables of type L to translate the Θ . Now, we will more specifically focus on a specific hierarchy of levels, where L = N and all the A s are the successor function and all R ss are the maximum function. This is the predicative hierarchy of P ∞ (Expl. 4), used in Agda for instance.

The grammar of universe level we are interested in is:

t, u ∈ L ::= x ∈ X | 0 | s t | max t u: constant L : TYPE . symbol 0 : L. symbol s : L ⇒ L. symbol max : L ⇒ L ⇒ L.
The question which arises in the translation is to have a convergent rewrite system such that for all t and u in L:

t ↓ = u ↓ if and only if ∀σ : X → N, t σ = u σ
where _ _ : L → (X → N) → N is the obvious interpretation in N:

0 σ = 0 N x σ = σ(x), if x ∈ X s t σ = t σ + N 1 N max t u σ = max N ( t σ , u σ )
Since max is associative and commutative (AC), we will propose an encoding having a weak version of this property:

t ↓ ≡ AC u ↓ if and only if ∀σ : X → N, t σ = u σ .
Since s (max t u = max (s t) (s u) , one can consider having a Max acting on a set of terms, which do not contain max.

Furthermore, we have for all n the equality max (s n x) x = s n x . To avoid declaring this rule infinitely often (once for every n), we add addition to our encoding. However, since this addition encodes iteration of the application of s, it is not an addition between two levels, but one between a ground natural number and a level. Furthermore, max (s n x) (s m 0) = s n x , if m < n. Hence, the symbol Max will also collect the value of the smallest possible ground natural that the result can be.

Hence, in our encoding, the normal forms are the Max i {j k + x k } k where:

(1) i, j 1 , . . . are ground naturals, (2) x 1 , . . . are distinct variables, (3) for all k, i j k . A separate type N, containing only ground natural numbers, is declared, to avoid confusion with levels.

Sets can be empty or singleton or union of sets. This union operator is an associative and commutative symbol. Furthermore, since singletons are of the form {i + x}, the constructor of singletons is denoted ⊕. Since constraint (1) is guaranteed by typing, we still have to implement the two constraints (2) and (3) presented in the description of the normal form:

The only non-left-linear rule of the encoding eliminates redundancies, ensuring that all variables in the normal forms are distinct, in order to satisfy the invariant [START_REF] Assaf | Dedukti: a logical framework based on the λπ-calculus modulo theory[END_REF].

( i ⊕ l ) ∪ ( j ⊕ l ) -→ (max N i j ) ⊕ l .
Intuitively, to flatten the entanglement of max and plus, we would like to have a rule stating that a + max(b, c) = max(a + b, a + c). However, to fulfill constraint (3), we added the invariant that the first argument of Max is larger than all the first arguments of the ⊕ occuring directly under it. Hence, we do not declare the expected computation rule of ⊕, but enforce this computation to be performed under a Max. Furthermore, for typing distinction between L and LSet, we introduce an auxiliary function mapping (i ⊕ _) to all the elements of a set. mapPlus i ( j ⊕ l ) -→ ( i + N j ) ⊕ l . mapPlus i ( l1 ∪ l2 ) -→ ( mapPlus i l1 ) ∪ ( mapPlus i l2 ). symbol Max :

N ⇒ LSet ⇒ L Max 0 N (0 N ⊕ x ) -→ x . Max i ( j ⊕ Max k l ) -→ Max (max N i ( j + N k )) ( mapPlus j l ). Max i (( j ⊕ Max k l ) ∪ tl ) -→ Max (max N i ( j + N k )) (( mapPlus j l ) ∪ tl ).
And finally we give rewrite rules for the symbols of the syntax:

0 -→ Max 0 N ∅. s x -→ Max 1 N (1 N ⊕ x ). max x y -→ Max 0 N ((0 N ⊕ x ) ∪ (0 N ⊕ y )).
This encoding is not confluent, as the following example illustrates:

Max i ( j ⊕ ( Max k ( j2 ⊕ ( Max k2 l )))) o Max (max N i ( j + N k )) ( mapPlus j ( j2 ⊕ ( Max k2 l ))) Max (max N i ( j + N k )) (( j + N j2 ) ⊕ ( Max k2 l )) Max (max N (max N i ( j + N k )) ( j + N j2 + N k2 )) ( mapPlus ( j + N j2 ) l ) i Max i ( j ⊕ ( Max (max N k ( j2 + N k2 )) ( mapPlus j2 l ))) Max (max N i ( j + N (max N k ( j2 + N k2 )))) ( mapPlus j ( mapPlus j2 l ))
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 L.

Proposition 18. The absence of variable of type N or LvlSet ensures the uniqueness of normal form (modulo AC) property.

Proof. Since there are no variables of type N and LSet, the function max N , + N and mapPlus are fully defined and cannot occur in the normal forms.

Hence, normal forms contain only 0 N , s N , Max, ∅, ⊕ and ∪. Among it, the only constructor of a L is Max, hence every level is either a variable or headed by Max.

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

Hence all normal forms are either a variable or of the form Max n s, with n closed natural and s a 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 ⊕ is smaller or equal to the first argument of the Max directly above the ⊕ 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 decribed have a different interpretation.

Eta-conversion

Many proof assistants implement, among other conversion rules, the η rule, which state that if f is a function, f ≡ η λ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 λ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 λΠ-modulo rewriting. Furthermore, we could replace it by λ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 λΠ-modulo rewriting as a logical framework with η hard-coded in the conversion (just like β is). But this is a path logical frameworks want to avoid. Indeed, if η is hard-coded, it is impossible to have a shallow encoding of the λ-calculus without η-conversion.

One could expect that η-expanding every term during the translation phase, could allow us to completely ignore η-conversion in the λΠ-calculus modulo rewriting. Indeed, with dependent types it might happen than an η-long term has a non-η-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. We then define a new type depending on the first one and its constructor. Now, the term e 1 is η-long and has type E 1 (d 1), but not E 1 (λ x, d 1 x) which is the η-long form of the type.

To overcome this issue, we propose to postpone η-expansion, until the type is fully instantiated. For this, we introduce in the translation a symbol ηE, which purpose is to tag with their types the subterms which may become η-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). η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 η-expansion is the identity for inhabitant of sorts (ηS), and genesrates λ's for inhabitants of products (ηP ). Furthermore, a rule state that η-expansion is an idempotent operation (ηI). To prove that adding those annotations in the encoding enriches enough the conversion to simulate η-equality, we will also add those annotations in the system we are translating, just like what is done in [START_REF] Geuvers | Modular proof of strong normalization for the calculus of constructions[END_REF][START_REF] Dowek | On the Definition of the Eta-long Normal Form in Type Systems of the Cube[END_REF].

For sake of readibility, we will study in this section, terms typed in a full PTS embeddable in C ∞ , like P ∞ and C ∞ defined in Expl. 4, in order to directly reuse the induction principle defined in [START_REF] Barthe | An induction principle for pure type systems[END_REF].

  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 ).

F

FDefinition 16 (

 16 To state properly the Correctness Theorem, one first has to define the translation of contexts: Context Translation). If Σ = x 1 : T 1 , . . . , x l : T l , Θ = i 1 , . . . , i m and Γ = y 1 : A 1 , . . . , y n : A n , then the translation is Σ; Θ; Γ = x 1 : Term sortOmega T 1 , . . . , x l : Term sortOmega T l , i 1 : L, . . . , i m : L, y 1 : Term |s A1 | S A 1 , . . . , y n : Term |s An | S A n . Theorem 17 (Correctness). Given a correct criterion for equality of levels (i.e. if two levels 1 and 2 are equals, their translations | i | L are convertible), for a Universe Polymorphic Full Pure Type System P , if Σ; Θ; Γ t : A, then Σ; Θ; Γ λΠ/P t : Term |s| S A , where s is the sort of A. Proof. By induction on the derivation. We assume that if Θ γ isLvl, then []; Θ; [] λΠ/P |γ| L : L, a property which can be proved by induction on the derivation, with the assumption that for all ∈ L, λΠ/P | | L : L. We then consider the 10 remaining cases: (var) By induction hypothesis, Σ; Θ; Γ λΠ/P A :Univ |s γ | S Hence Σ; Θ; Γ λΠ/P Term |s γ | S A : TYPE, so one can introduce a variable of this type. (ax) The translation of s γ is code (s |γ| L ) which lives in Univ (s' (ax_s |γ| L )), which is the reduct of the translation as type of s As(γ) . (abs) By induction hypothesis, Σ; Θ; Γ ,x : Term |s| S A λΠ/P t : Term |s | S B , hence, one has that λ(x : Term|s| S A ).t inhabits (x : Term |s| S A ) →Term |s | S B , which is the reduct of the translation as type of (x : A) → B. The other induction hypothesis Σ; Θ; Γ λΠ/P (x : A) → B : Univ |s γ | S ensures us that 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, Σ; Θ; [] λΠ/P A : Univ |s γ | S . Hence, one can use the (prod) rule of λΠ-modulo rewriting to move all the i : L from the context to the term.

  symbol ∅: LSet . infix ⊕: N⇒L⇒LSet . infix ac ∪: LSet⇒LSet⇒LSet . x ∪ ∅ -→ x .

F S C D 2 0 2 0 31: 10

 010 Encoding Agda Programs Using Rewriting symbol mapPlus : N ⇒ LSet ⇒ LSet . mapPlus i ∅ -→ ∅.

  symbol D : ( x : N) ⇒ TYPE . constant d : ( x : N) ⇒ D x . D 0 -→ N. D ( s x ) -→ N ⇒ D x .

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

  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 .

F

constant N : TYPE . constant 0 N : N. constant s N : N ⇒ N. definition 1 N := s N 0 N . symbol max N : N ⇒ N ⇒ N. max N 0 N y -→ y . max N x 0 N -→ x . max N (s N x ) (s N y ) -→ s N (max N x y ). infix + N : N ⇒ N ⇒ N. 0 N + N y -→ y .(s N x ) y -→ s N ( x + N y ).

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

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

Performing η-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:

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 [START_REF] Barthe | An induction principle for pure type systems[END_REF] ensures us that, if we annotate the applications with normal form, this property is verified, leading to:

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 , . . . , 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 η, we translate t by: The correctness of our translation relies on the preservation of conversion. This result comes from the three following lemmas: 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 ηS. We proceed by case on t for the remaining cases:

Proof of Lem. 23.

There, the measure is ⦃t, t u i/ x i i∈{1,...,n} ⦄. Depending on the shape of t, we have:

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

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 η or β reduction. (η) Then t = λx A .(u x A ) B and u is either a variable, an application or a λ-abstraction. In every case t = λ(x :

When we instantiate t in this case, we get: F S C D 2 0 2 0 31:14 Encoding Agda Programs Using Rewriting

Instantiating t in this case give:

Since v and w do not contain x free.

We have :

v and v [ w / x ] are respectively subterm and reduct of t, hence Lem. 23 applies.

From those three lemmas, one can conclude that

Theorem 25 (Correctness of the translation). If Γ t : A and t * u, then t * u .

Implementation

Agda [START_REF] Norell | Agda[END_REF][START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] 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 [START_REF] Deducteam | [END_REF][START_REF] Assaf | Dedukti: a logical framework based on the λπ-calculus modulo theory[END_REF] is an implementation of the λΠ-calculus modulo rewriting, which was recently enriched with conversion modulo associativity and commutativity. Developping a prototypical translator [START_REF] Cockx | Agda2dedukti[END_REF] 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 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 x:A 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:

31:16 Encoding Agda Programs Using Rewriting

The rule to define the η-expansion of an element of r states that if y is of type r, then y ≡ {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 [START_REF] Anders Danielsson | Agda standard library[END_REF].

Conclusion and Future Work

We presented in this article a correct encoding of universe polymorphism in λΠ-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 comon universe algebra. Furthermore, we proposed an operator ηE to encode shallowly a type-directed rule, like η-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 [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF][START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF], 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 λΠ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 [START_REF] Thiré | Sharing a Library between Proof Assistants: Reaching out to the HOL Family[END_REF].