Christophe Calvès
email: christophe.calves@gmail.com

Unifying Nominal Unification *

Keywords: Unifying Nominal Unification 1998 ACM Subject Classification F.4.2 Grammars and Other Rewriting Systems Keywords and phrases Unification, Nominal, α-equivalence, Term-graph rewriting Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

come   L'archive ouverte pluridisciplinaire

Introduction

Operators with binding are ubiquitous in computer science. Programs, logic formulas, types and proofs are some examples of systems that involve binding. Program transformations, optimisations and compilation, for instance, are defined as operations on programs and should work uniformly on α-equivalence classes. Manipulating terms up to α-equivalence is not easy [START_REF] Simon | The Implementation of Functional Programming Languages[END_REF]. Gabbay and Pitts introduced nominal syntax [START_REF] Gabbay | A new approach to abstract syntax with variable binding[END_REF][START_REF] Pitts | Nominal logic, a first order theory of names and binding[END_REF] to represent, in a simple and natural way, systems that include binders by extending first-order syntax to provide support for binding operators.

The nominal approach to the representation of systems with binders is characterised by the distinction, at the syntactical level, between atoms (or object-level variables), which can be abstracted (we use the notation a.t, where a is an atom and t is a term), and meta-variables (or just variables), which behave like first-order variables but may be decorated with atom permutations. Permutations are generated using swappings (e.g., (a b)•t means swap a and b everywhere in t). For instance, (a b)•λa.a = λb.b, and (a b)•λa.X = λb.(a b)•X where λ is here a function symbol (we will introduce the notation formally in the next section). As shown in this example, permutations suspend on variables. The idea is that when a substitution is applied to X in (a b)•X, the permutation will be applied to the term that instantiates X. Permutations of atoms are one of the main ingredients in the definition of α-equivalence for nominal terms.

Urban, Pitts and Gabbay [START_REF] Urban | Nominal unification[END_REF] showed that nominal unification, i.e. unification up to α-equivalence, is decidable. They gave an algorithm to find the most general solution to a nominal unification problem, if one exists. A naive implementation, representing terms as trees, is exponential. Cheney proved that a more general form, called equivariant unification, is NP-complete [START_REF] Cheney | Equivariant unification[END_REF]. Fortunately nominal unification was proven to be polynomial [START_REF] Cheney | Equivariant unification[END_REF] and even quadratic [START_REF] Levy | Nominal unification from a higher-order perspective[END_REF] using reduction to higher-order patterns [START_REF] Qian | Linear unification of higher-order patterns[END_REF].

Levy and Villaret [START_REF] Levy | An efficient nominal unification algorithm[END_REF], and Calvès and Fernández [START_REF] Calvès | Complexity and Implementation of Nominal Algorithms[END_REF][START_REF] Calvès | The first-order nominal link[END_REF] presented, independently, two very different algorithms to solve nominal unification in quadratic time and space. Both were inspired by the Paterson-Wegman first-order unification algorithm. But they dramatically differ in the way nominal constraints and equations are dealt with: Levy and Villaret use replacings (i.e. sequences of abstractions) and multi-equations rewriting system while Calvès and Fernández use environments (i.e. permutations and sets of atoms). While being two very different structures, environments and replacings share the same goal: representing constraints generated by abstractions. The actual complexity of nominal unification is still unknown. Could another representation for nominal or first-order constraints lead to a more efficient algorithm? To answer this question we need to abstract over technical details such as representation of these constraints.

Our constributions are:

We show that the algorithms in [START_REF] Levy | An efficient nominal unification algorithm[END_REF] and [START_REF] Calvès | Complexity and Implementation of Nominal Algorithms[END_REF][START_REF] Calvès | The first-order nominal link[END_REF] can be unified. The result is a general abstract nominal-unification algorithm that unifies any algorithm based on Paterson-Wegman first-order linear unification and nominal constraints. We develop a general notion of nominal modality to enable reasoning about any data structure representing nominal constraints. We showed that the unification algorithm actually relies on four modality operations, so does its complexity. We prove that these strutures are isomorphic. So in particular, environments and replacings are. This also means that any representation can be used to establish properties on any modality. We used this to exchange properties between replacings and environments.

The paper is structured as follows. Section 2 presents nominal terms. Section 3 introduces the notion of nominal modality as an abstraction of any data structure used to represent nominal constraints. Section 4 defines operations on modalities. Section 5 establishes properties on any modality. Then section 7 presents the unification algorithm on any modality. Section 8 is about the complexity of modalities' operations. Section 9 discusses related and future work. Finally section 10 concludes.

Background

Let Σ be a denumerable set of function symbols f , g, . . . ; X a denumerable set of variables X, Y, . . .; and A a denumerable set of atoms a, b, c, d . . . We assume that these sets are pairwise disjoint. In the intended applications, variables will be used to denote metalevel variables (unknowns), and atoms will be used to represent object-level variables, which can be bound (for instance, atoms may be used to represent the variables of a programming language on which we want to reason). Let Π denote the set of finite permutations over A. Its elements are written π,π i ,π ′ ,. . . In this paper, we represent permutations by lists of swappings ((a 1 b 1 ) . . . (a n b n )). The empty list is written id, inversion and composition are written respectively π -1 and π ◮ Definition 1. The set of nominal terms, denoted N , is generated by the grammar

• π ′ . The support is supp(π) = {a ∈ A | π(a) = a}. (# ab ) γ ⊢ a#b a # X ∈ γ (# X ) γ ⊢ a#X (# absa ) γ ⊢ a#a.s γ ⊢ a#s a = b (# absb ) γ ⊢ a#b.s γ ⊢ a#s 1 . . . γ ⊢ a#s n (# f ) γ ⊢ a#f (s 1 , . . . , s n ) γ ⊢ π -1 •a#s (# s ) γ ⊢ a#π•s (≈ a ) γ ⊢ a ≈ a (≈ X ) γ ⊢ X ≈ X γ ⊢ s 1 ≈ t 1 . . . γ ⊢ s n ≈ t n (≈ f ) γ ⊢ f (s 1 , . . . , s n ) ≈ f (t 1 , . . . , t n ) γ ⊢ ds(π, π ′ )#X (≈ π ) γ ⊢ π•X ≈ π ′ •X γ ⊢ s ≈ t (≈ absa ) γ ⊢ a.s ≈ a.t γ ⊢ s ≈ (a b)•t a#t a = b (≈ absb ) γ ⊢ a.s ≈ b.t
s, t, u, v, • • • ::= a | π•X | f (s 1 , . . . , s n ) | a.s
where a.s is an abstraction and π•X a suspension.

For example, a.a, a.f (b, g(a)) and a.(X, Y ) are nominal terms.

The action of a permutation π on a term s, written π•s, is defined by

π•a = π(a), π•(π ′ •X) = (π • π ′ ), π•a.s = π(a).π•s and π•f (s 1 , . . . , s n ) = f (π•s 1 , . . . , π•s n ).
◮ Definition 2 (Subterms). Let s and t be two nominal terms. s N t means that s is a subterm of t (possibly t itself). s ≺ N t means that s is a strict subterm of t.

Nominal constraints have the form a#t and s ≈ t (read "a fresh for t" and "s α-equivalent to t", respectively). A freshness context γ is a set of freshness constraints of the form a#X. We define the validity of constraints under a freshness context γ inductively, by a system of axioms and rules, using # in the definition of ≈ (see figure 1). In this figure, we write ds(π, π ′ )#X as an abbreviation for {a#X | a ∈ ds(π, π ′ )}, where ds(π, π ′ ) = {a | π•a = π ′ •a} is the set of atoms where π and π ′ differ (i.e., their difference set). a, b are any pair of distinct atoms. The relation ≈ is indeed an equivalence relation (see [START_REF] Urban | Nominal unification[END_REF] for more details).

Let R = P(N 2 ) be the set of binary relations on N and R α ∈ R be the α-equivalence relation on N . Let ∆ be the set of finite sets of atoms. Let δ,δ i ,δ ′ ,. . . denote elements of ∆.

Substitutions are mappings from variables X to nominal terms, written σ,σ ′ ,. . . . Composition of substitutions is written σ • σ ′ . tσ represent the term where every variable X in t has been replaced by σ(X).

Nominal Modality

We can express the relation f (s This section aims to express any α-equivalence between two nominal terms in terms of (modal) relations between their subterms. The unification algorithm relies on the ability to compute (efficiently) such relations. More precisely, these relations form a family and can be indexed. This section studies those indexes.

Nominal Pre-Modality

◮ Definition 3. Let R be in R and a, b be two atoms. Let (a ← b)•R ∈ R be the relation defined by:

(a ← b)•R = {(s, t) ∈ N 2 | (a.s, b.t) ∈ R} ◮ Proposition 1.
Let R be in R and let (a i , b i ) i∈{1...n} be a finite sequence of pair of atoms :

(a n ← b n )• . . . (a 1 ← b 1 )•R = {(s, t) ∈ N 2 | (a 1 . . . . a n .s, b 1 . . . . b n .t) ∈ R} ◮ Definition 4.
A nominal pre-modality, or pre-modality for short, is a set M provided with a function Φ M : M → R such that:

∃e ∈ M, Φ M (e) = R α (e) ∀m ∈ M ∀a, b ∈ A, ∃m ′ ∈ M, Φ M (m ′ ) = (a ← b)•Φ M (m) (.)
For example, R provided with Φ R = id is a pre-modality.

◮ Remark. In the rest of this paper Φ M (m) will be written R m . Furthermore, for any nominal terms s and t, (s, t) ∈ R m will be written s ≈ m t.

◮ Definition 5. Let M be a pre-modality. Let ∼ be the kernel pair of Φ M , i.e. the equivalence relation on M defined by: ∀m,

m ′ ∈ M, m ∼ m ′ ⇔ R m = R m ′ .
The equivalence class of m ∈ M is written m.

By abuse of notation, for any pre-modalities M and M ′ , we say that (m

∈ M ) ∼ (m ′ ∈ M ′ ) if R m = R m ′ .
◮ Proposition 2. Let M be a pre-modality, then so is M /∼ with Φ (M /∼ ) = (Φ M ) /∼ . Furthermore, Φ (M /∼ ) is an injection. ◮ Corollary 6. There is a unique e ∈ M /∼ such that R e = R α . e is called the neutral element of M /∼ .

In the rest of the paper, when it is not ambiguous, e will denote the neutral element of the considered pre-modality.

◮ Corollary 7. Let m ∈ M /∼ and a, b ∈ A. There is a unique m ′ ∈ M /∼ such that R m ′ = (a ← b)•R m . m ′ is written (a ← b)•m. ◮ Definition 8. Let M be a pre-modality. [M ] is defined as the least subset of M /∼ such that: e ∈ [M ] ∀a, b ∈ A, m ∈ [M ] ⇒ (a ← b)•m ∈ [M ] ◮ Corollary 9.
Let M be a pre-modality. For any m ∈ [M ] there exists a finite sequence of pair of atoms

(a i , b i ) i∈{1...n} such that m = (a 1 ← b 1 )• . . . (a n ← b n )•e.
◮ Proposition 3. For any pre-modality M , the restriction Φ

[M ] = (Φ M /∼ ) | [M ] : [M ] → [R] is a bijection. Furthermore Φ [M ] (e) = R α and Φ [M ] ((a ← b)•m) = (a ← b)•Φ [M ] (m).

Nominal Modality

◮ Definition 10. A nominal modality M , or modality for short, is a set provided with a bijection Φ

M : M → [R]. e = Φ -1 M (R α ) is called its neutral element. For any a, b ∈ A and m ∈ M , (a ← b)•m = Φ -1 M ((a ← b)•R m ).
◮ Corollary 11. Let M be a modality, then M is a pre-modality and

[M ] ∼ = M . Conversely, let M ′ be a pre-modality, then [M ′ ] is a modality. ◮ Proposition 4.
Let M and M ′ be two modalities. There exist a unique bijection φ :

M → M ′ such that: φ(e M ) = e M ′ where e M (resp. e M ′ ) is the neutral element of M (resp. M ′ ). ∀a, b ∈ A ∀m ∈ M, φ((a ← b)•m) = (a ← b)•φ(m)
Such a bijection is called a nominal-modality isomorphism, or modality isomorphism for short, and is writen Φ M →M ′ .

Environments

This section shows that the set of environments [START_REF] Calvès | Matching and alpha-equivalence check for nominal terms[END_REF] is a pre-modality. Thus, by isomorhism, properties on environments can be transposed to any modality.

◮ Definition 12. An environment is a pair (π, δ) of a permutation and a set of atoms. The set of environments (Π × ∆) is written E.

◮ Proposition 5. E is a pre-modality provided with the function Φ E : E → R : R (π,δ) = {(s, t) ∈ N 2 | s ≈ π•t ∧ δ # t} The neutral element of E /∼ is (id, ∅).
for any atoms a and b:

(a ← b)•(π, δ) = ((a π(b)) • π, (δ ∪ {π -1 (a)}) \ {b}).
◮ Proposition 6. Let ξ = (π, δ) and ξ ′ = (π ′ , δ ′ ) be two environments:

ξ ∼ ξ ′ ⇔ δ = δ ′ ds(π, π ′ ) ⊆ δ ◮ Proposition 7.
Let π be a permutation and δ = {a 1 , . . . , a n } ∈ ∆ (atoms a i are considered, without loss of generality, distinct), a ′ i = π(a i ) and b ∈ δ:

∀s, t ∈ N , s ≈ π•t ∧ δ # t ⇔ a ′ 1 .b. . . . a ′ n .b.s ≈ b. . . . b. 2n times π•t ◮ Proposition 8.
Let π be a permutation, there exists a finite sequence of pair of atoms

(a i , b i ) i∈{1...n} such that: ∀s, t ∈ N , s ≈ π•t ⇔ a 1 . . . . a n .s ≈ b 1 . . . . b n .t ◮ Proposition 9.
For any ξ = (π, δ) ∈ E there exists a finite sequence of pair of atoms

(a i , b i ) i∈{1...n} such that R (π,δ) = (a 1 ← b 1 )• . . . (a n ← b n )•R α . In other words, E /∼ = [E].
Thus, for any (pre-)modality M and m ∈ M , we can define the freshness set of m using the isomorphism between environments and M . Precisely: ◮ Definition 13. For any modality M and any m ∈ M , let ξ(m) ∈ E /∼ be the environment equivalence class defined by ξ(m) = Φ M →E /∼ (m). We write δ(m) for the finite set of atoms and Π(m) for the set of permutations such that ξ(m) = Π(m) × {δ(m)}.

Simple Replacings

Simple replacings [START_REF] Levy | An efficient nominal unification algorithm[END_REF], or replacings for short, were introduced by Levy and Villaret as a draft for generalized replacings. Using them to handle nominal constraints is inefficient in practice but being sequences of abstraction they are useful on the theoritical side.

◮ Definition 14. A replacing ℓ is a finite sequence of pair of atoms written (a i ← b i ) i∈{1...n} . The set of replacings is written L.

◮ Definition 15 (Concatenation). Let ℓ = (a i ← b i ) i∈{1...n} and ℓ ′ = (a ′ i ← b ′ i ) i∈{1...n ′ } be two replacings. The concatenation of ℓ and ℓ ′ , written ℓ :: ℓ ′ , is the sequence (a ′′ i ← b ′′ i ) i∈{1...(n+n ′ )} with a ′′ i (resp. b ′′ i ) = a i (resp. b i ) if 1 ≤ i ≤ n a ′ i-n (resp. b ′ i-n ) otherwise The empty sequence is written ε. ◮ Proposition 10. L provided with Φ L : L → R defined by Φ L ((a i ← b i ) i∈{1...n} ) = {(s, t) ∈ N 2 | a n . . . . a 1 .s ≈ b n . . . . b 1 .t} is a pre-modality. The neutral element of L /∼ is ε and, for any ℓ ∈ L, (a ← b)•ℓ = (a ← b) :: ℓ. ◮ Proposition 11. For any ℓ = (a i ← b i ) i∈{1...n} ∈ L, ℓ = (a 1 ← b 1 )• . . . (a n ← b n )•ε. In other words, L /∼ = [L].
◮ Definition 16. For any modality M and any m ∈ M , we write ℓ(m) ∈ L /∼ the replacing defined by ℓ(m) = Φ M →L /∼ (m).

Operations

This section presents all the operations on modal relations (and their modality conterparts) used in the unification algorithms.

Transposition

◮ Definition 17. Let R ∈ R be a relation. The transpose of R, written t R, is defined by

t R = {(s, t) ∈ N 2 | (t, s) ∈ R} ◮ Definition 18.
For any modality M and m ∈ M we can define the transpose of m, written t m,

as t m = Φ [R]→M ( t R m ). ◮ Proposition 12. Let ℓ = (a i ← b i ) i∈{1...n} ∈ L be a replacing, t ℓ = (b i ← a i ) i∈{1...n} . ◮ Proposition 13. For any modalities M and M ′ , ∀m ∈ M, Φ M →M ′ ( t m) = t (Φ M →M ′ (m)).

Support

◮ Definition 19. Let ξ = (π, δ) be an environment. The support of ξ, written, supp(ξ), is defined as supp(ξ) = (id, supp(π) ∪ δ).

◮ Proposition 14. Let ξ = (π, δ) and ξ ′ = (π ′ , δ ′ ) be two environments:

ξ ∼ ξ ′ ⇒ supp(ξ) = supp(ξ ′ ). Thus supp(_) is well-defined on E /∼ : supp(ξ) = supp(ξ).
◮ Definition 20. For any modality M and m ∈ M we can define supp(m) as

supp(m) = Φ E /∼ →M (supp(Φ M →E /∼ (m)))
◮ Proposition 15. For any modalities M and

M ′ ∀m ∈ M, Φ M →M ′ (supp(m)) = supp(Φ M →M ′ (m))

Monoid

◮ Definition 21 (Environment composition). Let ξ = (π, δ) and ξ ′ = (π ′ , δ ′ ) be two environments. The composition of ξ and ξ ′ , written ξ • ξ ′ , is defined as

ξ • ξ ′ = (π • π ′ , π ′-1 (δ) ∪ δ ′ ).
◮ Proposition 16. Let ξ ∈ E be an environment and e = (id, ∅) the neutral element of E:

ξ • e = e • ξ = ξ.
◮ Definition 22 (Relation composition). Let R, R ′ ∈ R be two relations. We define the composition of R and R ′ , written R • R ′ , as

R • R ′ = {(s, u) ∈ N 2 | ∃t ∈ N , (s, t) ∈ R ∧ (t, u) ∈ R ′ } ◮ Proposition 17. Let ξ, ξ ′ ∈ E be two environments, then R ξ•ξ ′ = R ξ • R ξ ′ . ◮ Corollary 23. Let R and R ′ be two relations in [R].
The following propositions hold:

R • R α = R α • R = R R • R ′ ∈ [R] So [R]
provided with R α as its neutral element and the relation composition (•) as its internal law is a monoid. ◮ Definition 24. Any modality M can be given a monoid structure whose neutral element is e M and whose internal law (•) :

M 2 → M is ∀m, m ′ ∈ M, m • m ′ = Φ [R]→M (R m • R m ′ ).

◮ Proposition 18. For any modalities M and M

′ ∀m, m ′ ∈ M, Φ M →M ′ (m • m ′ ) = Φ M →M ′ (m) • Φ M →M ′ (m ′ )

Properties

This section presents basic properties on modalities used in the unification algorithm. In the following M denotes a modality and m, m ′ , . . . denote elements of M .

Decomposition

These properties are proven by the isomorphism between M and E /∼ .

◮ Proposition 19. a.s ≈ m b.t ⇔ s ≈ (a←b)•m t ◮ Proposition 20. f (s 1 , . . . , s n ) ≈ m f (t 1 , . . . , t n ) ⇔ s 1 ≈ m t 1 ∧ • • • ∧ s n ≈ m t n ◮ Proposition 21. (a b)•s ≈ m t ⇔ s ≈ ((a←b)•(b←a)•e)•m t ◮ Proposition 22. s ≈ m (a b)•t ⇔ s ≈ m•((a←b)•(b←a)•e) t

Resolution

Decomposition propositions are able to express relations on nominal terms into relations on their subterms but they are stuck faced to relations such as X ≈ m X or (s

≈ m t ∧ s ≈ m ′ t).
This subsection shows how to deal with such cases.

◮ Proposition 23. s ≈ m s ⇔ s ≈ supp(m) s ◮ Proposition 24. s ≈ m t ∧ t ≈ m ′ u ⇔ s ≈ m t ∧ s ≈ m•m ′ u ⇔ s ≈ m•m ′ u ∧ t ≈ m ′ u ◮ Proposition 25. s ≈ m s ∧ s ≈ m ′ t ⇔ s ≈ supp(m)•m ′ t ◮ Proposition 26. s ≈t m•m s ⇔ δ(m) # s ◮ Proposition 27. m • t m • m = m ◮ Proposition 28 (For). For(m) = δ(supp(m)) ◮ Proposition 29 (Rew). Rew(m) = {(π(b) ← b) | b ∈ supp(π) \ δ(m)} where π ∈ Π(m).

Modal Problems

◮ Definition 27 (Equation). A solution of the equation s ≈ ? m t is a pair (σ, γ) where σ is a substitution and γ freshness context such that γ ⊢ sσ ≈ m tσ holds. Two equations are said to be equivalent if they have the same set of solutions. ◮ Definition 29 (Substitutions). We write X → m s for the elementary substitution defined, when δ(m) # X, by

◮ Definition 28 (Modal Probem

σ(X) = π•s where π ∈ Π(m) σ(Y ) = Y otherwise
◮ Definition 30 (Freshness constraints). We write m # X, when id ∈ Π(m), for the equation X ≈ ? m X. Notice that this is equivalent to δ(m) # X.

The unification algorithm of section 7.2 produces elementary substitution and freshness constraints. They are elementary parts of the incrementatly computed solution. To ease the reading of the paper we have chosen to write them as part of the problem but the reader should keep in mind that they are not inputs but outputs. The "problem" {X → m s, m ′ # Y, s ≈ ? m t} actually represents the modal problem {s ≈ ? m t} where the algorithm has already output the elementary substitution X → m s and the freshness constraint m ′ # Y .

◮ Definition 31 (Fail). fail is to be considered, in the algorithm, as an exception. It means that the problem does not have any solution.

Graph Representation

◮ Definition 32. The graph representation of a problem P, written G P , is the directed graph whose vertex (also called node) set, written G P V is the set of all nominal terms appearing in the problem: ◮ Remark. Note that equivalence of equations s ≈ ? m t and t ≈ ? t m s implies that an edge from s to t labelled by m is also an edge from t so s labelled by t m. Both are considered to be the same edge.

G P V = {r ∈ N | ∃s, t, m r N s ∧ s ≈ m t ∈
Term edges are good at representing term sharing, but they have the drawback that t is considered as a subterm of (a b)•t. So a clycle involving of term edge does not implies that the problem have no solution. For example the cycle

X ≈ ? e (a b) • (a b)•X, (a b) • (a b)•X N (a b)•X, (a b)•X N X
is valid. We need a notion of term edges such that an edge from s to t means that t is a subterm of s but s and t can not be equivalent up to a modality:

◮ Definition 33 (Strict subterm). A strict term edge is an edge s π t from s to t such that either s = a.((a

1 b 1 ) • • • • • (a n b n )•t) or s = f (. . . , (a 1 b 1 ) • • • • • (a n b n )•t, . . . ). s is called a strict parent of t.
If the graph representation of a problem has a cycle involving a strict term edge, then the problem has no solution.

◮ Definition 34 (Path). Let Path be a predicate on pairs of nodes. Path(s, t) = ⊤ if there exists a path from s to t. Let SPath be a predicate on pairs of nodes. SPath(s, t) = ⊤ if there exists a strict path (a path involving a strict term edge) from s to t.

◮ Definition 35 (Term Root). Given a problem P, a term root is a node in G P with no parent. A strict term root is a node with no strict parent.

◮ Definition 36 (Occurences). Given a problem P, the occurence of a node n, written occ(n) is defined as the number of its parents and equivalence arrows involing n:

occ(n) = |{t ∈ G P V | t N n ∈ G P ≺ N }| + |{(s, m) ∈ N × M | s ≈ m t ∈ G P ≈ }|
◮ Definition 37. Given a graph representation P . A ≈-connected component is a connected component for the graph (G P V , G P ≈ ) (same vertices but only equivalence edges).

◮ Remark. ≈-connected components represents classes of α-eqvuivalent terms up to a modality.

◮ Remark (Garbage collection). Note that, as a representation of a problem, when a term diseappear from the problem, its node in the graph and all the edges involved disapear too. More precisely, when a term root does not appear in any equivalence edges, this node is garbage collected. All of its children become term roots and may be garbage collected to.

Unification Algorithm

Though [START_REF] Levy | An efficient nominal unification algorithm[END_REF] and [START_REF] Calvès | The first-order nominal link[END_REF] both rely on the Paterson-Wegnam first-oder linear algorithm, they use very different approaches. This section shows that even this part of the algorithm can be unified. In addition, thanks to the support operation on modalities, the present algorithm can stay general even when dealing with freshness constraints (see propositions 23 and 26).

Rules

The following rules never create nominal terms. Instead they rewrite edges of the graph representation of the problem and create elementaty substitutions/freshness constaints.

◮ Definition 38 (Failure rules).

a ≈ ? m f (t 1 , . . . , t n ) → fail a ≈ ? m b.t → fail f (s 1 , . . . , s n ) ≈ ? m a.t → fail a ≈ ? m b when (a, b) ∈ R m → fail ◮ Definition 39 (Normalisation rules). s ≈ ? m s → s ≈ ? supp(m) s if id ∈ Π(m) s ≈ ? m s, s ≈ ? m ′ t → s ≈ ? m•m ′ t if id ∈ Π(m) s ≈ ? m t, s ≈ ? m ′ t → s ≈ ? m•supp( t m ′ •m) t if m = m ′
◮ Definition 40 (Top to Bottom rules).

(a b)•s ≈ ? m t → s ≈ ? ((a←b)•(b←a)•e)•m t a ≈ ? m b → if (a, b) ∈ R m f (s 1 , . . . , s n ) ≈ ? m f (t 1 , . . . , t n ) → s 1 ≈ ? m t 1 , . . . , s n ≈ ? m t n a.s ≈ ? m b.t → s ≈ ? (a←b)•m t X ≈ ? m r → X → m r, r ≈ ? t m•m r if occ(X) = 1 ∧ r = X X ≈ ? m X → m # X if occ(X) = 1 ∧ id ∈ Π(m) ◮ Definition 41 (≈-Component Exploration rule). s ≈ ? m u, u ≈ ? m ′ r → s ≈ ? m•m ′ r, u ≈ ? m ′
r This is clear that all these rules preserve the set of solution as their left-hand sides are equivalent to their right-hand ones as shown in section 5.

The Paterson-Wegman Strategy

In this section we unify [START_REF] Levy | An efficient nominal unification algorithm[END_REF] and [START_REF] Calvès | The first-order nominal link[END_REF] as a strategy for the rules of section 7.1.

The Strategy

The strategy explores nodes by traversing ≈-connected components and assigning to each node n a component representative (repr(n)). A component is reduced if all of its nodes are term roots (top to bottom). ◮ Definition 42. Let P be a problem. For any node n, repr(n) represents, if defined (⊥ otherwise), an equivalence edge n ≈ ? m r where r is the representative of the ≈-connected component of n. Initially repr(n) = ⊥ for every n. This defines a function repr on nodes treated as a global variable.

We want to reduce first ≈-connected components whose nodes are all term roots but looking for one would be inefficient. Instead we process a component until we find a node s which is not a term root. Let p be one of its parents. We need to reduce the component of p first to make s a term root. Any reduction performed on the component of s must wait for the one p to be resolved. We implement this priority system as a representative stack S. Only reduction involving the top element of S are allowed. This garantees that reductions are performed in the correct order. ◮ Definition 43. Let S be a node stack, treated as a global variable. We define two operations on S: push(n) pushes the node n on the stack and top represents its top element (if it exists). Note that when one node disappear from the problem, it is also removed from S.

This strategy performs stateful computations. The output (written O), the representative function repr and the representative stack S are global variables so we need to consider a state as a tupple composed of a problem and all of the global variables involved in the strategy. The state generated by Paterson-Wegman Strategy rules verifies some helpful properties so we only consider values of these variables that can be generated by the rules.

◮ Definition 44. An ouput, written O, is a set of elementary substitutions and freshness constraints generated by the Paterson-Wegman Strategy rules.

◮ Definition 45 (State). The set of states S is defined as the smallet set of 4-tupple (P, O, repr, S) (where P is a problem, O is an output, repr is a repesentative function and S is a representative stack) such that :

for any problem P, the initial state is (P, ∅, (_ → ⊥), ∅) ∈ S. if a state st ∈ S, and st ′ is obtained by applying one of the Paterson-Wegman Strategy rules on st, then st ′ ∈ S.

◮ Definition 46 (Unification Algorithm). Let P be a problem (the input of the algorithm), take (P, ∅, (_ → ⊥), ∅) as the initial state. Then rewrite it using the following rules until a normal form is reached. If fail is raised, the problem is considered to have no solution.

Otherwise consider the output of the normal state as the most-general unifier of the input problem.

Note that the following rules do work on states, but, in order to ease the reading of the paper, patterns use the expressions s ≈ ? m t and repr(s) to represent respectively the equivalence edge from s to t labelled by m and the image of s by the representative function. Similarly, right-hand sides use the expressions X → m r and m # X to represent respectively the addition to the output of the elementary substition and freshness constraint. The expression repr(s) := s ≈ ? m r means that the image of s by the representative function is set to to s ≈ ? m r. Failure rules are applied at every edge creation. This is done in constant time. Normal The top to bottom rules are only applied on equations repr(s) when occ(s) = 1:

◮ Definition 48 (Top to Bottom Representative rules). The following rules have to be applied only when the left-hand side is a repr(s) for some s such that occ(s) = 1 (repr(s) → . . . if occ(s) = 1):

(a b)•t ≈ ? m r → t ≈ ? ((a←b)•(b←a)•e)•m r a ≈ ? m b → if (a, b) ∈ R m f (s 1 , . . . , s n ) ≈ ? m f (r 1 , . . . , r n ) → s 1 ≈ ? m r 1 , . . . , s n ≈ ? m r n a.t ≈ ? m b.r → t ≈ ? (a←b)•m r X ≈ ? m r → X → m r, r ≈t m•m r if r = X X ≈ ? m X → m # X if id ∈ Π(m)
where (a b)•t, a, f (s 1 , . . . , s n ), a.t and X are instances of s and r, b, f (r 1 , . . . , r n ) and b.r are the representative.

The ≈-component exploration rule have to be applied only when r is the representative:

◮ Definition 49 (≈-Component Representative Definition rule).

s ≈ ? m u, repr(u) →        (repr(s) := s ≈ ? m•m ′ r), repr(u) if repr(s) = ⊥ fail if repr(s) = s ≈ ? m ′′ r ′ ∧ r ′ = r s ≈ ? m•m ′ r, repr(u) if repr(s) = s ≈ ? m ′′ r ∧ u = r
where repr(u) = u ≈ ? m ′ r and s ∈ {r, u}.

The fail correspond to the cyclic occurence checking. It occurs when a node s, whose repr(s) has already been defined as s ≈ ? m1 r 1 (which means s is in the ≈-connected component of r 1 ), also appear in the ≈-connected component of r 2 with r 1 = r 2 . The way representative are selected and defined by traversing term edges make that putting r 1 and r 2 in the same equivalence class would form a cycle.

Finally, we need a rule to initiate the repr propagation:

◮ Definition 50 (repr creation).

If S = ∅, then we select a node r, add repr(r) = r ≈ ? e r to the problem and push r on top of S. r is selected depending on the existance of such a form: if possible, take r of the form f (. . . ), a._ or an atom, otherwise, take a variable X as r. Let s such that repr(s) = s ≈ ? m r, r = top and s has a strict parent p. Then add repr(p) = p ≈ ? e p to the problem, fail if repr(p) = ⊥, and push p on top of S.

Correctness

To prove the correctness, we need to prove that every Paterson-Wegman Strategy is a equivalence on states (so the set of solutions is preserved through rewriting) and that the representative function and stack detect cycles in the solution's graph (occurs-check) (if fail is risen, there is no solution).

◮ Proposition 30. A state is equivalent to the problem

P ∪ {X ≈ ? (π,∅) s | X → m s ∈ O, π ∈ Π(m)} ∪ {X ≈ ? m X | m # X ∈ O}
By language abuse we call solutions of a state the solutions of its equivalent problem.

≈ ? (π,∅) s | X → m s ∈ O, π ∈ Π(m)} ∪ {X ≈ ? m X | m # X ∈ O}

Complexity

This section shows that Paterson-Wegman Strategy rules reach a nornal form in a linear number of steps. We consider here one execution of the algorithm on a problem P. The output, repr and S are treated as global variables. Formally, let P 0 be a problem. The initial state is st 0 = (P 0 , ∅, (_ → ⊥), ∅). Let [st 0 , st 1 , . . . ] be a sequence of states where st i+1 is obtained by applying a Paterson-Wegman Strategy rule on st i .

◮ Definition 53 (Size). The size of a graph representation G P , writen |G P |, is defined by

|G P | = |G P V | + |G P E | ◮ Definition 54 (Mesure).

Modal Complexity

The complexity of every rewriting steps depends on the complexity of modal operations which itself depends on the modality used.

Let P be a problem and A P be the set of atoms appearing in P. The unification algorithm does not introduce any atom. So any modal operation computed by any rewriting step only involves atoms in A P . If any modal operation can be computed in at most θ(|A P |), the complexity of the unification algorithm is at most θ(|A P | × µ(G P )).

As proven in [START_REF] Calvès | Matching and alpha-equivalence check for nominal terms[END_REF], modal operation on environments can be computed in θ(|A P |) using intergers as atoms and arrays as permutations and freshness sets. Thus using environments, the algorithm is quadratic in time.

Replacings

Computing eagerly replacings would be terribly inefficient. Levy and Villaret avoid this complexity by introducing generalized replacings which can be seen as a formulae of modal operations. Using subterm sharing, they get a directed acycling graphs of modal-operation formulas for which they compute the sets For(g) and Rew(g) to determine whether a ≈ ? g b is true or not. ◮ Remark. The definition in [START_REF] Levy | An efficient nominal unification algorithm[END_REF] does not contain supp(g). Instead, multiple occurences of the same variables are kept in multi-equations. ◮ Proposition 40. GL is a pre-modality.

◮ Proposition 41. GL /∼ = [GL]

The size of the acyclic graph representing modal-operation formulae is linear in the size of the input problem P because a linear number of Paterson-Wegman Strategy rules lead to a normal form and each rule involved a bounded number of modal operations. As proven in [START_REF] Levy | An efficient nominal unification algorithm[END_REF] we can check in quadratic time if the problem has a solution.

9

Related and Future Work Cheney [4] proved that higher-order pattern unification reduces to nominal unification. Levy and Villaret [START_REF] Levy | Nominal unification from a higher-order perspective[END_REF] proved the opposite side. These two results prove that higher-order pattern and nominal unification are equivalent. It would be interesting to adapt modalities to higher-order patterns.

Permissive nominal syntax [START_REF] Dowek | Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques[END_REF] is a modification to the original syntax to ease the writing of proofs. Given a term t, we know that there are infinitely many fresh atoms for t, but we need freshness constraints to set them. Permissive nominal syntax encodes directly in a term (on variables) which atoms may occur free or not inside. It would be interesting to investigate if our approach can be adapted to take into account this modification.

Conclusion

The unique isomorphism between modalities is a powerful tool to establish properties on a representation. Most of the propositions of section 5 where established by proving them on environments and then transposing to any modality by isomorhpism. Furthermore, the algorithm completely isolates nominal constraints from first-order ones. Even when dealing with freshness constraints thanks to Proposition 26.

Figure 1

 1 Figure 1 Inductive definition of α-equivalence and freshness relations.

4. 4

 4 Replacings operations ◮ Definition 25 (For). Let M be a modality and m ∈ M , we can define the set of forbidden atoms of m by For(m) = {a ∈ A | ¬(a ≈ m a)}. ◮ Definition 26 (Rew). Let M be a modality and m ∈ M , we can define the renaming function of m by Rew(m) = {(a ← b) ∈ A × A | a = b ∧ a ≈ m b}.

◮

  Definition 56 (Generalized Replacings). The set GL of generalized replacings is the set of terms generated by the grammar:GL = e | (a ← b)•GL | t GL | GL • GL | supp(GL).

  1 , . . . , s n ) ≈ f (t 1 , . . . , t n ) in terms of relations s i ≈ t i . But we can not express a.s ≈ b.t in terms of s ≈ t where a and b are two different atoms. The relation between s and t is not the α-equivalence but another relation, written s ≈ (a←b)•e t.

  ). A nominal modal problem P (or modal problem for short) is a set of equations of the form s ≈ ? Note that s ≈ m t is equivalent to t ≈t m s. So, in the following, every predicate, pattern, etc involving an equation s ≈ ?

m t . (σ, γ) is a solution of P if it is a solution for any equation s ≈ ? m t in P. Two problems are said to be equivalent if they have the same set of solutions. ◮ Remark. m t also matches the equation t ≈ ? t m s. For example, a ≈ ? (c←d)•e b ∈ {b ≈ ? (d←c)•e a}.

  P}. edge set, written G P E , is G P ≺ N ∪ G P ≈ where G P ≺ N is the set of termgraph edges. Let s N t be such an edge. It means that t is a direct proper subterm of of s, i.e. that either s = a.t, s = f (. . . , t, . . . ) or s = (a b)•t. s is called a parent of t and t is called a child of s. In the algorithm, permutation actions π•s are not applied but considered as syntactic constructions. For example, let t be the term (a b)(c d)•X. Its child is (c d)•X whose child is X. G P ≈ is the set of equations s ≈ ? m t considered as edges from s to t labelled by m and called equivalence edge: G P ≈ = P ∪ {s ≈ ? (a←b)•(b←a)•e t | s, t ∈ G P V s = (a b)•t}. Several structurally equal subterms can be represented as several nodes but there must be exactly one node per variable in the problem.

◮ Remark. Let s = (a b)•t be a term appearing in P. This relation is not only a term edge but also an equivalence relation so it is also represented as an equivalence edge. These relations form the set {s ≈ ? (a←b)•(b←a)•e t | s, t ∈ G P V s = (a b)•t} which is contained in G P ≈ . ◮ Remark.

  isation rules are applied mostly on repr at edge creation: ◮ Definition 47 (Representative Normalisation rules).

	t ≈ ? m t	→	t ≈ ? supp(m) t	if id ∈ Π(m)
	s ≈ ? m s, s ≈ ? m ′ t → s ≈ ? m r, repr(s) → repr(s) := s ≈ ? s ≈ ? m•m ′ t m•supp( t m ′ •m) r if m = m ′ if id ∈ Π(m)
	where repr(s) = s ≈ ? m ′ r. Furthermore, if s ≈ ? m ′ t or s ≈ ? m s is repr(s) (resp. t ≈ ? m t) then repr(s) becomes s ≈ ? m•m ′ t (resp. t ≈ ? supp(m) t).

◮

  Proposition 31. Every Paterson-Wegman Strategy rule transforms a state into an equivalent one or fail.Proof. Every rule that does not raise fail is an equivalence on the equivalent problem of a state.◭Now we need to prove that when fail is raised, then the state does not have any solution. One step of rewriting either alter the modality m (repr(s) becomes s ≈ ? m ′ r) or removes complety s from the problem.

◮ Proposition 32. Let s be a node such that repr(s) = s ≈ ? m r.

◮ Corollary 51. repr(s) = s ≈ ? m r ⇒ repr(r) = r ≈ ? m ′ r ∧ r ∈ S ◮ Proposition 33. S = [r 1 , . . . , r i , . . . ,

r j , . . . , r n ] ⇒ SPath(r i , r j ) where r n = top. ◮ Corollary 52. If S = [r 1 , . . . , r t , . . . , r s , . . . , r n ] and s ≈ m t ∈ P with repr(s) = s ≈ ? ms r s , repr(t) = t ≈ ? mt r t and r s = r t . Then the problem has no solution. ◮ Proposition 34. If fail is raised on a state, then it has no solution. ◮ Proposition 35. An output O is the most-general unifier of its equivalent problem {X

  The mesure of G P , written µ(G P ), is the sum of 1 per node in G P V . Proposition 36. µ(G P ) ≤ 3|G P | ◮ Proposition 37. The strategy reduces G P to a normal form in at most µ(G P ) steps of rewriting. ◮ Definition 55. A state (P, O, repr, S) is said to be in solved form either if P = ∅ or if fail has been raised. ◮ Proposition 38. Normal forms are solved form. ◮ Proposition 39. The algorithm computes the most-general unfier of a problem P if it exists or raise fail in a linear number of rewriting steps.

	2 per node whose repr(s) = ⊥.
	1 per equivalence edge.
	1 per equivalence edge s ≈

m t with id ∈ Π(m). 2 per equivalence edge s ≈ m t where repr(s) = s ≈ m ′ t. 3 per term edge.

◮


Cyril Bouvier

Paul Zimmermann

Division-Free Binary-to-Decimal Conversion

Keywords: decimal conversion, scaled remainder tree, GMP ✦

This article presents algorithms that convert multiple precision integer or floating-point numbers from radix 2 to radix 10 (or to any radix b > 2). Those algorithms, based on the "scaled remainder tree" technique, use multiplications instead of divisions in their critical part. Both quadratic and subquadratic algorithms are detailed, with proofs of correctness. Experimental results show that our implementation of those algorithms outperforms the GMP library by up to 50% (using the same low-level routines).

INTRODUCTION

Since computers usually work in binary and humans prefer decimal numbers, the conversion of multiple precision integers from radix 2 to radix 10 -or more generally to any radix b > 2 -is a fundamental operation. The binary-to-decimal conversion is implemented in most multiple precision libraries (GMP, PARI/GP, CLN, NTL to cite a few) or computer algebra systems (Maple, Mathematica, Sage). The classical way to perform this conversion is to repeatedly divide the given integer by the output radix b: the remainder gives the least significant digit of the output string, and one continues with the quotient until is becomes zero (see Section 4.4, Method 1a in [START_REF] Knuth | The Art of Computer Programming[END_REF]). A subquadratic version of that algorithm based on long division is well understood too (see Section 1.7.2 of [START_REF] Brent | Modern Computer Arithmetic, ser. Cambridge Monographs on Applied and Computational Mathematics[END_REF]).

An alternate algorithm, which is less known, replaces divisions by multiplications in the critical loop. The idea can be found in [START_REF] Stroud | A multiple-precision floating-point interpretive program for the Control Data 1604[END_REF], [START_REF] Sterbenz | Floating-Point Computation, ser. in Automatic Computation[END_REF] and [START_REF] Knuth | The Art of Computer Programming[END_REF]Section 4.4], where Knuth presents an algorithm -Method (2a) -to convert fractional numbers using multiplication, and says "it is certainly possible to convert between integers and fractions by multiplying or dividing by an appropriate power of b or B"; however no further details are given. A similar idea is used by Bernstein in [START_REF] Bernstein | Scaled remainder trees[END_REF] to compute U mod p 1 , U mod p 2 , ... where U, p 1 , p 2 , ... are integers; Bernstein calls the underlying structure a "scaled remainder tree".

In this article we present detailed algorithms based on the "scaled remainder tree" idea, both in the quadratic range (for small numbers) and in the subquadratic range (for large numbers). When given a nonnegative integer a of (at most) k digits in radix b, those algorithms first approximate the radix-b fraction a/b k by a binary fraction y/2 n , then this binary fraction is converted to radix b using a division-free algorithm. In the whole article we assume b fits in a machine word, and is not a power of two, in which case trivial algorithms exist.

E-mail: Cyril.Bouvier@inria.fr, Paul.Zimmermann@inria.fr

The article is organized as follows. After a description in Section 2 of classical algorithms, both in the quadratic and subquadratic case, Section 3 presents the divisionfree algorithms and their proof of correctness; Section 4 briefly discusses how those algorithms can be used to convert floating-point numbers; finally Section 5 compares our implementation of the algorithms of Sections 3 and 4 to the reference implementation of classical algorithms in GMP [START_REF] Granlund | the GMP development team, GNU MP: The GNU Multiple Precision Arithmetic Library[END_REF].

CLASSICAL DIVISION-FULL CONVERSION

The literature contains only a few references on multiple precision binary-to-decimal conversion. Apart from [START_REF] Knuth | The Art of Computer Programming[END_REF] and [START_REF] Brent | Modern Computer Arithmetic, ser. Cambridge Monographs on Applied and Computational Mathematics[END_REF], we found an article of Roman Maeder in The Mathematica Programmer (volume 6, issue [START_REF] Stroud | A multiple-precision floating-point interpretive program for the Control Data 1604[END_REF]1996). Most references only describe algorithms with division (except [START_REF] Knuth | The Art of Computer Programming[END_REF], but which does not consider multiple precision division-free conversion). We briefly outline those classical algorithms in this section.

Quadratic Algorithm

The straightforward quadratic conversion of a multiple precision integer a to radix b just consists of computing a mod b, which will give the least significant digit in radix b, and repeat with a ′ = ⌊a/b⌋, and so on, until we get zero. If the input a has n words, this algorithm clearly takes O(n 2 ) time, and the critical loop mainly divides a multi-word integer by one word, since we assumed the radix b fits into one machine word. In GMP, this corresponds to the mpn_divrem_1 function.

An easy way to speed up this algorithm is to first compute the largest power b j that fits into a word, divide by b j in each loop, which will produce a remainder r less than b j , and convert r into j digits in radix b using an auxiliary routine. This will divide the number of calls to mpn_divrem_1 by a factor of j, where j = 9 on a 32-bit computer, and j = 19 on a 64-bit computer for b = 10. This method is described in the documentation of GMP. Note that GMP uses the "scaled remainder tree" technique to convert r into j digits: instead of performing j divisions by b, GMP first approximates the fraction r/b j , then digits are extracted by multiplications.

Subquadratic Algorithm

The subquadratic classical conversion is described in detail in [START_REF] Brent | Modern Computer Arithmetic, ser. Cambridge Monographs on Applied and Computational Mathematics[END_REF], and is the algorithm used in GMP 5.1.2. Assuming the input number has at most k digits in radix b, with k a power of two, precompute b k/2 , b k/4 , b k/8 , ... Then compute q and r such that a = qb k/2 + r with 0 ≤ r < b k/2 , and divide recursively q and r (with remainder) by b k/4 , and so on until the number of digits to be printed is below a threshold k t , then we use the naive algorithm described in §2.1. This technique is called "remainder tree" in the literature.

The GMP documentation (in version 5.1.2) mentions that the "scaled remainder tree" technique might be used in the subquadratic case, however some brief experiments [...] didn't give a noticeable improvement; this is exactly the idea used in the algorithms we describe below.

DIVISION-FREE CONVERSION

Naive Algorithm

The naive conversion first computes a floating-point approximation x = y/2 n of a/b k . Since we assumed that a is nonnegative and has at most k digits in radix b, we have 0 ≤ a/b k < 1, thus the integer part of bx will reveal the most significant digit (in radix b) of a, more precisely the digit of weight b k-1 . Then we continue with the fractional part of bx, and so on until we get exactly k digits in radix b. Note: since the output radix b is fixed for a given computation, we do not explicitly state it in the parameters of our functions.

Algorithm 1 Naive conversion

Input: integers a and k such that a < b k Output: a string s of k digits in radix b (with potential leading zeros) 1: choose an integer n such that 2b k < 2 n 2:

y 0 ← ⌊(a + 1)2 n /b k ⌋ -1 3: return CONVERT NAIVE(y 0 , k, n) 4: 5: function CONVERT NAIVE(y 0 , k, n) 6: for i = 1 to k do 7: t i ← by i-1 8: s k-i ← ⌊t i /2 n ⌋ 9: y i ← t i mod 2 n 10: return (s k-1 , . . . , s 0 )
The main cost in Algorithm 1 is the multiplication of b by y i-1 in Step 7; a variant with truncation to reduce this cost is given in Algorithm 2. We prove the correctness of this variant in Theorem 3.

The choice of y 0 in Algorithms 1 and 2 is motivated by the inequality proven in the following lemma.

Algorithm 2 Naive conversion with truncation

Input: integers a and k, such that k ≥ 2 and a < b k Output: a string s of k digits in radix b (with potential leading zeros) 1: choose an integer n such that 2kb k < 2 n 2:

y 0 ← ⌊(a + 1)2 n /b k ⌋ -1 3: return CONVERT TRUNC(y 0 , k, n) 4: 5: function CONVERT TRUNC(y 0 , k, n) 6: choose a floating-point value 0 ≤ α ≤ log 2 (b) 7:
write n i for n -⌊iα⌋ 8:

for i = 1 to k do 9: t i ← by i-1 10: s k-i ← ⌊t i /2 ni-1 ⌋ 11: z i ← t i mod 2 ni-1
12:

y i ← ⌊z i /2 ni-1-ni ⌋ 13: return (s k-1 , . . . , s 0 ) Lemma 1.
Let a and k be nonnegative integers such that k ≥ 2 and a < b k . Let n be a nonnegative integer such that 2kb k < 2 n . Define y 0 as

y 0 = ⌊ (a + 1)2 n b k ⌋ -1. (1)
Then, the following inequality stands:

a + 1 2 < b k y 0 2 n < a + 1.
Proof: By definition of y 0 , one has

y 0 ≤ (a + 1)2 n b k -1 < y 0 + 1, so one can deduce a + 1 - 2b k 2 n < b k y 0 2 n ≤ a + 1 - b k 2 n . (2)
The condition

2kb k < 2 n with k ≥ 2 implies 4b k < 2 n . It follows a + 1/2 ≤ a + 1 -2b k /2 n . Lemma 2. Let y 0 , k, n be nonnegative integers such that k ≥ 2, 2kb k < 2 n and a + 1 2 < b k y 0 2 n < a + 1,
where a in a nonnegative integer such that a < b k . Then, the output of CONVERT TRUNC(y 0 , k, n) satisfies

a = k-1 i=0 s i b i with 0 ≤ s i < b, ∀i ∈ [0, k -1].
Proof: Using the hypothesis that b k y 0 < (a+1)2 n and a < b k and the fact that n 0 = n, we have y 0 < 2 n0 . Moreover, for i ∈ [1, k], due to line 11, one has 0

≤ z i < 2 ni-1 , so 0 ≤ y i < 2 ni after line 12. So, for i ∈ [1, k], one has 0 ≤ y i-1 < 2 ni-1 , thus 0 ≤ s k-i < b. For i ∈ [1, k],
the following equality stands:

by i-1 = s k-i 2 ni-1 + y i 2 ni-1-ni + r i ,
where

r i := t i mod 2 ni-1-ni . So, b k y 0 = s k-1 2 n b k-1 + b k-1 y 1 2 n-n1 + b k-1 r 1 = s k-1 2 n b k-1 + b k-1 r 1 + b k-2 2 n-n1 (2 n1 s k-2 + y 2 2 n1-n2 + r 2 ) . . . = k i=1 s k-i 2 n b k-i + k i=1 r i b k-i 2 n-ni-1 + y k 2 n-n k .
Using the hypothesis, the following inequalities hold:

a + 1 2 < k-1 i=0 s i b i + k i=1 r i b k-i 2 -ni-1 + y k 2 -n k < a + 1. (3) As 0 ≤ y k < 2 n k , we have 0 ≤ y k 2 -n k < 1. Moreover, since 0 ≤ r i < 2 ni-1-ni and 2 α ≤ b: 0 ≤ k i=1 r i b k-i 2 -ni-1 < k i=1 b k-i 2 -ni = k i=1 b k-i 2 iα-n ≤ k b k 2 n < 1 2 .
So, one can deduce

a -1 < k-1 i=0 s i b i < a + 1.
Since both a and Proof: The correctness of Algorithm 2 is proven by Lemma 1 and Lemma 2.

Algorithm 1, where no truncation occurs, corresponds exactly to Algorithm 2 with α = 0, which yields n i = n and r i = 0. Then Eq. (3) becomes:

a + 1 2 < k-1 i=0 s i b i + y k 2 -n k < a + 1, which gives a -1/2 < k-1 i=0 s i b i < a + 1 since 0 ≤ y k 2 -n k < 1.
In this case we can relax the result of Lemma 1 into a < b k y 0 /2 n < a + 1, which according to Eq. ( 2) holds as soon as 2b k < 2 n , which is exactly what we choose in Algorithm 1. This proves the correctness of Algorithm 1.

In Algorithm 2 (with truncation), the condition 2kb k < 2 n can be replaced by 2rb k < 2 n , where r ≥ 2 is an upper-bound on the number of truncations.

Note that the quadratic division-free conversion with truncation is very similar in complexity to the quadratic division-full conversion, since the working size decreases regularly from n to 0 bits throughout the algorithm. The main difference is that in the division-free algorithm, divisions are replaced with multiplications, which are cheaper.

Implementation details

In practice, in Algorithm 2, the digits are computed by blocks of j digits, where j is the largest integer such that b j fits in a word. This replaces the multiplication by b in line 9 by a multiplication by b j which has the same cost, as b j fits in a word, and decreases the number of such multiplications by a factor of j.

The remaining problem is to extract from the s k-i 's the j digits (instead of one digit previously). This is done by computing s k-i separately from the rest of the product. First, notice that s k-i is the highest word of the product of y i-1 by b j and is, up to a carry, the high word of the two-word product of the most significant word of y i-1 by b j . This two-word product can be performed by a series of multiplications by b, b 2 , b 3 or b 4 and the digit, or the 2, 3 or 4 digits, can be extracted from the high word with look-up tables. The low word of this two-word product is then added to the rest of the product b j y i-1 (performed with the mpn_mul_1 function of GMP). If a carry arises, the digits are corrected.

Subquadratic Algorithm

The idea of the subquadratic algorithm is the following: starting from a n-bit integer y such that yb k 2 -n approximates an integer a of k digits in radix b, one will compute two integers y h and y ℓ of about n/2 bits each, and corresponding integers k h , n h , k ℓ , n ℓ , such that y h b k h 2 -n h and y ℓ b k ℓ 2 -n ℓ approximate respectively the more significant part a h of a and its less significant part a ℓ (both in radix b). The following lemma shows that if yb k 2 -n is sufficiently near to a, then y h b k h 2 -n h and y ℓ b k ℓ 2 -n ℓ -as defined below -are both sufficiently near to a h and a ℓ respectively. Lemma 4. Let b ≥ 3 be the output radix. Let g ≥ 2 be an integer (rationale behind g: bound on the number of recursive calls). Let a, y, k and n be nonnegative integers and

d ≤ 1 such that a < b k and a -d < yb k 2 n < a + 1. ( 4
)
Let k h , k ℓ , n h and n ℓ be nonnegative integer and define k 0 as k = k h + k 0 and n 0 as n = n h + n 0 . The integers k h , k ℓ , k 0 , n h , n ℓ and n 0 should satisfy:

• k 0 ≥ 2, k ℓ ≤ k, n h ≤ n and n ℓ ≤ n, • 4gb k h < 2 n h and 4gb k ℓ < 2 n ℓ .
Let us define a h as a = a h b k0 +a 0 and y h as y = y h 2 n0 +y 0 where 0 ≤ a 0 < b k0 and 0 ≤ y 0 < 2 n0 . Moreover, let us define a ℓ as a ℓ = a mod b k ℓ (i.e., a ℓ corresponds to the k ℓ least significant digits of a in radix b). Finally, let us define y ℓ as

y ℓ = ⌊ (b k-k ℓ y) mod 2 n 2 n-n ℓ ⌋,
which means that after multiplying y by b k-k ℓ , we extract the n ℓ bits from position n -n ℓ to n -1.

Then, we have

a h < b k h , a ℓ < b k ℓ and a h - 1 4 < y h b k h 2 n h < a h + 1, (5)
a ℓ -d - 1 4g < y ℓ b k ℓ 2 n ℓ < a ℓ + 1. (6)
Proof: First, a ℓ < b k ℓ is satisfied by definition of a ℓ , and a h < b k h is satisfied by definition of a h and the fact that a < b k . Now, we will prove Eq. ( 5). We have from Eq. ( 4):

y h 2 n0 + y 0 2 n b k < a h b k0 + a 0 + 1, thus y h b k h 2 n h < a h + 1, since a 0 + 1 ≤ b k0 .
On the other side, again from Eq. ( 4):

y h 2 n0 + y 0 2 n b k > a h b k0 + a 0 -d ≥ a h b k0 + a 0 -1, thus y h b k h 2 n h > a h - 1 b k0 - y 0 b k h 2 n .
Since y 0 < 2 n0 and b k0 > 8 (remember b ≥ 3 and k 0 ≥ 2),

1 b k0 + y 0 b k h 2 n < 1 8 + b k h 2 n h < 1 8 + 1 4g ≤ 1 4 , since g ≥ 2.
This proves Eq. ( 5).

Finally, we will prove Eq. ( 6). Firstly, we assume a ℓd ≥ 0. We have from Eq. ( 4):

2 n a -d b k ℓ < yb k-k ℓ < 2 n a + 1 b k ℓ .
Writing a = a 1 b k ℓ +a ℓ , with a 1 representing the most significant digits, and taking the above inequality modulo 2 n , the terms in a 1 cancel:

2 n a ℓ -d b k ℓ < yb k-k ℓ mod 2 n < 2 n a ℓ + 1 b k ℓ .
Dividing by 2 n-n ℓ , we get:

2 n ℓ a ℓ -d b k ℓ -1 < y ℓ < 2 n ℓ a ℓ + 1 b k ℓ , thus: a ℓ -d - b k ℓ 2 n ℓ < y ℓ b k ℓ 2 n ℓ < a ℓ + 1.
We thus prove Eq. ( 6) for the less significant part. In the case where a ℓ -d < 0, the proof above is still valid for:

y ℓ b k ℓ 2 n ℓ < a ℓ + 1.
We also have, since y ℓ ≥ 0,

y ℓ b k ℓ 2 n ℓ ≥ 0 > a ℓ -d - 1 4g .
So Eq. ( 6) holds for every value of a ℓ . Note also that we did not assume that a h and a ℓ overlap up to here, i.e., k h + k ℓ ≥ k does not necessarily hold.

Algorithm 3 uses a scaled remainder tree; the main difference with Bernstein's work in [START_REF] Bernstein | Scaled remainder trees[END_REF] is that our scaled remainder tree is asymmetrical, and going to a left subtree requires no multiplication. In this algorithm the parameter a of function CONVERT REC is only here for proof purpose. This means that a h and a ℓ need not be computed at lines 9 and 10 during an actual run of the algorithm.

Algorithm 3 Subquadratic Division-Free Conversion

Input: integer a, radix b ≥ 3, threshold k t ≥ 3 Output: a string s of digits in radix b (with potential leading zeros) 1: function CONVERT REC(a, y, k, n, g)

2: if k ≤ k t then 3: return CONVERT TRUNC(y, k, n) 4: else 5: k h ← ⌊ k+1 2 ⌋ 6: k ℓ ← k -k h + 1 7:
Choose

n h ≤ n such that 4gb k h < 2 n h 8:
Choose n ℓ ≤ n such that 4gb k ℓ < 2 n ℓ 9:

a h ← ⌊ab k h -k ⌋ 10: a ℓ ← a mod b k ℓ 11: y h ← ⌊y2 n h -n ⌋ 12: y ℓ ← ⌊ (b k-k ℓ y) mod 2 n 2 n-n ℓ
⌋.

13:

s h ← CONVERT REC(a h , y h , k h , n h , g) 14: s ℓ ← CONVERT REC(a ℓ , y ℓ , k ℓ , n ℓ , g) 15:
if the trailing digit of s h is b-1 and the leading digit of s ℓ is 0 then 16:

s h ← s h + 1 17: return s = ⌊s h /b⌋b k ℓ + s ℓ 18: 19: k ← ⌈log b (a)⌉ 20: g ← max(⌈log 2 (k)⌉ + 1, k t ) 21: Choose n such that 4gb k < 2 n 22: y ← ⌊ (a+1)2 n b k ⌋ -1 23: return CONVERT REC(a, y, k, n, g)
Before we prove the correctness of Algorithm 3, we make a comment: the condition k t ≥ 3 ensures that k ≥ 4 in the recursive calls, thus k h ≥ 2 (if k h = 1 then k ℓ = k and the function would loop forever) and that the condition k 0 = k -k h ≥ 2 is always true. Lemma 5. Assume CONVERT REC is called with nonnegative integers a, y, k, n, g, and a real

d such that d ≤ 1/2, k > k t , g ≥ 2, a < b k and a -d < yb k 2 n < a + 1 (7) then a h < b k h and a ℓ < b k ℓ , a h - 1 4 < y h b k h 2 n h < a h + 1, a ℓ -d - 1 4g < y ℓ b k ℓ 2 n ℓ < a ℓ + 1. (8)
Moreover, for d ≤ 1 4 and at most g recursive calls, the inequalities

a - 1 2 < yb k 2 n < a + 1 and a < b k (9)
hold at any level of the recursion.

Proof: The hypothesis of this Lemma, the choices of k h and k ℓ , and lines 7 and 8 of Algorithm 3 allow us to use Lemma 4 to prove Eq. ( 8).

We can apply the result above recursively to a h and a ℓ and so on. So if we start from Eq. ( 7) with d ≤ 1/4, then after at most g recursive calls, we have at most t ≤ g successive right nodes, so we have

a - 1 4 - t 4g < yb k 2 n < a + 1
at any level of recursion. This proves Eq. ( 9). Lemma 6. Assume CONVERT REC is called with nonnegative integers a, y, k, n, g, and a real

d such that d ≤ 1/4, g ≥ 2, a < b k , k t ≤ g, 4gb k < 2 n
, that Eq. ( 7) is satisfied and that at most g recursive calls are made. Then, the output string s satisfies (identifying s and its value in radix b) s = a or s = a -1 (the case s = a -1 cannot happen if a = 0).

Proof: We consider the tree made of the recursive calls of function CONVERT REC. Let us call its height h. By hypothesis, we have h ≤ g. Using Lemma 5, we have that Eq. ( 9) is verified for all nodes of the tree.

We will prove the result by induction on h. For h = 0, we are in the case k ≤ k t . By hypothesis, we have k ≤ k t ≤ g, so 4kb k < 2 n . We also have by induction hypothesis a < b k . By using the same proof as for Lemma 2, but with the initial inequality of Eq. (9), we can prove that the output of CONVERT TRUNC gives s = a or s = a -1. For the case a = 0, as the output is always nonnegative, we have necessarily s = a.

For h > 0, we have by induction hypothesis, s h = a h or s h = a h -1, and s ℓ = a ℓ or s ℓ = a ℓ -1. But since k h + k ℓ = k + 1, s h and s ℓ overlap by one digit. We distinguish the following cases, where we denote by a h,0 the trailing digit of a h , by s h,0 the trailing digit of s h , by a ℓ,1 the leading digit of a ℓ (which equals a h,0 ), and by s ℓ,1 the leading digit of s ℓ . In the following, we consider values of s h and s ℓ just after line 14:

• s h = a h : no fixup occurs since s ℓ,1 = s h,0 or s ℓ,1 = s h,0 -1, so the case s h,0 = b -1 and s ℓ,1 = 0 is impossible (b ≥ 3). Thus the value s at line 17 equals a or a -1 depending on s ℓ being a ℓ or a ℓ -1;

• s h = a h -1 and a h,0 > 0: no fixup occurs since s h,0 = a h,0 -1, so s h,0 < b -1. Thus the value s at line 17 equals a or a -1 depending on s ℓ being a ℓ or a ℓ -1;

• s h = a h -1 and a h,0 = 0: in this case s ℓ,1 = a ℓ,1 = 0 (because if s ℓ = a ℓ -1, a ℓ > 0, so the leading digit remains the same) and s h,1 = b -1. So a fixup step occurs at line 15. After the fixup, we have s h = a h and, as in the first case, the value s at line 17 equals a or a -1 depending on s ℓ being a ℓ or a ℓ -1.

So the result is proven by induction on the height of tree made of the recursive calls.

Theorem 7. Assume Algorithm 3 is called with the integer a, then the output string s verifies s = a (identifying s and its value in radix b).

Proof: Using the inequality of line 21 of Algorithm 3 and Eq. ( 2), we can show that the call to the function CONVERT REC at line 23 of Algorithm 3 satisfies Eq. ( 7) with d = -3/4. Moreover, line 20 of Algorithm 3 ensures that at most g recursive calls will be made. So Lemma 6 can be applied, and we have s = a or s = a -1.

We will now show that the case s = a-1 is impossible. Having s = a -1 means that an error of one was done on the least significant digit. The least significant digit is handled by CONVERT TRUNC (basecase) after (at most) g recursive calls of CONVERT REC on the low part. This means that when CONVERT TRUNC is called, we have

a -d 0 - g 4g < yb k 2 n < a + 1,
with d 0 = -3/4 being the error before the first call to CONVERT REC, as seen above. Thus, when CON-VERT TRUNC is called, the hypotheses of Lemma 2 are satisfied, thus the output of CONVERT TRUNC will be a. So no error can be done on the least significant digit, and so we necessarily have s = a.

Theorem 8. Given an input a of n bits, Algorithm 3 has complexity O(M (n) log n), where M (n) is the time needed to multiply two n-bit numbers.

Proof: Since k t is a constant, it suffices to consider the recursive case. Since g is a constant too, we have n h = n/2 + O(1) and similarly for n ℓ . As mentioned earlier, lines 9 and 10 are not performed in a real implementation. The computation of y h at line 11 is for free, since it consists of extracting the upper bits of y. The multiplication b k-k ℓ y at line 12 costs 2M (n/2) since y has n bits, and b k-k ℓ has ∼ n/2 bits. (We can compute b k-k ℓ on the fly without changing the asymptotic complexity up to a constant multiplicative factor; in practice one will precompute b k-k ℓ , and ensure the same b k-k ℓ value is needed at each level of the recursive tree.) Thus if C(n) denotes the cost of the algorithm for n-bit input, we have

C(n) = 2C(n/2)+2M (n/2)+O(n), which yields C(n) = O(M (n) log n).

Using a middle product to compute y ℓ

The computation of y ℓ on line 12 of Algorithm 3 can be done by computing a middle product [START_REF] Harvey | The Karatsuba integer middle product[END_REF]. A product of a 2N -bit integer by a N -bit integer gives a 3N -bit result that can be divided in 3 parts of N bits each. A middle product is the computation of the N -bit middle part. The computation of y ℓ falls into this scheme. By taking k h = ⌊(k + 1)/2⌋ and n ℓ as small as possible, we ensure b k-k ℓ < 2 n-n ℓ +1 . So, the product on line 12 is the middle product of y (of size n) by b k-k ℓ (of size n -n ℓ + 1 ≃ n/2), as we only need the n ℓ ≃ n/2 middle bits.

For small sizes (less than a couple of thousands words) we can use the mpn_mulmid function of GMP. For larger sizes we use an FFT middle product. This means that to compute the product of x (of size n/2) by y (of size n), one computes xy mod 2 n + 1 with an FFT algorithm and gets the middle product from the n/2 high bits of the n-bit result.

In both cases, by using the middle product, we compute either y ℓ or y ℓ -1, the latter one with very low probability. So this adds a -1/(4g) term on the leftmost term of Eq. ( 6) in Lemma 4 and leaves the other terms unchanged. In order to ensure that CONVERT TRUNC still returns a or a -1, we just have to change the condition 4gb k < 2 n into 8gb k < 2 n everywhere in the algorithm.

FLOATING-POINT CONVERSION

A floating-point number is represented in a binary computer as x•2 e , where the integer x is the n-bit significand, and e is the exponent. Since the algorithms presented in Section 3 first compute a fractional approximation y2 -n of ab -k , when converting a floating-point number we have such an approximation for free, especially when e is near -n, which means the floating-point number we consider is in the vicinity of 1 (or -1 if negative).

On the contrary, when using the classical conversion, to obtain the integer a such that ab -k approximates y2 -n , one will need to multiply y by b k , and then divide by 2 n . This adds an overhead with respect to the integer conversion routine.

EXPERIMENTAL RESULTS

We did implement our algorithms in GMP, using the low-level GMP routines, thus the time differences are due to differences in the algorithms, and not in the lowlevel arithmetic.

All timings were obtained with GMP 5.1.2 on an AMD Phenom II X2 B55 processor running at 3Ghz, with 8Gb of memory and gcc 4.7.3, with optimization level -O3. GMP uses a quadratic algorithm up to GET_STR_PRECOMPUTE_THRESHOLD words (29 words in our experiment). The output radix is always b = 10.

Quadratic Algorithm

Figure 1 compares our implementation of Algorithm 2 with the GMP mpz_get_str function, for 1 to 50 words. Our implementation is up to about 55% faster than GMP (between 20 and 28 words), then when the number of words increases the subquadratic algorithm used by GMP wins over Algorithm 2 which has quadratic complexity (the crossover happens around 240 words).

Figure 2 compares the conversion of a floating-point approximation of 2/3 with GMP and with our implementation of Algorithm 3, for 1 to 100 words. As noted in Section 4, this is the optimal case for the "scaled remainder tree" algorithm, since no initial division is needed, whereas the classical algorithm requires an initial multiplication. The speedup over GMP decreases from 84% (for one word) to 74% (for 100 words). Our algorithm is faster than GMP until around 2100 words.

Subquadratic Algorithm

For those experiments, the threshold between the quadratic and subquadratic case was k t = 3700, which means that Algorithm 3 outperforms Algorithm 2 up from about 200 words. In Algorithm 3, the GMP mpn_mulmid function was used to compute the middle product up to 2500 words, otherwise the middle product was computed with an FFT algorithm.

Figure 3 compares our implementation of Algorithm 3 with the GMP mpz_get_str function, up to ten million words. Algorithm 3 outperforms GMP up from about 250000 words. Around ten million words, our implementation is about 19% faster than GMP.

Figure 4 compares the conversion of a floating-point approximation of 2/3 with GMP and with our implementation of Algorithm 3, up to 50000 words. The speedup over GMP is around 65% for 250 words and then stabilizes around 50% for more than 2500 words. For ten million words, the speedup over GMP is around 55%.

k- 1 i=0Theorem 3 .

 13 s i b i are integers, the equality follows. Algorithm 1 and Algorithm 2 return the k digits of a in base b.

Fig. 1 .

 1 Fig. 1. Integer conversion: comparison with GMP for small sizes.

Fig. 2 .

 2 Fig. 2. Floating-point conversion: comparison with GMP for small sizes.

Fig. 3 .

 3 Fig. 3. Integer conversion: comparison with GMP for larger sizes.

Fig. 4 .

 4 Fig. 4. Floating-point conversion: comparison with GMP for larger sizes.

ACKNOWLEDGMENTS

Both authors thank Alain Filbois who helped them to optimize the implementation of the quadratic algorithm on modern processors. Paul Zimmermann thanks Petr Filipsky who motivated him to work on this problem, by asking an answer to Exercise 1.35 of [2]. The detailed feedback of the three anonymous referees helped a lot to improve the final version of this paper.