John Ellis

Hongbing Fan

Jeffrey Shallit

The Cycles of the Multiway Perfect Shuffle Permutation †

Keywords: permutation, perfect shuffle, k-way shuffle, cycle decomposition, linear time algorithm

The (k, n)-perfect shuffle, a generalisation of the 2-way perfect shuffle, cuts a deck of kn cards into k equal size decks and interleaves them perfectly with the first card of the last deck at the top, the first card of the second-to-last deck as the second card, and so on. It is formally defined to be the permutation ρ k,n : i → ki (mod kn + 1), i ∈ {1, 2, . . . , kn}. We uncover the cycle structure of the (k, n)-perfect shuffle permutation by a group-theoretic analysis and show how to compute representative elements from its cycles by an algorithm using O(kn) time and O((log kn) 2 ) space. Consequently it is possible to realise the (k, n)-perfect shuffle via an in-place, linear-time algorithm. Algorithms that accomplish this for the 2-way shuffle have already been demonstrated.

Introduction

The (k, n)-perfect shuffle cuts a deck of kn cards into k equal size subdecks and interleaves those subdecks perfectly. After the shuffle, the first card of the last subdeck becomes the first card of the new deck, the first card of the second-to-last subdeck becomes the second card, and so on. See Figure 1. This is a generalisation of the well-known 2-way perfect shuffle. We define the (k, n)-perfect shuffle permutation to be the permutation ρ k,n : i → ki (mod (kn + 1)), i ∈ {1, 2, . . . , kn}.

The perfect shuffle has many interesting mathematical properties and applications in computer science. The group structure of the 2-way perfect shuffle and some applications to network design are given in [START_REF] Diaconis | The mathematics of perfect shuffles[END_REF] and [START_REF] Medvedoff | Groups of perfect shuffles[END_REF]. A family of parallel computer architectures and associated algorithms are based on the 2-way perfect shuffle. See, for example, [START_REF] Stone | Parallel processing with the perfect shuffle[END_REF][START_REF] Batcher | Decomposition of perfect shuffle networks[END_REF][START_REF] Leighton | Introduction to Parallel Algorithms and Architectures[END_REF]. In [START_REF] Ellis | In situ, stable merging by way of the perfect shuffle[END_REF] it is shown that the classic problem of merging two lists in-place, with stability, can be reduced to the problem of accomplishing the 2-way perfect shuffle in-place. It may be that k-way shuffling is applicable to k-way merging. Hence efficient realisations of shuffling permutations could permit efficient simulation of parallel algorithms on sequential machines, and may open up new merging methods. We have in mind the algorithmic problem of permuting, in-place, a list represented by a one-dimensional array of elements indexed by the integers 1 through kn. By "in-place" we mean without the use of substantial extra space over and above that which the list elements already occupy. To be precise, we allow ourselves no more than O((log kn) 2 ) extra bits for program variables and data structures. This definition was originally proposed by Knuth [Knu73, Section 5.5, Exercise 3]. The intention was to permit some fixed number of program variables plus recursion.

Permutations are made up of disjoint cycles and it is easy to move all the elements of one cycle, using just one extra location, by a so-called "cycle leader" algorithm [START_REF] Fich | Permuting in place[END_REF]. The method proceeds by repeatedly making a space in the list, computing the index of the element that belongs in that space and moving that element, and thus creating a new space. For example, to permute ρ 2,3 = (1 2 4)(3 6 5), we can move the elements as indicated in Figure 2. In that figure, the numbers on the arrows define the order in which the moves take place.

If we can easily find an unmoved element with which to start a new cycle when the current cycle terminates, then the entire task becomes easy. This is the case for some commonly used permutations such as reversal and cyclic shifts. In those cases, if the current cycle was started at location i and elements remain to be moved at the end of the current cycle, then it is easy to show that the element at location i + 1 has yet to be moved. The problem with the perfect shuffle is that the cycle structure is more complicated, and it is no longer immediately apparent how to compute the beginning of a new cycle when needed.

We analyse the structure of the generalised perfect shuffle permutation in terms of the size, number and location of its cycles. Then we construct an in-place, O(kn) time procedure that computes a set containing one element from each cycle. A cycle leader algorithm can use this set to realise the perfect shuffle in-place and in time linear in the total number of elements being shuffled.

We call this set of elements a set of seeds (called cycle leaders in [START_REF] Fich | Permuting in place[END_REF]). The seed set is a set of array indices with the following properties:

1. No two seeds are in the same cycle.

Every cycle contains a seed.

The methods in [START_REF] Fich | Permuting in place[END_REF] can be used to compute a seed set for any permutation of n elements in time O(n log n) and using O((log n) 2 ) bits. We show how to compute a seed set using O((log kn) 2 ) space and O(kn) time. A linear time and in-place algorithm for the 2-way perfect shuffle was given by Ellis and Markov [START_REF] Ellis | In situ, stable merging by way of the perfect shuffle[END_REF]. That method does not compute a seed set. An alternative method [START_REF] Ellis | Computing the cycles in the perfect shuffle permutation[END_REF], which does compute a seed set, uses about half the number of moves at the expense of more arithmetic, as compared to the first method. The method described in this paper is a generalisation of this latter method. We give a characterisation of the cycles of ρ k,n in group theory terms and we present a linear time, in-place algorithm for computing a seed set.

The Algebraic Structure of the Cycles of ρ k,n

We use some basic concepts from number theory and group theory. Most of them can be found in, for example, [START_REF] Jones | Theory of Numbers[END_REF][START_REF] Agnew | Explorations in Number Theory[END_REF][START_REF] Herstein | Topics in Algebra[END_REF][START_REF] Bach | Algorithmic Number Theory[END_REF][START_REF] Baker | A concise introduction to the theory of numbers[END_REF]. We are concerned with the ring of integers modulo n, where m (mod n) denotes the integer that is congruent to m and contained in {0, 1, . . . , n -1}. The ring of integers modulo n, denoted by Z/(n), is the set {0, 1, . . . , n -1} together with operations + and • defined by

a + b = (a + b) (mod n), a • b = ab (mod n).
Clearly, the zero element and unit element of Z/(n) are 0 and 1 respectively. For convenience, we write ab instead of a • b, and x instead of x (mod n) when x is assumed to be an element of Z/(n). The group of units of Z/(n) is denoted by (Z/(n)) * . (Z/(n)) * = {a ∈ Z/(n) : gcd(a, n) = 1}, where gcd denotes greatest common divisor. The group (Z/(n)) * has ϕ(n) elements, where ϕ is the Euler ϕ function. When n = 2, 4, p l or 2p l (where p is an odd prime and l ≥ 1), there exists a primitive root of n, so that (Z/(n)) * is cyclic and (Z/(n)) * is isomorphic to the additive group Z/(ϕ(n)).

Now we consider the cycle structure of the permutation ρ n,k . Let C be a cycle of ρ k,n and a be an element of C. Let m = kn + 1. By the definition of ρ k,n , we know that C = (a, ka, k 2 a, . . . , k r-1 a) where r is the least positive integer with k r a ≡ a (mod m). Let g = gcd(a, m) and d = m g . Then d = 1 and k r a g ≡ a g (mod d) and gcd(k,

d) = gcd( a g , d) = 1. This implies that k, a g ∈ (Z/(d)) * and that {1, k, . . . , k r-1 } = k d is a subgroup of (Z/(d)) * generated by k and { a g , k a g , . . . , k r-1 a g } = {1, k, . . . , k r-1 } a g is a coset of k d in (Z/(d)) * . Hence C is formed from the set k d a g m d = {a, ka, k 2 a, . . . , k r-1 a}. That is, C is formed from m d times a coset of k d in (Z/(d)) * .
Conversely Theorem 1 The r-tuple (a 0 , a 1 , . . . , a r-1 ) is a cycle of the (k, n)-perfect shuffle permutation if and only if there is a nontrivial divisor d of kn + 1 and an a ∈ (Z/(d)) * such that r is the least positive integer such that k r ≡ 1 (mod d) and a i = a(kn+1) d k i mod (kn + 1) for i = 0, 1, . . . , r -1.

Example. Let k = 3 and n = 17. Then kn + 1 = 52, and the nontrivial divisors of 52 are 2, 4, 13, 26, 52. We then find the following cycles (not all values of a are shown):

d a

The Computation of a Seed Set

In what remains we will use "divisor" to mean "nontrivial divisor". To compute a seed set it is sufficient, by Theorem 1, to compute a complete set of coset representatives of k d in (Z/(d)) * for each divisor d of kn + 1. We can speed up this computation by using the decomposition properties of integers and abelian groups.

Let d be a divisor of kn+1 and let the prime factorisation of d be q u 1 1 q u 2 2 • • • q u s s where q 1 > q 2 > • • • > q s . By the Chinese Remainder Theorem (see for example [BS96, Theorem 5.5.4]), we know that the mapping

f (x) = ( f 1 (x), f 2 (x), . . . , f s (x)), where f i (x) = x mod q u i i (1)
is an isomorphism from the ring Z/(d) to the ring Z/(q u 1 1 ) ⊕ Z/(q u 2 2 ) ⊕ • • • ⊕ Z/(q u s s ). Therefore the units of the two rings correspond to each other, so that the restriction of f on (Z/(d)) * forms an isomorphism from the group (Z/(d)) * to the group

(Z/(q u 1 1 ) ⊕ Z/(q u 2 2 ) ⊕ • • • ⊕ Z/(q u s s )) * = (Z/(q u 1 1 )) * × (Z/(q u 2 2 )) * × • • • × (Z/(q u s s )) *
([BS96, Lemma 5.6.1]). Furthermore, f induces an isomorphism on the group quotients,

f * : (Z/(d)) * / k d → (Z/(q u 1 1 )) * × (Z/(q u 2 2 )) * × • • • × (Z/(q u s s )) * / ( f 1 (k), f 2 (k), . . . , f s (k))
where

( f 1 (k), f 2 (k), . . . , f s (k)) denotes the subgroup of (Z/(q u 1 1 )) * × (Z/(q u 2 2 )) * × • • • × (Z/(q u s s )) * gen- erated by ( f 1 (k), f 2 (k), . . . , f s (k)).
If q i is an odd prime, or q i = 2 and u i ≤ 2, then we deduce from our earlier remarks that (Z/(q u i i )) * is a cyclic group. Let g i be a primitive root of q u i i and

w i = ind g i f i (k) (mod q u i i ). Since w i is the least positive integer such that g w i i = f i (k) (mod q u i i ) and f i (k) = k mod q u i i , w i is also the index of k (mod q u i i ). Therefore, (Z/(q u i i )) * = g i ∼ = Z/(ϕ(q u i i )) with the isomorphism φ(g x i ) = x. Clearly, φ( f i (k)) = w i . If q i =
2 and u i ≥ 3, then i = s. We know that 2 u s does not have a primitive root, but the order of 5 (mod 2 u s ) is 2 u s -2 , and the set

{(-1) v 5 u : u = 0, 1, . . . , 2 u s -2 -1, v = 0, 1}
forms a reduced set of residues modulo 2 u s . See for example [START_REF] Baker | A concise introduction to the theory of numbers[END_REF], page 25. Therefore, for any odd integer x, there exists a unique pair (w(x), w ′ (x)) such that w(x) ∈ {0, 1, . . . , 2 u s -2 -1} , w ′ (x) ∈ {0, 1} and x ≡ (-1) w ′ (x) 5 w(x) (mod 2 u s ). Hence (Z/(2 u s )) * ∼ = Z/(2 u s -2 ) × Z/(2) with isomorphism φ(x) = (w(x), w ′ (x)). Let w s , w ′ s be such that (-1) w ′ s 5 w s ≡ f s (k) ≡ k (mod 2 u s ). Suppose that q s = 2 or q s = 2 and u s ≤ 2. Then the mapping h((g x 2 1 , g x 2 2 , . . . ,

g x s s )) = (x 1 , x 2 , . . . , x s ) (2)
is an isomorphism from the group

(Z/(q u 1 1 )) * × (Z/(q u 2 2 )) * × • • • × (Z/(q u s s )) * to the group Z/(ϕ(q u 1 1 )) × Z/(ϕ(q u 2 2 )) × • • • × Z/(ϕ(q u s s )) and h maps ( f 1 (k), f 2 (k), . . . , f s (k)) = (g w 1
1 , q w 2 2 , . . . , g w s s ) to (w 1 , w 2 , . . . , w s ). Therefore, h induces an isomorphism

h * : (Z/(q u 1 1 )) * × (Z/(q u 2 2 )) * × • • • × (Z/(q u s s )) * / ( f 1 (k), f 2 (k), . . . , f s (k)) ∼ = (Z/(ϕ(q u 1 1 )) × Z/(ϕ(q u 2 2 )) × • • • × Z/(ϕ(q u s s )))/ (w 1 , w 2 , . . . , w s ) . (3)
Hence, if we take a complete set of coset representatives of

(w 1 , w 2 , . . . , w s ) in Z/(ϕ(q u 1 1 )) × Z/(ϕ(q u 2 2 )) × • • • × Z/(ϕ(q u s s )),
transform it first by h -1 and then by f -1 , we will obtain a set of seeds corresponding to d. Alternatively, suppose that q s = 2 and u s ≥ 3. Then q i , i = 1, . . . , s -1 are odd primes and the mapping

h ′ ((g x 1 1 , . . . , g x s-1 s-1 , (-1) v 5 u )) = (x 1 , . . . , x s-1 , u, v) (4)
is an isomorphism from the group

(Z/(p u 1 1 )) * × • • • × (Z/(p u s-1 s-1 )) * × (Z/(2 u s )) * to the group Z/(ϕ(q u 1 1 )) × • • • × Z/(ϕ(q u s-1 s-1 )) × Z/(2 u s -2 ) × Z/(2) and h ′ (( f 1 (k), . . . , f s-1 (k), f s (k))) = h ′ ((g w 1 1 , . . . , g w s-1 s-1 , (-1) w ′ s 5 w s )) = (w 1 , . . . , w s-1 , w s , w ′ s ).
Therefore, h ′ induces an isomorphism

h ′ * : (Z/(q u 1 1 )) * × • • • × (Z/(q u s-1 s-1 )) * × (Z/(2 u s )) * / ( f 1 (k), f 2 (k), . . . , f s (k)) ∼ = (Z/(ϕ(q u 1 1 )) × • • • × Z/(ϕ(q u s-1 s-1 )) × Z/(2 u s -2 ) × Z/(2))/ (w 1 , . . . , w s-1 , w s , w ′ s ) (5)
Hence, again, if we take a complete set of coset representatives of the above groups, first transform it by h ′ -1 and then by f -1 , we will obtain a subset of a seed set corresponding to d.

The computation of the complete coset representatives of the group quotients can be accomplished using the following theorem, which is of independent interest. Theorem 2 Let s and t 1 ,t 2 , . . . ,t s be positive integers and

G = Z/(t 1 ) × Z/(t 2 ) × • • • × Z/(t s ) (6)
be an abelian group with (w 1 , w 2 , . . . , w s ) ∈ G. Let lcm denote the least common multiple and let a i , b i , c i be defined by the following relations:

a i = gcd(w i ,t i ), 1 ≤ i ≤ s; b 0 = 1; (7) b i = t i /a i , 1 ≤ i ≤ s; c i = a i gcd(lcm(b 0 , b 1 , b 2 , . . . , b i-1 ), b i ), 1 ≤ i ≤ s.
Then the following statements hold:

(i) | (w 1 , w 2 , . . . , w s ) | = lcm(b 1 , . . . , b s-1 , b s ); (ii) (c 1 , c 2 , . . .

, c s ) is the lexicographically least non-zero element and generator of the subgroup

(w 1 , w 2 , . . . , w s ) ;

(iii) {(e 1 , e 2 , . . . , e s ) : 0 ≤ e i < c i } is a complete set of coset representatives of (w 1 , w 2 , . . . , w s ) in G.

Proof

We first prove (i) and (ii) by induction on s, the number of groups in the product (6). If s = 1, then b 1 = t 1 /a 1 and c 1 = a 1 gcd(1, b 1 ) = a 1 = gcd(w 1 ,t 1 ). Since 0 ≤ c 1 ≤ t 1 and w 1 < t 1 and xw 1 + yt 1 = c 1 for some integers x and y, it follows that c 1 = xw 1 mod t 1 . Hence c 1 ∈ w 1 and c 1 ⊆ w 1 . However, w 1 = z gcd(w 1 ,t 1 ) = zc 1 implies that w 1 ⊆ c 1 . Hence c 1 = w 1 . For any t, 1 ≤ t < c 1 , since gcd(w 1 ,t 1 ) = c 1 and c 1 ∤ t, the congruence w 1 x ≡ t (mod t 1 ) has no solution, so that t ∈ w 1 . Therefore c 1 is the lexicographically least non-zero element of w 1 . Hence

w 1 = {xc 1 : 0 ≤ x < t 1 /c 1 }. It follows that | w 1 | = | c 1 | = t 1 /c 1 = b 1 = lcm(b 1
). Thus (i) and (ii) are true when s = 1.

Suppose now that (i) and (ii) are true when 1 ≤ s ≤ j -1. We prove that they remain true for s = j. Clearly, the group (w 1 , w 2 , . . . , w j ) is a subgroup of (w 1 , w 2 , . . . , w j-1 ) × w j . By the induction hypothesis, | (w 1 , w 2 , . . . , This implies that t(w 1 , w 2 , . . . , w j ) = (w 1 , w 2 , . . . , w j ). Therefore, | (w 1 , w 2 , . . . , w j ) | = lcm(b 1 , b 2 , . . . , b j ), and so (i) is true. Let (c ′ 1 , c ′ 2 , . . . , c ′ j ) be the lexicographically least non-zero element in (w 1 , w 2 , . . . , w j ) . Then (c ′ 1 , c ′ 2 , . . . , c ′ j-1 ) is an element of (w 1 , w 2 , . . . , w j-1 ) . By the induction hypothesis, (c 1 , c 2 , . . . , c j-1 ) is the lexicographically least element of w 1 , w 2 , . . . , w j-1 , so that (c ′ 1 , c ′ 2 , . . . , c ′ j-1 ) ≥ (c 1 , c 2 , . . . , c j-1 ). However, (c 1 , c 2 , . . . , c j-1 ) ∈ (w 1 , w 2 , . . . , w j-1 ) . Hence there exists an integer x such that x(w 1 , w 2 , . . . , w j-1 ) = (c 1 , c 2 , . . . , c j-1 ). But c j-1 ). It remains to show that c ′ j = c j . Consider the mapping f : (w 1 , w 2 , . . . , w j-1 , w j ) → w j such that f (x 1 , x 2 , . . . , x j-1 , x j ) = x j . Then f is a homomorphism. The kernel of f is (w 1 , w 2 , . . . , w j-1 , 0) and (w 1 , w 2 , . . . , w j-1 , 0) ∼ = (w 1 , w 2 , . . . , w j-1 ) . Since f is a homomorphism, f ( (w 1 , w 2 , . . . , w j-1 , w j ) ) is a subgroup of w j and isomorphic to the group quotient (w 1 , w 2 , . . . , w j-1 , w j ) / (w 1 , w 2 , . . . ,

x(w 1 , w 2 , . . . , w j-1 , w j ) = (c 1 , c 2 , . . . , c j-1 , xw j ) ≥ (c ′ 1 , c ′ 2 , . . . , c ′ j-1 , c ′ j ). Hence (c ′ 1 , c ′ 2 , . . . , c ′ j-1 ) ≤ (c 1 , c 2 , . . . , c j-1 ). It follows that (c ′ 1 , c ′ 2 , . . . , c ′ j-1 ) = (c 1 , c 2 , . . . ,
w j-1 , 0) . Therefore | f ( (w 1 , w 2 , . . . , w j-1 , w j ) )| = | (w 1 , w 2 , . . . , w j ) )/ (w 1 , w 2 , . . . , w j-1 , 0 | = lcm(b 1 , b 2 , . . . , b j ) lcm(b 1 , b 2 , . . . , b j-1 ) . (8)
Since (ii) is true for a product of a single group by the initial case, a j is a lexicographically least element of w j in Z/(t j ) and a j = w j . Therefore the least element of f ( (w 1 , w 2 , . . . , w j ) ) in a j is

a j b j lcm(b 1 ,b 2 ,...,b j ) lcm(b 1 ,b 2 ,...,b j-1 ) = a j b j lcm(b 1 , b 2 , . . . , b j-1 ) lcm(b 1 , b 2 , . . . , b j-1 , b j ) = a j gcd(lcm(b 1 , b 2 , . . . , b j-1 ), b j ) = c j .
But c j is also a generator of f ( (w 1 , w 2 , . . . , w j ) ) in a j and b j-1 ) .

| c j | = lcm(b 1 , b 2 , . . . , b j ) lcm(b 1 , b 2 , . . . ,
This implies that c ′ j = f (c ′ 1 , c ′ 2 , . . . , c ′ j ) ≥ c j . Since the image in f of any element in the coset (w 1 , w 2 , . . . , w j-1 , 0) + (0, . . . , 0, c j ) is (0, . . . , 0, c j ), it follows that (c 1 , c 2 , • • • , c j-1 , c j ) ∈ (w 1 , w 2 , • • • , w j ) . Then, by the choice of (c ′ 1 , c ′ 2 , . . . , c ′ j ), (c ′ 1 , c ′ 2 , . . . , c ′ j-1 , c ′ j ) ≤ (c 1 , c 2 , . . . , c j-1 , c j ). This implies that c ′ j ≤ c j . Therefore, c ′ j = c j and (c 1 , c 2 , • • • , c j )
is the lexicographically least non-zero element of (w 1 , w 2 , . . . , w j ) .

By the induction hypothesis, (c 1 , c 2 , . . . , c j-1 ) is a generator of the group (w 1 , w 2 , . . . , w j-1 ) and

| (c 1 , c 2 , . . . , c j-1 ) | = lcm(b 1 , b 2 , . . . , b j-1 ). Hence we have | (c 1 , c 2 , . . . , c j-1 , c j ) | = lcm(lcm(b 1 , b 2 , . . . , b j-1 ), | c j |) = lcm(lcm(b 1 , b 2 , . . . , b j-1 ), lcm(b 1 , b 2 , . . . , b j ) lcm(b 1 , b 2 , . . . , b j-1 ) ) = lcm(b 1 , b 2 , . . . , b j ).
This implies that (c 1 , c 2 , . . . , c j-1 , c j ) = (w 1 , w 2 , . . . , w j-1 , w j ) . Hence (i) and (ii) are true. Finally, we prove (iii). Let E = {(e 1 , e 2 , . . . , e s ) : 0 ≤ e i < c i }. Let e, e ′ be distinct elements of E and, without loss of generality, assume that e < e ′ . Then e ′e < (c 1 , c 2 , . . . , c s ) and so e ′e ∈ (w 1 , w 2 , . . . , w s ) . This implies that e and e ′ are not in the same coset of (w 1 , w 2 , . . . , w s ) in Z/(t 1 ) × Z/(t 2 )ו • •×Z/(t s ). However, the number of cosets of (w 1 , w 2 , . . . , w s ) in Z/(t 1 )×Z/(t 2 )×

• • •×Z/(t s ) is t 1 t 2 • • •t s /lcm(b 1 , b 2 , .
. . , b s ), and we have

|E| = c 1 • • • c s = a 1 gcd(lcm(b 0 ), b 1 ) • • • a s gcd(lcm(b 1 , . . . , b s-1 ), b s ) = (a 1 • • • a s ) gcd(lcm(b 0 ), b 1 ) • • • gcd(lcm(b 1 , b 2 , . . . , b s-1 ), b s ) = (a 1 • • • a s )(b 1 • • • b s ) lcm(b 1 , . . . , b s ) = t 1 • • •t s lcm(b 1 , . . . , b s )
.

Therefore E is a complete set of coset representatives of (w 1 , w 2 , . . . , w s ) in G. ✷

The Algorithm and Complexity Analysis

In this section, we present an algorithm based on the principles described in the previous section. The analysis of the time and space complexity of the algorithm follows that presented in [START_REF] Ellis | Computing the cycles in the perfect shuffle permutation[END_REF] for the 2way shuffle.

The Seed Set Generator for the (k, n)-Perfect Shuffle Permutation

Step 1 Let m = kn + 1 and S = / 0.

Step 2 Compute the prime factorisation of m, say m = p e 1 1 p e 2 2 • • • p e r r where

p 1 ≥ p 2 ≥ • • • ≥ p r .
Step 3 For each prime factor p i , compute a primitive root of p i and call it g i,1 . If e i ≥ 2, compute a primitive root of p 2 i and call it g i,2 .

Step 4 For each prime factors p i , compute w i,1 := ind g i,1 k (mod p i ). If e i ≥ 2, compute w i,2 := ind g i,2 2 (mod p 2 i ).

Step 5 Compute each divisor of m and its prime factorisation. As a divisor d is generated, carry out steps 5.1 to 5.3.

Step 5.1 Let the prime factorisation of d be q u 1 1 q u 2 2 • • • q u s s where q 1 ≥ q 2 ≥ • • • ≥ q s . For each prime factor q i of d, suppose j is the index such that q i = p j . Define g i as follows: if u i = 1 then g i = g j,1 , if p j = 2 then g i = g j,2 , if p j = 2 and u i ≥ 2 then g i = g j,2 , otherwise g i = 5. Define w i = w j,1 if u i = 1 or w i = w j,2 if u i = 2. Otherwise, if p i = 2, compute w i = ind g i j (mod q u i i ) or if p i = 2 and u i ≥ 3, compute and define w i , w ′ i such that (-1) w ′ i 5 w i ≡ j (mod 2 u i ).

Step 5.2 Set b 0 = 1. Compute c i for i = 1, 2, . . . , s by

t i = 2 u i -2 , if p i = 2, u i ≥ 3; ϕ(q u i i ), otherwise; a i = gcd(w i ,t i ), b i = t i /a i , c i = a i gcd(lcm(b 0 , b 1 , b 2 , . . . , b i-1 ), b i ) (9)
Step 5.3 If q s = 2, or q s = 2 and u s ≤ 2, for every integer vector (k 1 , k 2 , . . . , k s ) with 0 ≤ k i < c i , solve the system of congruences

         x ≡ g k 1 1 (mod q u 1 1 ) x ≡ g k 2 2 (mod q u 2 2 ) . . . x ≡ g k s s (mod q u s s ) (10)
Obtain a solution x in {1, 2, . . . , d} and add xm d to S.

Otherwise, for every integer vector (k 1 , k 2 , . . . , k s , k ′ s ) with 0 ≤ k i < c i and k ′ s = 0, 1, solve the system of congruences

               x ≡ g k 1 1 (mod q u 1 1 ) x ≡ g k 2 2 (mod q u 2 2 ) . . . x ≡ g k s-1 s-1 (mod q u s-1 s-1 ) x ≡ (-1) k ′ s 5 k s (mod 2 u s ) (11)
obtain a solution x in {1, 2, . . . , d} and add xm d to S.

Step 6 Output S.

Proof of Correctness: If d is not divisible by 2 u i with u i ≥ 3, by Theorem 2 and equation (10), we know that in step 5.3, each vector (k 1 , k 2 , . . . , k s ) with 0 ≤ k i < c i is a coset representative of the quotient

(Z/(ϕ(q u 1 1 )) × Z/(ϕ(q u 2 2 )) × • • • × Z/(ϕ(q u s s )
))/ (w 1 , w 2 , . . . , w s ) Then the solution of equation ( 10)

x = f -1 (h -1 ((k 1 , k 2 , . . . , k s ))) = f -1 ((g k 1 1 , g k 2 2 , . . . , g k s s
)) where f and h are defined by forms (1) and (2) respectively, corresponds to a coset representative of quotient (Z/(d)) * / k d and therefore, xm d corresponds to a seed of a cycle by Theorem 1. If d is divisible by 2 u s , u s ≥ 3, then by Theorem 2, each vector (k 1 , . . . , k s-1 , k s , k ′ s ) with 0 ≤ k i < c i and k ′ s = 0, 1 corresponds to a coset representative (k 1 , . . . , k s-1 , k s , k ′ s ) of (w 1 , . . . , w s-1 , w s , w ′ s ) in Z/(t 1 ) × • • • × Z/(t s-1 ) × Z/(t s ) × Z/(2). Hence it corresponds to a seed xm d of a cycle, by Theorem 1, since x = f -1 h ′ -1 ((k 1 , . . . , k s-1 , k s , k ′ s )) where x is the solution of equation ( 11) and f and h ′ are defined by the forms (1) and (4) respectively. ✷

The algorithm just given is a generalisation of that presented in [START_REF] Ellis | Computing the cycles in the perfect shuffle permutation[END_REF]. There it was shown, using some known results regarding the number and distribution of primitive roots, that the entire computation of a seed set for the 2-way shuffle can be accomplished using O(n) arithmetic operations.

The difference between the algorithm for the k-way shuffle and that for the 2-way shuffle is in the computation of the indices. We can use the same method for computing ind g i 2 to compute ind g i k. We can solve the congruence (-1) w ′ i 5 w i ≡ k (mod 2 u i ) using the usual Hensel lifting technique (see for example [START_REF] Von | Modern Computer Algebra[END_REF]) in O(u 3 i ) = O(kn) bit operations. These differences do not increase the overall time complexity of the algorithm. Therefore the more general algorithm can also be realised in time O(kn).

The extra space needed for the variable used by the algorithm is the same as that in [START_REF] Ellis | Computing the cycles in the perfect shuffle permutation[END_REF], so the space complexity is also O((log kn) 2 ).

We conclude that a seed set for the (k, n)-perfect shuffle permutation can be computed in-place and in time linear in the total number of elements being shuffled. It follows that the (k, n)-perfect shuffle permutation can be realised in-place and in linear time by way of a cycle leader algorithm as described in the introduction. We leave as open questions whether or not this result can be used to generalise the 2-way merge algorithm in [START_REF] Ellis | In situ, stable merging by way of the perfect shuffle[END_REF] to k-way merging and whether or not the space requirement can be further reduced.

Fig. 1 :

 1 Fig. 1: The (3, 4)-perfect shuffle illustrated

Fig. 2 :

 2 Fig. 2: Realising the Perfect Shuffle

  , for any nontrivial divisor d of m (that is, d|m and d = 1), let k d be the subgroup of (Z/(d)) * generated by k, and let r = | k d | and a ∈ (Z/(d)) * . Then, by definition, r is the least positive integer such that k r ≡ 1 (mod d) and k r a ≡ a (mod d) and k r am d ≡ am d (mod d m d ) ≡ am d (mod m). Therefore, ( am d , k am d , . . . , k r-1 am d ) is a cycle of the (k, n)-perfect shuffle permutation. In summary, we have the following theorem regarding the cycle structure of the (n, k)-perfect shuffle permutation:

  w j-1 ) | = lcm(b 1 , b 2 , . . . , b j-1 ) and | w j | = b j . Then, lcm(b 1 , b 2 , . . . , b j-1 )(w 1 , w 2 , . . . , w j-1 ) = (w 1 , w 2 , . . . , w j-1 ) and b j w j = w j . Since lcm(lcm(b 1 , b 2 , . . . , b j-1 ), b j ) = lcm(b 1 , b 2 , . . . , b j ) and is a multiple of both lcm(b 1 , b 2 , . . . , b j-1 ) and b j , it follows that lcm(b 1 , b 2 , . . . , b j )(w 1 , w 2 , . . . , w j ) = (w 1 , w 2 , . . . , w j ). Since lcm(lcm(b 1 , b 2 , . . . , b j-1 ), b j ) is the least common multiple of lcm(b 1 , b 2 , . . . , b j-1 ) and b j , then for any 0 ≤ t < lcm(b 1 , b 2 , . . . , b j ), either 0 ≤ t mod lcm(b 1 , b 2 , . . . , b j-1 ) < lcm(b 1 , b 2 , . . . , b j-1 ) or 0 ≤ t mod b j < b j .

† This work was supported by the Natural Sciences and Engineering Research Council of Canada 1365-8050


Frédéric Saubion
email: frederic.saubion@univ-angers.fr

Igor Stéphan
email: igor.stephan@univ-angers.fr

A Unified Framework to Compute over Tree Synchronized Grammars and Primal Grammars

Keywords: Tree Grammars, Proof Systems, Prolog Implementation

Tree languages are powerful tools for the representation and schematization of infinite sets of terms for various purposes (unification theory, verification and specification ...). In order to extend the regular tree language framework, more complex formalisms have been developed. In this paper, we focus on Tree Synchronized Grammars and Primal Grammars which introduce specific control structures to represent non regular sets of terms. We propose a common unified framework in order to achieve the membership test for these particular languages. Thanks to a proof system, we provide a full operational framework, that allows us to transform tree grammars into Prolog programs (as it already exists for word grammars with DCG) whose goal is to recognize terms of the corresponding language.

Introduction

Tree languages [START_REF] Comon | Tree Automata Techniques and Applications[END_REF][START_REF] Gecseg | Handbook of Formal Languages, volume 3, chapter Tree Languages[END_REF] have been extensively studied and have many applications in various areas such as term rewriting, term schematization, specification and verification ... Languages can be handled either from the generation point of view (i.e. grammars) or from the recognition point of view (i.e. automata). Regular tree languages [START_REF] Comon | Tree Automata Techniques and Applications[END_REF][START_REF] Gecseg | Handbook of Formal Languages, volume 3, chapter Tree Languages[END_REF] are very close to regular word grammar with tree (ie terms † ) as basic objects. They have nice closure properties (concerning complementation, union and intersection) and the membership test and the emptiness test are decidable. Moreover they can be defined using a notion of finite automata which can be easily used to test the membership of a term to a given language. Therefore, from a practical point of view, tree automata appear to be easily implementable tools for recognition. But, these notions are not sufficient to describe more complex sets of terms (non regular tree languages). In this paper, we focus on two particular non regular classes of tree languages defined by their associated notion of tree grammars: Tree Synchronized Grammars and Primal Grammars. The purpose of this paper is to define a uniform and operational framework to describe and implement a membership test procedure for these languages.

Tree Synchronized Grammars (TSG) [START_REF] Limet | E-Unification by Means of Tree Tuple Synchronized Grammars[END_REF] and Primal Grammars (PG) [START_REF] Hermann | Unification of infinite sets of terms schematized by primal grammars[END_REF] are issued from the E-unification framework. E-unification [START_REF] Plotkin | Building-in equational theories[END_REF] is known to be undecidable in general, but, as explained in [START_REF] Limet | Primal Grammars for R-unification[END_REF], some decidable classes can be characterized by using such tree languages. Due to their specific definitions introducing control in the derivation process, a notion of automata can not be easily derived for these two classes of tree languages. Their expressive power can be highlighted by the two following simple examples.

Example 1 (TSG)

We want to define the language corresponding to { f (s n (z), s 2n (z)) | n ∈ N} which is obviously not a regular language. The language description problem lies in the fact that, informally, each time a function symbol s is produced in the first argument of f one has to produce two in the second argument. In fact, the growth of the first argument has to be synchronized with the second. Tree Synchronized Grammars take this control into account by allowing packs of synchronized production rules instead of usual single grammar productions rules.

Example 2 (PG) In this second example, we want to describe the language of all the integer lists [n, . . . , 0]. Integer are represented with z (for the zero integer) and successor function s and lists are built thanks to the binary constructor * and the empty list ⊥ (i.e. the list [2, 1, 0] is obtained as * (s(s(z)), * (s(z), * (z, ⊥))). This language is also not regular.

The main problem here is the relation between the different arguments of the list you are constructing. Once you have generated an element s n (z), next element of the list must be s n+1 (z). It appears that you have to count the depth of successive argument. By introducing counters variables in the production rules, Primal Grammars are able to handle this language. One has to remark that the language of the first example cannot be generated using PG while the language of the second example cannot be described by a TSG. Due to these two specific control mechanisms (synchronization and counter variables), the standard notion of automata does not appear clearly. Inspired by the implementation of Definite Clause Grammars [START_REF] Cohen | Parsing and compiling using prolog[END_REF] that allows to write word grammars as Horn clauses in a Prolog environment, our aim is to propose a similar approach for these particular tree languages. The key idea is to define a proof framework to describe the behavior of tree grammars and therefore to provide a proof theoretical semantics for grammar derivations. In this context, we change from syntactic generation of trees to logical deduction (i.e. productions rules are translated into logical formulas and grammar derivations into logical inferences). Then, the membership test, for a language described by a grammar, just consists in proving a particular formula in a sequent calculus using a proof system. This approach provides a uniform framework for the definition and use of both type of grammars. The method can be briefly described as follows; Production rules are translated into logical formulas built over linear logic syntax [START_REF] Girard | Linear Logic[END_REF] to handle the problem of synchronization (this idea was already investigated in [START_REF] De Groote | A Note on Kobayashi's and Yonezawa's "Asynchronous Communication Model Based on Linear Logic[END_REF]. Then, a sequent calculus proof system, inspired by the proof system of D. Miller [START_REF] Miller | A Multiple-Conclusion Meta-Logic[END_REF], allows us to translate derivations into proof searches. The same job can be adapted for Primal Grammars. The equivalence between the notion of grammar computation and our notion of proof is established by a correctness and completeness result. The last part of our work consists in refining this initial proof system in order to introduce a notion of strategy in the proof search and thus to get a goal directed procedure. At this step, both transformation function and logical inference system can be easily translated into Prolog Horn clauses. Of course, it should be noticed that our system also works for Regular Tree Languages, since they are included in TSG. Note that an alternative algorithm has been proposed for the membership test of a TTSG in [START_REF] Gouranton | Synchronized Tree Languages Revisited and New Applications[END_REF]. This paper is an extension of the previous work [START_REF] Saubion | On Implementation of Tree Synchronized Languages[END_REF] and is organized as follows. Section 2 presents basic definitions of Tree Synchronized Grammars, Primal Grammars and proof systems. Section 3 described how the different formalism can be translated into linear logic formulas. The proof system is defined and refined in Section 4. Section 5 is the implementation issue of our work and we conclude in Section 6.

Preliminaries

In this paper, we recall here some notions about tree grammars and linear logic proof systems. We refer the reader to [START_REF] Comon | Tree Automata Techniques and Applications[END_REF][START_REF] Gecseg | Handbook of Formal Languages, volume 3, chapter Tree Languages[END_REF][START_REF] Girard | Linear logic, its syntax and semantics[END_REF][START_REF] Girard | Linear Logic[END_REF][START_REF] Limet | E-Unification by Means of Tree Tuple Synchronized Grammars[END_REF][START_REF] Miller | A Multiple-Conclusion Meta-Logic[END_REF] for more details. We first introduce the two specific grammar formalisms we deal with in this paper. The original formalisms have been adapted to unify and simplify the presentation.

Tree Synchronized Grammars

Let L be a finite set of symbols (a signature), T (L) denotes the first-order algebra of ground terms over L. L is partitioned in two parts: the set F of terminal symbols, and the set N of non terminal symbols. Upper-case letters denote elements of N . t|u denotes the subterm of t at occurrence u and t[u ← v] denotes the term obtained by replacing in t the subterm t|u by v. t [v] denotes a term containing a subterm v at a particular occurrence and O(t) denotes the set of occurrences in t. C(X 1 , ..., X n ) denotes a term with occurrences: {1...n} such that C(X 1 , ..., X n )|i = X i . C will be called a context. We first define the notion of productions for TSG. We require that F ∩ N = / 0 and that each element of F ∪ N has a fixed arity. We refer the reader to [START_REF] Dershowitz | Rewrite Systems, volume B[END_REF] for more details on these basic notions.

Definition 1 (Productions)

A production is a rule of the form X ⇒ t where X ∈ N and t ∈ T (L) . A pack of productions is a set of productions denoted {X 1 ⇒ t 1 , . . . , X n ⇒ t n }.

• When the pack is a singleton of the form We can then define the notion of TSG.

{X 1 ⇒ C(Y 1 , . . . ,Y n )}

Definition 2 (TSG)

A TSG is defined by a 4-tuple (F , N , PP, T I) where

• F is the set of terminals,
• N is the finite set of non terminals,

• PP is a finite set of packs of productions,

• T I is the axiom of the TSG denoted (I, #) where I is a non terminal and # a new symbol added to the signature.

Note that, the axiom is a pair due to the control of synchronizations. Basically, counters are associated to non terminal symbols to ensure the integrity of the application of synchronized productions.

Back to example 1, we wanted to define the language corresponding to { f (s n (z), s 2n (z)) | n ∈ N}. The corresponding TSG consists of the following production rules:

R 0 : I ⇒ f (X,Y ) R 1 : X ⇒ z R 2 : Y ⇒ z P 1 : {R 3 : X ⇒ s(X), R 4 : Y ⇒ s(s(Y ))}
where X,Y are non terminal symbols and f , s, z terminal symbols. P 1 : {R 3 , R 4 } denotes that, using the pack of production P 1 , R 3 and R 4 have to be applied at the same time (synchronization).

Definition 3 (Computations of a TSG)

The set of computations of a TSG Gr = (F , N , PP, T I), denoted Comp(Gr), is the smallest set defined by:

• T I is in Comp(Gr), • if t is in Comp(Gr), t| u = (X, c) and the free production X ⇒ C(Y 1 , . . . ,Y n ) is in PP then t[u ← C((Y 1 , c), . . . , (Y n , c))] is in Comp(Gr),
• if t is in Comp(Gr) and there exists n pairwise different occurrences u 1 , . . . , u n of t such that ∀i ∈ [1, n] t| u i = (X i , c i ) and c i = a and the pack of productions

{X 1 ⇒ Y 1 , . . . , X n ⇒ Y n } ∈ PP, then t[u 1 ← (Y 1 , b)] . . . [u n ← (Y n , b)] (where b is a new symbol) is in Comp(Gr).
The symbol ⇒ denoting also the above two deduction steps, a derivation of Gr is a sequence of computations T I ⇒ t 1 ⇒ . . . ⇒ t n .

Always following Example 1, one possible derivation of this grammar is thus (where a is a new symbol):

(I, #) ⇒ R 0 f ((X, #), (Y, #)) ⇒ P 1 f (s((X, a)), s(s((Y, a)))) ⇒ R 1 f (s(z), s(s(Y, a))) ⇒ R 2 f (s(z), s(s(z)))
As mentioned in the introduction, counters are introduced to control the application of the synchronized production rules. The previous definition imposes that only non terminals having the same control symbol can be used in a synchronized production. It should be noticed that TSG were originally defined using tuple of counters. Here, as we already did, concerning tuples of terms in the definition of the axiom, we consider a single counter to control synchronization in order to simplify the presentation of the basic concepts. The second step of this derivation clearly illustrates the notion of synchronized production rules.

Definition 4 (Recognized Language)

The language recognized by a TSG Gr, denoted Rec(Gr), is the set of trees composed of terminal symbols Comp(Gr) ∩ T (F ).

Primal Grammars

In this section, we recall definitions related to primal grammars which have been introduced by M. Hermann and R. Galbavý in [START_REF] Hermann | Unification of infinite sets of terms schematized by primal grammars[END_REF]. To avoid too long developments, some notations have been modified to fit ours. More details can be found in [START_REF] Hermann | Unification of infinite sets of terms schematized by primal grammars[END_REF].

The control mechanism introduced by Hermann and Galbavý is based on the notion of counter variables which are variables having integer values. The schematization is achieve by introducing a particular type of rewrite system.

Definition 7 (Presburger rewrite system) A Presburger rewrite system contains for each defined functions f the following pair of Presburger rewrite rules:

• basic rule f (0, c; x) → Pbg t 1
• and the inductive rule which have one of the following forms:

f (n + 1, c; x) → Pbg t 2 [u ← f (n, c; x)] f (n + 1, c; x) → Pbg t 2 [u ← f (n, c 1 , ..., c i-1 , c i + 1, c i+1 , ..., c n ; x)]
where c is a vector of counter variables, x a vector of ordinary variables and u ∈ O(t 2 ),

To simplify the presentation, we omit here some additional conditions that are needed to ensure decidability properties of PG. We refer the reader to [START_REF] Hermann | Unification of infinite sets of terms schematized by primal grammars[END_REF] for more details.

From the previous definitions, we can now define a primal grammar and its associated language.

Definition 8 (Primal term grammar) A primal term grammar (or primal grammar for short) is a quadruple G = (F , D,R ,t) where C is a set of constructors, D the set of defined functions, R is a Presburger rewrite system and t a primal term called axiom.

The language generated by such a primal term grammar is the set of terms L(G) = {σt ↓ R | σ affects a ground integer value to each counter variable of t }. Note that, as usual, σt ↓ R represents the normal form of σt w.r.t. the system R (see [START_REF] Baader | Term Rewriting and All That[END_REF] for details on rewriting).

Intuitively, a PG generates terms thanks to a rewrite system R which is controlled by counter variables. Elements of the schematized language are then obtained by completely instantiating the terms with ground substitutions if needed.

Back to the introducing Example 2, let G be a primal grammar defined by

F = {suc, z, * }, D = { f , g}, R
is composed by the 4 Presburger rewrite rules

g(0) → Pbg z, g(s(n)) → Pbg s( g(n)), f (0) → Pbg z, f (s(n)) → Pbg g(s(n)) * f (n)
and the axiom f (c).

To simplify the notation, (, ) are omitted in the use of binary function * and moreover, the list reduced to one element * (z, ⊥) is simply denoted as z. Using the precedence f ≻ g, our Presburger rules fit Definition 7.

f (1) → Pbg g(1) * f (0) → Pbg g(1) * z → Pbg s( g(0)) * z → s(z) * z. So L(G) = {z, s(z) * z, . . . , suc n (z) * suc n-1 (z) * • • • * z, . . . }

Linear Logic and Sequent Calculus

We recall here some basic notations and notions related to first order and linear logics [START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | Linear logic, its syntax and semantics[END_REF], and proof systems in sequent calculus [START_REF] Miller | A Multiple-Conclusion Meta-Logic[END_REF].

Let us consider a first order logic signature Σ with V a countable set of variables, Σ F a finite set of function symbols with fixed arity and Σ N a finite set of predicate symbols. T (Σ F ,V ) denotes the first order term algebra built over Σ F and V and T (Σ F ) denotes the set of ground terms. Atoms are, as usual, built over predicates symbols and terms. A substitution is a mapping from V to T (Σ F ,V ) which is extended to T (Σ F ,V ) . A substitution assigning t to a variable x will be denoted {x ← t}. We introduce some linear logic ‡ notations: •denotes the linear implication and ⊗ denotes the multiplicative conjunction (see [START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | Linear logic, its syntax and semantics[END_REF] for the precise definitions of these connectives).

A formula A •-B 1 ⊗ ... ⊗ B n will be called a clause. The set Σ f ormula is the set of Σ-formulas built using atoms and the logic connectives. We recall basic notations for sequent calculus. ‡ Intuitively, the key idea of linear logic we use here is that, when performing logical inferences, some hypothesis can be consumed. This means that, along a proof, some formulas are persistent (as in usual first order logic) but some formulas can only be used once.

Definition 9 (Sequent) A sequent will be written as Σ : ∆ → G where Σ is the signature, ∆ a multiset of Σ-formulas and G a Σ-formula.

From these sequents we can built proof systems.

Definition 10 (Proof System) A proof system consists of a set of inference rules between sequents. An inference rule is presented here as:

Σ : ∆ → G Σ ′ : ∆ ′ → G ′
We use the classical notion of proof (i.e. there is a proof of a sequent in a proof system if this sequent is the root of a proof tree constructed using inference rules with empty leaves).

3 From TSG and PG Computation to Proof Search

In this section, we define the translation of grammar production rules into linear logic formulas. Then, designing a particular proof system, we show that usual grammar computations as defined in Definitions 3 and 8 can be reduced to proof searches using this system.

Transformation of TSG into Linear Logic Formulas

Given a TSG (F , N , PP, T I), the set PP of production rules is partitioned into PP f ree the set of free production rules and PP sync the set of packs of synchronized production rules. We define now a transformation function Ψ which is decomposed into two different mappings (corresponding respectively to the transformation of free and synchronized production rules). A predicate symbol and a variable will be associated to each non terminal.

Definition 11 (Transformation Function Ψ T SG )

Let σ N : N → Σ N be the mapping that translates every non terminal symbol into a predicate symbol (to simplify, we will write σ N (N) = n). Let σ V : N → V be the mapping that transforms every non terminal symbol into a logical variable (we will write σ V (N) = N). For the sake of readability, universal quantifications have been omitted when clear. Let σ PP f ree : PP f ree → Σ f ormula be the mapping that translates every free production rule into a Σ-formula and σ PP sync : PP sync → Σ f ormula the mapping that translates every pack of synchronized production rules into a Σ-formula.

Free productions

Let N → g(N 1 , . . . , N p ) and N → t in PP f ree .

σ PP f ree (N → g(N 1 , . . . , N p )) = n(g(N 1 , . . . , N p ), c) •-n 1 (N 1 , c) ⊗ . . . ⊗ n p (N p , c) σ PP f ree (N → t) = n(t, c) •-1 Synchronized Productions Let S = {R | P ∈ PP sync ∧ R ∈ P} and {R 1 ; . . . ; R n } ∈ PP sync : σ PP sync ({R 1 , . . . , R n }) = ∀c∃nc(σ S (R 1 , c, nc) ⊗ . . . ⊗ σ S (R n , c, nc))
where σ S : S ×C ×C → Σ f ormula is defined § , for N → g(N 1 , . . . , N p ) and N → t in S, as:

σ S (N → g(N 1 , . . . , N p ), c, nc) = n(g(N 1 , . . . , N p ), c) •-n 1 (N 1 , nc) ⊗ . . . ⊗ n p (N p , nc) σ S (N → t, c, nc) = n(t, c) •-1 Let Σ Ψ = Σ F ∪ Σ N and Ψ((F , N , PP, T I)) = σ PP f ree (PP f ree ) ∪ σ PP sync (PP sync )
(in the following, Ψ will denote a set of formulas obtained from a TSG and will be called a TSG program). At this step, a particular sequent calculus defines the semantics of Ψ.

A similar transformation function can be defined for primal grammars.

Transformation of PG into Linear Logic Formulas

We suppose in the following that Presburger rewrite systems are such that each definite symbol not appearing in the left hand side of a rule must also appear linearly in the right hand side. This is not in fact a restriction since multiple occurrences of a same symbol can be replaced by a new symbol with the same definition. This transformation does not modify the primal grammar definition.

Given a primal grammar (F , D,R , A), the functionσ D : D → Σ D maps each defined symbol N to a predicate symbol (we will use the notation

σ D (N) = n). σ V : D → V is the function that maps each defined symbol N to a logical variable ( σ V (N) = N). We use the notation c = (c 1 , . . . , c ar c (N)-1 ), c ′ = (c 1 , . . . , c i-1 , s(c i ), c i+1 , . . . , c ar c (N)-1 ) and ∀i ∈ [1..p], c i ⊑ c.
σ R : R → Σ f ormule is the function that maps to each Presburger rewrite rule a formula: § The set C denotes a set of counters (i.e. new symbols which are not in the current signature).

∀(N(0) → t) ∈ R , σ R (N(0) → t) = n(0,t) •-1 ∀(N(0, c) → g(N 1 ( c 1 ), . . . , N p ( c p ))) ∈ R , σ R (N(0, c) → g(N 1 ( c 1 ), . . . , N p ( c p ))) = n(g(N 1 , . . . , N p , 0, c)) •-n 1 (N 1 , c 1 ) ⊗ . . . ⊗ n p (N p , c p ) ∀(N(s(c 0 ), c) → g(N 1 ( c 1 ), . . . , N p ( c p ))[N(c 0 , c)]) ∈ R , σ R (N(s(c 0 ), c) → g(N 1 ( c 1 ), . . . , N p ( c p ))[N(c 0 , c)]) = n(g(N 1 , . . . , N p )[N], c 0 , c) •-n 1 (N 1 , c 1 ) ⊗ . . . ⊗ n p (N p , c p ) ⊗ n(N, c 0 , c) ∀(N(s(c 0 ), c) → g(N 1 ( c 1 ), . . . , N p ( c p ))[N(c 0 , c ′ )]) ∈ R , σ R (N(s(c 0 ), c) → g(N 1 ( c 1 ), . . . , N p ( c p ))[N(c 0 , c ′ )]) = n(g(N 1 , . . . , N p )[N], s(c 0 ), c)•-n 1 (N 1 , c 1 ) ⊗ . . . ⊗ n p (N p , c p ) ⊗ n(N, c 0 , c ′ )
As previously defined for TSG, we get the notion of PG program Ψ from the above definition. After these syntactic transformations, there is no more need to distinguish the two different types of grammar definition. We propose a uniform proof system which allows us to handle both formalisms at once.

The Proof System FG

In this section, we define a sequent calculus proof system inspired by the system Forum of D. Miller [START_REF] Miller | A Multiple-Conclusion Meta-Logic[END_REF].

Our proof system FG (Forum for Grammars) is defined by the following inference rules and defines the basic proof theoretical semantics of a TSG (resp. PG) program Ψ. In order to simplify the presentation, we have omitted Ψ in the sequents since, of course, it does not change.

Definition 12 (FG system)

[1]

Σ :→ 1 [Sync] Σ, α : C 1 θ, . . . ,C r θ, ∆ → G Σ : ∆ → G where ∀c∃nc(C 1 ⊗ . . . ⊗C r ) ∈ Ψ, θ = {c ← β, nc ← α}, β ∈ Σ, α ∈ Σ. [Back !] Σ : ∆ 1 → A 1 σ . . . Σ : ∆ p → A p σ Σ : ∆ 1 , . . . , ∆ p →G where C = (H •-A 1 ⊗ . . . ⊗ A p ) ∈ Ψ and Hσ = G.
[Back ?]

Σ : ∆ 1 → A 1 σ . . . Σ : ∆ p → A p σ Σ : (H •-A 1 ⊗ . . . ⊗ A p ), ∆ 1 , . . . , ∆ p →G
where Hσ = G.

Comments: It should be noticed that we distinguish free production rules and synchronized production rules (see the definition of the transformation function Ψ in Section 3.1). Clearly free productions appear as clauses H •-A 1 ⊗ ... ⊗ A n and packs of synchronized productions appear as formulas ∀c∃nc(C 1 ⊗ ... ⊗ C n ) where the C i 's are H •-A 1 ⊗ ... ⊗ A n and are called linear clauses (in the following linear clause will always refer to a clause generated by synchronization rules). Clauses corresponding to free productions in Ψ are persistent along the proof and are used in the inference [Back !] (this corresponds to a step of the grammar derivation using this free production). The treatment of a pack of synchronization is performed thanks to the rules [Sync] and [Back ?]. The first step consists in generating the formula corresponding to this pack in ∆ (rule [Sync]). The control is ensured by the instantiation of the counter variables with new symbols added to the signature Σ in rule [Sync]. Since ∆ is the linear logic part of our system, the linear clauses will be consumed when used by rule [Back ?] (in the philosophy of linear logic). This ensures the integrity of the synchronization and the control of the simultaneous application of the different productions of this pack. [Back?] and [Back!] lead to branching in the search tree.

As a consequence, our system FG is a subset of Forum (i.e. our rules can be expressed in Forum).

Proof:

The rules of FORUM used in this proof can be found in [START_REF] Miller | A Multiple-Conclusion Meta-Logic[END_REF]. We introduce the program Ψ in the proof to keep the initial FORUM presentation.

Proof of the correctness of 1 w.r.t. FORUM

Let 1 ≡ ⊥ •-⊥ in Σ : Ψ; ⊥ → [⊥L] Σ : Ψ; ⊥ → [decide 1 ] Σ : Ψ; ⊥ → ⊥ [⊥R] [•-R] Σ : Ψ; → 1 Proof of the correctness of [Sync] w.r.t. FORUM Let C ⊗C ′ ≡ (⊥ •-((⊥ •-C) & (⊥ •-C ′ ))
) and [⊗L] :

Σ : Ψ;C,C ′ , ∆ -→ G Σ : Ψ;C,C ′ , ∆ -→ ⊥, G [⊥R] Σ : Ψ;C, ∆ -→ ⊥ •-C ′ , G [•-R] Σ : Ψ;C, ∆ -→ ⊥, ⊥ •-C ′ , G [⊥R] Σ : Ψ; ∆ -→ ⊥ •-C, ⊥ •-C ′ , G [•-R] Σ : Ψ; ∆ -→ (⊥ •-C) & (⊥ •-C ′ ), G [ & R] Σ : Ψ; ⊥ → [⊥L] [•-L] Σ : Ψ; ∆ C⊗C ′ -→ G and ∃xB ≡ (∀xB ⊥ ) ⊥ ≡ ⊥ •-(∀x(⊥ •-B)) and [∃L] (y ∈ Σ): y, Σ : Ψ; ∆, B{x ← y}→G y, Σ : Ψ; ∆, B{x ← y}→⊥, G [⊥R] y, Σ : Ψ; ∆→⊥ •-B{x ← y}, G [•-R] [∀R] Σ : Ψ, ∃xB; ∆→∀x(⊥ •-B), G Σ : Ψ; ⊥ → [⊥L] [•-L] Σ : Ψ; ∆ ∃xB → G in Σ, β, α : Ψ;C 1 {c ← β, nc ← α}, . . . ,C n {c ← β, nc ← α}, ∆ → G [⊗L] n-1 Σ, β, α : Ψ; ∆ C 1 {c ← β,nc ← α}⊗...⊗C n {c ← β,nc ← α} -→ G [∃L] Σ, β : Ψ; ∆ ∃nc(C 1 {c ← β}⊗...⊗C n {c ← β}) -→ G [∀L] Σ, β : Ψ; ∆ ∀c∃nc(C 1 ⊗...⊗C n ) -→ G Σ, β : ∀c∃nc(C 1 ⊗ . . . ⊗C n ) ∈ Ψ; ∆ → G [decide 2 ] with α( = β) ∈ Σ.

Proof of the correctness of [Back !] and [Back

?] w.r.t. FORUM Let t 1 , . . . ,t n ∈ T (Σ F ), ρ = {x 1 ← t 1 , . . . , x n ← t n } with Hρ = G and δ ⊗ = Σ : Ψ; ∆ p-1 →A p-1 ρ Σ : Ψ; ∆ p →A p ρ . . . Σ : Ψ; ∆ 1 →A 1 ρ Σ : Ψ; ∆ 2 , . . . , ∆ p →A 2 ρ ⊗ . . . ⊗ A p ρ Σ : Ψ; ∆ 1 , . . . , ∆ p →A 1 ρ ⊗ . . . ⊗ A p ρ and C ⊗C ′ ≡ (⊥ •-((⊥ •-C) & (⊥ •-C ′ ))) and
Σ : Ψ; ∆ → C Σ : Ψ; ⊥ → [⊥L] [•-L] Σ : Ψ; ∆ ′ → C ′ Σ : Ψ; ⊥ → [⊥L] [•-L] Σ : Ψ; ∆ (⊥•-C) -→ Σ : Ψ; ∆ ′ (⊥•-C ′ ) -→ [ & L] Σ : Ψ; ∆, ∆ ′ (⊥•-C) & (⊥•-C ′ ) -→ Σ : Ψ; ∆, ∆ ′ , ((⊥ •-C) & (⊥ •-C ′ )) → [decide 1 ] Σ : Ψ; ∆, ∆ ′ , ((⊥ •-C) & (⊥ •-C ′ )) → ⊥ [⊥R] [•-R] Σ : Ψ; ∆, ∆ ′ → C ⊗C ′ in δ ⊗ Σ : Ψ; ∆ 1 , . . . , ∆ p →A 1 ρ ⊗ . . . ⊗ A p ρ Σ : Ψ; Hρ -→ G [initial] [•-L] Σ : Ψ; ∆ 1 , . . . , ∆ p Hρ•-A 1 ρ⊗...⊗A p ρ -→ G [∀L] n Σ : Ψ; ∆ 1 , . . . , ∆ p ∀x 1 ...x n (H•-A 1 ⊗...⊗A p ) -→ G Σ : Ψ; (∀x 1 . . . x n (H •-A 1 ⊗ . . . ⊗ A p )), ∆ 1 , . . . , ∆ p →G [decide 2 ] and δ ⊗ Σ : Ψ; ∆ 1 , . . . , ∆ p →A 1 ρ ⊗ . . . ⊗ A p ρ Σ : Ψ; Hρ -→ G [initial] [•-L] Σ : Ψ; ∆ 1 , . . . , ∆ p Hρ•-A 1 ρ⊗...⊗A p ρ -→ G [∀L] n Σ : Ψ; ∆ 1 , . . . , ∆ p ∀x 1 ...x n (H•-A 1 ⊗...⊗A p ) -→ G Σ : Ψ; (∀x 1 . . . x n (H •-A 1 ⊗ . . . ⊗ A p )), ∆ 1 , . . . , ∆ p →G [decide 2 ] ✷

Correctness and Completeness of FG

The correctness and completeness of the system FG is ensured by two theorems: one w.r.t. the TSG and the other w.r.t. PG.

Correctness and Completeness of FG w.r.t. TSG

We have to prove the following theorem. The set of instantiated productions of a computation of a TSG Gr = (F , N , PP, T I) denoted IP(Gr) is the smallest set defined by:

• if t is in Comp(Gr), t|u = (X, β), and R = (X→g(Y 1 , . . . ,Y n )) is in PP f ree then R(β) = ((X, β)⇒g((Y 1 , β), . . . , (Y n , β))) is in IP(Gr),
• if t is in Comp(Gr) and there exists n pairwise different occurrences u 1 , . . . , u n of t such that ∀i ∈ [1, n],t|u i = (X i , c i ) and c i = β and the pack of productions

P = {R 1 = X 1 →g 1 (Y 1 1 , . . . ,Y 1 n 1 ), . . . , R r = X r →g r (Y r 1 , . . . ,Y r n r )} ∈ PP (where α is a new symbol) then P(α, β) = {(X 1 , β)⇒g 1 ((Y 1 1 , α), . . . , (Y 1 n 1 , α)), . . . , (X r , β)⇒g n ((Y r 1 , α), . . . , (Y r n r , α))} = {R 1 (α, β), . . . , R r (α, β)} is included in IP(Gr).
Let σ I : IP(Gr) → Σ f ormula be the mapping that translates every instantiated productions into a Σ f ormula :

σ I ((X, β)⇒g((Y 1 , α), . . . , (Y n , α))) = x(g(Y 1 , . . . ,Y n ), β) •-y 1 (Y 1 , α) ⊗ . . . ⊗ y n (Y n , α)
A presynchronised production is a production of the form (X, β)→C((Y 1 , α), . . . , (Y n , α)) where C is a context of terminal symbols, β, α two new symbols and Y 1 , . . . ,Y n non terminals. The set of computations of a TSG Gr enlarged by presynchronised productions Φ is Comp(Gr) plus

• t[u ← C((Y 1 , α), . . . , (Y n , α))] if t is in the computation of Gr enlarged with Φ, t|u = (X, β) and ((X, β)→g((Y 1 , α), . . . , (Y n , α))) is in Φ.
If s is the number of instances of packs of productions used during a TSG derivation (t * ⇒ t ′ ):

• Σ Ψ ∪ {#} plus the set of counters used during the derivation is denoted Σ(t * ⇒ t ′ ) and

• the set of instances of synchronized productions is denoted

Φ(t * ⇒ t ′ ).
If s is the number of instances of packs of productions used during a TSG derivation ((I, #) * ⇒ t):

• the h th pack of productions used during this TSG derivation is denoted

P h (β h , α h ), 1 ≤ h ≤ s,
• the family of sets {Σ h } 0≤h≤s is defined by induction:

Σ 0 = Σ Ψ ∪ {#} and ∀h, 0 ≤ h < s, Σ h+1 = Σ h ∪ {α h+1 },
• the family of sets {∆ h } 0≤h≤s is defined by induction:

∆ 0 = / 0 and ∀h, 0 ≤ h < s, ∆ h+1 = ∆ h ∪ {R 1 , . . . , R p /{R 1 , . . . , R p } = σ I (P h+1 (β h+1 , α h+1 ))} (Remark: ∆ s = σ I (Φ((I, #) * ⇒ t))).

Proof of FG ⇒ TSG.

First, we prove by structural induction that if there exists a FG proof (with only instances of the [Back !],

[Back ?] and [START_REF] Brisset | Compilation de λProlog[END_REF] rules) for (Σ s : ∆ s →n(t, β)) then there is a derivation ((N, β) * ⇒ t) for the TSG enlarged by the set of presynchronised productions Φ s with σ I (Φ s ) = ∆ s .

Base Cases: Only the case [Back

?] + [1] is treated, the case [Back !] + [1] is similar. Σ s : →1 [1] Σ s : (n(t, β) •-1)→n(t, β) [Back ?]
with the linear clause (n(t, β) •-1) from a presynchronised production ((N, β)→t). Then (N, β)⇒t for the TSG enlarged with {((N, β)→t)} and σ

I ({(N, β)⇒t)}) = {(n(t, β) •-1)}.
Induction cases: Only the case [Back ?] is treated, the case [Back !] is similar.

∇ 1 . . . ∇ p Σ s : ∆ 1 →n 1 (t 1 , α) Σ s : ∆ p →n p (t p , α) Σ s : ∆ 1 , . . . , ∆ p , n(g(N 1 , . . . , N p ), β) •-n 1 (N 1 , α) ⊗ . . . ⊗ n p (N p , α)→n(t, β) [Back ?]
with α ∈ Σ s .

By induction hypothesis ∀i, 1 ≤ i ≤ p, there exists a derivation (N i , β) * ⇒ t i for the TSG enlarged with the set of presynchronised productions Φ i and ∆ i = σ I (Φ i ). Then there exists a derivation (N, β) * ⇒ t for the TSG enlarged with the presynchronised productions

p i=1 Φ i ∪ {(N, β)→g((N 1 , α), . . . , (N p , α))} and ∆ s = p i=1 σ I (Φ i ) ∪ {σ I ((N, β)→g((N 1 , α), . . . , (N p , α)))}.

✷ Synchronization Rule Introduction:

We begin with a definition.

Definition 13 (Restricted FG proof)

A FG proof is in restricted form if all the instances of the [Sync] rule are at the root of the proof.

First, we prove by induction on k if there exists a restricted FG proof for(Σ Ψ , # : →i(t, #)):

∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ Ψ , # : →i(t, #) [Sync] 1
then there exists a restricted FG proof for (Σ k : ∆ k →i(t, #)):

∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ k : ∆ k →i(t, #) [Sync] k+1
The case k = 0 is trivial. Now we assume 0 < k ≤ s. By induction hypothesis, there exists a FG proof for (Σ k-1 : ∆ k-1 →i(t, #)) with sk + 1 instances of the [Sync] rule, then :

∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ k-1 , α : ∆ k-1 , σ S (R 1 , c, nc)θ, . . . , σ S (R p , c, nc)θ→i(t, #) [Sync] k+1 [Sync] k Σ k-1 : ∆ k-1 →i(t, #) with P k = {R 1 , . . . , R p }, p > 1 and β ∈ Σ k-1 , α ∈ Σ k-1 and θ = {c ← β, nc ← α} and a derivation (I, #)⇒t) for the TSG enlarged with Φ k-1 , σ I (Φ k-1 ) = ∆ k-1 . But ∆ k = ∆ k-1 ∪ {σ S (R 1 , c, nc)θ, . . . , σ S (R p , c, nc)θ} and Σ k = Σ k-1 ∪ {α} then ∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ k : ∆ k →i(t, #) [Sync] k+1
Finally, we prove by induction on k that if there exists a restricted FG proof for (Σ Ψ , # : →i(t, #)):

∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ Ψ , # : →i(t, #) [Sync] 1
then there exists a derivation ((I, #) * ⇒ t) for the TSG enlarged with Φ k , σ I (Φ k ) = ∆ k .

The case k = s is a consequence of the previous result. Now we assume that 0 ≤ k < s. By induction hypothesis on the proof (with P k+1 = {R 1 , . . . , R p }, p > 1):

∇ Σ s : ∆ s →i(t, #) [Sync] s . . . Σ k , α : ∆ k+1 →i(t, #) [Sync] k+1 Σ k : ∆ k →i(t, #) . . . Σ Ψ , # : →i(t, #) [Sync] 1
there exists a derivation ((I, #) * ⇒ t) for the TSG enlarged with Φ k+1 and σ I (Φ k+1 ) = ∆ k+1 . But ∆ k+1 = ∆ k ⊎ {σ S (R 1 , c, nc)θ, . . . , σ S (R p , c, nc)θ} (θ = {c ← β, nc ← α}) so in the derivation, the presynchronised productions {R i (β, α)} 1≤i≤p can be replaced by the instance P k+1 (β, α) of the pack P k+1 . ✷

Proof of TSG ⇒ FG.

First, we prove by induction on the structure of derivation: if there exists a derivation

g((N 1 , β), . . . , (N l , β)) * ⇒ g(t 1 , . . . ,t l ) (1)
for a TSG then there exists for every k, 1 ≤ k ≤ l, a FG proof for

(Σ((N k , β) * ⇒ t k ) : σ I (Φ((N k , β) * ⇒ t k )) → n k (t k , β)) (2)
Base cases: Only the case with a pack of productions is treated, the case with a free production is similar.

Let {N 1 → t 1 , . . . , N r → t r } ∈ PP sync and the derivation (g((N 1 , β), . . . , (N r , β)) ⇒ g(t 1 , . . . ,t r )). Then for every k, 1 ≤ k ≤ r there exists a FG proof:

Σ Ψ , β :→ 1 Σ Ψ , β : (n k (t k , β) •-1) → n k (t k , β) with Φ((N k , β) ⇒ t k ) = {(N k , β) ⇒ t k } σ I (Φ((N k , β) ⇒ t k )) = {n k (t k , β) •-1} Φ(g((N 1 , β), . . . , (N r , β)) ⇒ g(t 1 , . . . ,t r )) = {(n 1 (t 1 , β) •-1), . . . , (n r (t r , β) •-1)}.
Induction cases: Only the case with a pack of productions is treated, the case with a free production is similar. Let

{N 1 → g 1 (N 1 1 , . . . , N p 1 1 ), . . . , N r → g r (N 1 r , . . . , N p r r )} ∈ PP sync (3)
and a derivation (g((N 1 , β), . . . , (N r , β)) ⇒ g(g 1 ((N Then by induction hypothesis, for every k, 1 ≤ k ≤ r and i k , 1 ≤ i k ≤ p k there exists a FG proof:

δ i k k = ∇ i k k Σ((N i k k , α) ⇒ t i k k ) : σ I (Φ((N i k k , α) ⇒ t i k k )) → n i k k (t i k k , α) For every k, 1 ≤ k ≤ r, σ I (Φ((N k , β) * ⇒ g k (t 1 k , . . . ,t p k k ))) = σ I ( p k i=1 Φ((N i k k , α) * ⇒ t i k k ) ∪ {(N k , β) ⇒ g k ((N 1 k , α), . . . , (N p k k , α))}) = p k i=1 σ I (Φ((N i k k , α) * ⇒ t i k k )) ∪ {σ I ((N k , β) ⇒ g k ((N 1 k , α), . . . , (N p k k , α)))} = p k i=1 σ I (Φ((N i k k , α) * ⇒ t i k k )) ∪ {n k (g k (N 1 k , . . . , N p k k ), β) •-n 1 k (N 1 k , α), . . . , n p k k (N p k k , α)}
Then for every k, 1 ≤ k ≤ r there exits a FG proof (the signatures of δ

i k k , 1 ≤ i k ≤ p k , are augmented with β): δ 1 k . . . δ p k k Σ((N k , β) * ⇒ g k (t 1 k , . . . ,t p k k )) : σ I (Φ((N k , β) * ⇒ g k (t 1 k , . . . ,t p k k ))) → n k (g k (t 1 k , . . . ,t p k k ), β) Σ((N k , β) * ⇒ g k (t 1 k , . . . ,t p k k )) = p k i k =1 Σ((N i k k , α) * ⇒ t i k k ) ∪ {β} and Φ(g((N 1 , β), . . . , (N r , β)) * ⇒ g(g 1 (t 1 1 , . . . ,t p 1 1 ), . . . , g r (t 1 r , . . . ,t p r 1 ))) = r k=1 Φ((N k , β) * ⇒ g k (t 1 k , . . . ,t p k k ))).
By the result above, we have the following corollary:

Corollary 1 If there exists a derivation ((I, #) * ⇒ t) for a TSG then there exists a FG proof for (Σ s :

∆ s → i(t, #)).
Now we prove by induction on h: if there exists a FG proof for (Σ s : ∆ s → i(t, #)) then there exists an FG proof for (Σ h : ∆ h → i(t, #)). The base case h = 0 is trivial, now we assume that 0 < h ≤ s.

Σ h+1 = Σ h ∪ {α h+1 } and ∆ h+1 = ∆ h ∪ {R h+1
1 , . . . , R h+1 p /{R h+1 1 , . . . , R h+1 p } = σ I (P h+1 (β h+1 , α h+1 ))}. By induction hypothesis, there exists a FG proof for:

∇ Σ h , α h+1 : ∆ h , R h+1 1 , . . . , R h+1 p → i(t, #)
so there exists a FG proof:

∇ Σ h , α h+1 : ∆ h , R h+1 1 , . . . , R h+1 p → i(t, #) [Sync] Σ h : ∆ h → i(t, #)

✷

This achieves the first part of the correctness and completeness of our transformation. We now have to provide a similar theorem for Primal Grammars.

Correctness and Completeness of FG w.r.t. PG

Proof of PG =⇒ FG.

We prove by induction on the length of a PG derivation if there exists a PG derivation ( f (m 0 , m) * ⇒ Pbg t), with f ∈ D and m 0 ∈ N and m ∈ N ar( f )-1 then there exists a FG proof for (Σ Ψ : Ψ; →

f (t, m 0 , m))
The right hand-side of the sequent (Σ Ψ : Ψ; ) does not vary and is omitted.

Case l = 1: f (m 0 , m)⇒ Pbg t then m 0 = 0 and there exists a basic rule ( f (0, c) → t) ∈ R and a linear clause

(∀ c( f (t, 0, c) •- 1
)) ∈ Ψ and a FG proof:

→1 [1]
→ f (t, 0, m)

[Back !]
Case l > 1: Only the case with the last applied rule as an instance of the second inductive rule ¶ is treated, the case for the first inductive rule is similar. So m 0 = s(m -1 ) and there exists a context C with

t = C(t 1 , . . . ,t p )[t ′ ] and an inductive rule ( f (s(c 0 ), c)→ Pbg C( f1 ( c 1 ), . . . , fp ( c p ))[ f (c 0 , c + )]) ∈ R . So ∀i ∈ [1..p], fi ( m i ) k i ≤l ⇒ Pbg t i , f (m -1 , m + ) k ′ ≤l ⇒ Pbg t ′ and Σ p i=1 k i + k ′ = l -1.
Then by induction hypothesis, there exist FG proofs for ∀i ∈ [1..p], (→ f i (t i , m i )):

δ i → f i (t i , m i )
and there exists a FG proof for (→ f (t ′ , m -1 , m + )):

δ ′ → f (t ′ , m -1 , m + ) Moreover, σ R ( f (s(c 0 ), c)→ Pbg C( f1 ( c 1 ), . . . , fp ( c p ))[ f (c 0 , c + )]) = ∀c 0 ∀ c∀F 1 . . . ∀F p ∀F( f (C(F 1 , . . . , F p )[F], s(c 0 ), c) •-f 1 (F 1 , c 1 ) ⊗ . . . ⊗ f p (F p , c p ) ⊗ f (F, c 0 , c + ))
Then there exists a FG proof for (→ f (C(t 1 , . . . ,t p )[t ′ ], s(m -1 ), m)):

δ 1 δ p δ ′ → f 1 (t 1 , m 1 ) . . . → f p (t p , m p ) → f (t ′ , m -1 , m + ) [Back !] → f (C(t 1 , . . . ,t p )[t ′ ], s(m -1
), m) ¶ We write k = ar( f ) and c = (c 1 , . . . , c k ) and m = (m 1 , . . . , m k ) and c + = (c 1 , . . . , c i-1 , s(c i ), c i+1 , . . . , c k ) and m + = (m 1 , . . . , m i-1 , s(m i ), m i+1 , . . . , m k ) and ∀i ∈ [1..p], c i is a subsequence of c and m i is a subsequence of m on the same positions.

{ F 0 : ∀c(∀X∀Y (i( f (X,Y ), c) •-x(X, c) ⊗ y(Y, c))), F 1 : ∀c(x(z, c) •-1), F 2 : ∀c(y(z, c) •-1), F 3 : ∀c∃nc ((∀X(x(s(X), c) •-x(X, nc))) ⊗ (∀Y (y(s(s(Y )), c) •-y(Y, nc)))) } δ 1 δ 2 [Back !] F 0 #, β : x(s(X), #) •-x(X, β), y(s(s(Y )), #) •-y(Y, β) → i( f (s(z), s(s(z))), #) [Sync] F 3 # :→ i( f (s(z), s(s(z))), #)
where

δ 1 :            1 [Back !] F 1 #, β :→ x(z, β) [Back ?] #, β : x(s(X), #) •-x(X, β) → x(s(z), #)
and

δ 2 :            1 [Back !] F 2 #, β :→ y(z, β) [Back ?] #, β : y(s(s(Y )), #) •-y(Y, β) → y(s(s(z)), #)
4 From Linear Logic to Prolog From now on, there is no more need to distinguish TSG and PG since they have been embedded into the same formalism (i.e. linear logic formulas). From an operational point of view, it appears clearly that the previous system FG does not provide any strategy for a proof search (especially concerning the use of the rule [Sync]). Furthermore, a refinement will help us to get the implementation of the system. Therefore, we define a goal directed proof system FG dir with the following inference rules. We define the set operator ⊎ as

⊎ 1≤i≤n A i = ∪ 1≤i≤n A i such that ∀1 ≤ i, j ≤ n, i = j, A i ∩ A j = / 0. if ∀c∃nc(C 1 ⊗ . . . ⊗C r ) ∈ Ψ, 1 ≤ j ≤ r,C j θ = (H •-1), Hσ = G i , ∆ i = / 0, C 1 θ, . . . ,C j-1 θ,C j+1 θ, . . . ,C r θ = (⊎ 1≤k( =i)≤n ∆ ′ k ), β ∈ Σ, α ∈ Σandθ = {c ← β, nc ← α}. [Axiom ! dir ] Σ : ((∆ 1 → G 1 ), . . . , (∆ i-1 → G i-1 ), (∆ i+1 → G i+1 ), . . . , (∆ n → G n )) Σ : ((∆ 1 → G 1 ), . . . , (∆ n → G n )) if H •-1 ∈ Ψ, ∆ i = /
0 and there exists a substitution σ such that Hσ = G i .

[Axiom ? dir ] Σ : (∆ 1 → G 1 ), . . . , (∆ i-1 → G i-1 ), (∆ i+1 → G i+1 ), . . . , (∆ n → G n ) Σ : (∆ 1 → G 1 ), . . . , (∆ n → G n ) if ∆ i = {H •-1}, there exists a substitution σ such that Hσ = G i .
The main difference introduced by this system is that synchronizations and reduction are led by the goal to be solved. We now have to prove that this system is equivalent to our initial system FG. The equivalence of the two systems is ensured by the following theorem:

Theorem 3 (FG dir ⇔ FG) There exists a proof of a sequent in the system FG if and only if there exists a proof of this sequent in the system FG dir .

Proof: This proof is inspired by [START_REF] Stéphan | Nouvelles fondations pour la programmation en logique disjonctive[END_REF]. The transformation of a FG proof tree into a FG dir proof derivation is achieved by recombining the different branches of the proof into a single derivation and then collapsing the synchronization rule with its first corresponding linear clause. The intermediate system FG lin is needed to achieve the first part of the proof.

Definition 15 (FG lin System)

[Back ! lin ] (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ i-1 : ∆ i-1 → G i-1 ), (Σ i : ∆ ′ 1 → A 1 σ), . . . , (Σ i : ∆ ′ p → A p σ), (Σ i+1 : ∆ i+1 → G i+1 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n )
where

(H •-A 1 ⊗ . . . ⊗ A p ) ∈ Ψ, Hσ = G i and ∆ i = ⊎ 1≤k≤p ∆ ′ k .
[Back ? lin ] (Σ 1 :

∆ 1 → G 1 ), . . . , (Σ i-1 : ∆ i-1 → G i-1 ), (Σ i : ∆ ′ 1 → A 1 σ), . . . , (Σ i : ∆ ′ p → A p σ), (Σ i+1 : ∆ i+1 → G i+1 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n ) where C = (H •-A 1 ⊗ . . . ⊗ A p ) ∈ ∆ i , Hσ = G i and ∆ i \ {C} = ⊎ 1≤k≤p ∆ ′ k . [Sync lin ] (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ i-1 : ∆ i-1 → G i-1 ), (Σ i , α : C 1 θ, . . . ,C r θ, ∆ i → G i ), (Σ i+1 : ∆ i+1 → G i+1 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n ) where ∀c∃nc(C 1 ⊗ . . . ⊗C r ) ∈ Ψ, α ∈ Σ i , β ∈ Σ i and θ = {c ← β, nc ← α}. [Axiom ! lin ] (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ i-1 : ∆ i-1 → G i-1 ), (Σ i+1 : ∆ i+1 → G i+1 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n )
where

(H •-1) ∈ Ψ, ∆ i = / 0 and Hσ = G i . [Axiom ? lin ] (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ i-1 : ∆ i-1 → G i-1 ), (Σ i+1 : ∆ i+1 → G i+1 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n )
where ∆ i = {(H •-1)} and Hσ = G i .

Lemma 1 (FG ⇔ FG lin )

There exists proofs of the sequents ∀i, 1 ≤ i ≤ n, (Σ i : ∆ i → G i ) in the system FG if and only if there exists a proof of the sequent (Σ 1 :

∆ 1 → G 1 ) . . . (Σ n : ∆ n → G n ) in the system FG lin .
Proof of FG => FG lin . We prove by induction on the structure of a FG proof if ∀i, 1 ≤ i ≤ n there exists a FG proof of (Σ i : ∆ i → G i ) then there exists a FG lin proof of (Σ 1 :

∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n ).

Base case [Back ?] + [1]:

The FG proof is as follows:

Σ :→ 1 Σ : H •-1 → G with Hσ = G
Then the derivation:

(Σ :→ G) [Axiom ! lin ]
is a FG lin proof.

Base case [Back !] + [1]:

This case is similar to the [Back ?] + [START_REF] Brisset | Compilation de λProlog[END_REF] base case.

Induction case [Sync]: The inference at the root of the proof is an instance of the [Sync] rule:

∇ α, Σ : C 1 θ, . . . ,C r θ, ∆ → G [Sync] Σ : ∆ → G with (∀c∃nc(C 1 ⊗ . . . ⊗C r )) ∈ Ψ, β ∈ Σ, α ∈ Σ and θ = {c ← β, nc ← α}.
By induction hypothesis, for the FG proof tree: ∇ α, Σ : C 1 θ, . . . ,C r θ, ∆ → G there exists a FG lin proof:

D (α, Σ : C 1 θ, . . . ,C r θ, ∆ → G)
Then the following derivation:

D (α, Σ : C 1 θ, . . . ,C r θ, ∆ → G) (Σ : ∆ → G) is a FG lin proof.
Induction case [Back ?]: The inference at the root of the proof is an instance of the [Back ?] rule:

∇ 1 ∇ p Σ : ∆ 1 → A 1 σ . . . Σ : ∆ p → A p σ Σ : H •-A 1 ⊗ . . . ⊗ A p , ∆ 1 , . . . , ∆ p → G with Hσ = G.
By induction hypothesis for every 1 ≤ i ≤ n there is a FG lin proof:

S l i . . . {S j } j∈I i . . . (Σ : ∆ i → A i σ)
Let give the following FG lin derivation ∀i, 1 ≤ i ≤ p:

S l i , {(Σ : ∆ k → A k σ)} i<k≤p D i        . . . {S j } j∈I i ∪ {(Σ : ∆ k → A k σ)} i<k≤p . . . (Σ : ∆ i → A i σ), {(Σ : ∆ k → A k σ)} i<k≤p
with Hσ = G 1 . By induction hypothesis, ∀ j, 1 ≤ j ≤ p, there exists a FG proof:

∇ ′ j Σ 1 : ∆ ′ j → A j σ
and ∀i, 2 ≤ i ≤ n, there exists a FG proof:

∇ i Σ i : ∆ i → G i
Then the proof tree:

∇ ′ 1 ∇ ′ p Σ 1 : ∆ ′ 1 → A 1 σ . . . Σ 1 : ∆ ′ p → A p σ Σ 1 : ∆ ′ 1 , . . . , ∆ ′ p → G 1 is a FG proof.
D (Σ 1 , α : C 1 θ, . . . ,C r θ, ∆ 1 → G 1 ), (Σ 2 : ∆ 2 → G 2 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n )
with ∀c∃nc(C 1 ⊗ . . . ⊗C r ) ∈ Ψ, β ∈ Σ 1 , α ∈ Σ 1 and θ = {c ← β, nc ← α}. By induction hypothesis, there exist ∀i , 2 ≤ i ≤ n, a FG proof:

∇ i Σ i : ∆ i → G i and a FG proof: ∇ 1 Σ 1 , α : C 1 θ, . . . ,C r θ, ∆ 1 → G 1
Then the proof tree:

∇ 1 Σ 1 , α : C 1 θ, . . . ,C r θ, ∆ 1 → G 1 Σ 1 , α : ∆ 1 → G 1 is a FG proof.

✷

The following definitions and lemmas are technical ones to establish the equivalence between FG lin and FG dir systems.

Lemma 2 (FG Restriction Lemma)

If there exists a FG proof then there exists a restricted FG proof.

Proof of the FG restriction. By (a double) induction on the distance between the closer instance of the [Sync] rule to the root and the root, (and the number of instances of [Sync] rule which is straight forward), we prove that if there exists a FG derivation then there exists a restricted FG derivation with the same first and last resolvents.

Base case: An instance of the [Sync] rule is already at the root.

Induction case:

The instance of the rule at the root of the derivation is either an instance of [Back !],

[Back ?] or [START_REF] Brisset | Compilation de λProlog[END_REF] rules. The [START_REF] Brisset | Compilation de λProlog[END_REF] is trivial. The [Back ?] case is only treated, the [Back !] is similar. The derivation is of the form (without loss of generality i = 1):

∇ Σ : ∆ 1 → A 1 σ . . . Σ : ∆ p → A p σ Σ : ∆ → G with C = (H •-A 1 ⊗ . . . ⊗ A p ) ∈ ∆, Hσ = G, ∆ \ {C} = ⊎ 1≤k≤p ∆ p .

Definition 18 (Ordered FG lin proof)

A FG lin proof is ordered if the order on the Eigenvariables induced by the instances of the [Sync lin ] rules is the same as the one induced by their initial instances.

Lemma 3 (FG lin Restriction Lemma)

If there exists a FG lin proof then there exists an restricted FG lin proof.

Proof of the restriction lemma for FG lin . By (a double) induction on the distance between the closer instance of the [Sync lin ] rule to the root and the root, (and the number of instances of [Sync lin ] rule which is straight forward), we prove that if there exists a FG lin derivation then there exists a restricted FG lin derivation with the same first and last resolvents.

Base case: An instance of the [Sync lin ] rule is already at the root.

Induction case:

The instance of the rule at the root of the derivation is either an instance of [Back ! lin ],

[Axiom ! lin ], [Back ? lin ] or [Axiom ? lin ] rules. The [Back ? lin ] case is only treated, there others are similar. The derivation is of the form (without loss of generality i = 1):

∇ (Σ 1 : ∆ ′ 1 → A 1 σ), . . . , (Σ 1 : ∆ ′ p → A p σ), (Σ 2 : ∆ 2 → G 2 ), . . . , (Σ n : ∆ n → G n ) (Σ 1 : ∆ 1 → G 1 ), . . . , (Σ n : ∆ n → G n ) with C = (H •-A 1 ⊗ . . . ⊗ A p ) ∈ ∆ 1 , Hσ = G 1 and ∆ 1 \ {C} = ⊎ 1≤k≤p ∆ ′ p .
By induction hypothesis, there exists a FG lin derivation ∇ ′ with an instance of the [Sync lin ] rule at the root, the same number of instances of the [Sync lin ] rule and the same first and last resolvents as ∇. A restricted FG lin derivation is obtained by permuting this instance of the [Sync lin ] rule and the instance of the [Back ? lin ] rule and inserting in the signature of every sequents of the descendants of (Σ 1 :

∆ ′ k → A k σ) (∀k, 1 ≤ k ≤ p)

✷ Lemma 4 (Ordered Lemma)

If there exists a FG lin proof then there exists a restricted, ordered FG lin proof.

Proof of the order lemma for FG lin . By the restriction lemma, for any FG lin proof there exists a restricted FG lin proof. The existential introduction induces a partial order on the Eigenvariables. The order on the initial instances respects this partial order. Two instances of [Sync lin ] rule can be permuted if this permutation respects the partial order. The order of the initial instances can be chosen as the order of introduction of the Eigenvariables. ✷

Lemma 5 (FG lin ⇔ FG dir )

There exists a proof of the sequent (Σ 1 :

∆ 1 → G 1 ) . . . (Σ n : ∆ n → G n ) in the system FG lin if and only if there exists a proof of the sequent (Σ 1 : ∆ 1 → G 1 ) . . . (Σ n : ∆ n → G n ) in the system FG dir .
Proof of FG lin => FG dir . We prove by induction on the number of instances of the [Sync lin ] rule if there exists a restricted, ordered FG lin derivation of (# :→ G) then there exists a FG dir derivation of (# :→ G) with the same last resolvent.

Case l = 0: The FG lin derivation contains no instance of [Sync lin ] rule so this derivation is also a FG dir derivation.

Case l > 0: The restricted, ordered FG lin derivation is composed of two parts:

• a derivation R containing only instances of the [Back ! lin ], [Axiom ! lin ], [Back ? lin ] and [Axiom ? lin ] rules:

∇ (Σ, α : ∆,C 1 θ, . . . ,C r θ → G)
• and a derivation S containing only l instances of [Sync lin ] rule with the last applied on

∀c∃nc(C 1 ⊗ . . . ⊗C r ) ∈ Ψ, θ = {c ← β, nc ← α}, β ∈ Σ, α ∈ Σ : (5) (Σ, α : ∆,C 1 θ, . . . ,C r θ → G) (Σ : ∆ → G) . . . (# :→ G)
By induction hypothesis R contains the initial instance corresponding to the instance of this

R ′    ∇ (Σ, α : ∆ ′ 1 ∪ ∆ ′′′ 1 → A 1 σ), . . . , (Σ, α : ∆ ′ p ∪ ∆ ′′′ p → A p σ), (Σ, α : ∆ 2 ∪ ∆ ′′ 2 → G 2 ), . . . , (Σ, α : ∆ n ∪ ∆ ′′ n → G n ) D ′          (Σ, α : ∆ 1 ∪ ( 1≤k≤p ∆ ′′′ k ) ∪ {H •-A 1 ⊗ . . . ⊗ A p } → G 1 ), (Σ, α : ∆ 2 ∪ ∆ ′′ 2 → G 2 ), . . . , (Σ, α : ∆ n ∪ ∆ ′′ n → G n ) . . . (Σ, α : ∆,C 1 θ, . . . ,C r θ → G) with C 1 θ, . . . ,C j-1 θ,C j+1 θ, . . . ,C r θ = (⊎ 1<k≤n ∆ ′′ k ) ⊎ (⊎ 1≤k≤p ∆ ′′′ k ), ⊎ 1≤k≤p ∆ ′ k = ∆ 1 , C j θ = H •-A 1 ⊗ . . . ⊗ A p , Hσ = G 1 .
The derivation R is restricted and ordered then R ′ contains only instances of the [Back ! lin ], [Axiom ! lin ], [Back ? lin ] and [Axiom ? lin ] rules (on non initial instances) then the derivation R ′ is also a FG dir derivation. Let D ′′ be the same derivation as D ′ without the instances C k θ, 1 ≤ k ≤ r and α. Since the derivation R is ordered the derivation D ′′ is still a FG lin derivation. So by induction hypothesis on the FG lin derivation below formed from S without the last inference and D ′′ :

(Σ : ∆ 1 → G 1 ), . . . , (Σ : ∆ n → G n ) . . . (Σ : ∆ → G) . . . (# :→ G)
there is a FG dir derivation D ′′′ :

(Σ : ∆ 1 → G 1 ), . . . , (Σ : ∆ n → G n ) . . . (# :→ G)
So the derivation:

R ′    ∇ (Σ, α : ∆ ′ 1 ∪ ∆ ′′′ 1 → A 1 σ), . . . , (Σ, α : ∆ ′ p ∪ ∆ ′′′ p → A p σ), (Σ, α : ∆ 2 ∪ ∆ ′′ 2 → G 2 ), . . . , (Σ, α : ∆ n ∪ ∆ ′′ n → G n ) D ′′′      (Σ : ∆ 1 → G 1 ), . . . , (Σ : ∆ n → G n ) . . . (# :→ G) with {C 1 θ, . . . ,C j-1 θ,C j+1 θ, . . . ,C r θ} = (⊎ 1<k≤n ∆ ′′ k ) ⊎ (⊎ 1≤k≤p ∆ ′′′ k ) and ⊎ 1≤k≤p ∆ ′ k = ∆ 1 in a FG dir derivation. ✷ Proof of FG dir => FG lin .
We prove by induction on the number of instances of the [Sync+ dir ] or [Sync1 dir ] rules if there exists a FG dir derivation of (# :→ G) then there exists a FG lin derivation of (# :→ G) with the same last resolvent.

Case l = 0: The FG dir derivation contains no instance of [Sync+ dir ] nor [Sync1 dir ] rule so this derivation is also a FG lin derivation.

Case l > 0: The FG dir derivation is composed of two parts:

• a derivation R containing only instances of the [Back ! dir ], [Axiom ! dir ], [Back ? dir ] and [Axiom ? dir ] rules;

• and a derivation D containing only l instances of [Sync+ dir ] or [Sync1 dir ] rule;

We have to mention here that this system provides a goal directed approach for the recognition of an element of a tree language. This kind of operation is not practically possible using the initial grammar definition which gives a method to produce elements of the language but does not give any strategy to recognize an element. The introduction of unification and variable renaming in the system FG dir would also ensure the generation of the element of the language. This has to be formally proved thanks to a lifting lemma (as it is done for the SLD resolution of Prolog [START_REF] Lloyd | Foundations of Logic Programming[END_REF]). As a consequence, the generation is available in the Prolog implementation of our system described in the next section.

Concerning the decidability of our approach, it is clear that problems encountered with DCG's appear here (mainly due to left recursions and empty transitions). Since Prolog is the underlying framework, the problems related to its depth left first strategy also occur. Thus, termination of our method depends on this search strategy.

Implementation Issue

This section briefly describes how the implementation can be achieved from the previous inference system. At this time, a library is able, taking a TSG (resp. a PG) as input, to provide, as output, a predicate phrase_TSG (resp. phrase_PG) which can recognize or generate a term for the defined language from the axiom. The implementation of the method described along this paper can be divided in two parts: the translation of the grammar into linear logic formulas (described in Section 3.1) and the implementation of the proof system FG dir in Prolog. The following presentation of this implementation is related to Example 1.

Management of signature and linear context

The extension of the signature (i.e. new symbols introduced by existential quantifiers of synchronization) is inspired by the management of essentially universal quantifier (quantifier pi in the body of clauses) of λProlog [START_REF] Brisset | Compilation de λProlog[END_REF]: only the cardinality of this extension is needed.

The management of linear clauses is meta-programmed by a linear program continuation LPC (i.e. a set containing the remaining linear clauses introduced by instances of [Sync+ dir ] or [Sync1] which have to be used later). This technique is inspired by the management of intuitionistic implication of λProlog [START_REF] Hodas | Logic Programming in a Fragment of Intuitionistic Linear Logic[END_REF][START_REF] Brisset | Compilation de λProlog[END_REF].

Transformation Function

Back to Example 1, the transformation is illustrated here by the implementation of the clause F 0 which corresponds to the free production R 0 .

i(C, f(X, Y), SigmaIn, SigmaOut, DeltaIn, DeltaOut) :x(C, X, SigmaIn, SigmaInter, DeltaIn, DeltaInter), y(C, Y, SigmaInter, SigmaOut, DeltaInter, DeltaOut).

SigmaIn, SigmaInter and SigmaOut represent the cardinality of the extension of the signature. DeltaIn, DeltaInter and DeltaOut represent the LPC.

Implementation of the Proof System FG dir in Prolog

The inference rules [Back !] and [Axiom !] are handled by the reduction mechanism of Prolog.

phrase_TSG(f(s(z),s(s(z))),i) LPC i(0,f(s(z),s(s(z)))) {} (I,0) x(0,s(z)),y(0,s(s(z)))

{} f((X, 0), (Y, 0)) x(1,z),y(0,s(s(z))) {Cy} f(s((X, 1)), (Y, 0)) y(0,s(s(z))) {Cy} f(s(z), (Y, 0)) y(1,z) {} f(s(z), s(s((Y, 1)))) {} f(s(z), s(s(z)))

Practical Use of the System

We can now illustrate the complete use of our system on PG's Example 2. The user has only to write as input the following prolog clause: in order to provide the description of the PG thanks to the predicate sigma pg. The execution of this clause produces file pg with trace.pl, containing a predicate phrase pg, which can be loaded and used for grammar recognition as: This execution shows that s(z) * z belongs to the PG and how it can be generated from the PG. The source code of this implementation is available at: http://www.info.univ-angers.fr/pub/stephan/Research/Download.html.

Conclusion

In this paper, we describe an implementation scheme for particular types of tree language including specific control features. The main idea is to provide an uniform framework in order to compute over tree grammars. As it has been done for word grammars with DCG [START_REF] Cohen | Parsing and compiling using prolog[END_REF], we propose a transformation method that allows us to get a set of Prolog Horn clauses from a grammatical definition of a tree language. This method consists in translating grammar derivation into proof search using a sequent calculus proof system based on linear logic. By successive refinements, we get a goal directed procedure implemented in Prolog.

Since such tree languages appear as powerful tools for the schematization of sets of terms to represent solutions of symbolic computation problems, it seemed necessary to define a method to use these representations. Moreover, this approach allows us to embed various formalism into a unique framework, were computations can include Regular Languages, TSG and PG.

Theorem 1 (

 1 Correctness and Completeness of FG w.r.t. TSG) Given a TSG (F , N , PP, (I, #)), the corresponding T SG program Ψ and t ∈ T (Σ F ), (Σ Ψ , # :→ σ N (I)(t, #)) has a proof in FG w.r.t. the T SG program Ψ if and only if ((I, #) * ⇒ t). Prologue to the proof of Correctness and completeness of FG w.r.t. TSG.

Theorem 2 (

 2 Correctness and Completeness of FG w.r.t. PG) Given a PG (F , D,R , A), the corresponding PG program Ψ and c ∈ N ar c (A) and t ∈ T (F ). (Σ Ψ : Ψ; → σ D (A)(t, c)) has a proof in FG if and only if (A( c) * ⇒ t).

Definition 17 (

 17 By induction hypothesis, there exists a FG derivation ∇ ′ with an instance of the [Sync] rule at the root, the same number of instances of the [Sync] rule and the same first and last resolvents as ∇. A restricted FG derivation is obtained by permuting this instance of the [Sync] rule and the instance of the [Back ?] rule and inserting in the signature of every sequents of the descendants of (Σ :∆ k → A k σ) (∀k, 1 ≤ k ≤ p)in the derivation ∇ ′ the constant α inserted by the instance of the [Sync] rule. ✷ At this stage, we need more intermediate definitions to continue the proof. Definition 16 (Restricted FG lin proof) A FG lin proof is in restricted form if all the instances of the [Sync lin ] rule are at the root of the proof. Initial instance) The initial instance w.r.t. an instance of the [Sync lin ] rule is the instance of [Back ? lin ] or [Axiom ? lin ] rules which uses for the first time one of the linear clauses introduced by the [Sync lin ] rule.

  in the derivation ∇ ′ the constant α inserted by the instance of the [Sync lin ] rule.

  pg_with_trace :name(FileName, "pg_with_trace.pl"), open(FileName,write,Stream), sigma_pg(pg(f,[f,g],[ [(f(0) -> z), (f(s(n)) -> g(s(n))*f(n))], [(g(0) -> z),(g(s(n)) -> s(g(n)))] ]),Stream), close(Stream).

|

  ?-phrase_pg(s(z)*z,f,[s(0)]).

  • if c 1 , . . . , c k are counter expressions, t 1 , . . . ,t n are primal terms and f ∈ D such that car( f ) = k andar( f ) = k + n, then f (c 1 , . . . , c k ;t 1 , . . . ,t n ) is a primal term,• if t 1 , . . . ,t n are primal terms and c is a constructor with the arity ar(c) = n the c(t 1 , . . . ,t n ) is a primal term.

	Definition 5 A counter expression is an expression built over 0, successor function s and a set of counter
	variables C nt. s(c) means 1 + c if c is a counter expression. The ground counter expression s n (0) is
	interpreted as the integer n.
	Now, we recall the notion of primal term.
	Definition 6 (Primal Algebra) The algebra of primal terms is defined over a set of functions D (whose
	elements f are called defined functions and have a counter arity car( f ) and a standard arity ar( f )), a set
	of constructor symbols F , a set of ordinary variables X and a set of counter variables C nt. This is the
	smallest set such that
	• each ordinary variable of X is a primal term,

  Induction cases [Axiom ! lin ], [Axiom ? lin ] and [Back ! lin ]: The cases [Axiom ! lin ], [Axiom ? lin ] and [Back ! lin ] are similar to the [Back ? lin ] induction case. Induction case [Sync lin ]: The inference at the root of the proof is an instance of the [Sync lin ] rule (without loss of generality i = 1):

† In the following and without any loss of generality, we consider always terms as the basic elements of tree languages 1365-8050 c 2002 Discrete Mathematics and Theoretical Computer Science (DMTCS), Nancy, France

Acknowledgements

We would like to thank Miki Hermann, Sébastien Limet and Piere Réty for fruitful discussions on this work.

✷

Proof of PG ⇐ FG. We prove by induction on the structure of a FG proof if there exists a FG proof for (Σ Ψ : Ψ; → f (t, m 0 , m)), [START_REF] Dershowitz | Rewrite Systems, volume B[END_REF] with f ∈ D and m 0 ∈ N and m ∈ N ar( f )-1 then there exists a PG derivation ( f (m 0 , m) * ⇒ Pbg t) The right hand-side of the sequent (Σ Ψ : Ψ; ) does not vary and is omitted.

Base case: There exists a proof of → f (t,m 0 , m) 1 so m 0 = 0 and there exists a linear clause ∀ c( f (t, 0, c) •-1) ∈ Ψ and a basic rule f (0, c) → t ∈ R ). Then f (0, m)⇒ Pbg t.

Induction cases: There exists a FG proof for (→ f (t, m 0 , m)). The only possible inference rule applied at the root of the proof is an instance of the [Back !] rule. Only the case for a linear clause obtained from the second inductive rule is treated, the cases for the basic rule or the first inductive rule are similar.

We have a FG proof of shape

with the linear clause

and ∀i ∈ [1..p] δ i a proof with the root (→ f i (t i , m i )) and δ ′ a proof with the root (→n(t ′ , m -1 , m + )).

For all proofs δ i , i ∈ [1..p], by induction hypothesis, there exist PG derivations fi ( m i )⇒ Pbg t i and for the proof δ ′ , by induction hypothesis, there exists a PG derivation f (m -1 , m + )⇒ Pbg t ′ . Then by

Application

We address here Example 1 on TSG to illustrate how the transformation and proof system FG work. We build the derivation tree for the TSG program Ψ. Σ Ψ is omitted in the left hand side of the sequents of the following proof in order to simplify the notation, we only mention the new symbols added to the signature along the proof and universal quantifiers are omitted in the sequents:

We denote k = ar( f ) and c = (c 1 , . . . , c k ) and m = (m 1 , . . . , m k ) and

.p], c i is a subsequence of c and m i a subsequence of m on the same positions.

Definition 14 (FG dir system)

Then the derivation:

is a FG lin proof.

Induction case [Back !]: This case is similar to the [Back ?] case.

✷ Proof of FG lin => FG. We prove by induction on the structure of a FG lin proof if there exists a FG lin proof of (Σ 1 :

Base case [Axiom ? lin ]: The FG lin proof is as follows:

with Hσ = G.

The proof tree:

is a FG proof.

Base case [Axiom ! lin ]:]

This case is similar to the [Axiom ?] base case.

Induction case [Back ? lin ]: The inference at the root of the proof is an instance of the [Back ? lin ] rule (without loss of generality i = 1):

The [Sync+ dir ] case is only treated, the [Sync1 dir ] case is similar.

The derivation D is of the form (without loss of generality i = 1):

[Back ? dir ] and [Axiom ? dir ] so it is also a FG lin derivation. By induction hypothesis on the FG dir derivation D ′ containing l -1 instances of [Sync+ dir ] or [Sync1 dir ] rules there exists a FG lin derivation:

Let D ′′′ be the same derivation as D ′′ but for all (Σ ′ :

Then the derivation:

Reduction strategy

Due to the leftmost selection rule and the depth-first search strategy of Prolog the reduction strategy is a left-outermost strategy as shown on the trace below for the goal phrase_TSG(f(s(z),s(s(z))),i) (the clause (y(0, s(s(Y)), SI, SO, DI, DO) :-y(1, Y, SI, SO, DI, DO)) is denoted Cy). The first column is the (simplified † † ) prolog trace, the second one contains the linear program continuation and the third one the term already recognized.