François Morain
email: morain@lix.polytechnique.fr

Modular equations for some η-products

Keywords:

The classical modular equations involve bivariate polynomials that can be seen to be univariate with coefficients in the modular invariant j. Kiepert found modular equations relating some η-quotients and the Weber functions γ 2 and γ 3 . In the present work, we extend this idea to double η-quotients and characterize all the parameters leading to this kind of equation. We give some properties of these equations, explain how to compute them and give numerical examples.

1.

Introduction

Let η denote Dedekind's function. When N > 1 is an integer, η-quotients of the form f = d|N η(z/d) r d are functions for Γ 0 (N ) when the integer r d 's satisfy some properties known as Newman's Lemma [START_REF] Newman | Construction and application of a class of modular functions[END_REF]. In other words, there exists a bivariate polynomial Φ[f ](X, J) such that Φ[f ](f (z), j(z)) = 0 for all z, where j is the classical modular invariant.

In some cases, there exist equations of the form Φ[f ](X, G 3 , G 2 ) where Φ[f ](f (z), γ 3 (z), γ 2 (z)) = 0 for the Weber function γ 3 , γ 2 . Kiepert was the first to compute modular equations of this type for f = w p = η(z/p)/η(z) for p ≤ 29 (see [START_REF] Kiepert | Über Theilung und Transformation der elliptischen Funktionen[END_REF]). Weber cites some examples in [14, §72] and Antoniadis [START_REF] Antoniadis | Über die Berechnung von Multiplikatorgleichungen[END_REF] extended this to p ≤ 61.

In the present work, we study such equations for the double η-quotients w e p 1 ,p 2 , as introduced in [START_REF] Enge | Constructing elliptic curves over finite fields using double etaquotients[END_REF]. We give all parameters (p 1 , p 2 , e) leading to equations in γ 2 and γ 3 .

Section 2 recalls known facts on Weber and η functions. Section 3 deals with the case of w p where we introduce a faster variant of the classical algorithm to compute the modular equation via series expansions. Section 4 proves the necessary results for w p 1 ,p 2 , gives algorithms to compute the equations in the spirit of Section 3, and we add numerical examples.

Notations: If u is some function, we will note Φ[u](X, J) the corresponding modular equation. If u = j(nz), we will note Φ n to simplify.

Preliminaries

2.1 Properties of the functions γ 2 and γ 3

We will use the traditional notations

T = 1 1 0 1 , S = 0 -1 1 0
and use the notation f • M to denote the function z → f (M z). The modular invariant is j(z) = j(q) = 1/q + 744 + • • • with q = exp(2iπz). The classical Weber functions are γ 2 (q) = j(q) 1/3 = q -1/3 (1 + 248q + 4124q 2 + 34752q 3 + 213126q 4 + O(q 5 )) ∈ q -1/3 (1 + Z[[q]]), γ 3 (q) = (j(q) -1728) 1/2 = q -1/2 (1 -492 q -22590 q 3 + O q 5 ) ∈ q -1/2 (1 + Z[[q]]).

If n is an integer, we note ζ n = exp(2πi/n). Remember that j is invariant through T and S and that

γ 2 • T = ζ -1 3 γ 2 , γ 2 • S = γ 2 , (1)
γ 3 • T = -γ 3 , γ 3 • S = -γ 3 . (2)
Moreover, we have [14, §55] Let us precise this result in a special case.

Proposition 2.2 Let T (q) be invariant as in Theorem 2.1. Suppose that T (q) ∈ q -a/b Z[[q]] for an irreducible fraction a/b > 0 with b | 6. When b = 1, T (q) is a polynomial in j(q). When b = 2, T (q)/γ 3 (q) is a polynomial in j(q). For b = 3, T /γ i 2 is a polynomial in j(q) where i ≡ -a mod 3. For b = 6, T /(γ i 2 γ 3 ) is a polynomial in j(q), where i ≡ -(a + 3)/2 mod 3. In all cases, the polynomial in j(q) has integer coefficients.

Proof: in all cases, the integer i is chosen in such a way that the resulting series T ′ is invariant through S and T , therefore a rational function in j. Noting that T ′ has integer coefficients, by the Hasse principle, so does the polynomial.

From the algorithmic point of view, we have to recognize a polynomial with integer coefficients applied to j(q), given the first terms of the series T (q). Note that we need the order of this series to be > 0. We proceed step by step.

function RecognizePolyInJ(T ) Input: a series T = c v q v + • • • + O(q 1
) with integer coefficients, v ≤ 0 and c v = 0.

Output: a polynomial P (X) of degree -v such that T = P (j(q)).

while

i ≤ 0 do { at this point R = r i q i + • • • + O(q 1 ) with r i = 0 } 2.1 P := P + r i X -i ; 2.2 R := R -r i j(q) -i ; 2.3 i := valuation(R); 3. return P .
Note that we can precompute the powers of j(q) whenever needed, so that each call to the function requires O(v 2 ) operations. In large cases, computations can be done using results computed modulo small primes and reconstructed via the CRT (as done by Atkin, see [START_REF] Morain | Calcul du nombre de points sur une courbe elliptique dans un corps fini : aspects algorithmiques[END_REF]).

Formulas for the η-function

The following is taken from [START_REF] Enge | Modular curves of composite level[END_REF] and will be our main tool in the computations of Section 4.

Theorem 2.3 Let M = a b c d ∈ Γ be normalised such that c ≥ 0, and d > 0 if c = 0. Write c = c 1 2 λ(c) with c 1 odd; by convention, c 1 = λ(c) = 1 if c = 0. Define ε(M ) = a c 1 ζ ab+c(d(1-a 2 )-a)+3c 1 (a-1)+ 3 2 λ(c)(a 2 -1) 24 . For K ∈ N write u K a + v K Kc = δ K = gcd(a, Kc) = gcd(a, K). Then η z K • M = ε a δ K -v K Kc δ K u δ K (cz + d) η δ K z + (u K b + v K Kd) K δ K ,
where the square root is chosen with positive real part.

We can decompose the formula into several parts:

ε(M ) = Jac(M )ζ E(M ) 24
where we distinguish the Jacobi symbol part and the exponent of ζ 24 ; then, we have the squareroot part Q(M ) and the η-part N (M ). When dealing with a η-quotient, the aboves formulas are applied by multiplicativity on the different pieces η(z/d) (see below).

3 Generalized Weber functions

Definition and properties

Let N > 3 be an odd integer. For all factorizations N = ad, let e = gcd(a, d) and consider the functions

P c,d,a = i (a-1)/2 c e √ d η((c + dz)/a) η(z)
for 0 ≤ c < a with gcd(c, e) = 1. These functions were introduced in [14, §72]. It is easy to see that

P 0,1,N = i (N -1)/2 η(z/N )/η(z) = i (N -1)/2 w N (z)
where the function w N was studied in [START_REF] Enge | Generalized Weber functions[END_REF]. Weber proves that in all cases, P 24 c,d,a are roots of a modular equation. In some cases, the results are better, for instance:

Theorem 3.1 If gcd(N, 6) = 1, 12 | c, then the P 2 c,d,a γ N -1 2 γ (N -1)/2 3
are roots of a modular equation.

Computations in the prime order case

For a prime N = p > 3, this setting simplifies to

x 0,p,1 = p η(pz) η(z) 2 , x 12h,1,p = (-1) (p-1)/2   η 12h+z p η(z)   2 , 0 ≤ h < p.
Theorem 3.2 The numbers x c,d,a γ 2 (z) p-1 γ 3 (z) (p-1)/2 are roots of a modular equation whose coefficients are rational functions of j(z). In particular, the constant term is (-1) (p-1)/2 p.

Antoniadis extended the results of Kiepert to p ≤ 61 and gave more properties of the polynomials [START_REF] Antoniadis | Über die Berechnung von Multiplikatorgleichungen[END_REF]. He computed the equation by solving a linear system in the unknown coefficients of the equation, using the q-expansion of j(q) and the fact that x 0,p1 must be a root of the equation.

A standard approach (already known to Enneper [7, §52]) is to compute the powers sums of the roots of the equation, recognize them as polynomials in our variables, and then terminate using the classical Newton relations. Inspecting our roots, we see that the q-expansion of x 0,p,1 has positive order, and all x 12h,1,p have negative order. So the power sums can be computed using the x 12h,1,p only; we can find formulas for the q-expansion of p-1 h=0 x k 12h,1,p if needed. A better approach is to look at the reciprocal polynomial, whose roots are the 1/x 0,p,1 and 1/x 12h,1,p and only the first one contributes to the power sums. Write (p -1)/12 = e ′ /δ as an irreducible fraction with 6 | δ. Noting that

p/x 0,p,1 = q (1-p)/12 (1 + • • • ) = q -e ′ /δ (1 + • • • ),
we see that all powers are expressible as functions whose expansions satisfy Proposition 2.2. The algorithm is:

1. compute S k = p/x k 0,p,1 and recognize it as a polynomial in the usual variables. 2. use Newton's formulas. 3. Remove the powers of p. Note that the largest power is (p/x 0,p,1 ) p+1 = q -(p 2 -1)/12 (1 + • • • ) where the exponent is an integer as soon as p > 3. Therefore, we need up to (p 2 -1)/12 terms in the j-series.

We have S 1 = 11/x 0,11,1 = q -5/6 -2q 1/6q 7/6 + 2q 13/6 + O(q 19/6 ).

Dividing by γ 2 γ 3 , we find 1 + 242q + O(q 2 ) which must be a polynomial in j(q), hence the constant 1. The other coefficients are given in Table 1. We have replaced γ 2 (resp. γ 3 ) by G 2 (resp. G 3 ). The corresponding polynomial is (after reductions between variables)

Φ[-w 2 11 ](F, G 2 ) = F 12 -G 3 G 2 F 11 -242G 2 2 F 10 -19965G 3 F 9 -585640G 2 F 8 + 159440490F 6 -285311670611.
Taking its reciprocal and removing the spurious powers of p yields: 4 -4368737795118764J 3 + 669619352632925750J 2 -33921007872189625000J + 233702090524237500000) q -55/6 -22q -49/6 + 209q -43/6 -1078q -37/6 + 2926q -31/6 -1672q -25/6 -15169q -19/6 +47234q -13/6 -31350q -7/6 -107426q -1/6 + 218680q 5/6

F 12 -990F 6 + 440G 2 F 4 + 165G 3 F 3 + 22G 2 2 F 2 + G 3 G 2 F -11, k (11/x 0,11,1 ) k q -5/3 -4q -2/3 + 2q 1/3 + • • • = G 2 2 (J -1244) q -5/2 -6q -3/2 + 9q -1/2 + 10q 1/2 + • • • = G 3 (J 2 -1002J + 59895) q -10/3 -8q -7/3 + 20q -4/3 -70q 2/3 + • • • = G 2 (J 3 -2488J 2 + 1510268J -135655520) q -25/6 -10q -19/6 + 35q -13/6 -30q -7/6 -105q -1/6 + 238q 5/6 + • • • = G 3 G 2 2 (J 3 -2246J 2 + 1287749J -145411750) q -5 -12q -4 + 54q -3 -88q -2 -99q -1 + 540 -418q + • • • = J 5 -3732J 4 + 4586706J 3 -2059075976J 2 + 253478654715J -2067305393340 q -35/6 -14q -29/6 + 77q -23/6 -182q -17/6 + 924q -5/6 -1547q 1/6 + • • • = G 3 G 2 (J 5 -3490J 4 + 4063139J 3 -1796527998J 2 + 247854700555J -4740750382830) q -20/3 -16q -17/3 + 104q -14/3 -320q -11/3 + 260q -8/3 + 1248q -5/3 -3712q -2/3 +1664q 1/3 + • • • = G 2 2 (J 6 -4976J 5 + 9210680J 4 -7786404608J 3 + 2955697453292J 2 -418137392559040J + 12629117378938720) q -15/2 -18q -13/2 + 135q -11/2 -510q -9/2 + 765q -7/2 + 1242q -5/2 -7038q -3/2 + 8280q -1/2 +9180q 1/2 + • • • = G 3 (J 7 -4734J 6 + 8386065J 5 -6877048710J 4 + 2611195915626J 3 -398512009001700J 2 + 16457557949779815J -41283301866181650) q -25/3 -20q -22/3 + 170q -19/3 -760q -16/3 + 1615q -13/3 + 476q -10/3 -11210q -7/3 +22440q -4/3 + 1615q -1/3 -64600q 2/3 + • • • = G 2 (J 8 -6220J 7 + 15382190J 6 -19242776200J 5 + 12809764457825J
+ • • • G 3 G 2 2 (J 8 -5978J 7 + 14256527J 6 -17312108670J 5 + 11327366012605J 4 -3889904574252522J 3 + 631138185556080950J 2 -38141443583282670180J + 473098671409604281800) q -10 -24q -9 + 252q -8 -1472q -7 + 4830q -6 -6048q -5 -16744q -4 + 84480q -3 -113643q -2 -115920q -1 + 534612 -370920q + • • • J 10 -7464J 9 + 23101236J 8 -38353325536J 7 + 36913772324730J 6 -20784851556729552J 5 +6580486714450069928J 4 -1063011399511905159360J 3 + 72005127765018136775955J 2 -1322204967509387392211000J + 1424583710586688670191932 Table 1: Computations for p = 11.
already computed by Weber.

Note that one drawback of the approach is the large degree and sizes of the coefficients before reduction via Newton formulas. However, if computations are performed using CRT primes, this is not a problem, since we compute the final polynomial modulo the primes.

The smallest cases are

Φ[w 2 5 ](X, G 2 ) = X 6 + 10 X 3 -G 2 X + 5, Φ[-w 2 7 ](X, G 3 ) = X 8 + 14X 6 + 63X 4 + 70X 2 + G 3 X -7, Φ[w 2 13 ](X, J) = X 14 +26 X 13 +325 X 12 +2548 X 11 +13832 X 10 +54340 X 9 +157118 X 8 +333580 X 7 +509366 X 6 + 534820 X 5 + 354536 X 4 + 124852 X 3 + 15145 X 2 + (746 -J) X + 13.
Remark. We concentrated here on the prime index case. The same work can be done on composite ones. Note also that we could use resultants for that task, noting the following. Suppose p is prime and M is an integer prime to p; write N = pM . Write

w s pM (z) = (w p (z)w M (z/p)) s .
On the other hand:

Φ[w s 1 p ](w s 1 p (z), j(z)) = 0, Φ[w s 2 M ](w s 2 M (z/p), j(z/p)) = 0, Φ p (j(z), j(z/p)) = 0. Writing Z = w s pM (z), X = w p (z), Y = w M (z/p
), the different quantities are related via the algebraic equations:

Z = X s Y s , Φ[w s 1 p ](X s 1 , J) = 0, Φ[w s 2 M ](Y s 2 , J ′ ) = 0, Φ p (J, J ′ ) = 0,
and the variables can be eliminated via resultants to get a modular equation in Z and J, that needs to be factored to get the correct polynomial.

4 Double η-quotients

Definition and statement of the result

For primes p 1 and p 2 , let

w s p 1 ,p 2 =   η z p 1 η z p 2 η z p 1 p 2 η(z)   s = w p 1 (z) w p 1 (z/p 2 )
s where s = 24 gcd(24,(p 1 -1)(p 2 -1)) is the smallest integer such that sr is an integer, where r = (p 1 -1)(p 2 -1)/24. Note that s | 24; and s | 6 when p 1 and p 2 are odd primes. It is shown in [START_REF] Enge | Modular curves of composite level[END_REF] that the function w s p 1 ,p 2 is a function on Γ 0 (p 1 p 2 ); properties of the classical modular equation are also given.

We can now state the result that we will prove in this Section. The following Lemma is used in the Theorem.

Lemma 4.1 Let δ ∈ {2, 3, 6} be as above and suppose N = p 1 p 2 ≡ 1 mod δ. Then p i ≡ -1 mod δ.

Proof: For δ = 2, N ≡ 1 mod 2 gives the answer. When 3 | δ, we cannot have p i = 3 since N ≡ 1 mod δ. For δ to be equal to 3 (resp. 6), surely we cannot have p i ≡ 1 mod 3 (resp. 6). This leaves p i ≡ -1 mod 3 (resp. 6).

The proof of the Theorem will take use several intermediate results that we will present in as much a compact way as possible. When p 1 = p 2 , we will make the convention that p 1 is odd (so that we may have p 2 = 2). Moreover, we let u and v be two integers such that up 1 + vp 2 = 1. To simplify the proofs, we will be mostly looking at properties using p 2 , this case being complicated when p 2 = 2. Reciprocally, using p 1 and p 2 supposes that p 1 = p 2 . The results and proofs are of course symmetrical by exchanging p 1 and p 2 . In case of equality, we will write p 1 = p 2 = p.

The conjugates of w p 1 ,p 2

In [START_REF] Enge | Modular curves of composite level[END_REF] are given the conjugates of w s p 1 ,p 2 (with some minor typos). Here, we need precise the expansions of w p 1 ,p 2 . In view of Theorem 2.3, the value of w p 1 ,p 2 • M can be composed as

w p 1 ,p 2 • M = Jac(M )ζ E(M ) 24 Q(M )N (M )
where the first part cumulates Jacobi symbols, the second the exponents of ζ 24 , the third one is the product of the squareroots and the last one the η quotient. To ease notations, we also put

φ = ζ 24r 24 = ζ (p 1 -1)(p 2 -1) 24
. We use the notations and philosophy of computations from [START_REF] Enge | Modular curves of composite level[END_REF].

Proposition 4.2 Let p 1 and p 2 be two primes. In all cases, we have the N + 1 following conjugate functions:

M w p 1 ,p 2 • M ord l T ν = 1 ν 0 1 A ν (z) = η z+ν p 1 η z+ν p 2 η(z+ν)η z+ν p 1 p 2 -r p 1 p 2 ζ -νr N = w p 1 ,p 2 (z + ν), 0 ≤ ν < N S = 0 -1 1 0 B(z) = η(p 1 z)η(p 2 z) η(z)η(p 1 p 2 z) = w p 1 ,p 2 (N z) -r 1
The remaining p 1 + p 2 conjugates are:

M w p 1 ,p 2 • M ord l M 1,µ = µp 2 -1 1 0 C 1,ν (z) = φ θ 1 (ν) ε 1 η z+ν p 1 η(p 2 (z+ν)) η(z+ν)η p 2 (z+ν) p 1 , 0 ≤ ν < p 1 r p 1 φ θ 1 (ν) ε 1 ζ νr p 1 M 1,0 = vp 2 -up 1 1 1 M 2,µ = µp 1 -1 1 0 C 2,ν (z) = φ θ 2 (ν) ε 2 η(p 1 (z+ν))η z+ν p 2 η(z+ν)η p 1 (z+ν) p 2 , 0 ≤ ν < p 2 r p 2 φ θ 2 (ν) ε 2 ζ νr p 2 M 2,0 = up 1 -vp 2 1 1
where in the case of

C 2,ν , we set ν ≡ -(µp 1 ) -1 mod p 2 , v 2 = (1 + p 1 µν)/p 2 for µ = 0 (equivalently ν = 0; µ = 0 corresponds to ν = 0). When ν > 0, we get θ 2 (ν) = µ((p 2 + 1)v 2 + 1) + ν if p 2 = 2, (3p 1 + 2) ν+1 2 if p 2 = 2.
Moreover

θ 2 (0) = uv(p 2 + 1) + u -1 if p 2 = 2, (3u+2)(u-1) 2 if p 2 = 2.
Also,

ε 2 = p 1 p 2 if p 2 = 2, 1 if p 2 = 2.
When p 1 = p 2 = p, we must consider the p -1 following conjugate functions:

matrix w p,p • M ord l M µ = µp -1 1 0 C ν (z) = √ pε(ν)ζ θ(ν) 24 η(pz) 2 η(z)η z+ ν p , 1 ≤ ν < p p-1 12 √ pε(ν)ζ pθ(ν)-ν 24p where 1 = -µν + vp, ε(ν) = -ν p if p odd (resp. 1 when p = 2) and θ(ν) = pν (1 -µ 2 ) + (-3 p + 2 + v) µ -3 + 3 p if p is odd, 0 if p = 2.
Proof: the cases of the A ν matrices and of B are treated without difficulty, as in [START_REF] Enge | Modular curves of composite level[END_REF]. The value of Q(M ) is 1, unless we are dealing with the case p 1 = p 2 = p. The computations for the C matrices involve non-zero exponents for ζ 24 .

Case p 1 = p 2 :

In the same lines as in [START_REF] Enge | Modular curves of composite level[END_REF], we first prove the result for C 2,ν when ν > 0. Iterate over 1 ≤ µ < p 2 and define ν = -(µp 1 ) -1 mod p 2 ∈ {1, . . . , p 2 -1}, v 2 = (1 + µνp 1 )/p 2 . Note that ν → µ is an involution and the corresponding v 2 's are equal. Moreover, iterating over 1 ≤ µ < p 2 is the same as iterating over 1 ≤ ν < p 2 . We find

N (M 2,µ ) = η(p 1 z)η((z + ν)/p 2 ) η(z)η(p 1 (z + ν)/p 2 ) = ζ ν(1-p 1 ) 24 η(p 1 (z + ν))η((z + ν)/p 2 ) η(z + ν)η(p 1 (z + ν)/p 2 ) .
(a) Assume first p 2 = 2. We compute Jac(M 2,µ ) = p 1 p 2 , and the total exponent of ζ 24 is

ν(1 -p 1 ) + E(M 2,µ ) = (p 1 -1) p 2 ν p 1 µ 2 + p 2 ν + 2 µ p 2 -µ v 2 -ν -µ = (p 1 -1)((p 2 -1)(νµ 2 p 1 + ν + 2µ) + µ(1 -v 2 + µνp 1 )) = (p 1 -1)(p 2 -1)(νµ 2 p 1 + ν + 2µ + µv 2 ) = (p 1 -1)(p 2 -1)(µ((p 2 + 1)v 2 + 1) + ν)
where we have used p 2 v 2 = 1 + µνp 1 twice. When p 2 = 2, we find Jac(M 2,µ ) = 1 and the total exponent of ζ 24 is

ν(1 -p 1 ) + E(M 2,µ ) = (p 1 -1) (3p 1 µ 2 (ν + 1) + µ(3µ -1) + ν)/2.
Since ν is odd, µ = 1 and the exponent reduces to

(p 1 -1)(3p 1 + 2) ν + 1 2 . (b) For C 2,0 , N (M 2,0 ) = η(p 1 (z + 1))η(z/p 2 ) η(z + 1)η(p 1 z/p 2 ) = ζ p 1 -1 24 η(z/p 2 )η(p 1 z) η(z)η(p 1 z/p 2 ) ,
Assume first p 2 = 2. Then Jac(M 2,0 ) = p 1 p 2 and the exponent of ζ 24 is

p 1 -1 + E(M 2,0 ) = -(p 1 -1)((p 2 -1)(p 1 u 2 -2u + 1) + u(p 1 u + v -1)) = -24r(p 1 u 2 -2u + 1 -uv) = 24r(uv(p 2 + 1) + u -1).
When p 2 = 2, we find Jac(M 2,0 ) = 1 and the total exponent of ζ 24 is

(p 1 -1) (3u + 2)(u -1) 2 .
Case p 1 = p 2 = p: In all cases:

N (M µ ) = √ p η(pz) 2 η(z)η(z + ν/p)
where 1 = -µν + vp.

When p = 2, we find Jac(M µ ) = µ p and the exponent given by θ(ν). When p = 2, Jac(M µ ) = 1 and the exponent given by v -1 = 0.

Action of T and S

This section is devoted to the proofs of the actions of T and S on our basic functions as stated in the following two propositions.

Proposition 4.3 (i) B • T = φ -1 B. (ii) For 0 ≤ ν < N -1, we have A ν • T = A ν+1 ; A N -1 • T = φ -1 A 0 . (iii) For 0 ≤ ν < p 2 -1, C 2,ν • T = φ θ 2 (ν)-θ 2 (ν+1) C 2,ν+1 ; C 2,p 2 -1 • T = φ θ 2 (p 2 -1)-θ 2 (0)+1 C 2,0 . (iv) For 1 ≤ ν < p, C ν • T = ζ 2p-2 24 C ν .
Proof of Proposition 4.3: (i), (ii) and (iv) are direct applications of Theorem 2.3.

(iii) For 0 ≤ ν < p 2 -1, one has C 2,ν • T = φ θ 2 (ν)-θ 2 (ν+1) C 2,ν+1 . For ν = p 2 -1: C 2,p 2 -1 • T = φ θ 2 (p 2 -1) ε 2 η z+p 2 p 2 η (p 1 (z + p 2 )) η(z + p 2 )η p 1 (z+p 2 ) p 2 = φ θ 2 (p 2 -1) ε 2 η z p 2 + 1 η (p 1 z + N ) η(z + p 2 )η p 1 z p 2 + p 1 = φ θ 2 (p 2 -1) ε 2 ζ 1+N -p 1 -p 2 24 η z p 2 η (p 1 z) η(z)η p 1 z p 2 = φ 1+θ 2 (p 2 -1)-θ 2 (0) C 2,0 .
Proposition 4.4 For all primes p 1 and p 2 , one has

(i) (A 0 , B) • S = (B, A 0 ).
(ii) When 0 < ν < p 1 p 2 and gcd(ν, p 1 p 2 ) = 1:

A ν • S = φ θ 3 (ν) A ω
where 1 = -ων + v 12 (p 1 p 2 ) and

θ 3 (ν) = -ων 2 -2ν + ω + 3 + νv 12 if p 2 = 2, ω + ν(v 12 (1 -2p 1 ) + 2) if p 2 = 2.
Suppose from now on that p 1 = p 2 . The following hold: (iii) When 0 < ν = p 1 ρ < p 1 p 2 :

A ν • S = φ θ 4 (ρ) C 2,̟
where 1 = -̟ν + wp 2 , and

θ 4 (ρ) = -θ 2 (̟) + ρ(w(p 2 + 1) + 1) + ̟ if p 2 = 2, -θ 2 (̟) + 3 p 1 +1 2 ρ 2 + ρ(3w -2) + ̟ if p 2 = 2. (iv) When 0 < ν < p 2 , use µ ≡ -1/(νp 1 ) mod p 2 and C 2,ν • S = A µp 1 . (v) We have C 2,0 • S = C 1,0 × φ -2θ 1 (0) if p 2 = 2, φ -θ 1 (0)+ u 2 p 1 p 1 +1 2 + 1-u 2 if p 2 = 2.
Proof: (i) We first get:

w p 1 ,p 2 • (T ν • S) = w p 1 ,p 2 • ν -1 1 0
and the case ν = 0 yields immediately A 0 • S = B. On the other hand, we also have the reassuring result that

B • S = w p 1 ,p 2 (-N/z) = w p 1 ,p 2 (z) = A 0 (z).
(ii) When gcd(ν, p 1 p 2 ) = 1, we write 1 = -ων + v 12 (p 1 p 2 ), and find

N (M 2,µ • S) = η((z + ω)/p 1 )η((z + ω)/p 2 ) η(z)η((z + ω)/p 1 /p 2 ) = ζ ω 24 A ω .
When p 2 = 2, Jac(M 2,µ • S) = 1 and the total exponent of ζ 24 is

ω + E(M 2,µ • S) = -ων 2 (24r -1) + ν(-48r + 1 + v 12 (1 -p 1 -p 2 )) + 24r(ω + 3) = 24r(-ων 2 -2ν + ω + 3) + ν(ων + 1 + v 12 (1 -p 1 -p 2 )) = 24r(-ων 2 -2ν + ω + 3 + νv 12 ) = 24rθ 3 (ν).
When p 2 = 2, we also have Jac(M 2,µ • S) = 1 and the exponent of

ζ 24 becomes (p 1 -1)(ω + ν(v 12 (1 -2p 1 ) + 2)).
The same type of computations show that the results also holds for p 1 = p 2 = 2.

(iii) Suppose now that ν = ρp 1 , 1 ≤ ρ < p 2 . We write 1 = -̟ν + wp 2 . In all cases

N (M 2,µ • S) = η(p 1 z)η((z + ̟)/p 2 ) η(z)η((p 1 (z + ̟))/p 2 ) = ζ -p 1 ̟+̟ 24 η(p 1 (z + ̟))η((z + ̟)/p 2 ) η(z + ̟)η((p 1 (z + ̟))/p 2 ) = ζ -p 1 ̟+̟ 24 φ -θ 2 (̟) ε 2 C 2,̟ . Assume p 2 = 2. We get Jac(M 2,µ • S) = p 1 p 2 .
The partial exponent is given by

-̟(p 1 -1) + E(M 2,µ • S) = (p 1 -1)(p 2 p 1 ̟ρ 2 + (-w + 2p 2 -1)ρ + (p 2 -1)̟) = (p 1 -1)(p 2 ρ(p 1 ρ̟) + (-w + 2p 2 -1)ρ + (p 2 -1)̟) = (p 1 -1)(p 2 ρ(wp 2 -1) + (-w + 2p 2 -1)ρ + (p 2 -1)̟) = (p 1 -1)(p 2 -1)(ρ(w(p 2 + 1) + 1) + ̟)
yielding the final result. When p 2 = 2, we find Jac(M 2,µ • S) = 1 and

-̟(p 1 -1) + E(M 2,µ • S) = (p 1 -1) ρ(3w -2) + 3 p 1 + 1 2 ρ 2 + ̟ .
(iv) For 1 ≤ ν < p 2 , we compute µ ≡ -1/(νp 1 ) mod p 2 and

C 2,ν • S = w p 1 ,p 2 • µp 1 -1 1 0 • S = η((z + p 1 µ)/p 1 )η((z + p 1 µ)/p 2 ) η(z + p 1 µ)η((z + p 1 µ)/p 1 /p 2 ) = A p 1 µ .
(v) In all cases, we compute

Jac(M • S)N (M • S) = p 2 p 1 η(z/p 1 )η(p 2 z -p 2 ) η(z -1)η(p 2 z/p 1 ) = p 2 p 1 ζ 1-p 2 24
η(z/p 1 )η(p 2 z) η(z)η(p 2 z/p 1 ) .

When p 2 = 2, this yields

Jac(M • S)N (M • S) = ζ 1-p 2 24 φ -θ 1 (0) C 1,0 . The exponent of ζ 24 is 1 -p 2 + E(M • S) = (p 2 -1)(p 1 p 2 v 2 + (u + 1 -2p 1 )v + p 1 -1) = (p 1 -1)(p 2 -1)(-uv(p 1 + 1) -v + 1) = 24r(-uv(p 1 + 1) -v + 1) = -24rθ 1 (0) so that C 2,0 • S = φ -2θ 1 (0) C 1,0 . When p 2 = 2, the exponent of ζ 24 becomes -1 + E(M • S) = (p 1 -1) u 2 p 1 p 1 + 1 2 + 1 -u 2 ,
so that the final answer is φ Proof:

-θ 1 (0)+ u 2 p 1 p 1 +1 2 + 1-u 2 C 1,0 .
(i) When p = 2:

A ν • S = √ p ρ p η(pz) 2 η(z)η(z + ̟/p) ζ -ρ 2 p̟+(-3 p+2+w)ρ+p̟-3+3 p 24 = √ p -̟ p 1/ √ pε(̟)ζ -θ(̟) 24 C ̟ ζ -ρ 2 p̟+(-3 p+2+w)ρ+p̟-3+3 p 24 = ζ -ρ 2 p̟+(-3 p+2+w)ρ+p̟-3+3 p-θ(̟) 24 C ̟ = C ̟ using θ(̟) = p̟ (1 -ρ 2 ) + (-3 p + 2 + w) ρ -3 + 3 p.
When p = 2, ρ = 1 implying ̟ = w = 1 and

A 2 • S = √ 2ζ w-1 24 η(2z) 2 η(z)η(z + ̟/2) = ζ -θ(2) 24 C 1 = C 1 .
(ii) In all cases, we get

C ν • S = η((z + pµ)/p) 2 η(z + pµ)η((z + pµ)/p 2 ) = A µp .

Finding invariant functions

The idea is simple. Using the explicit actions given above, we need to find suitable modifications of the functions B, A ν , C 1,ν , C 2,ν such that the action of T and S on any power sum coincides with the action on γ 2 , γ 3 or the product γ 2 γ 3 , as given in Section 4.3.

Note that B e • T = ζ -24re 24 B e . Write re = t/δ and remark that this fraction is irreducible (s being prime to t implies δ is). This leads to set χ = φ -e = ζ -24re 24 = ζ -t δ , a primitive δ-th root of unity.

The aim of this Section is to prove the following Theorem from which Theorem 4.1 will follow.

Theorem 4.6 Assume we are in the conditions of Theorem 4.1. Define the functions

A ′ ν = χ α 0 -ν A e ν , B ′ = B e ; C ′ 1,ν = χ θ 1 (ν)-ν C e 1,ν , C ′ 2,ν = χ θ 2 (ν)-ν C e 2,ν ; C ′ ν = χ µ C e ν ,
where µ ≡ -1/ν mod p and

α 0 =    1 if δ = 2, 0 if δ = 3, 3 if δ = 6, making χ α 0 = (-1) δ+1 = χ -α 0 = χ -3 .
Then, for all integers k, the quantity

S k = B ′ k + N -1 ν=0 A ′ ν k + p 1 -1 ν=0 C ′ 1,ν k + p 2 -1 ν=0 C ′ 2,ν k = B ′ k + S A,k + S C 1 ,k + S C 2 ,k satisfies S k • (T, S) = (χ k , χ α 0 k )S k .
With these notations, we have Proposition 4.7 The following hold: (a)

B ′ • T = χB ′ . (b) {A ′ ν } ν • T = {χA ′ ν } ν . (c) {C ′ i,ν } ν • T = {χC ′ i,ν } ν . (d) For all ν, C ′ ν • T = χC ′ ν .
Proof: (a) and (c) follow easily from Proposition 4.3. (b) We first obtain A e N -1 • T = χA e 0 . Let us explain how the choice A ′ ν comes from. For some function α to be precised later, let us put A ′ ν = χ α(ν) A e ν , for which C ′ ν . A glance at Table 2 shows that p 2 -1 ≡ 0 mod (24/e), which implies 2e(p -1) ≡ -(p -1) 2 e mod 24 and therefore ζ 2e(p-1) 24 = χ. The actual value of α is in fact dictated by the other invariance properties that follow.

A ′ ν • T = χ α(ν) A e ν+1 = χ α(ν)-α(ν+1) A ′ ν+1 , A ′ N -1 • T = χ α(N -1) χA e 0 = χ α(N -1)+1-α(0) A ′ 0 . We must find α s.t. α(ν) -α(ν + 1) ≡ 1 mod δ, 0 ≤ ν < N -1,
Remark. This proposition shows at the same time that we cannot expect some nice T -action when N ≡ 1 mod δ.

Let us turn our attention to the S-action on our candidate functions, using the notations of Proposition 4.4.

Proposition 4.8 (i) (B ′ , A ′ 0 ) • S = χ α 0 (A ′ 0 , B ′ ). (ii) When gcd(ν, p 1 p 2 ) = 1, A ′ ν • S = χ α 0 A ′ ω . (iii) For ν = p 1 ρ, A ′ ν • S = χ α 0 C ′ 2,̟ . (iv) For 1 ≤ ν < p 2 , µ ≡ -1/(νp 1 ) mod p 2 and C ′ 2,ν • S = χ α 0 A ′ µp 1 . (v) C ′ 2,0 • S = χ α 0 C ′ 1,0 . (vi) For ν = ρp, 1 ≤ ρ < p, set 1 = -̟ρ + wp. For all p, A ′ ν • S = χ α 0 C ′ ̟ . (vii) For 1 ≤ ν < p, setting µ ≡ -1/ν mod p, we have C ′ ν • S = χ α 0 A ′ µp .
Proof:

(i) We have B ′ • S = χ -α 0 A ′ 0 ; A ′ 0 • S = χ α 0 B ′
and the result follows from χ -α 0 = χα 0 . (ii) Proposition 4.4 can be rewritten

A ′ ν • S = χ ω-ν-θ 3 (ν) A ′ ω
and we simplify the exponent using 1 = -ων + v 12 mod δ, which leads to:

A ′ ν • S = A ′ ω χ -3 if p 2 = 2, χ ν(-3+v 12 (2p 1 -1)) if p 2 = 2.
When p 2 = 2, we use χ -3 = χ α 0 . The p 2 = 2 can occur only for δ = 3, in which case p 1 ≡ -1 mod 3 and the exponent is χ is 0.

(iii) For ν = ρp 1 : we use 1 = -̟ν + wp 2 to get

A e ν • S = χ -θ 4 (ρ) C e 2,̟ or χ -α 0 +ν A ′ ν • S = χ -θ 4 (ρ) χ ̟-θ 2 (̟) C ′ 2,̟
and we need simplify:

-θ 4 (ρ) -θ 2 (̟) + α 0 + ̟ -ν.
Using the definition of θ 4 , we get

A ′ ν • S = C ′ 2,̟ χ α 0 -ρ((p 2 +1)w+p 1 +1) if p 2 = 2, χ α 0 -ρ (3 p 1 +1 2 )ρ+p 1 +3w-2 if p 2 = 2.
and we conclude using p i ≡ -1 mod δ.

(iv) For 1 ≤ ν < p 2 , we compute µ ≡ -1/(νp 1 ) mod p 2 and

C ′ 2,ν • S = χ θ 2 (ν)-ν A e µp 1 = χ θ 2 (ν)-ν-α 0 +µp 1 A ′ µp 1 .
Simplifying the exponent gives

C ′ 2,ν • S = A ′ µp 1 χ -α 0 +µ((p 2 +1)v 2 +p 1 +1) if p 2 = 2, χ -α 0 +4p 1 +1 if p 2 = 2.
where for p 2 = 2, we used ν = µ = 1. We conclude as in (iii).

(v) When p 2 = 2, we start from

C e 2,0 • S = χ 2θ 1 (0) C e 1,0 from which χ -θ 2 (0) C ′ 2,0 • S = χ θ 1 (0) C ′ 1,0 or C ′ 2,0 • S = χ θ 1 (0)+θ 2 (0) C ′ 1,0
and the exponent is

uv(p 1 + p 2 + 2) + u + v -2.
This quantity is ≡ u + v -2 mod δ since p i ≡ -1 mod δ. Moreover 1 ≡ p 1 (u + v) mod δ and finally the exponent is -3 mod δ.

When p 2 = 2, we have

χ -θ 2 (0) C ′ 2,0 • S = χ -u 2 p 1 p 1 +1 2 + 1-u 2 C ′ 1,0 or C ′ 2,0 • S = χ -(p 2 1 +p 1 -3)u 2 -3 2
C ′ 1,0 , and this is χ 0 since this can only happen when δ = 3.

(vi) Since 1 = -̟ρ + wp, we can write

A ′ ν • S = χ α 0 -ν-κ(̟) C ′ ̟ .
and the result comes from the definition of κ.

(vii) C e ν • S = A e µp or C ′ ν • S = χ κ(ν) χ -α 0 +µp A ′
µp , and we conclude as in (vi).

Properties of the modular equation

From the preceding sections, we see that

Φ(F ) = (F -B ′ ) N -1 ν=0 (F -A ′ ν ) p 1 -1 ν=0 (F -C ′ 1,ν ) p 2 -1 ν=0 (F -C ′ 2,ν )
is a modular equation whose coefficients can be expressed in terms of j, γ 2 or γ 3 depending on the value of δ. Before doing this, we may express these coefficients as Puiseux series.

Proposition 4.9 With the usual notations: (a) the coefficient of smallest order of Φ is q -2re ; (b) the trace has order re;

(c) when p 1 = p 2 , Φ(0) = 1; (d) when p 1 = p 2 = p, Φ (0)
= (-p) e(p-1)/2 when p is odd and 2 4 when p = 2.

Proof: (a) the coefficient of smallest order comes from the coefficient of F ψ(N )-N -1 which has the order of

B ′ N -1 ν=0 A ′ ν or -re + N -1 ν=0 -re N = -2re. When p 1 = p 2 , ψ(N ) -N -1 = p 1 + p 2 ; when p 1 = p 2 = p, this is p -1.
Note that all other terms have orders stricly less than this bound.

As an example, when s = e, the degree of the equation in J is 2rs and the corresponding term is J 2rs F ψ(N )-N -1 . Moreover

B ′ N -1 ν=0 A ′ ν = N -1 ν=0 χ α 0 -ν ζ -reN (N -1)/2 N q -2re (1 + • • • ) = χ N α 0 -N (N -1)/2 ζ -24reN (N -1)/2 24N q -2re (1 + • • • ) = χ α 0 -N (N -1)/2 ζ -24reN (N -1)/2 24N q -2re (1 + • • • ), using N ≡ 1 mod δ.
When N is odd, this reduces to

χ α 0 -N (N -1)/2+(N -1)/2 q -2re (1 + • • • ) = χ α 0 -(N -1) 2 /2 q -2re (1 + • • • ).
(b) The dominant term in the sum of the conjugates is that of B ′ , namely q -re .

(c) For p 1 = p 2 :

p 2 -1 ν=0 C ′ 2,ν = p 2 -1 ν=0 χ θ 2 (ν)-ν χ -θ 2 (ν) ε e 2 ζ νre p 2 q er/p 2 (1 + • • • ) = χ -p 2 (p 2 -1)/2 ε p 2 e 2 ζ rep 2 (p 2 -1)/2 p 2 q er (1 + • • • ).
Multiplying all together, we find the norm to be of valuation 0, hence a constant

ϑ = χ α 0 -N (N -1)/2 ζ -24reN (N -1)/2 24N χ -p 1 (p 1 -1)/2 ε p 1 e 1 ζ rep 1 (p 1 -1)/2 p 1 χ -p 2 (p 2 -1)/2 ε p 2 e 2 ζ rep 2 (p 2 -1)/2 p 2 = (ε p 1 1 ε p 2 2 ) e χ α 0 -N (N -1)/2-p 1 (p 1 -1)/2-p 2 (p 2 -1)/2 ζ -24reN ((N -1)/2-(p 1 +p 2 -2)/2) 24N
.

When p 2 = 2 (with p 1 odd), we have δ = 3 always, meaning α 0 = 0 and N ≡ 1 mod 3. Therefore, noting that e is always even:

ϑ = 2 p 1 p 1 e χ 1 ζ -24reN (p 1 -1)/2 24N = χ (p 1 +1)/2 = 1 since p 1 ≡ -1 mod 3.
When p 2 = 2, both p i being odd, we may use the quadratic reciprocity law to find

ϑ = (-1) e(p 1 -1)(p 2 -1)/4 χ α 0 -N (N -1)/2-p 1 (p 1 -1)/2-p 2 (p 2 -1)/2 ζ -24reN ((N -1)/2-(p 1 +p 2 -2)/2) 24N
.

Since p 1 + p 2 -2 is even, we obtain

ϑ = ζ 3(24re) 24 χ α 0 -N (N -1)/2-p 1 (p 1 -1)/2-p 2 (p 2 -1)/2+(N -1)/2-(p 1 +p 2 -2)/2 = χ α 0 -3-N (N -1)/2-p 1 (p 1 -1)/2-p 2 (p 2 -1)/2+(N -1)/2-(p 1 +p 2 -2)/2 = χ -N (N -1)/2-p 1 (p 1 -1)/2-p 2 (p 2 -1)/2+(N -1)/2-(p 1 +p 2 -2)/2 ,
and by inspection, this is always 1.

(d) When p 1 = p 2 = p, we get

p-1 ν=1 C ′ ν = p-1 ν=1 χ κ(ν) p e/2 ε(ν) e ζ eθ(ν) 24 ζ -eν 24p q e(p-1)/12 (1 + • • • ) = χ p(p-1)/2 p e(p-1)/2 p-1 ν=1 ε(ν) e ζ e p-1 ν=1 θ(ν) 24 ζ -ep(p-1)/2 24p q 2er (1 + • • • ).
The quantity p-1 ν=1 ε(ν) is 1 for p = 2; when p is odd since p 2 ≡ 1 mod 24 and the fact already used that χ α 0 = χ -3 .

Computing the modular equations using series expansions

There a variety of methods to compute the modular equations. For large computations, it is possible to use suitably modified versions of [START_REF] Enge | Computing modular polynomials in quasi-linear time[END_REF] or [START_REF] Bröker | Modular polynomials via isogeny volcanoes[END_REF]. Also, we can use resultants in the same spirit as in the remark at the end of Section 3, noting that w s p 1 ,p 2 = (w p 1 (z)/w p 1 (z/p 2 )) s . Here, we content ourselves to use series expansions and nice formulas that can help us for small cases. Also, this will add new properties to our equations.

Looking carefully at the expression for S k , we see that the terms in C 1 , C 2 or C cannot contribute to the modular equation, since they have positive order. Therefore, we need only consider the expansions of B ′ k and S A,k . Doing this, we see that the useful terms for S A,k are for j ≤ -ktN ′ /N . Since B ′ k = q -rek (1+• • • ) and 1 ≤ k ≤ ψ(N ). We need at least reψ(N ) terms in the last coefficient. Since B ′ is the product and quotient of very sparse series, it might be worthwhile to compute its powers by successive applications of special routines handling this kind of computations. It is possible to compute nice formulas for the S A,k , in the spirit of the ones to come, but we do not need them.

A second algorithm consists in grouping

Φ(F ) = P B (F )P A (F )P C 1 (F )P C 2 (F )
and to compute P A (resp. P C 1 and P C 2 ) via its power sums that are given in the preceding propositions.

Inspired by the approach of section 3.2, the third algorithm uses the reciprocal polynomial, whose powers sums will depend on the C ′ 1,ν and C ′ 2,ν only:

Σ k = p 2 -1 ν=0 1 C ′ 2,ν k + p 1 -1 ν=0 1 C ′ 1,ν k ,
which is a process involving p 1 + p 2 . We will prove two useful results (propositions 4.10 and 4.11 below) to help us compute these quantities.

Proposition 4.10 For all integers k = 0,

S C 2 ,k = p 2 ε ke 2 q kt/δ j≥ktp ′ 2 /p 2 c k,jp 2 -ktp ′ 2 q j ,
where (p 2 + 1)/δ = p ′ 2 and the c k,i are explicitly given in the proof.

Proof: put w = q 1/p 2 , ζ = ζ p 2 and write

η (p 1 z) η z p 2 η(z)η p 1 z p 2 = w p 1 p 2 /24 (1 + ∞ i=1 a i w p 1 p 2 i ) w 1/24 (1 + ∞ i=1 a i w i ) w p 2 /24 (1 + ∞ i=1 a i w p 2 i ) w p 1 /24 (1 + ∞ i=1 a i w p 1 i ) = w r C 12 (w) with C 12 (q) = 1 + • • • ∈ Z[[q]
] (which is symmetrical in p 1 and p 2 ), from which

C ′ 2,ν = χ θ 2 (ν)-ν χ -θ 2 (ν) ε e 2 (wζ ν ) re C 12 (wζ ν ) e . and S C 2 ,k = ε ke 2 w kre p 2 -1 ν=0 χ -kν ζ kreν C 12 (wζ ν ) ek . Writing C 12 (w) ek = ∞ i=0 c k,i w i (remark this is valid irrespective of the sign of k), the inner sum becomes ∞ i=0 c k,i w i p 2 -1 ν=0 (χ -k ζ kre+i ) ν , in which the root of unity is χ -k ζ kre = ζ 24kre 24 ζ kre = ζ 24krep 2 +24kre 24p 2 = ζ 24kre(p 2 +1) 24p 2
. Now, we use the fact that p 2 ≡ -1 mod δ, so that re(p 2 + 1) = tp ′ 2 where p ′ 2 = (p 2 + 1)/δ. The above sum is now

∞ i=0 c k,i w i p 2 -1 ν=0 ζ ktp ′ 2 +i ν = p 2 ∞ i≡-ktp ′ 2 mod p 2 c k,i w i = p 2 w -ktp ′ 2 j≥ktp ′ 2 /p 2 c k,jp 2 -ktp ′ 2 q j .
leading to the result.

Proposition 4.11 In case p 1 = p 2 = p, for all k = 0,

S C,k ∈ q -1/24 η(pz) 2 η(z) ek Z[[q]] = q Kk/δ Z[[q]],
where all series are explicited in the proof.

Proof: One uses ζ = ζ p in S C,k = p ek/2 η(pz) 2 η(z) ek p-1 ν=1 ε(ν) ek χ kκ(ν) ζ ekθ(ν) 24 η(z + ν/p) ek = p ek/2 η(pz) 2 η(z) ek p-1 ν=1 ε(ν) ek q -ek/24 ζ -ekν/24 χ kκ(ν) ζ ekθ(ν) 24 (1 + ∞ i=1 a i q i ζ iν ) ek = p ek/2 q -1/24 η(pz) 2 η(z) ek p-1 ν=1 ε(ν) ek χ kκ(ν) ζ ekθ(ν) 24
ζ -ekν/24 C(qζ ν ) ek where C(q) = 1 1 + ∞ i=1 a i q i . Writing C(q) ek = ∞ i=0 c k,i q i (same remark on the sign of k), the inner sum of the preceding relation is now

p-1 ν=1 ε(ν) ek χ kκ(ν) ζ ekθ(ν) 24 ζ -ekν/24 ∞ i=0 c k,i (qζ ν ) i = ∞ i=0 c k,i q i p-1 ν=1 ε(ν) ek χ kκ(ν) ζ ekθ(ν) 24 (ζ -ek/24 ζ i ) ν . (3)
Let's treat the case p = 2 first, with e = 8. We get

S C,k = 2 4k q -1/24 η(2z) 2 η(z) 8k ∞ i=0 c k,i q i (ζ -k 2 ζ i 2 ) = (-2 4 ) k q -1/24 η(2z) 2 η(z) 8k ∞ i=0 c k,i (-q) i .
For p odd, the root of unity in the inner sum of (3) is

ε(ν) ek ζ ek(p(-(p-1) 2 κ(ν)+θ(ν))-ν) 24p (ζ i ) ν , the exponent of ζ 24p being p(-(p -1) 2 µ + pν (1 -µ 2 ) + (-3 p + 2 + v) µ -3 + 3 p) -ν.
When p = 3 and e = 3, we find

ζ k(-32 µ+8 ν-8 ν µ 2 +18) 24 = (ζ -16 µ+4 ν-4 ν µ 2 +9 12 ) k = (ζ 3 4 • ζ ν 3 ) k , leading to S C,k = 3 3k/2 ζ 3k 4 q -1/24 η(3z) 2 η(z) 3k ∞ i=0 c k,i q i 2 ν=1 ε(ν) k (ζ i+k 3 ) ν .
When k is even, this boils down to

S C,k = (-3) 3k/2 q -1/24 η(3z) 2 η(z) 3k   2 i≡-k mod 3 c k,i q i - i ≡-k mod 3 c k,i q i   = (-3) 3k/2 q -1/24 η(3z) 2 η(z) 3k 3 i≡-k mod 3 c k,i q i - ∞ i=0 c k,i q i . When k is odd S C,k = 3 3k/2 ζ 3k 4 q -1/24 η(3z) 2 η(z) 3k ∞ i=0 c k,i q i 2 ν=1 ε(ν) k (ζ i+k 3 ) ν 20 and 2 ν=1 ε(ν) k (ζ i+k 3 ) ν = -ζ i+k 3 + ζ 2(i+k) 3 = 0 if i + k ≡ 0 mod 3, (-1) (i+k) mod 3 √ -3 otherwise, from which S C,k = (-3) (3k+1)/2 q -1/24 η(3z) 2 η(z) 3k ∞ i+k ≡0 mod 3
(-1) (i+k) mod 3 c k,i q i .

When p > 3, we get q -1/24 η(pz) 2 η(z

) ek   p ∞ i+ekp ′ ≡0 mod p c k,i q i - ∞ i=0 c k,i q i   .
When k is odd, remarking that e is always odd from Table 2, the sum is now S C,k = p ek/2 ζ ek(p-1) 8

q -1/24 η(pz) 2 η(z)

ek ∞ i=0 c k,i q i p-1 ν=1 ε(ν)(ζ i+ekp ′ p ) ν .
But p-1 ν=1 ε(ν)(ζ i+ekp ′ p ) ν = 0 when i + ekp ′ ≡ 0 mod p since there are the same number of quadratic residues and non-quadratic residues modulo p. When i + ekp ′ ≡ 0 mod p, ζ i+ekp ′ p is a primitive p-th root of unity. Remember that [START_REF] Ireland | A classical introduction to modern number theory[END_REF]Ch. 6] x residue ζ x p -

x non residue

ζ x p = -1 p p.
Let g be a generator of (Z/pZ) * . If u is an integer, then = (-1) (3+ek(p-1)/2)/2 . As a last point, the dominant term of S C,k is q ke(p-1)/12 . When p = 2 and e = 8, this is 2k/3, whereas re = 1/3; when p = 3, e = 3, we get k/2, whereas re = 1/2. For p > 3, we have e = 1 and we compare (p -1)/12 and re = (p -1)/2 • (p -1)/12. Looking at the valuation of 2 and 3, we deduce that re = t/δ and (p -1)/12 = p ′ /δ.

Conclusion

We have studied modular equations involving γ 2 and γ 3 for double η-quotients. As a result, more compact modular equations can be stored and used, with application to the SEA algorithm (see for instance [START_REF] Morain | Calcul du nombre de points sur une courbe elliptique dans un corps fini : aspects algorithmiques[END_REF]), or CM computations, as motivated for instance by [START_REF] Rubin | Choosing the correct elliptic curve in the CM method[END_REF] (see [START_REF] Morain | Implementations notes concerning the Rubin-Silverberg algorithms[END_REF]).

It seems natural to conjecture that more general functions can exhibit the same properties. Experiments can be conducted on Newman functions, using for instance the resultant approach, leading to new instances of the theorems. This will described in another article.

Theorem 2 . 1

 21 (a) Any function invariant by T and S is a rational function of j. (b) Any function f satisfyingf • T = -f and f • S = -f is equal to γ 3 times a rational function of j. (c) Any function f satisfying f • T = ζ ∓1 3 f and f • S = f is equal to γ ±1 2 times a rational function of j. (d) Any function f satisfying f • T = -ζ ∓1 3 f and f • S = -f is equal to γ 3 γ ±12times a rational function of j. (Note that -ζ ∓1 3 = ζ ±1 6 .)

Proposition 4 . 5

 45 We suppose that p 1 = p 2 = p. Then (i) When ν = ρp, 1 ≤ ρ < p, set 1 = -̟ρ + wp. Then A ν • S = C ̟ .(ii) For all p, and all 1 ≤ ν < p, one has C ν • S = A µp where µ ≡ -1/ν mod p.

and α(N - 1 )

 1 α(0) + 1 ≡ 1 mod δ. The first set of equations gives us α(ν) ≡ α(0)-ν mod δ and the second α(0)-(N -1) ≡ α(0) mod δ, which is possible only when N ≡ 1 mod δ. Setting α 0 = α(0) yields the result. (d) Proposition 4.7 gives us C ′ ν • T = ζ 2e(p-1) 24

1 - 1 ν=1-pνµ 2 1 ν=1pµ( 1 - 2 .

 112112 using Wilson's theorem.When p = 2, e = 8, δ = 3, we findϑ = χ α 0 -N (N -1)/2 ζ -24reN (N -1)/2 24N χ p(p-1)/2 p e(p-1)/2 ζ µ 2 ) + (-3p + 2 + v)µ -3 + 3p = (p -3p + 2)S 0 + 3(p -1) 2 + p-+ vµwhere S 0 = p-1 ν=1 ν. Using 1 = -µν + vp, the sum becomespvp) + vµ = p-1 ν=1 µ(pvp 2 + v) ≡ pS 0 mod 24in all cases: when p > 3, p 2 ≡ 1 mod 24; when p = 3, ν = 1 (resp. ν = -1) leads to µ = -1, v = 0 (resp. µ = 1, v = 0). Therefore, the exponent of ζ 24 is ≡ e(-(p -1)/2 + (-p + 2)S 0 + 3(p -1) 2 ) ≡ -e(p -7)(p -1) 2 /2 mod 24, p-1)/2 χ α 0 +(N -1)/2-N (N -1)/2+p(p-1)/2+(p-7)/2 = -1 p e p e(p-1)/2 χ α 0 -(p 4 -3p 2 -8)/For instance, when p = 3, e = 3, δ = 2, we find ϑ = (-1)3 3 (-1) 1-31 = -3 3 . More generally, as soon as p > 3, ϑ = -1 p e p e(p-1)/2 χ α 0 -3 = -1 p e p e(p-1)/2

1 ).∞

 1 2 µ+pν (1-µ 2 )+(-3 p+2+v)µ-3+3 p 24) ek (ζ -ek+24i 24p ) ν = ζ (ν-ν µ 2 -µ+3)p+µ v-3 Write p 2 -1 = 24p ′ to obtain ζ ek(p-1) 8 (ζ ekp ′ +i p ) ν . When k is even, this gives S C,k = p ek/2 ζ ek(p-1) 8 q -1/24 η(pz) 2 η(z) i+ekp ′ ≡0 mod p c k,i q i -i+ekp ′ ≡0 mod p c k,i q i

8 p 2 = (- 1 )

 821 ekp ′ ≡ 0 mod p, we set Ω(i + ekp ′ ) = u such that g u ≡ i + ekp ′ mod p. Then (ek+1)/2 q -1/24 η(pz) 2 η(z) ek ∞ i=0,i+ekp ′ ≡0 mod p (-1) Ω(i+ekp ′ ) c k,i q i .When p ≡ 1 mod 4, the first terms simplify to ζ ek(p-1)/4 (p-1)/4 ; when p ≡ 3 mod 4, we get -ζ

4. 7 2 F

 72 Tables of equations for double η-quotientsΦ[w 8 2,2 ](F, G 2 ) = F 6 -G 2 F 5 + 208 F 3 + 31 G 2 F 2 + G 2 + 16, Φ[w 3 3,3 ](F, G 3 ) = F 12 -G 3 F 11 -522 F 10 + 27 G 3 F 9 -10557 F 8 -162 G 3 F 7 -14076 F 6 -18 G 3 F 5 -9801 F 4 + 163 G 3 F 3 + (486 -G 2 3 )F 2 -9 G 3 F -27. Φ[w 3,7 ](F, G 3 ) = F 32 -G 3 F 31 -514 F 30 +21 G 3 F 29 -12585 F 28 -147 G 3 F 27 -25158 F 26 +322 G 3 F 25 -5103 F 24 +378 G 3 F 23 +80556 F 22 -1638 G 3 F 21 -21994 F 20 -28136 F 18 +1620 G 3 F 17 +25650 F 16 -252 G 3 F 15 -3944 F 14 -322 G 3 F 13 -14938 F 12 + 22 G 3 F 11 -(G 2 3 -2940)F 10 -10 G 3 F 9 + 1953 F 8 +G 3 F 7 -462 F 6 + 7 G 3 F 5 + 15 F 4 -G 3 F 3 -10 F 2 + 1.

Table 2 :

 2 Theorem 4.1 Let p 1 , p 2 be two primes, N = p 1 p 2 , s = 24/ gcd(24, (p 1 -1)(p 2 -1)), e = s a divisor of s and δ = s/e. If N ≡ 1 mod δ and the parameters are chosen in Table 2, then there exists a modular equation Φ[(-1) δ+1 w e p 1 ,p 2 ] whose coefficients are rational functions in γ 3 , γ 2 . Values of p 1 and p 2 leading to a modular equation Φ[(-1) δ+1 w e p 1 ,p 2 ].

	p 1	p 2	s e δ
	2	2	24 8 3
	2	5 mod 12	6 2 3
	2	11 mod 12 12 4 3
	3	3	6 3 2
	3	7 mod 12	2 1 2
	3	11 mod 12 6 3 2
	5 mod 12 5 mod 12	3 1 3
	5 mod 12 11 mod 12 3 1 3
	7 mod 12 7 mod 12	2 1 2
	7 mod 12 11 mod 12 2 1 2
	11 mod 12 11 mod 12 6 1 6


Nicolas Tabareau
email: nicolas.tabareau@inria.fr

Aspect-Oriented Programming: a language for 2-categories

Keywords: category theory, aspect-oriented programming, lambda-calculi category theory, aspect-oriented programming, lambda-calculi

Aspect-Oriented Programming (AOP) started ten years ago with the remark that modularization of so-called crosscutting functionalities is a fundamental problem for the engineering of large-scale applications. Originating at Xerox PARC, this observation has sparked the development of a new style of programming featured that is gradually gaining traction, as it is the case for the related concept of code injection, in the guise of frameworks such as Swing and Google Guice. However, AOP lacks theoretical foundations to clarify this new idea. This paper proposes to put a bridge between AOP and the notion of 2-category to enhance the conceptual understanding of AOP. Starting from the connection between the λ-calculus and the theory of categories, we propose to see an aspect as a morphism between morphisms-that is as a program that transforms the execution of a program. To make this connection precise, we develop an advised λ-calculus that provides an internal language for 2-categories and show how it can be used as a base for the definition of the weaving mechanism of a realistic functional AOP language, called MinAML. Finally, we advocate for a formalization of more complex AOP languages (eg. with references or exceptions) using the notion of enriched Lawvere theories.

Introduction

Aspect-Oriented Programming Aspect-Oriented Programming (AOP) [START_REF] Kiczales | Aspect-Oriented Programming[END_REF] promotes better separation of concerns in software systems by introducing aspects for the modular implementation of crosscutting concerns. Indeed, AOP provides the facility to intercept the flow of control in an application and perform new computations. In this approach, computation at certain execution points, called join points, may be intercepted by a particular condition, called pointcut, and modified by a piece of code, called advice, which is triggered only when the runtime context at a join point meets the conditions specified by a pointcut. Using aspects, modularity and adaptability of software systems can be enhanced. In the AOP terminology, the algorithm that controls which aspects can be executed at each join point is called a weaving algorithm.

Much of the research on aspect-oriented programming has focused on applying aspects in various problem domains and on integration of aspects into fullscale programming languages such as Java. However, aspects are very powerful and the development of a weaving mechanism becomes rapidly a very complex task. While some research efforts [START_REF] Jagadeesan | A calculus of untyped aspectoriented programs[END_REF][START_REF] Walker | A theory of aspects[END_REF][START_REF] Wand | A semantics for advice and dynamic join points in aspect-oriented programming[END_REF] have made significant progress on understanding some of the semantic issues involved, the algebraic explanation of aspect features has never reached the beauty and simplicity of the connection between the λ-calculus and cartesian closed categories. We believe that this is the main reason why AOP never found its place in theoretical computer science fields.

Giving a precise meaning to aspects in AOP is a fairly complicated task because the definition of a single piece of code can have a very rich interaction with the rest of the program, whose effect can come up at anytime during the execution. The main purpose of this paper is to formalize this interaction. Namely, we propose to put a bridge between AOP and the notion of 2-category. Starting from the connection between the λ-calculus and category theory, we propose to see an aspect as a 2-cell, that is as a morphism between morphisms. In the programming point of view, this means that an aspect can be seen as a program which transforms the execution of programs.

In this perspective, a weaving algorithm that defines the interaction of a collection of aspects with a given program will be understood as the computation of a normal form in the underlying 2-category of interest. Thus, an algorithm that is usually defined by hand and described coarsely in AOP systems becomes here a basic notion of rewriting theory.

The definition of an internal language for cartesian closed 2-category will be the keystone of this paper, the basis to give a precise meaning to the possible interactions of a single aspect with the rest of the code.

λ-calculus and cartesian closed categories Category theory and programming languages are closely related. It is now folklore that the typed λ-calculus is the internal language of cartesian closed categories. In this paradigm, objects of the category correspond to types in the typed λ-calculus and morphisms between objects A and B of the category correspond to λ-terms of type B with (exactly) one free variable of type A. The composition of morphisms corresponds to substitution, a notion that is at the heart of β-reduction-the fundamental rule of the λ-calculus.

This interpretation of the λ-calculus started in the early 80's from the work of John Lambek and Philip Scott [START_REF] Lambek | Cartesian closed categories and typed lambda-calculi[END_REF][START_REF] Lambek | Introduction to higher order categorical logic[END_REF][START_REF] Scott | Some aspects of categories in computer science[END_REF]. Soon later, Robert Seely proposed a 2-categorical interpretation of the λ-calculus [START_REF] Seely | Modelling computations: a 2-categorical framework[END_REF] where β-reduction constructs 2-cells between terms and their β-reduced version. This perspective is in line with the thought that 2-cells can be seen as rewriting rules between morphisms (or terms). This idea has been pushed further by Barnaby Hilken in [START_REF] Hilken | Towards a proof theory of rewriting: the simply typed 2λcalculus[END_REF] where he developed a 2-dimensional λ-calculus that corresponds to the free 2-category with lax exponentials.

Recall that a 2-category C is basically a category in which the class C(A, B) of morphisms between any objects A and B is itself a category. In other words, a 2-category is a category in which there exists morphisms

f : A → B
between objects , and also morphisms α : f ⇒ g between morphisms. The morphisms f : A → B are called 1-cells and the morphisms α : f ⇒ g are called 2-cells.

Seely's interpretation shows how typed λ-calculus can naturally be viewed as a 2-category. In this paper, we define an advised λ-calculus extending the typed λ-calculus with 2-dimensional primitives that enable to describe any 2-cell of a cartesian closed 2-category. Those additional primitives construct a kind of 2-dimensional terms that we will (by extension) call aspects. The resulting language, called λ 2 -calculus, defines an internal language for cartesian closed 2-category and will be the base of our explanation of aspects in AOP.

AOP and 2-categories

The keystone of this paper is to consider aspects in AOP as 2-cells in a 2-category just as functions (more precisely λ-terms) are interpreted as morphisms in a category. But this simple idea raises interesting and difficult issues:

• What is the good notion of variables at a 2-dimensional level?

• What is the extended notion of β-reduction?

• How to describe vertical and horizontal composition of a 2-category in the language of typed λ-calculi?

Once this effort to develop an internal language for cartesian closed 2-categories has been done, it becomes simpler to describe the interaction of an aspect with the rest of a program. Indeed, the 2-dimensional constructors of the λ 2 -calculus enable to faithfully describe all situations in which an aspect can be applied to a given program.

Let us anticipate on the description of the λ 2 -calculus to give an example straightaway. Suppose that we have defined an aspect α : sqrt ⇒ sqrt • abs which rewrites all calls to a square root function to ensure that inputs are nonnegative. This aspect can be seen as a piece of advice whose pointcut intercepts the square root function and proceeds with the absolute value of the original argument of the function. The effect of α on the program p = λx. sqrt(sqrt(x)) will be described by the composed 2-cell

β = λX. α • α • X : p ⇒ p that transforms the program p into the program p = λx. sqrt(abs(sqrt(abs(x)))).
The aspect β is automatically generated from the aspect α and constructors of the λ 2 -calculus. Note that one could argue that this violates one of the primary design goals of AOP, which is to allow separation of cross-cutting concerns. Indeed, each aspect is monomorphic in the sense that the aspect β in the example above is specific to the program p. It could seem unfortunate as an important goal of AOP languages is that the aspect may be oblivious to the target program -in 2-categorical/λ-calculus terms what seems needed is naturality/parametricity in the scaffolding. However, this is not the point of view adopted in the λ 2 -calculus. The idea is that a single definition of the aspect α above will generate all the possible combinations of this aspect with 2-dimensional primitives of the language and other constant aspects.

Of course, existing AOP languages do not look like the λ 2 -calculus so we show how programs of a simple functional language with aspects, introduced by David Walker and colleagues in [START_REF] Walker | A theory of aspects[END_REF] and called MinAML, can be translated into the λ 2 -calculus. As claimed above, the semantics of such programs is provided by a weaving algorithm that corresponds to the computation of a normal form in the underlying 2-category.

At the end of this article, we explain how this algebraic account of AOP can drive the definition of aspects in more powerful languages extended with references, exceptions or any programming primitives that are well-understood in category theory. This could be done by using a 2-categorical version of computational monads introduced by Eugenio Moggi [START_REF] Moggi | Notions of computation and monads[END_REF]-and used for example in Haskell-to extend the λ 2 -calculus smoothly. This 2-categorical extension can be seen as a particular case of the recent work of Martin Hyland, Gordon Plotkin and John Power on enriched Lawvere theories [START_REF] Hyland | Combining effects: sum and tensor[END_REF].

Note that the work of Kovalyov [START_REF] Kovalyov | Modeling Aspects by Category Theory[END_REF] on modeling aspects by category theory is in accordance with the school of category theory for software design. In this paper, category theory is used as a foundational model for programming languages, which is a completely different line of work. About higher order algebras We have identified the higher order notion provided by 2-categories as a suitable setting where programs are interpreted by 1-cells and aspects (or more generally program transformations) are interpreted by 2-cells. At this stage, one could wonder whether it would have been more fruitful to work with other higher order notions in category theory like bicategories or double categories. Both are generalization of 2-categories, the former where the horizontal composition is not strictly associative, the latter where one can distinguish between horizontal and vertical morphisms. We believe that the refinement proposed by bicategories or double categories is not necessary to interpret AOP programs as application is always associative and there is no meaningful distinction between horizontal and vertical programs of a given type.

On the other hand, one could wonder whether a simpler setting such as order-enriched categories would not be sufficient to interpret AOP language and define a weaving algorithm using rewriting theory. It is indeed the case if one consider only "pure" aspects that have no effect on the program. In this case, an aspect is just a program transformation and thus two aspects between the same programs will always be equal. But when aspects can have side effect such as logging on the screen, this is not true anymore and the full power of 2-categories is required (see for example Section 5.2).

Note that most of AOP systems consider aspects that can intercept other aspects. But then, one needs to define some stratification in the flow of execution to control the weaving of aspects. This mechanism can be explained with a notion of execution levels [START_REF] Tanter | Execution levels for aspect-oriented programming[END_REF] that prevents aspects of lower levels to intercept aspects of higher levels of execution. It would be interesting to consider this notion of aspects intercepting aspects through execution levels in the light of n-categories or weak ω-categories. A relation between Martin-Löf Intensional Type Theory and weak ω-categories has recently been settled [START_REF] Garner | Types are weak omega-groupoids[END_REF][START_REF] Lumsdaine | Weak ω-categories from intensional type theory[END_REF] and could be a good basis for the study of execution levels.

Plan of the paper We introduce ( §2) the language of cartesian closed 2category and define the notion of polynomial 2-category. After that, we define ( §3) the λ 2 -calculus, an extension of the λ-calculus with 2-dimensional primitives that will be the basis for the interpretation of aspects. We then show ( §4) that the λ 2 -calculus is an internal language for cartesian closed 2-category and use ( §5) this language to give a formal semantics of a functional AOP language called MinAML. Finally, we conclude ( §6) sketching how this work can serve to study more powerful AOP languages (with references or exceptions) using advanced work on enriched Lawvere theory.

Cartesian closed 2-Categories in a nutshell

In this section, we briefly introduce cartesian closed 2-categories. We also present an extension of the notion of polynomials for 2-category, an extension that will be the base for the connection between the λ 2 -calculus and cartesian closed 2-categories.

A glance at 2-categories

An abstract view on 2-categories is to see them as categories enriched over Cat, the cartesian category of categories (for more details about enriched category theory, see the monograph of Max Kelly [START_REF] Kelly | Basic Concepts of Enriched Category Theory[END_REF]). Even if this point of view will become important at the end of this article, we prefer to give a more concrete definition. A 2-category C has a class of objects (also called 0-cells), usually noted A, B, . . . , a class of morphisms (also called 1-cells) between objects, usually noted f : A → B and a class of morphisms between morphisms (also called 2-cells), usually noted α : (f ⇒ g) :: A → B (or simply α : f ⇒ g when there is no confusion). A 2-cell α : (f ⇒ g) :: A → B is generally diagrammatically represented as a 2-dimensional arrow between the 1-dimensional arrows f and g A g ? ?

f α B .
0-and 1-cells form a category called the underlying category of C -with identity on A denoted by id A and composition of morphisms f and g denoted by g • f . 2-cells may be composed "horizontally" and "vertically". We write

β • α : f • f ⇒ g • g
for the horizontal composite of two 2-cells α : f ⇒ g and β : f ⇒ g , represented diagrammatically as

A g ? ? f α B g ? ? f β C = A g • g ? ? f • f β•α C
and we write α * β : f ⇒ h for the vertical composite of two 2-cells α : f ⇒ g and β : g ⇒ h, represented diagrammatically as

A h D D g / / f β α B = A h ? ? f α * β B .
The vertical and horizontal composition laws are required to define categoriesthey are associative and there are identities

1 f : f ⇒ f for each 1-cell f : A → B.
The identity for the horizontal composition is given by 1 id A , and one requires that

1 g•f = 1 g • 1 f .
Note that the horizontal composition is extended to a composition between a 2-cell α and a 1-cell f by implicitly regarding the 1-cell f as the identity 2-cell 1 f .

There is one remaining law of compatibility between the horizontal and the vertical composition. This law, called the interchange law, guarantees that the two ways of reading the diagram

A h D D g / / f β α B h D D g / / f β α C
are equal. From an AOP point of view, this property guarantees that applications of pieces of advice at disjoint part of a program do not interfere with each other. This means that we can still reason modularly in presence of aspects as long as the transformation deals with disjoint part of the program. The different associativity, unit and interchange laws guarantee a fundamental property of 2-categories: each labelled pasting diagram has a unique composite. From an AOP point of view, this means that the application of a piece of advice (without side effect) at one point of a program must not perturb the application of other pieces of advice at other points of the same program.

Just as a 2-category is a Cat-category, a 2-functor consists of a functor enriched over Cat. In other words, a 2-functor from C to D is a map from i-cells to i-cells (i being 0,1 and 2) that preserves all the structure of a 2-category on the nose. In particular, each 2-functor defines a functor between the underlying categories.

A 2-natural transformation is a Cat-natural transformation, i.e., a natural transformation between the underlying ordinary functors that also respects 2cells.

Cartesian 2-categories

A 2-category C is said to be cartesian when the diagonal 2-functor ∆ n : C → C n has right 2-adjoints for all n. More concretely in a cartesian 2-category, every pair of objects A and B is equipped with two projection morphisms

π 1 : A 1 × A 2 → A 1 π 2 : A 1 × A 2 → A 2 .
satisfying the following universal property: for every pair of 2-cells

α 1 : f 1 ⇒ g 1 : X → A 1 α 2 : f 2 ⇒ g 2 : X → A 2
there exists a unique 2-cells

α 1 , α 2 : f 1 , f 2 ⇒ g 1 , g 2 : X → A 1 × A 2
satisfying the two equalities (where i is either 1 or 2)

X g1,g2 ; ; f1,f2 # # α1,α2 A 1 × A 2 πi / / A i = X gi > > fi αi A i RR n°7527
We also require that C has a particular object 1, called the terminal object, such that there exists a unique 1-cell skip A : A → 1 and 1 skip A : skip A ⇒ skip A is the unique 2-cell of that type.

Observe that the underlying category of a cartesian 2-category is also cartesian (instantiate every 2-cell in the universal property with the identity 2-cell) and that × can be extended to a 2-functor by

α × β = π 1 • α, π 2 • β .
From a λ 2 -calculus point of view, the object 1 is represented by the type Unit and the unique 1-cell of that type is the constant term skip-the 1-cell skip A is interpreted by λx : A. skip. Then, the unique aspect on skip A is the identity aspect.

Closure in a cartesian 2-category

A cartesian 2-category C is closed when the 2-functor (-) × A has a right 2- adjoint (-) A for all objects A of C.
More concretely, a cartesian closed 2-category is equipped with a family of functors

Λ A,B,C : C(A × B, C) → C(B, C A )
and a family of morphisms

eval A,B = A × B A → B such that eval • (1 A × Λ(α)) = α and Λ(eval • (1 A × β)) = β for every 2-cell α : f ⇒ g : A × B → C and β : f ⇒ g : B → C A .
Again, we remark that the underlying category of a cartesian closed 2-category is also cartesian closed.

Polynomial cartesian closed 2-category

To state the connection between cartesian closed 2-category and the λ 2 -calculus, we need define the 2-category C[X] of polynomials over an indeterminate 2-cell

X : (x ⇒ x ) :: 1 → A and indeterminate arrows x, x : 1 → A of a 2-category C. Indeed, a polynomial 2-cell α(X) : (t(x) ⇒ t (x )) :: 1 → B
will be seen as an aspect with one free 2-variable X, and the arrows t(x) and t (x ) will be seen as terms with respective free 1-variables x and x . The objects of C[X] are the same as those of C, the morphisms are formal expressions built from the morphism forming operations of C and either from the symbol x or the symbol x ; and the 2-cells are formal expressions built from the symbol X : x ⇒ x and the 2-cell forming operations of C. We note H X the canonical embedding of C into C[X] which is the identity on objects, morphisms RR n°7527 and 2-cells. Just as it is the case for cartesian closed categories [START_REF] Lambek | Cartesian closed categories and typed lambda-calculi[END_REF][START_REF] Lambek | Introduction to higher order categorical logic[END_REF], this 2-category of polynomials is cartesian closed as soon as C is cartesian closed, and furthermore C[X] satisfies the following universal property. Applying this universal property that the identity 2-functor on C leads to a normal form theorem called functional completeness.

Corollary 1 (Functional completeness) For every polynomial 2-cell

α(X) : f (x) ⇒ f (x ) : 1 → B
in an indeterminate X : (x ⇒ x ) :: 1 → A, there exists a unique 2-cell

β : (g ⇒ g ) :: 1 → B A such that eval • (X × β) = α(X) in C[X].
It is also possible to form a 2-category C[X 1 , . . . , X n ] of polynomials by adjoining a finite set of indeterminate 2-cells X i : (x i ⇒ x i ) :: 1 → A i where the variables x i or x i have to be distinct. Using product, one may show that

C[X 1 , . . . , X n ] ≡ C[Z]
for an indeterminate Z : (z ⇒ z ) ::

1 → A 1 × • • • × A n .
3 The λ 2 -calculus

Types, terms and aspects

The grammar of the λ 2 -calculus generated by a set of sort names S is presented in Figure 1. The sets of types and terms is closed under the traditional λcalculus operations. For the second dimension, we construct a set of aspects For every type A, we suppose given a denumerable set of variables x, . . . that induces a denumerable set of 2-variables X : (x ⇒ x) :: A Note that we can have multiple variables of a given type but there exists only one 2-variable of a given 2-type. This simplifies the equational theory of the λ 2calculus but 2-variables have to be fused when composed vertically (see Section 3.4). In [START_REF] Hilken | Towards a proof theory of rewriting: the simply typed 2λcalculus[END_REF], this issue is overcome differently by using de Bruijn indices. All the construction for pairing, abstraction and horizontal composition are extended to aspects and there is a notion of vertical composition α * β which means that the transformations performed by α and β are applied successively. We use the word "free" and "bound" in the usual sense for a 2-dimensional variable X in an aspect α. The main aspect forming operation asp. t → t : (t ⇒ t ) :: A defines an aspect that transforms a closed term t of type A into another closed term t of type A. It is crucial in the construction that the two terms are closed. Indeed, we do not accept aspect of the form asp. x → y : (x ⇒ y) :: A where x and y are variables. Such an aspect would transform any term of type A into any term of type A.

types A ::= S | Unit | A × B | A → B terms t ::= f | x | skip | λx. t | t(t) | t, t | π i (t) aspects α ::= a | X | asp. t → t | α * α | α • α | α, α | λX. α Figure
We require that the class of aspects is closed under all aspect-forming operations except for the aspect asp. t → t which must always exist only for identity aspects on constant terms, that is when t = t is a constant term.

Note that there may be additional types (S), constant terms (f ) and constant aspects (a) in the language. As for the asp. constructor, constant aspects must be defined on closed typed terms.

Typing rules

The typing rules of the λ 2 -calculus are given in Figure 2. Terms are typed in the presence of a context Γ that stipulates the type of variables while aspects Observe that Rule Vertical-composition expects the same term t 2 at the common boundary of α and β. We would like to emphasize that we do not implicitly assume here that the equational theory is decidable. Indeed, the absence of conversion principle implies that only one 2-type can be assigned to an aspect in a given environment. So to decide if two aspects can be composed vertically, it is sufficient to check the syntactical equality of the term t 2 at the boundary.

RR n°7527 Variable Γ, x : A x : A Abstraction Γ, x : A t : B Γ λx. t : A → B Application Γ t : A → B Γ u : A Γ t(u) : B Bottom Γ skip : Unit Pairing Γ t : A Γ t : B Γ t, t : A × B Projection Γ π A1,A2 i : A 1 × A 2 → A i 2-Variable ∆, X : (x ⇒ x) :: A X : (x ⇒ x) :: A Aspect t : A t : A ∆ asp. t → t : (t ⇒ t ) :: A 2-Pairing ∆ α : (t ⇒ t ) :: A ∆ β : (u ⇒ u ) :: B ∆ α, β : ( t, u ⇒ t , u ) :: A × B 2-Abstraction ∆, X : (x ⇒ x) :: A α : (t ⇒ t ) :: B ∆ λX. α : (λx. t ⇒ λx. t ) :: A → B 2-Application ∆ β : (t ⇒ t ) :: A → B ∆ α : (u ⇒ u ) :: A ∆ β • α : (t(u) ⇒ t (u )) :: B Vertical-composition ∆ α : (t 1 ⇒ t 2 ) :: A ∆ β : (t 2 ⇒ t 3 ) :: A ∆ α * β : (t 1 ⇒ t 3 ) :: A
Rule 2-Variable introduces a 2-variable in the context ∆. Rule Aspect checks that an aspect asp. t → t transforms a closed typed term t into another closed term t of the same type.

Additional constant terms and aspects of the language are given with their specific typing rules.

Equations between terms and aspects

The equality relation . = between terms or between aspects of the same type and with the same free variables is defined as the least congruence relation derived from the equations below (we assume that all aspects used in the equation below are well-typed). Equality on terms is standard and is defined as in [START_REF] Lambek | Cartesian closed categories and typed lambda-calculi[END_REF][START_REF] Lambek | Introduction to higher order categorical logic[END_REF][START_REF] Scott | Some aspects of categories in computer science[END_REF]. When two aspects α : (t ⇒ t ) :: A and β : (u ⇒ u ) :: A are equal, we automatically know that t .

= u and t . = u .

The converse is not true in general. In the example above, we have no guarantee that α can be given the type (u ⇒ u ) :: A. This is because we can not apply equality on terms independently from equality on aspects, that is we do not have a conversion principle..

π i • α 1 , α 2 . = α i (c) [surjective pairing] π 1 • α, π 2 • α . = α
Here, π i stands for the identity aspect asp. π i → π i .

2. Specific axioms for lambda-calculus

(a) [α-conversion] λX. α[X] . = λY. α[Y ] (b) [β-rule] (λX. α) • β . = α[β/X] (c) [η-rule] α . = λX. (α • X)
The notation α[β/X] denotes the aspect α where every occurrence of X has been replaced by β and α denotes the canonical form of α (see Section 3.4)

Specific axioms on the vertical composition of aspects

RR n°7527

(a) [Identity for vertical composition]

X * X . = X (asp. f → f ) * α . = α f constant α * (asp. f → f ) . = α f constant (b) [Associativity for vertical composition] (α * β) * γ . = α * (β * γ) (c) [Distributivity over other operations] (β • α) * (β • α ) . = (β * β ) • (α * α ) (λX. α) * (λX. β) . = λX. α * β α, β * α , β . = α * α , β * β
Note that β-reduction is less usual as it involves the computation of a canonical form α before the application of the substitution. The canonical form is here to make sure that 2-dimensional variables are fused (using the identity rule). Indeed, the vertical composite

(λX. α • X) * (λX. β • X)
must be equal to the abstraction

λX. (α * β) • X.
(see the next section for more details).

The rules above constitute an extension of the rules for the traditional λcalculus plus a management of 2-dimensional constructions. Note that specific axioms for horizontal composition (eg. associativity or identity) are not required as they can be deduced from the definition of substitution. There may be additional equations in the definition of the language.

Substitution and canonical form

As explained above, the definition of β-reduction requires to fuse the 2-dimensional variables. Indeed, because of vertical composition, the syntactical substitution of a 2-variable by an aspect does not preserve equality and is even not well defined on an arbitrary aspect. For example, consider the two equal aspects λX. X * X . = λX. X

While the later aspect is just the identity, the substitution is not well-defined in general for the former aspect-it only makes sense when substituting by an aspect of the form α : (t ⇒ t) :: A. This indicates that before the application of the substitution, we need to compute the canonical form of the aspect. Given an aspect α, the aspect α is defined as the normal form of the rewriting system obtained by orienting equations in (3.a) and (3.c) from left to right. Intuitively, this rewriting system puts the vertical composition inside the aspect syntax tree and eliminates redundant 2-variables X * X.

This rewriting system is confluent (there is no critical pair) and it is not difficult to show that it is terminating using a decreasing cost function on aspects κ(α) that emphasizes vertical compositions

• κ(asp. t → t ) = κ(X) = 1 • κ(α * β) = 2 κ(α)+κ(β) • κ(β • α) = κ( α, β ) = κ( α, β ) = κ(α) + κ(β) • κ(λX. α) = κ(α) + 1
As an illustration, let us compute the canonical form of the previous example

(λX. α • X) * (λX. β • X) . = λX. (α • X) * (β • X) . = λX. (α * β) • (X * X) . = λX. (α * β) • X
Then main interest of such a canonical form is that each 2-variable does not appear in a vertical composite.

Proposition 2 In a well-typed aspect α : (t ⇒ t ) :: A with one free 2-variable X, every sub-aspect of the form

α 1 * α 2
does not contains X.

Proof When α 1 * α 2 is in canonical form, this means that the syntactical trees of α 1 and α 2 do no start with the same constructor. But we know that α 1 and α 2 agree on the term they have in common. As the λ 2 -calculus does not support a conversion rule, this means that both aspects are closed and so do not contain X.

We can deduce from the previous proposition that substitution is well-defined on aspects in canonical form.

About strong normalization

The question of whether the λ 2 -calculus calculus is strongly normalising amounts to define a strongly normalizing rewriting system by orienting each equality relation in a proper way.

As it is the case for the λ-calculus with equalities, there is no reason for a given λ 2 -calculus to be strongly normalizing. This is because we have no guarantee that the added equations on extra constant terms or aspects can be turned into a strongly normalizing system.

But we can consider the question for the pure λ 2 -calculus-that is the λ 2calculus without additional constant terms, aspects or equalities. Let us orientate all equalities (except for α-conversion and η-expansion) of Section 3.3 from left to right. Note that the resulting rewriting system (that we note ) only satisfies a weak form of subject reduction : Proposition 3 If ∆ α : (t ⇒ t ) :: A and α β, then their exists a sequence of reductions β * β such that ∆ β : (u ⇒ u ) ::

A and t . = u, t . = u .
This weak version of subject reduction has two origins : (1) a local reduction can momentarily break the typing of vertical composition until a similar reduction is performed in the other branch of the composition; (2) the computation at the level of aspects (given by substitution) induces a computation at the level of terms and thus preserves the 2-types of aspects only up to equality between terms.

Church-Rosser Property The rewriting system without β-reduction is leftlinear and confluent. The only critical pairs are given by harmless conflicts between associativity and other rules for vertical composition. Using Müller's Theorem [START_REF] Müller | Confluence of the lambda calculus with left-linear algebraic rewriting[END_REF], we can deduce that the rewriting system plus β-reduction is also confluent.

Strong normalization via reducibility candidate

The technique of reducibility candidates as developed in [START_REF] Girard | Proofs and types, volume 7 of Cambridge tracts in theoretical computer science[END_REF] can adapted to the λ 2 -calculus calculus.

The notion of neutrality is extended accordingly: an aspect is called neutral if it is not of the form α, β , λX. α or asp. t → t .

Proposition 4 Equality in the pure λ 2 -calculus is decidable.

Cartesian closed 2-categories and the λ 2 -calculus

The definition above leaves a lot of freedom. There are many λ 2 -calculus. As it is the case for the traditional λ-calculus, one can think of the λ 2 -calculus as the λ 2 -calculus freely generated by a given set S of sort names, with no additional type, term, aspect or equation. But there are many more λ 2 -calculi, as many as 2-categories.

Internal language of a Cartesian closed 2-category

Given a cartesian closed 2-category C, we define the λ 2 -calculus L(C) as follows:

1. types are objects of C, Unit is the terminal object, A × B the cartesian product and A → B the exponentiation in C,

terms with free variables

x 1 : A 1 , . . . , x n : A n are morphisms of polynomial 2-cells in the cartesian closed 2-category C[X 1 , . . . , X n ],
where

X i : (x i ⇒ x i ) :: 1 → A i is a 2-dimensional indeterminate,
3. aspects with free variables

X 1 : (x 1 ⇒ x 1 ) :: A 1 , . . . , X 1 : (x n ⇒ x n ) :: A n are polynomial 2-cells in C[X 1 , . . . , X n ],
where RR n°7527

X i : (x i ⇒ x i ) :: 1 → A i is a 2-dimensional indeterminate.
Lambda abstraction is given by functional completeness of Corollary 1. We define α . = β to hold if it holds as polynomial 2-cells. It is not difficult to check that L(C) satisfies that equational theory of the λ 2 -calculus.

Interpreting the λ 2 -calculus in a Cartesian closed 2category

Given a typed λ 2 -calculus L, we define the cartesian closed 2-category C(L) as follows:

1. objects of C(L) are the types of L,

morphisms from

A to B of C(L) are pairs (x, t(x))
where t(x) : B contains no other free variable than x : A. Two morphisms (x, t(x)) and (y, t (y)) are equal when λx. t(x) . = λy. t (y) in L,

3. 2-cells from (x, t(x)) to (x , t (x )) are aspects (X, α(X))
where α(X) : (t(x) ⇒ t (x )) :: B.

contains no other free variable than X : (x ⇒ x ) :: A. Two 2-cells (X, α(X)) and (X, β(X)) are equal when

α(X) . = β(X) in L.
We can define the interpretation of identities, composition, abstraction and pairing in the expected way.

Identity 2-cells We define identity 2-cells by

1 (x,t(x)) = (X, I(t(x)))
where the 2-cell I(t) is constructed by induction on t : Compositions The vertical composition is simply given by the vertical composition of aspects

• I(f ) = asp. f → f for any constant term f • I(y) = Y : (y ⇒ y) :: A • I(λy. u) = λY. I(u) • I(u (u)) = I(u ) • I(u) • I( u, u ) = I(u), I(u ) RR n°7527 types A ::= S | Unit | A × B | A → B terms t ::= x | f | skip | λx. t | t(t) | t, t | π i (t) | proceed(t) aspects α ::= [ ] | [around f (x) = t]
(X, α(X)) * (Y, β(Y )) = (X, α(X) * β(X))
Horizontal composition is obtained by first computing the canonical form and then substituting

(Y, β(Y )) • (X, α(X)) = (X, β(α(X))) Pairing (X, α(X)), (X, β(X)) = (X, α(X), β(X) )
Abstraction The functor Λ A,B,C is given by

Λ A,B,C (Z, α(Z)) = (X, λY. α( X, Y ))
Evaluation. The morphism eval A,B from A × (A → B) to B is given by

eval A,B = (X, π 2 (X) • π 1 (X))
We let the reader check that for any λ 2 -calculus L, C(L) is a cartesian closed 2-category.

We can now state the property that makes the λ 2 -calculus an internal language for cartesian closed 2-categories.

Proposition 5 For any cartesian closed 2-category C and any λ 2 -calculus L,

C(L(C)) ∼ = C and L(C(L)) ∼ = L.
The first isomorphism presupposes the notion of morphisms between cartesian closed 2-categories, which is given by cartesian closed 2-functors. The second isomorphism presupposes the notion of morphisms between λ 2 -calculi. This can be defined as for traditional λ-calculus with the notion of translations, ie. maps Φ that transport types to types, terms to terms (including mapping the ith variable of type A to the ith variable of type Φ(A)), aspects to aspects (including mapping the ith variable of type (x ⇒ x ) :: A to the ith variable of type (Φ(x) ⇒ Φ(x )) :: Φ(A)) and preserve all the type-, term-or aspect-forming operations and equations on the nose.

Note that it is possible to extend this isomorphism at a 2-categorical level by defining a notion corresponding to natural transformations between translations.

Weaving in the λ 2 -calculus

Using the correspondence between the λ 2 -calculus and cartesian closed 2-categories, we can now define a weaving algorithm in terms of categorical rewriting.

As sketched in the introduction, given a term t(x) : B of a λ 2 -calculus L where x is of type A, we will consider all the possible interactions of the (constant) aspects defined in L with t(x) by considering the category C(L)(A, B). This category contains all aspects that transform terms of type A → B and so the execution of an aspect corresponds to the application of a morphism in that category. Thus, the result of the weaving algorithm is given by the normal form of the image of t(x) in that category.

More precisely, the set of woven terms is defined as

Woven(t(x)) = {(t (x), α) | (x, t(x)) α -→ (x, t (x)) is a maximal reduction in the category C(L)(A, B)}
Of course, such a normal form has no reason to be unique or even to exist. The purpose of specific AOP languages is often to provide more advanced definitions of aspects that guarantee the uniqueness and sometimes the existence of such a normal form so that the set Woven(t(x)) is a singleton for every term t(x).

Uniqueness of the normal form

Observe that all the work on aspect composition can be understood as a way to combine aspects while conserving uniqueness of the definition of the woven program. For example, when multiple pieces of advices can be applied at the same join point in AspectJ, precedence orders are (arbitrarily) defined, based on the order in which definitions of pieces of advice syntactically appear in the code. More algebraic approaches have been proposed (see eg. [START_REF] Lopez-Herrejon | A disciplined approach to aspect composition[END_REF]).

Existence of a normal form

The absence of a normal form is often understood as a circularity in the application of aspects. This problem is difficult to overcome and can arise even in simple programs. For instance, the work of Eric Tanter on execution levels is precisely a way to introduce a hierarchy in the application of aspects and thus to avoid basic circular definition [START_REF] Tanter | Execution levels for aspect-oriented programming[END_REF]. Other lines of work have proposed to restricted the power of pieces of advice (for example using a typing system [START_REF] Dantas | Harmless advice[END_REF]) in order to guarantee that the execution of the program is not critically perturbed.

MinAML

This section gives the semantics of a concrete AOP language called MinAML by a translation to the λ 2 -calculus. More precisely, given a program p, we will construct a λ 2 -calculus λ p , whose underlying 2-category defines a rewriting system from which we can deduce the definition of a weaving algorithm.

MinAML is a version (without conditionals and before and after advice) of the language introduced in [START_REF] Walker | A theory of aspects[END_REF] to give a first AOP language with a formal semantics. The absence of before and after advice is unimportant as they can both be encoded with an around advice. But the main difference between the original MinAML is that we do not address here the question of scoping of aspects. Indeed, unlike AspectJ which allows programmers to refer to any method that appears anywhere in their program, even private methods of classes, the functions referred to by pieces of advice in the work of David Walker and colleagues must be in scope. This scoping mechanism is orthogonal to the question addressed in this paper and would introduce unnecessary complications in definition of the associated λ 2 -calculus and of the weaving mechanism. Indeed, the definition of the underlying 2-category associated to a program in MinAML, as well as the corresponding rewriting system, would have to evolve with the change of scope. We have thus decided to omit this mechanism in the definition of the language and work with a global scope.

Syntax

MinAML is an extension of the λ-calculus with products in two steps. The first extension is usual: we introduce declaration names that can be used to define names for terms of the language with the let constructor let f = t.

We suppose given a set of declaration names, noted f, g, . . .

The second extension is the introduction of aspects with the constructor

around f (x) = t
which indicates that at execution, the application of the function f with argument x is replaced by the term t. Using the terminology introduced at the beginning of the article, the term f (x) defines the pointcut of the aspect and the term t defines its advice.

When declaring pieces of advice, the programmer can choose either to replace f entirely or to perform some computations interleaved with one (or more) execution of f (possibly with new arguments) using the keyword proceed. Let us slightly rewrite the history and say that the keyword proceed has been introduced to tackle the case where a pointcut can intercept more than one function. In that situation, the programmer may want to run the intercepted function without knowing its name, which can be using the keyword proceed. This is not possible in MinAML but we have kept this keyword as it also emphasizes that the function f executed by the piece of advice through proceed is not strictly identical to the intercepted function f . More precisely, the function f behaves as f but can no longer be intercepted by the aspect. This avoids trivial circular definitions in the application of aspects.

In the same way when multiple aspects intercept the same function f , one must define on order in the weaving mechanism. For simplicity, we have decided to choose the order of declaration in the program.

The grammar of MinAML is fully described in Figure 3. A program p is constituted of a list of declarations ds, a list of aspects α and a term t. The fact that there is only a global scope for aspects in our calculus is enforced by the stratified structure of a program. The term [ ] stands for the empty list, [h] stands for the singleton list with element h and l l denotes the concatenation of lists.

Extension to effectful aspects

So far, an aspect of MinAML is always pure. As sketched in the introduction, in order to exploit the full power of the λ 2 -calculus, we need to add effectful that transforms log(n) into n and prints n to the screen.

Variable Γ, x : A; ∆ x : A Name Γ; ∆, f : A f : A Bottom Γ; ∆ skip : Unit Abstraction Γ, x : A; ∆ t : B Γ; ∆ λx.t : A → B Application Γ; ∆ t : A → B Γ; ∆ u : A Γ; ∆ t(u) : B Pairing Γ; ∆ t : A Γ; ∆ t : B Γ; ∆ t, t : A × B Binding ; ∆ t : A ; ∆, f : A p : B ; ∆ let f = t; p : B Around x : A; ∆, f : A ⇒ A t[f /proceed] : A ; ∆, f : A → A p : B ; ∆, f : A → A around f (x) = t; p : B

A simple example

Let us now express in this language the example developed in the introductionof an aspect that ensures that all calls to the sqrt function are performed on non-negative values. To make the example richer, we also define an aspect that applies the function log (before the function abs) to the argument of sqrt so that the argument will then be printed out by the aspect Log_asp. The following program of MinAML (where we use some usual primitives on integers) defines such aspects and run sqrt on the negative value -4.

P = [let sqrt = λx. √ x, let abs = λx. |x|] [around sqrt(x) = proceed(log(x)), Log_asp, around sqrt(x) = proceed(abs(x))] [sqrt(-4)]

Typing

The typing rules for λ-terms presented in Figure 4 are standard. Programs are typed in the presence of a context Γ; ∆. Γ stipulates the type of variables and ∆ stipulates the type of declaration names. This dichotomy enables to force free variables appearing in the definition of a piece of advice to be associated with declaration names only. Note that this fact was also enforced by the stratified nature of a program, which is a set of declaration names ds, then a set of aspects α and finally a term t. Thus, when trying to type a name's declaration or an aspect, the context Γ is necessary empty. Nevertheless, we have chosen to make this also explicit in the typing so that introducing a more general scoping mechanism would not require any change in the typing rules.

Rule Binding for the let binder requires that the open variables appearing in t are related to declaration names.

In Rule Around, one assume that a declaration name f of type A → A is already defined in ∆ and check that t (where every occurrence of proceed is replaced by f ) has type A assuming that the argument x of f (x) has type A and is the only variable in the environment Γ. In that case, the program around f (x) = t; p is given the same type as the program p.

It is important that declaration names can only be bound to terms defined on declaration names. In this way, an aspect in MinAML is not be able to intercept a term with free variables in the same way as an aspect in λ 2 -calculus cannot be defined between open terms.

A translation into the pure λ 2 -calculus

We now present the translation of a typed program p = ds α t into the λ 2 -calculus. More precisely, we will define a λ 2 -calculus L p based on declarations present in ds and aspects present in α. The construction of L p goes in two steps:

(1) we produce a list of aspects α and a mapping γ from declaration names in ds to integers. As a declaration name f can be intercepted by more than one aspect, we introduce a fresh declaration name f i each time we translate an aspect whose pointcut relies on f . This transformation can be written with an Ocaml-like function using the fold_l function.

let trans_asp(a,b) = match (a,b) with | ((γ,A),(around f (x) = t)) -> (γ[f → γ(f ) + 1], A++[asp. f γ(f ) → λx. t[f γ(f )+1 /proceed]]) in (γ, α ) = fold_l(trans_asp,(let γ x = 1,[]),α)
where γ[f → γ(f ) + 1] stands for the map γ whose value on f has been incremented by 1. That is, the ith aspect that intercept f , let say around f (x) = t will thus be translated into the aspect

asp. f i → λx. t[f i+1 /proceed]
that intercept f i and proceeds with f i+1 . In this way, we construct a sequence of declaration names

f 1 (= f ), f 2 , . . . , f γ(f )
that drives the list of aspects that can intercept the application of the function f .

(2) we define a list of aspects ds by translating each declaration

let f = t into the aspect asp. f γ(f ) → t.
This transformation can be written with an Ocaml-like function using the map function.

let trans_eq(d) = match d with | let f = t -> [asp. f γ(f ) → t] in ds = map trans_eq ds
The λ 2 -calculus L p is generated by the constant terms

{f i | f ∈ ds and 1 ≤ i ≤ γ(f )}
-that represent all declaration names introduced in the translation of aspectsand by the list of aspects α and ds . Let us present the effect of the translation on the program P above. The λ 2 -calculus L P is generated by the constant terms sqrt 1 , sqrt 2 , sqrt 3 , abs 1 and by the four aspects a 1 : asp. sqrt 1 → λx. sqrt 2 (log(x)) a 2 : asp. sqrt 2 → λx. sqrt 3 (abs 1 (x)) a 3 : asp. sqrt 3 → λx. √ x a 4 : asp. abs 1 → λx. |x|

Weaving in MinAML

Once the λ 2 -calculus L p has been generated, the weaving algorithm is defined as in Section 4.3. Namely, we computed the normal form (if it exists) in the corresponding category-observe that, as usual, the ordering of pieces of advice guarantees that there is at most one normal form. This gives us the interleaved program that we can then execute using the strong normalization of the pure λ 2 -calculus.

Weaving on a simple example

Let us now explained the behavior of the weaving algorithm on the simple example P. The computation can be described by the following sequence of reduction (where some extra β-reduction has been performed to make the reading easier):

sqrt 1 (-4) a1•I(-4) ------→ sqrt 2 (log(-4)) I(sqrt2)•Log_asp•I(-4) ---------------→ sqrt 2 ((λx. x)(-4)) = sqrt 2 (-4) a2•I(-4) ------→ sqrt 3 (abs 1 (-4)) a3•I(abs1(-4))
---------→ abs 1 (-4)

I( √ -)•a4•I(-4) ----------→ | -4| = 2 RR n°7527
Observe the particular kind of parametricity describes in the introduction. Indeed, a single definition of the aspect Log_asp generates all the possible combinations of that aspect with 2-dimensional primitives of the language, and in particular the aspect I(sqrt 2 ) • Log_asp • I(-4) used in the computation of the weaving on sqrt 1 (-4).

6 Extensions to more complex aspects A way to add conditionals in MinAML, and thus to be able to define conditional pointcuts, is thus to work in a cartesian closed 2-category equipped with finite coproducts. An aspect, whose pointcut is conditional on the values of the arguments of the intercepted function, will thus be described by a 2-cell

A 1 ⊕ A 2 g1⊕g2 : : f1⊕f2 $ $ α1⊕α2 B 1 ⊕ B 2 .
In that situation, the weaving mechanism will just be defined in the same way, and the choice will be resolved when we interpret morphisms that come from terms that reduce to values in the original language. In that case, there is no ambiguity in the branch that is taken during the execution. This static weaving can be seen as a partial evaluation that will be dynamically completed. So the weaving of aspects is still static but contains a lot of choices. For example, the term

A 1 ⊕ A 2 f1⊕f2 / / B 1 ⊕ B 2
in the example above will be woven into

A 1 ⊕ A 2 g1⊕g2 / / B 1 ⊕ B 2
whereas the same term precomposed with the first injection (that resolves the choice between f 1 and f 2 )

A 1 inj 1 / / A 1 ⊕ A 2 f1⊕f2 / / B 1 ⊕ B 2
will directly be woven into

A 1 g1 / / B 1 .
More generally, this is the way we understand dynamic weaving of aspects in the language of 2-categories: a static weaving that contains all the possibilities which are dynamically resolved at computation.

Extensions using enriched Lawvere theories

We conclude this article by sketching how to extend MinAML with references, exceptions or other notions of computation. The idea is to reuse the categorical interpretation of those notions in a 2-categorical setting in order to stick to our previous construction.

References or exceptions (among many other notions) are traditionally interpreted using the Kleisli construction over the suitable strong monad, called in that case a computational monad [START_REF] Moggi | Notions of computation and monads[END_REF]. For example, the state monad T for references is defined on objects by

T A = S → (S × A).
The type S represents the memory in which references are registered. Then a term of type A → B in a λ-calculus with references is interpreted as a morphism of type A → B in the Kleisli category, that is a morphism of type

A → T B ∼ = (S × A) → (S × B).
Such a morphism explicitly manages the memory state associated to references.

The key to extend MinAML with references is to define a 2-monad that extends the definition of the state monad on 2-categories. Then we can use the 2-dimensional version of the Kleisli construction to define the categorical interpretation of MinAML with references. We can do the same thing for exceptions and the associated exception monad.

Using the correspondence between strong monads and Lawvere theories, and the work of Martin Hyland, Gordon Plotkin and John Power on enriched Lawvere theories [START_REF] Power | Enriched Lawvere theories[END_REF][START_REF] Hyland | Combining effects: sum and tensor[END_REF], this indicates that we have to work with Cat-enriched Lawvere theories. Note that their motivation to extend the work of Eugenio Moggi to an enriched setting is the remark that in denotational semantics, the base category is not Set but rather the category ω-Cpo of ω-cpos and continuous functions. It appears that in our work on AOP, the base category is not Set but rather Cat.

This approach provides an algebraic way to formalize powerful AOP languages. We believe that Cat-enriched Lawvere theories are required for a clean definition of the complex mechanisms that show up in AOP.

Conclusion

The idea of the paper is to approach AOP (and more generally type-preserving program transformation) from a category-theoretic prospective, in order to complement the software engineering approach. We believe that this approach could have substantial benefit at the level of conceptual understanding of what AOP actually is.

More precisely, we identify (cartesian closed) 2-categories as a suitable setting in which programs can be seen as 1-cells and aspects (or more generally program transformations) can be seen as 2-cells. To make this analogy precise, we develop a language for 2-categories called the λ 2 -calculus, as a 2-dimensional extension of the traditional λ-calculus, and show that it is an internal language for cartesian closed 2-categories. We also show that the pure λ 2 -calculus is strongly normalizing.

We then demonstrate the applicability of our construction by translating a more realistic functional AOP language called MinAML into the λ 2 -calculus. This translation enables to interpret a program of MinAML in a cartesian closed 2-category and to define the weaving algorithm as the computation of normal form in a rewriting system based on that 2-category. The well-foundedness of the weaving algorithm is thus given by the existence of a normal form in the corresponding rewriting system. We briefly sketch how to extend our categorical setting to interpret conditional pointcuts using finite coproducts.

At the end of the article, we discuss an algebraic way to extend the λ 2calculus with various notions of computation using enriched Lawvere theory. This nice formulation of algebraic theories in an enriched setting enables to transpose the notion of computational monads of Eugenio Moggi at the level of 2-categories. We believe that this model-theoretic account of computation is necessary to understand the complex interaction between AOP mechanisms and traditional notions of computation.

Proposition 1

 1 Given a cartesian closed 2-category C and an indeterminate 2-cell X : (x ⇒ x ) :: 1 → A of C, let F : C → D be a cartesian closed 2-functor into another cartesian closed 2-category D and α : a ⇒ b : 1 → F (A) be a 2-cell of D. Then there exists a unique cartesian closed 2-functor (ie. a 2-functor that preserves product and closure up to isomorphisms) F α : C[X] → D with F α (X) = α and such that the diagram C

Figure 2 :

 2 Figure 2: Typing rules of the λ 2 -calculus

1 .

 1 Specific axioms for products (a) [terminal object] α . = asp. skip → skip for all α : (t ⇒ t ) :: Unit (b) [projections]

Figure 3 :

 3 Figure 3: The grammar of the MinAML

Figure 4 :

 4 Figure 4: Typing rules of MinAML

6. 1

 1 Adding conditional pointcutsConditionals are given in category theory by finite coproductsA ⊕ B.

  1: The grammar of λ 2 -calculus which transform terms into other terms. An aspect α that transforms the term t of type A into the term t of type A will be noted

α : (t ⇒ t ) :: A Note that this can be thought of as a stratified instance of a dependent type theory, where 2-types can include terms. But the main difference between Martin-Löf type theory lies in the absence of a conversion rule-if t = u and α : (t ⇒ t ) :: A, it is not in general the case that α : (u ⇒ t ) :: A.

RR n°7527