Alexander Bulinski

Alexander Bulinski On The

Newman Conjecture

ON THE NEWMAN CONJECTURE

Keywords: stationary random fields, positive association, central limit theorem, uniform integrability, slowly varying functions, the Newman conjecture. 2010 AMS classification: 60F05, 60G60

We consider a random field, defined on an integer-valued d-dimensional lattice Z d , with covariance function satisfying a condition more general than summability. Such condition appeared in the well-known Newman's conjecture concerning the central limit theorem (CLT) for stationary associated random fields. As was demonstrated by Herrndorf and Shashkin, the conjecture fails already for d = 1. In the present paper, we show the validity of modified conjecture leaving intact the mentioned condition on covariance function. Thus we establish, for any integer d ≥ 1, a criterion of the CLT validity for the wider class of positively associated stationary fields. The uniform integrability for the squares of normalized partial sums, taken over growing parallelepipeds or cubes in Z d , plays the key role in deriving their asymptotic normality. So our result extends the Lewis theorem proved for sequences of random variables. A representation of variances of partial sums of a field using the slowly varying functions in several arguments is employed in essential way.

Introduction

The study of asymptotical behavior of the (normalized) sums of random variables is the vast research domain of Probability Theory having various applications. The limit theorems established for independent summands form here the classical core. In this regard one can refer to the monographs [START_REF] Gnedenko | Limit Distributions for Sums of Independent Random Variables[END_REF], [START_REF] Zolotarev | Modern Theory of Summation of Random Variables[END_REF], [START_REF] Ibragimov | Independent and Stationary Sequences of Random Variables[END_REF], [START_REF] Petrov | Limit Theorems of Probability Theory: Sequences of Independent Random Variables[END_REF]; see also references therein.

Stochastic models described by means of families of dependent random variables arose at the beginning of the last century. Thus the Gaussian and Markov processes, martingales, solutions of the stochastic differential equations, mixing processes appeared as well as other important classes (see, e.g., [START_REF] Bulinski | Theory of Stochastic Processes[END_REF], [START_REF] Kallenberg | Foundations of Modern Probability[END_REF]). Moreover, much attention has been paid to studying of random fields.

Since the 1960s due to the problems of mathematical statistics, reliability theory, percolation and statistical physics there arose the stochastic models based on the families of variables possessing various forms of positive or negative dependence (see, e.g., [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF]). The key role in these models belongs to the notion of association (in statistical physics the well-known FKGinequalities imply the association). We will use the following concept extending that introduced in [START_REF] Esary | Association of random variables, with applications[END_REF].

Definition 1 ( [START_REF] Newman | Asymptotic independence and limit theorems for positively and negatively dependent random variables[END_REF]) A real-valued random field X = {X t , t ∈ T } is called positively associated 3 (one writes X ∈ PA) if, for any finite disjoint sets I = {s 1 , . . . , s m } ⊂ T , J = {t 1 , . . . , t n } ⊂ T and all bounded coordinate-wise nondecreasing Lipschitz functions f : R m → R, g : R n → R, one has cov(f (X s 1 , . . . , X sm ), g(X t 1 , . . . , X tn )) ≥ 0.

(

Recall that a random field X is called associated ( [START_REF] Esary | Association of random variables, with applications[END_REF]), if the definition above is satisfied without the hypothesis I ∩J = ∅. Obviously association implies positive association. Note that any family of (real-valued) independent random variables is automatically associated. Many other important examples can be found in [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF].

For a random field X = {X t , t ∈ T } and a finite set U ⊂ T introduce

S(U) = t∈U X t .
Further on we will consider random fields defined on a lattice T = Z d and a probability space (Ω, F , P). In the seminal paper by Newman [START_REF] Newman | Asymptotic independence and limit theorems for positively and negatively dependent random variables[END_REF] the central limit theorem (CLT) was established for associated (strictly) stationary random field X = {X t , t ∈ Z d } under finite susceptibility condition that is when the covariance function is summable:

σ 2 := j∈Z d cov(X 0 , X j ) < ∞. (2)
Namely, these simple assumptions imply for a field X the following relation

S n -ES n n law -→ Z ∼ N (0, σ 2 ) as n → ∞, n = (n 1 , . . . , n d ) ∈ N d , (3)
here

S n = S([0, n] ∩ Z d ), [0, n] = [0, n 1 ] × . . . × [0, n d ], n = n 1 . . . n d , N (0, σ 2
) is a Gaussian law with parameters 0 and σ 2 , law -→ stands for weak convergence of distributions. The goal of this work is to provide the criteria of the CLT validity for positively associated stationary random fields with finite second moment (and in general without condition (2)).

Main results

At first it is reasonable to recall several definitions.

Definition 2 A function L : R d + → R \ {0}
is called slowly varying (at infinity) if, for any vector a = (a 1 , . . . , a d ) ⊤ with positive coordinates,

L(a 1 x 1 , . . . , a d x d ) L(x 1 , . . . , x d ) → 1 as x = (x 1 , . . . , x d ) ⊤ → ∞, (4)
i.e. x 1 → ∞, . . . , x d → ∞. For such functions we write L ∈ L(R d + ).

3 or weakly associated 2

We operate with column vectors and use the symbol ⊤ for transposition. A function L : N d → R \ {0} is called slowly varying (at infinity) if, for any vector a = (a 1 , . . . , a d ) ⊤ ∈ N d , relation (4) holds with additional assumption that x ∈ N d . Then we write L ∈ L(N d ).

For example the function d k=1 log(x k ∨ 1) where

x ∈ R d + belongs to L(R d + ).
Remark 1 It is well-known that not every function belonging to L(N d ) admits extension to a function from the class L(R d + ) even for d = 1. However, it is not difficult to verify that if a coordinate-wise nondecreasing function L ∈ L(N d ), then H(x) := L([ x]) belongs to L(R d + ). Here x = (x 1 ∨ 1, . . . , x d ∨ 1) ⊤ for x ∈ R d , and [x] = ([x 1 ], . . . , [x d ]) ⊤ , i.e. one takes the integer part of each component of x.

During a long time there was no solution to the Newman conjecture on possible replacement of requirement [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF] appearing in CLT by a milder condition. Namely, he considered the partial sums S(U) taken over "integer cubes" U and believed that instead of (2) it suffices to assume that for associated strictly stationary random field

X = {X j , j ∈ Z d } with EX 2 0 < ∞ the function K(r) = j∈Z d : j ≤r cov(X 0 , X j ), r ∈ N, (5)
belongs to L(N) where

• is the Euclidean norm in R d .
Unfortunately it turned out that this beautiful hypothesis is not true even for d = 1. The first counterexample was constructed by Herrndorf [START_REF] Herrndorf | An example of the central limit theorem for associated random sequences[END_REF], and then Shashkin [START_REF] Shashkin | On Newman's central limit theorem[END_REF] showed that condition (2) has in a sense the optimal character.

It is worth mentioning also that the Newman CLT was generalized in [START_REF] Bulinski | Statistical variant of the CLT for associated random fields[END_REF] for partial sums S(U) taken over regularly growing subsets of Z d . Further extensions are discussed in Chapter 3 of [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF].

Definition 3 A family X = {X j , j ∈ N d } is called uniformly integrable if lim c→∞ sup j∈N d E|X j |I{|X j | ≥ c} = 0.
For a (wide sense) stationary random field X = {X j , j ∈ Z d } introduce the function

K X (n) = j∈Z d :-n≤j≤n cov (X 0 , X j ), n ∈ N d . If a = (a (1) , . . . , a (d) ) ⊤ and b = (b (1) , . . . , b (d) ) ⊤ are vectors in R d , the notation a ≤ b means that a (k) ≤ b (k) for all k = 1, . . . , d. We write a < b whenever a (k) < b (k) for any k = 1, . . . , d.
The following result extends the Lewis theorem proved in [START_REF] Lewis | Limit theorems for partial sums of quasi-associated random variables[END_REF] for a sequence of random variables.

Theorem 1 Let a strictly stationary random field

X = {X j , j ∈ Z d } ∈ PA, 0 < EX 2 0 < ∞ and K X (•) ∈ L(N d ). Then X satisfies CLT, i.e. S n -ES n √ varS n law -→ Z ∼ N (0, 1) as n → ∞, (6)
if and only if the family

{(S n -ES n ) 2 /( n K X (n)), n ∈ N d } is uniformly integrable.
Consider now a sequence of growing "integer cubes"

C r = (0, r] d ∩ Z d , r ∈ N.
Theorem 2 Let a strictly stationary random field

X = {X j , j ∈ Z d } ∈ PA, 0 < EX 2 0 < ∞ and K(•) ∈ L(N). Then S(C r ) -ES(C r ) varS(C r ) law -→ Z ∼ N (0, 1) as r → ∞, (7)
if and only if the sequence ((S(C r ) -ES(C r )) 2 /(r d K(r))) r∈N is uniformly integrable.

Theorem 2 shows what one has to assume additionally, for a class of positively associated strictly stationary random fields, besides the condition that the function K(•) is slowly varying to guarantee that the Newman conjecture holds true for any dimension d ∈ N. In [START_REF] Newman | Normal fluctuations and the FKG inequalities[END_REF] the author discussed his conjecture and noted without proof that the "mild version" of that hypothesis takes place under the additional condition of uniform integrability of the sequence appearing in Theorem 2 above. Therefore Theorems 1 and 2 show that in fact we do not change the initial problem but clarify its essential feature. We do not deal here with a renorm group approach (do not consider the partition of R d by the congruent cubes) but study the partial sums S n taken over any growing "integer blocks".

Proofs of the main results

We start with simple auxiliary statements.

Lemma 1 Let a function L belonging to L(N d ) be coordinate-wise nondecreasing. Then there exist non-random vectors q n = (q

(1) n , . . . , q (d) n ) ⊤ ∈ N d , where n = (n 1 , . . . , n d ) ⊤ ∈ N d , such that q (k) n ≤ n k , q (k) n n k → 0 for k = 1, . . . , d, q n → ∞ and L(n) L(q n ) → 1 as n → ∞. (8)
Proof. According to Remark 1 we can assume without loss of generality that L is extended to a function belonging to the class L(R d + ). For any R = (R (1) , . . . , R (d) ) ⊤ ∈ N d we can choose N 0 (R) ∈ N d in such a way that Then M 0 (r) < M 0 (r + 1) for r ∈ N. For arbitrary r ∈ N and n ≥ M 0 (r)

L(n 1 , . . . , n d ) L n 1 R (1) , . . . , n d R (d) -1 ≤ 1 R for all n ≥ N 0 (R). Now we take a sequence (R(r)) r∈N such that R(r) ∈ N d and R(r) < R(r + 1) for each r ∈ N. Introduce M 0 (1) = N 0 (R( 1
L(n 1 , . . . , n d ) L n 1 R (1) (r) , . . . , n d R (d) (r) -1 ≤ 1 R(r)
.

Let us define non-random sequences (ε

(k) j ) j∈N where k = 1, . . . , d, putting ε (k) j = 1/R (k) (r) for M (k) 0 (r) ≤ j < M (k) 0 (r + 1).
For any ε > 0 take r 0 ∈ N in such a way that 1/ R(r 0 ) < ε. Further on, for n such that M 0 (r) ≤ n < M 0 (r + 1) where r ≥ r 0 , one has

1 ≤ L(n 1 , . . . , n d ) L(n 1 ε (1) n 1 , . . . , n d ε (d) n d ) = L(n 1 , . . . , n d ) L n 1 R (1) (r) , . . . , n d R (d) (r) ≤ 1 + 1 R(r) ≤ 1 + 1 R(r 0 ) ≤ 1 + ε.
Then we can take q n = ([n 1 ε

(1)

n 1 ], . . . , [n d ε (d) n d ]) ∨ ([log n 1 ], . . . , [log n d ]) ∨ 1,
to ensure the validity of (8).

Lemma 2 Let X = {X j , j ∈ Z d } be a wide sense stationary random field with nonnegative covariance function. Assume that

K X (•) ∈ L(N d ). Then varS(U n ) ∼ n K X (n) as n → ∞ ( 9
)
where

U n = {j ∈ Z d : 1 ≤ j ≤ n}, n ∈ N d . Conversely, if varS(U n ) ∼ n L(n) as n → ∞, where L ∈ L(N d ), then L(n) ∼ K X (n) as n → ∞. Proof. Let K X (•) ∈ L(N d ). Due to the (wide-sense) stationarity of X one has cov(X i , X j ) = R(i -j) for i, j ∈ Z d . Thus varS(U n ) = i,j∈Un cov(X i , X j ) = i,j∈Un R(i -j) = m∈Z d :-(n-1)≤m≤n-1 (n 1 -|m 1 |) . . . (n d -|m d |)R(m) ≤ n m∈Z d :-(n-1)≤m≤n-1 R(m) ≤ n K X (n), (10)
as the function R is nonnegative. Take any c ∈ (0, 1) and n ≥ 1 1-c 1 (i.e. cn ≤ n -1, n ∈ N d ). Using again nonnegativity of R we can write

varS(U n ) = m∈Z d :-(n-1)≤m≤n-1 (n 1 -|m 1 |) . . . (n d -|m d |)R(m) ≥ (1 -c) d n m∈Z d :-cn≤m≤cn R(m) = (1 -c) d n K X ([cn]).
In view of Remark 1 we come to the relation

(1 -c) d n K X ([cn]) ∼ (1 -c) d n K X (n), n → ∞, n ∈ N d .
Consequently, varS(U n ) ∼ n K X (n) as n → ∞, because c can be taken arbitrary close to zero. Now suppose that varS(U n ) ∼ n L(n) as n → ∞, where L ∈ L(N d ). Then for any ε > 0 and all n sufficiently large (i.e. each component of n is large enough), application of (10) leads to the inequality

K X (n) ≥ varS(U n ) n ≥ (1 -ε)L(n). (11)
For a fixed q ∈ N, q > 1, and n r ∈ N, m r ∈ Z such that |m r | ≤ n r where r = 1, . . . , d, one has

q q -1 1 - |m r | n r q ≥ q q -1 1 - n r n r q = 1.
Therefore, taking into account condition R ≥ 0 we verify that

K X (n) ≤ q q -1 d m∈Z d :-n≤m≤n R(m) d r=1 (n r q -|m r |) n r q ≤ q q -1 d d r=1 n r q -1 m∈Z d :-nq≤m≤nq R(m) d r=1 (n r q -|m r |) = q q -1 d varS(U qn ) qn ∼ q q -1 d L(qn), n → ∞. ( 12
)
As q can be chosen arbitrary large, using ( 11) and ( 12) we conclude that the desired statement holds.

Proof of Theorem 1. Necessity. Suppose that ( 6) is satisfied. Then

(S n -ES n ) 2 varS n law -→ Z 2 as n → ∞.
Indeed, if the random variables Y n law -→ Y , then for any bounded continuous function

h : R → R one has h(Y n ) law -→ h(Y ) as n → ∞. Obviously, (S n -ES n ) 2 varS n ≥ 0 and E(S n -ES n ) 2 varS n = 1.
Thus uniform integrability of the family {(S n -ES n ) 2 /varS n , n ∈ N d } follows from the analogue of Theorem 1.5.4 established in [START_REF] Billingsley | Convergence of Probability Measures[END_REF] for a sequence of random variables indexed by points of N. In view of Lemma 2 we can claim that (9) holds. Consequently, the family

{(S n -ES n ) 2 /( n K X (n)), n ∈ N d } is also uniformly integrable.
Sufficiency. If the function K X is bounded we see that ( 2) is valid and Theorem 3.1.12 of [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF] implies that (6) is satisfied. Thus we will assume further that a function

K X is unbounded. Set K X (t) := K X ([t] ∨ 1) for t = (t 1 , . . . , t d ) ⊤ ∈ R d + where [t] = ([t 1 ], . . . , [t d ])
⊤ . This extension of the initial function K X belongs to L(R d + ) as K X is coordinate-wise nondecreasing on N d (a field X ∈ PA, therefore its covariance function is nonnegative). Further on we assume that the function K X is extended on R d + as indicated above.

Let the vectors q n , n ∈ N d , be constructed according to Lemma 1. It is not difficult to find a non-random family of vectors {p n , n ∈ N d }, where p n takes values in N d , such that

q (k) n ≤ p (k) n ≤ n k , q (k) n /p (k) n → 0 and p (k) n /n k → 0 for k = 1, . . . , d as n → ∞. (13)
Now we apply the Bernstein partitioning method. For n, j ∈ N d and introduced p n and q n consider the blocks

U (j) n = {u ∈ N d : (j k -1)(p (k) n + q (k) n ) < u k ≤ j k p (k) n + (j k -1)q (k) n , k = 1, . . . , d}, where u = (u 1 , . . . , u d ). Let J n = {j ∈ N d : U (j) n ⊂ U n } and W n = j∈Jn U (j) n , G n = U n \ W n , n ∈ N d .
In other words W n consists of "large blocks" (having the "size" p

n along each of the k-th axis for k = 1, . . . , d), separated by "corridors" belonging to the set G n . Put v n = n K X (n). Then, for each t ∈ R and n ∈ N d we obtain

E exp it v n S n -e -t 2 2 ≤ E exp it v n S n -E exp it v n j∈Jn S(U (j) n ) + E exp it v n j∈Jn S(U (j) n ) - j∈Jn E exp it v n S(U (j) n ) + j∈Jn E exp it v n S(U (j) n -e -t 2 2 =: 3 r=1 Q r , here i 2 = -1, Q r = Q r (n, t
) and S n = S(U n ) as previously. Taking into account that |e ix -e iy | ≤ |x -y| for all x, y ∈ R, and using the Lyapunov inequality we get

Q 1 ≤ |t| v n E|S(G n )| ≤ |t| v n (ES(G n ) 2 ) 1/2 .
A random field X ∈ PA, therefore cov (X j , X u ) ≥ 0 for any j, u ∈ N d . Thus in view of wide-sense stationarity of X we come to the relations

ES(G n ) 2 ≤ j∈Gn u:-n≤u-j≤n cov(X j , X u ) ≤ card G n K X (n) ≤ K X (n) d k=1 (m (k) n q (k) n + p (k) n + q (k) n ) 1≤l≤d,l =k n l
where card G stands for the cardinality of a set G, m

(k) n = [n k /(p (k) n + q (k)
n )], k = 1, . . . , d. Due to [START_REF] Ibragimov | Independent and Stationary Sequences of Random Variables[END_REF] and [START_REF] Petrov | Limit Theorems of Probability Theory: Sequences of Independent Random Variables[END_REF] we get the inequality

ES(G n ) 2 n K X (n) ≤ d k=1 m (k) n q (k) n + p (k) n + q (k) n n k → 0, n → ∞.
Consequently, Q 1 (n, t) → 0 for each t ∈ R as n → ∞.

For any n ∈ N d the family {S(U (j) n ), j ∈ J n } ∈ PA (see, e.g., Theorem 1.1.8 in [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF]). Enumerate elements of this family to obtain the collection of random variables {Y n,s , s = 1, . . . , M n } where

M n = card J n . It is easily seen that d k=1 m (k) n ≤ M n ≤ d k=1 (m (k) n + 1).
Recall that for complex-valued random variables Y and V (absolute square integrable) the covariance cov(Y, V ) := E(Y -EY )(V -EV ), where the bar denotes the conjugation. Due to Theorem 1.5.3 of [START_REF] Bulinski | Limit Thorems for Associated Random Fields and Related Systems[END_REF] one has

Q 2 ≤ Mn-1 s=1 cov exp it v n Y n,s , exp - it v n Mn l=s+1 Y n,l ≤ 4t 2 v 2 n 1≤s,l≤Mn,s =l cov(Y n,s , Y n,l ) ≤ 4t 2 n K X (n) j∈Un u∈Un,|u-j|>qn cov(X j , X u ) where |u| = max k=1,...,d |u k |. Obviously, for j ∈ U n {u ∈ U n , |u -j| > q n } ⊂ {u ∈ N d : j -n ≤ u ≤ j + n} \ {u ∈ N d : |u -j| ≤ q n }.
Therefore, the inequality

j∈Un u∈Un,|u-j|>qn cov(X j , X u ) ≤ n (K X (n) -K X (q n ))
and [START_REF] Petrov | Limit Theorems of Probability Theory: Sequences of Independent Random Variables[END_REF] imply that Q 2 (n, t) → 0 for each t ∈ R as n → ∞.

For any n ∈ N introduce a vector (Z n,1 , . . . , Z n,Mn ) ⊤ having the independent components and such that the law of Z n,k coincides with the law of Y n,k /v n , k = 1, . . . , d. Due to Lemma 2 for all s = 1, . . . , M n

varZ n,s = varZ n,1 ∼ p n K X (p n )/ n K X (n), n → ∞. (14)
Thus

Mn s=1 varZ n,s = M n varZ n,1 → 1, n → ∞, (15)
since

M n p n ∼ d k=1 [n k /(p (k) n + q (k) n )]p (k) n ∼ n and K X (p n )/K X (n) → 1 as n → ∞.
For arbitrary ε > 0, taking into account the stationarity of X, we have

Mn s=1 EZ 2 n,s I{|Z n,s | > ε} = M n n K X (n) EY 2 n,1 I{Y 2 n,1 > ε 2 n K X (n)} = M n p n K X (p n ) n K X (n) E S(U (1)
n ) 2 p n K X (p n ) I S(U (1)
n ) 2 p n K X (p n ) > ε 2 n K X (n) p n K X (p n ) → 0, n → ∞,
in view of ( 14), [START_REF] Zolotarev | Modern Theory of Summation of Random Variables[END_REF] and because

n K X (n) p n K X (p n ) → ∞ as n → ∞.
We also used uniform integrability of {S(U

n ) 2 /( p n K X (p n )), n ∈ N d }. Indeed, this is a subfamily of the uniformly integrable family {S 2 n /( n K X (n)), n ∈ N d }. The Lindeberg theorem (see, e.g., [START_REF] Kallenberg | Foundations of Modern Probability[END_REF], p. 69) implies that Thus Q 3 (n, t) → 0 for each t ∈ R as n → ∞. The proof is complete.

Proof of Theorem 2. For a wide-sense stationary random field X = {X j , j ∈ Z d } introduce the function R X (r) = j∈Z d :|j|≤r cov(X 0 , X j ), r ∈ N.

This function R X (•) is close in a sense to K(•) defined in [START_REF] Esary | Association of random variables, with applications[END_REF]. They coincide if d = 1. Clearly, for d ≥ 1 K(r) ≤ R X (r) ≤ K(r √ d), r ∈ N.

Consequently, if K ∈ L(N), then R X ∈ L(N), and vise versa if R X ∈ L(N), then K ∈ L(N). Now for a sequence (C r ) r∈N it is not difficult to obtain the desired result following the scheme of the proof of Theorem 1 and using R X instead of K X .

Remark 2 Lemma 2 shows that in Theorems 1 and 2 instead of normalizations √ varS n and varS(C r ) for partial sums one can use n K X (n) and r d/2 K(r), respectively.

  )) and M 0 (r + 1) = (M 0 (r) ∨ N 0 (R(r + 1))) + 1 for r ∈ N where, as usual, 1 = (1, . . . , 1) ⊤ ∈ R d and (a(1) , . . . , a(d) ) ∨ (b(1) , . . . , b (d) ) = (a(1) ∨ b(1) , . . . , a (d) ∨ b(d) ).

EE

  exp{itZ n,s }exp -t 2 2 → 0, n → ∞.It remains to note that j∈Jn exp{itZ n,s }.

The work is partially supported by RFBR grant 10-01-00397.

Lomonosov Moscow State University and University Paris-6 -Pierre and Marie Curie.

Acknowledgments. The author is grateful to Professors I.Kourkova and G.Pages for invitation to LPMA of the University Pierre and Marie Curie, he would like also to thank all the members of the LPMA for hospitality.


Guillaume Munch-Maccagnoni

From delimited CPS to polarisation

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Continuation-passing style (CPS) translations are a paradox in the theory of programming languages, because they show that the λ calculus, this purely functional, idealised paradigm of computation, can be diverted so as to seemingly contradict the purely functional paradigm:

1. CPS translations give firm grounds for the notion of evaluation order, by "hard-coding" the order in the structure of the resulting term (Plotkin [Plo75]).

2. They give semantics of non-functional operators like call/cc.

3. Using continuation-passing it is possible to manipulate the output of the computation, not only the input. This highlights the possible symmetry between the two notions (see e.g. Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF]), and thus further departs from the functional point of view.

Understanding which abstract structures are involved in these translations is fruitful: the call-by-value CPS translation for instance inspired no less than the use of strong monads to describe the semantics of effects in call-by-value programming languages (Moggi [Mog89]). Monads however are not sufficient to describe all the existing CPS semantics, as they do not account for the symmetry inherent to CPS: for instance, the call-by-name CPS translation of Lafont, Reus and Streicher [START_REF] Lafont | Continuation semantics or expressing implication by negation[END_REF] is categorically dual to the call-by-value one (Selinger [Sel01]) -which means that if we see computation from an external point of view, the dynamics of expressions in the one coincide with the dynamics of evaluation contexts in the other. Therefore, while some CPS semantics account for monadic constructions, some others account for comonadic ones.

Polarisation

λµ n/v CPSn/v 1) / / / / LC 2) λ LLP 3) o o
A single structure which accounts for both of these dual constructions yet exists in proof theory, under the form of Girard's polarised classical logic (LC) [START_REF]A new constructive logic: Classical logic[END_REF]. LC was invented to provide a constructivisation of classical logic that would retain the symmetries of classical logic -at the cost of relaxing other properties such as the associativity of composition [START_REF] Laurent | Polarized and focalized linear and classical proofs[END_REF]. The most important symmetry kept is the involutivity of negation, by which ¬¬A is not only equivalent to A, but isomorphic to it.

Here we are concerned about understanding how notions such as polarities and the involutive negation of LC, once endowed with the proper computational interpretation, give a better view of what we can encode with CPS translations.

To do so, we show how CPS translations can be factored through LC, and isolate the three above aspects in successive steps.

Step 1) explains strictness (as in call-by-value) and laziness (or demand-driven-ness, as in call-by-name rather than call-byneed) of a λ calculus with control operators (such as Parigot's µ [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF]) as the result of a choice, for the constructs of a language, of polarities of LC. Conversely this allows us to see LC through Curry-Howard as a programming language with (call/cc-related) effects that mixes demand-driven computations and data-driven computations (an interpretation that we introduced in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]).

Step 2) is the standard translation from LC to Laurent's socalled Polarised Linear Logic (LLP) [START_REF] Laurent | Etude de la polarisation en logique[END_REF]. We show how at the level of the computational interpretation it relates the polarities of LC to the ones of LLP. While in LC expressions of both polarities may carry effects, in LLP they take a lower-level form: positives denote primitive elements of data (such as values), while negatives are defined by how they react to such data. These primitive ingredients yield demand-driven and data-driven computations in a construction that generalises in a symmetric fashion the monadic semantics of call-by-value -the latter only accounting for the positive part of LC.

Step 3) translates the intuitionistic-looking LLP into the lambda-calculus. It introduces specificities of CPS translations that seem orthogonal to their understanding: "administrative" redexes appear, and a gross simplification is introduced on the structure of the polarity-changing negation. This has the consequence of blurring, from the point of view of CPS, the distinction between terms and evaluation contexts that LLP and LC can describe.

But we are also concerned with generalising polarisation to broader forms of effects, and to this effect we give a similar decomposition for delimited CPS translations.

Delimited CPS translations

Danvy and Filinski introduced in [START_REF] Danvy | A functional abstraction of typed contexts[END_REF] the shift (S) and reset ([•]) control operators in call-by-value λ calculus. The shift operator reifies the current evaluation context under the form of a continuation, and passes it to its argument, like the call/cc control operator. However, unlike call/cc, it only captures the context up to the nearest reset operator -this is why we speak of delimited continuations. Beside standard call-by-value reductions, it has the following reductions:

[E(S(λ f .t))] → [(λ f .t)(λx.E(x))] [V ] → V
Amongst other proposals of calculi with composable first-class continuations, the one of Danvy and Filinski met practical and theoretical success.

To name a few, a result of Filinski [Fil94] showed the considerable expressiveness of these operators: any monadic effect that is expressible -that is, whose laws can be expressed as pure functional terms -is available in direct-style through the use of shift and reset. For instance, with the following:

([k ()] s))

[t] V computes like t in which a memory cell has been initialised to the value V . (We adapted this example from [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF].)

Delimited control operators have also been used to model linguistic phenomena (see Shan [Sha04] for an introduction). And in logic itself, these operators have been used (in a limited fashion) to internalise Markov's principle into intuitionistic logic (Herbelin [Her10]).

Danvy and Filinski describe a denotational semantics under the form of a CPS translation. In this translation, continuations may return and be composed. As a consequence, contrarily to usual CPS translations, the order of evaluation of the target matters, and Danvy and Filinski chose a target in call-by-value. This translation is well understood from the point of view of monadsand the particular type system Danvy and Filinski provide on top of their calculus itself can be described by "annotated" monads (Wadler [Wad94]).

This monadic analysis of the translation and the type system is paralleled by our polarised analysis; and, as far as the positive (call-by-value) part is concerned, our contribution resides in our analysis of the target of Danvy-Filinski's CPS translation.

We found in the literature an analysis of this target that relies on a second CPS translation in order to account for its call-byvalue semantics; and in this last translation it is important that continuations are used linearly (as remarked by Kameyama & Hasegawa for their completeness result [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]). Moreover, it is the composition of the two translations, or "double" CPS translation, that is studied in practice.

Here we see the target of Danvy-Filinski's (single) CPS translation through Girard's linear logic and the so-called "boring" translation [START_REF] Girard | Linear logic[END_REF] based on the !(P ⊥ & Q) coding of implication. This translation indeed yields a semantics of call-by-value (Maraist et al. [START_REF] Maraist | Call-by-name, call-by-value, call-by-need, and the linear lambda calculus[END_REF]), and more precisely, corresponds to Moggi's monadic model [START_REF] Moggi | Computational lambda-calculus and monads[END_REF] where the strong monad is commutative (see Benton & Wadler [BW95]). Thus our axiomatisation of the target corresponds to Moggi's computational calculus together with the following equation that accounts for commutativity:

let x be t in (let y be u in v) = η let y be u in (let x be t in v) . (1)
We call this calculus λ × v , because it turns out to be essentially an extension with pairs of Plotkin's call-by-value λ calculus, which already had implicit in its definition that the order of evaluation (left-to-right or right-to-left) of function application did not matter [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF]. With a clear definition of the target, we can focus our analysis on single rather than double CPS translations.

The cornerstone of our approach is that the "boring" semantics of call-by-value allows us to link up with the polarised approach of LLP and LC. This approach is based on the decomposition of the type of continuations into the exponential modality ! of LLP and the polarity-changing negation that comes from linear logic: ¬ R P = !P ⊥ (we write ¬ R the intuitionistic negation).

Delimited CPS translations replace negation by implication, which can be understood in the context of CPS translations as an annotated negation modality: ¬ Q P def = P → Q. Now, this annotated negation modality can be seen through the "boring" translation as an annotated exponential:

¬ Q P = ! Q P ⊥ def = !(P ⊥ & Q)
(It is an exponential in the sense that ! P is a functor that at least enjoys ! P (A& B) ≃ ! P A⊗ ! P B, since & distributes over &. The idea that we can consider various kinds of exponentials in linear logic is common, see e.g. Danos, Joinet and Schellinx [START_REF] Vincent Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF].) Thus, we can imagine a variant of LLP (which we call LLP ! P ? P ) which is obtained from linear logic by replacing the usual exponential by the annotated modalities ? P and ! P . Then on top of it we can build a variant of LC, whose computational interpretation is a calculus in which we can retrieve existing delimited control calculi.

We can see the fact that LLP lends itself to analogies with callby-value -rather than call-by-name -λ calculus as a theoretical argument in favour of Danvy and Filinski's choice. Indeed, if the target of the CPS translation had been in call-by-name (as in Sabry's variant of the calculus [START_REF] Sabry | Note on axiomatizing the semantics of control operators[END_REF]), then we would have been unable to provide a polarised decomposition.

The interest of polarisation is that it allows us to account for CPS translations that are not directly related to the monadic approach, such as the semantics of call-by-name λµ calculus and indeed of LC itself. We show that this is also the case with delimited control by decomposing a call-by-name variant of Danvy-Filinski's calculus that has been introduced in Herbelin & Ghilezan [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF].

Method

The key technical aspect of this work is the use of a syntax that gives an independent status to evaluation contexts, with their own variables and binders, in the lineage of Curien and Herbelin's λµ μ calculus [START_REF] Curien | The duality of computation[END_REF], which can also be seen as a term assignment for sequent calculus. We introduced L foc in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF] in order to refine the λµ μ calculus to provide a computational interpretation of LC. We see such a notation as a tool for the mind, with which we strive to express the more properties of semantics with the fewest possible symbols.

Another key technical aspect is that we rely on a decomposition of shift and reset into operators that are simpler from the point of view of CPS translations: the µ operator of Parigot [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF] together with a dynamically-scoped continuation variable written tp. This decomposition has been introduced with the λµ tp v calculus of Ariola, Herbelin and Sabry [START_REF] Ariola | A typetheoretic foundation of continuations and prompts[END_REF] and Herbelin provided a syntax for it à la λµ μ in [START_REF] Herbelin | C'est maintenant qu'on calcule, au coeur de la dualité[END_REF].

Technical contribution

λµ tp n/v CPSn/v 1) / / / / L foc, tp 2) CPS z z u u u u u u u u u u λ × v LLP ! P ? P 3) o o
In Section 1, we produce a polarised calculus for delimited control that we call L foc, tp . It is a symmetric (yet confluent) variant of λµ tp that extends L foc . We describe its sound CPS semantics into λ × v . We show that this calculus contains both λµ tp v and its call-by-name variant λµ tp n [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF], in the sense that the constructs of these languages can be defined in L foc, tp and that these definitions induce translations -1) -through which the CPS translations factor.

We also study the typed versions of these calculi and introduce a type-and-effect system for L foc, tp , extension of LC, with annotations of effects related to shifts of polarities. This type system decomposes the type-and-effect systems of λµ tp v and λµ tp n .

In Section 2, we define a system that is essentially Laurent's LLP [START_REF] Laurent | Etude de la polarisation en logique[END_REF] in which the exponentials enjoy a richer structure. We call the system LLP ! P ? P (we omit additives, of which we have no use for our goal). We show how the CPS translation of L foc, tp factors through LLP ! P ? P in a manner that recalls the translation of LC into LLP: 2) & 3).

We explain the modalities ! P and ? P by describing a translation of LLP ! P ? P into LL similar to the one described for LLP by Laurent [START_REF] Laurent | Etude de la polarisation en logique[END_REF].

In Section 3 we compare our approach with extant works.

A polarised calculus for delimited control

We introduce in Fig. 1 a polarised calculus of delimited control (L foc, tp ). The L foc part accounts for polarised classical logic (as in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]), while the tp part account for the delimited control operators of the λµ tp v calculus [START_REF] Ariola | A typetheoretic foundation of continuations and prompts[END_REF].

We describe its CPS semantics and we show that CPS translations of the (call-by-value) λµ tp v calculus of Ariola, Herbelin & Sabry and the (call-by-name) λµ tp n calculus of Herbelin & Ghilezan factor in the following manner:

λµ tp v CPSv POS / / L foc, tp CPS | | x x x x x x x x x λµ tp n CPSn NEG / / L foc, tp CPS | | x x x x x x x x x λ ∧ v λ ∧ v
where the top arrow relies moreover on the derivability of implication in L foc, tp (modulo administrative reductions for the second diagram).

Proposition 1 (Confluence). The reduction → is confluent.

Proof. The reduction → 0 is defined by an orthogonal pattern rewrite system, which implies confluence for → (Nipkow [START_REF] Nipkow | Higher-order critical pairs[END_REF]).

Understanding L foc, tp

1.1.1 Generalities on system L Our syntax models computation as the rewriting of pairs 〈t || e〉, also written c for commands. This rewriting is seen as the interaction between expressions (programs) 〈t | and their context of evaluation | e〉. Thus they are kind of abstract machines states, but abstract ones in the sense that the syntax features variables and binders.

The first example of such a machine is Krivine's abstract machine. It has abstraction, application and a control operator as expressions, and stacks as evaluation contexts:

〈t u || E〉 → 〈t || u • E〉 λx.t u • E → t [u/x] E µα.c E → c [E/α]
This machine describes a call-by-name reduction strategy.

Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF] gave an equally elegant machine for computing in call-by-value: the λµ μQ calculus. It only requires to introduce a new kind of binders on the right.

〈t u || E〉 → 〈t || u • E〉 λx.t u • E → u µx.〈t || E〉 V µx.c → c [V /x] µα.c E → c [E/α]
The µx.c binder must be understood as the "let x be in ..." context, as the one of Moggi's computational λ calculus [START_REF] Moggi | Computational lambda-calculus and monads[END_REF]. The second line reads:

Ē[(λx.t) u] → Ē[let x be [u] in t]
if Ē is some term with a hole that corresponds to the evaluation context E.

One advantage of working with solid contexts is that the equational theory becomes simplified. For instance, the following equation of Moggi's calculus for x fresh in v: let x be t in (let y be u in v) ≃ let y be (let x be t in u) in v becomes superfluous since it can be derived from other rules [START_REF] Curien | The duality of computation[END_REF].

The important remark of Curien and Herbelin was that for the following two tentative reductions:

c[µx.c ′ /α] ? ← -µα.c µx.c ? -→ c ′ [µα.c/x]
then the left one, giving priority to expressions, corresponds to call-by-value, denoting a strict reduction of the expression, while

::= V + | t - (pos. values) V + ::= x | (V, V ′ ) | {t -} (pos. terms) t + ::= x | (V, V ′ ) | {t -} | µα.c | µ tp.c (neg. terms) t -::= α | µ(κ, κ ′ ).c | µ{α}.c | µx.c | tp (commands) c ::= 〈t + || t -〉 = α 〈t -|| t + 〉
Reductions. Let → the contextual closure of the following rewrite rules:

(µα) µα.c t -→ 0 c[t -/α] (µx) V + µx.c → 0 c[V + /x] (µ(κ, κ ′ )) (V, V ′ ) µ(κ, κ ′ ).c → 0 c[V /κ, V ′ /κ ′ ] (µ{α}) {t -} µ{α}.c → 0 c[t -/α] (µ tp) * µ tp. V + tp t -→ 0 V + t - * with tp possibly free in V +
tp is not subject to α conversion.

Equations. The following equations are contextual:

(η + ) µα. t + α = η t + (η -) * µq. q t -= η t - (c V ) * V µq. t + µq ′ .c = η t + µq ′ . V µq.c (η tp ) µ tp.c tp = η c (c tp ) * µ tp. W µq.c t -= η W µq. µ tp.c t - *
where q is x, {α} or (κ, κ ′ ) and where W is V + or µ tp.c ′ . Note that the syntax in Fig. 1 allows for the two writings t + t -and t -t + , which are considered equal in the same way as the λ calculus equates λx.x and λ y. y. Note also that reduction rules always give priority to positives t + over negatives t -, in the sense that µx.c only reduces when supplied a value V + . This priority is further reflected in our convention that negative terms are values.

We will show how to derive both call-by-name and call-byvalue abstractions and applications, and then we will explain what computational and logical meaning we give to an equality like t + t -= α t -t + .

The call-by-value implication can be derived if we choose to write t + t -instead of t -t + (that is, if we read t + as expressions).

Example 2 (Call-by-value implication). Given t + , u + positive terms of L foc, tp and u -a negative term, we define:

λx.t + def = {µ(x, α). t + α } t + • u - def = µ{α}. t + µx. α (x, u -) t + u + def = µα. t + u + • α .
It is an easy exercise to check that these definitions allow us to retrieve the reduction rules described above for call-by-value.

Conversely, the call-by-name implication can be derived if we choose to write t -t + instead of t + t -(that is, if we read t -as expressions).

Example 3 (Call-by-name implication). Given t -, u -negative terms and V a positive value of L foc, tp , we define:

λα.t - def = µ(α, x). t -x t -• V def = (t -, V ) t -u - def = µx. t -u -• x
The reader might be surprised -here and later -to see the call-by-name abstraction written λα rather than λx. This is due to the fact that we encode expressions with negative terms, and therefore our notation for negative variables (α, β...) apply, while the positive co-variables are written x, y... We found it necessary -with apologies to the reader -to make the difficult choice of going against tradition with our notations, because the distinction between polarities of variables is more important to stress in L foc than the distinction between variables and covariables.

Similarly to the call-by-value case, and modulo the exchange of notations between α's and x's, one can easily check that these definitions allow us to retrieve the rules of reduction above for the Krivine machine (in particular stacks E become of the form V + ).

... and polarisation

At this point the reader might think that our syntax is just an artificial way of writing the two deterministic variants of Curien-Herbelin λµ μ or Wadler's Dual Calculus with one syntax, based on a play on words (we leave the tp part aside for the moment). This is only an illusion caused be our choice of presentation, as we explain now.

As made clear by Wadler [START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF], the rules of negation in sequent calculus can be interpreted computationally as the constructors that exchange expressions and contexts -such constructors, written not, are unary, and they are such that if t is an expression, then not(t) is a context; and conversely.

In the Dual Calculus, not(t) is always a value even if t is not, and the constructs are given the following reduction rule:

not(t) not(u) → 〈u || t〉
c : (⊢ Γ, T ) ⊢ V : P * ; Γ ⊢ t -: N | Γ, T ⊢ t + : P Q | Γ, T Implicit negation (X ) ⊥ def = X ⊥ (P * ⊗ Q * ) ⊥ def = P * ⊥ & Q * ⊥ ´NP ⊥ def = ˆN ⊥ P
where N P ⊥ is N ⊥ P and N ⊥ is defined dually, such that A ⊥⊥ = A.

Identity (ax + ) ⊢ x : P; x : P ⊥ (ax -) ⊢ α : N | α : N ⊥ P , tp : P c : (⊢ x : N , Γ, T ) (µ -) ⊢ µx.c : N | Γ, T c : (⊢ α : P Q , Γ, T ) (µ + ) ⊢ µα.c : P Q | Γ, T ( tp) ⊢ tp : N | tp : N ⊥ c : (⊢ Γ, tp : P) (µ tp) ⊢ µ tp.c : P Q | Γ, tp : Q ⊢ t + : P Q | Γ, tp : R ⊢ t -: P ⊥ Q ; ∆ (cut) t + t -: ( ⊢ Γ, ∆, tp : R) Structure ⊢ V + : P; Γ (der) ⊢ V + : P Q | Γ, tp : Q ⊢ t -: N | Γ, tp : P (prom) ⊢ t -: N P ; Γ c : ( ⊢ Γ, T ) (w + ) c : ( ⊢ x : N , Γ, T ) c : (⊢ x : N , y : N , Γ, T ) (c + ) c x y : (⊢ x : N , Γ, T ) c : ( ⊢ Γ, T ) (w -) c : ( ⊢ α : P Q , Γ, T ) c : (⊢ α : P Q , β : P Q , Γ, T ) (c -) c α β : (⊢ α : P Q , Γ, T )
Plus rules similar to (w ± ) and (c ± ) for t + , t -and V which we do not mention. Thus if we go back to L foc, tp , we see that our equality:

Logic ⊢ V : P * ; Γ ⊢ V ′ : Q * ; ∆ (⊗) ⊢ (V, V ′ ) : P * ⊗ Q * ; Γ, ∆ c : (⊢ κ : N * , κ ′ : M * , Γ, T ) ( & ) ⊢ µ(κ, κ ′ ).c : N * & M * | Γ, T ⊢ t -: N P ; Γ (´) ⊢ {t -} : ´NP ; Γ c : (⊢ α : P Q , Γ, T ) (ˆ) ⊢ µ{α}.c : ˆPQ | Γ, T
t -t + = α t + t -
amounts to no less than omitting the constructors for negation -in the same way as negation is implicit in the proof nets of linear logic, for instance. As a consequence, negation becomes involutive, since, when not is unwritten, not(not(t)) is same as t.

Here we encounter the two "traps" mentioned by Girard [START_REF]A new constructive logic: Classical logic[END_REF]. Trap #1: our α-equality above forces negation to be involutive; but it is false to think that forcing ¬¬A to be isomorphic to A was sufficient -just taking call-by-value or call-by-name classical logic and imposing this isomorphism as an additional axiom would not work, since this results in equating all terms (see e.g. [START_REF]A new constructive logic: Classical logic[END_REF][START_REF] Selinger | Control categories and duality: On the categorical semantics of the lambda-mu calculus[END_REF]).

Trap #2: identifying t + t -with t -t + is not essential to our approach. In fact we could have made this involutive negation explicit in the syntax, as did Girard for LU [START_REF]On the unity of logic[END_REF] or Danos et al. for LK η pol [START_REF]A new deconstructive logic: Linear logic[END_REF]. Their descriptions of the explicit involutive negation amount to the following: we observe that double negation is not involutive in the Dual Calculus because not(not(t)) (of type ¬¬A) is a value even when t (of type A) is not -thus their computational behaviour can be different (for instance for t = µα.c with α fresh in c). The solution is to get rid of the restriction by which not(t) is a value, by allowing the computation to continue under not in case t is not a value.

We can do so by introducing rules like the following:

∀t non-value, not(t) u → ς µx. not(x) u t
(and symmetrically). On the left-hand side of this reduction, not(t) takes precedence whatever the u, while in the right-hand side, t takes precedence. Thus not(t) must be a positive expression, while t must be a positive context. We conclude that the connective of negation must exchange polarity of formulae (contrarily to the negations of e.g. the Dual Calculus), and only exists in a calculus where there are both positive and negative expressions.

We made this negation implicit instead of explicit in L foc , for one reason: the CPS translation of LC is sort of an unsound semantics for the polarity-changing negation, in the sense that it anyway forces the identification of t + t -with t -t + (see Section 2.1). Therefore our analysis would be no better informed if we had explicit rules for negation: these rules would simply be mapped to the identity transformation on CPS terms.

Polarised connectives

On the logical side, the want for symmetry and in particular an involutive negation is certainly of interest. But here, we are also interested in polarisation because it allows us to mix positive and negative expressions.

The calculus we present has constructors for the multiplicative connectives of polarised classical logic, which are written ⊗ (the positive conjunction) and & (the negative disjunction) which can be understood as a strict pair and a primitive and symmetric version of implication. Additives (the lazy pair & and the strict sum ⊕) as well as units are omitted since they are not useful for decomposing CPS translations.

L foc, tp has a negation which we chose to leave implicit in the syntax, as we have already discussed. Also, it has coercions of polarities, or shifts, which can be implicit in the notation -for instance we can form strict pairs with negative terms. They can also be explicit using the "unary patterns" {•} and µ{•}.c2 , associated to the connectives ´and ˆ. Explicit shifts are typically used at the root of a term, such as in the definition of call-by-value λ abstraction above. We could simulate explicit shifts by implicit ones, but our particular design choice will provide us accuracy in the decomposition of CPS translations, by allowing us to treat particularly such cases where the shift is at the root. Now, if we go back to the definitions of λ abstraction, we see that

• ⊥ &
• is indeed a primitive version of implication if we define the follow-ing:

λx.t - def = µ(x, y). t -y
From such a construct, we see that it is possible to derive the call-by-value (resp. call-by-name) λ abstraction defined above by only introducing the appropriate polarity coercions. (We compare such a primitive implication to a direct-style variant of Levy's Call-By-Push-Value paradigm [START_REF] Blain | Call-by-push-value: A subsuming paradigm[END_REF] which provides a similar decomposition of call-by-value and call-by-name implications in a non-symmetric setting.)

η restriction

On a more technical side, we note that positive terms enjoy what is called the η restriction in Danos et al. [START_REF]A new deconstructive logic: Linear logic[END_REF], that is, any non-value is of the form µα.c or µ tp.c, which is one way of expressing the focalisation of positive constructors. This corresponds also to the notion of administrative normal form, where (for instance) a pair of strict terms t and u (computed from left to right, say) is not given in the syntax but defined as:

(t, u) def = let x be t in let y be u in (x, y) which in L foc is represented by µα. t µx. u µ y.〈(x, y) || e〉 .
This means that our diagrams omit (if we wanted to be consistent with traditions) one additional trivial step responsible for the restriction to administrative normal forms, starting from a variant of L foc, tp without this η restriction, where focalisation is expressed instead through reduction rules like the following:

(t, u) e → t µx. u µ y.〈(x, y) || e〉 if (t, u) is not a value
The corresponding trivial translation step replaces (t, u) by its above definition, which reflects the arbitrary choice between leftto-right and right-to-left evaluation for the strict pair.

Delimited control operators

Following Ariola, Herbelin & Sabry [AHS04], we can derive shift and reset as follows:

S(t + ) def = µα. t + λx.µ tp.〈x || α〉 tp [t + ] def = µ tp. t + tp
To help understand the rules associated to tp, let us introduce the following notation:

tp = t 1 ; . . . ; tp = t n def = µ tp. • • • µ tp.c t 1 • • • t n
and let us write σ = ( tp = t 1 ; . . . ; tp = t n ) for such a thing looking like an environment. Note that the definition does not yield uniqueness of the decomposition of a command c under the form c ′ [σ]. Now we can look at the rules of L foc, tp , in particular the ones related to tp, as if they were rules of an environment-machine:

µ tp.c t -[σ] = c[ tp = t -; σ] V + tp tp = t -; σ → V + t -[σ] c tp = tp; σ = η c[σ] c tp = µq.c ′ ; tp = t -; σ = η c tp = µq.c ′ tp = t -; σ
The environment σ is only accessed when the variable tp comes in head-position, that is to say, is encountered against a value V + .

It is therefore sensible to consider a head-reduction strategy → h ⊆ → for terms of L foc, tp defined by the following:

c[σ] → h c ′ [σ] whenever c → 0 c ′ .
With this head-reduction we recover (an abstract and symmetric variant of) the environment machines for λµ tp v of Herbelin and Ghilezan [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF]. (See also Herbelin's [Her05].)

CPS translation

See Fig. 3 for the syntax of the target of our CPS translations (λ × v ), and Fig. 4 for the CPS translation of L foc, tp into λ × v . The abstraction for a pair is obtained with λ(x, y).t

def = λz.let (x, y) be z in t . Remark 4. In λ × v , if t → admin u, then t ≃ u.
Proof. We note that we have in general:

(λx.u) t = η (λx.u) (let x be t in x) = η let x be t in (λx.u) x → let x be t in u
Here we have u = E * [x] with E * a finite sequence of linear contexts and therefore we can conclude (by induction on E * ) with a sequence of = η equivalences.

Proposition 5 (Compositionality). For p a command or a term, x and α variables, V a value, V + a positive value and t -a negative term, one has:

V V + x VAL = V VAL V +VAL x p V + x CPS = p CPS V +VAL x p t -α CPS = p CPS t -CPS k α .
Proof. Here and in the remaining of the paper, proofs that are omitted are routine verification.

Proposition 6 (Simulation).

If L foc, tp ⊢ c → c ′ then λ × v ⊢ c CPS → + c ′ CPS .
Proof. The result holds for → 0 by case analysis. We conclude by induction on the definition of a contextual closure for → 0 .

Proposition 7 (Soundness).

If L foc, tp ⊢ c ≃ c ′ then λ × v ⊢ c CPS ≃ c ′
CPS . (Here and for other systems defined in this paper, we always define

≃ def = (= η ∪ ↔) * .)
Proof. Proof is routine; the key observation for the cases of the (c tp ) and (c V ) rules is that (λq.t) u ≃ let q be u in t in λ × v .

A type-and-effect system

We propose in Fig. 2 a type system for L foc, tp which is an extension with annotations of effects of Girard's LC -or more precisely of Danos et al's LK η pol [START_REF]A new deconstructive logic: Linear logic[END_REF]. In order to obtain a convenient type system, we had to add an intermediate judgement that corresponds to the stoup3 of LC [START_REF]A new constructive logic: Classical logic[END_REF]. This distinguished formula, which asserts a linearity constraint stronger than classical provability, is inspired by Andreoli's focusing proof search discipline [START_REF] Andreoli | Logic programming with focusing proof in linear logic[END_REF]. Its purpose in [START_REF]A new constructive logic: Classical logic[END_REF] is to formulate the focalising cut elimination procedure. (See Curien & the author's [START_REF] Curien | The duality of computation under focus[END_REF] for a variant of L foc where the role of the stoup is emphasised.)

Our stoup appears in the judgement ⊢ V : P * ; Γ where V is a value, possibly negative, and P * is of the form P or N P . We feel that allowing negatives in the stoup -a choice directly related to our convention that negatives are values -is a sensible choice for having a good treatment of coercions between polarities in our sequent calculus.4

Syntax

V ::= x | λx.t | (V, V ) t ::= V | t t | let x be t in t | let (x, y) be t in t Reduction rules (λx.t) V → t [V /x] let x be V in t → t [V /x] let (x, y) be (V, V ′ ) in t → t[V /x, V ′ / y]
Equational theory Linear evaluation contexts are defined with:

E ::= let q be in t | let q be t in | t | t
where q stands for x and (x, y).

λx.(V x) = η V let q be t in q = η t let q be t in E[u] = η E[let q be t in u] let q be V in λx.t = η λx.let q be V in t Administrative reduction We define for any n ≥ 0, λx.E 1 [• • • [E n [x]]] t → admin E 1 [• • • [E n [t]]] Figure 3: A λ v calculus with pairs: λ × v . VAL : V → V CPS : t + → t x VAL def = x V +CPS def = k V +VAL (V, V ′ ) VAL def = (V VAL , V ′ VAL ) (µα.c) CPS def = let k α be k in c CPS {t -} VAL = t -VAL def = t -CPS µ tp.c CPS def = k c CPS CPS : c → t t + u -CPS = u -t + CPS def = t +CPS u -CPS k
(κ being x or α in the source, and x or k α in the target.)

CPS : t -→ V α CPS def = k α tp CPS def = λx.x µx.c CPS def = λx.c CPS (µ(κ, κ ′ ).c) CPS def = λ(κ, κ ′ ).c CPS (µ{α}.c) CPS def = λk α .c CPS Figure 4: The CPS translation of L foc, tp into λ × v .
CPS translation We assume that λ × v is given a standard system of simple types with connectives →, ×. What justifies our type system is that it is mapped through the CPS translation into the type system of λ × v . Positive and annotated negative types translate as follows:

X CPS def = X ´NP CPS def = (N ⊥ ) CPS → P CPS (P * ⊗ Q * ) CPS def = P * CPS × Q * CPS N P CPS def = (N ⊥ ) CPS → P CPS
Judgements translate as follows:

c : (⊢ Γ, tp : P)

Γ ⊥ CPS ⊢ c CPS : P CPS ⊢ V : P * | Γ Γ ⊥ CPS ⊢ V CPS : P * CPS ⊢ t -: N | Γ, tp : P Γ ⊥ CPS ⊢ t -CPS : N P CPS ⊢ t + : P Q | Γ, tp : R Γ ⊥ CPS , k : P ⊥ Q CPS ⊢ t +CPS : R CPS with Γ ⊥ CPS = x : N ⊥ CPS , k α : P ⊥ Q CPS whenever Γ = ( x : N , α : P Q ).
The fact that the type system we gave for L foc, tp maps into a system of simple types for λ × v could be checked directly, but it will become obvious once we decompose the translation in smaller steps through LLP in Section 2.

Call-by-value delimited control

Proposition 8 (Soundness). If λµ tp

v ⊢ p ≃ p ′ then λ × v ⊢ p CPSv ≃ p ′
CPSv where p is a term or a command. 5 We differ from [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF] in the treatment of administrative redexes.

If we wanted to be closer, we would have defined (t u) CPSv = t CPSv (λx.u CPSv (λ y.x ( y, k)) k ) k and µα.c CPSv = c CPSv k k α . But then we lose the fact that the administrative variable k is bound linearly. Yet the second part of the decomposition (Section 2) prompted us to be careful to treat "administratively" only those redexes that bind variables in a linear manner.

We come close to having a simulation result as well, but do not, essentially because of the structural substitution defined in the figure .  The definitions in Example 2 canonically induce a translation • POS from terms and commands of λµ tp v to terms and commands of L foc, tp (just take [e] to | e〉, x to x, µα to µα and µ tp to µ tp):

λµ tp v • POS --→ L foc, tp Proposition 9 (Soundness). If λµ tp v ⊢ p ≃ p ′ then L foc, tp ⊢ p POS ≃ p ′
POS where p is a term or a command.

Proof. Routine verification except for λx.(V x) ≃ V . The latter follows from the fact that we have {µx. V µ{α}.〈α || x〉 } ≃ V as a consequence of the rule (c V ).

Proposition 10 (Factoring). For p a command or a term of λµ tp v , we have p POS CPS = p CPSv . The CPS translation is essentially6 the one of Herbelin & Ghilezan. However we replaced Herbelin & Ghilezan's target calculus (a call-by-name λ calculus with pairs) by λ × v . We could do so because the image of this CPS translation is indifferent to the evaluation strategy as far as reduction rules are concerned. This is witnessed by the fact that this alternate semantics validates the same rules of reductions.

Call-by-name delimited control

However, with λ × v as a target, the translation no longer validates the equation [ tp] µ n tp.c = η c given in [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF], in the sense that we do not have

Reductions

The following reductions are contextual:

(λx.t) V → t [V /x] (µα.c) t → µβ.c [β] ( t) α (β fresh) V (µα.c) → µβ.c [β] (V ) α (β fresh) [e] µα.c → c [e/α] µ tp.[ tp] V → V (even if tp occurs in V ) (where c [β] E[ ] α is the structural substi- tution: "replace all occurrences of the form [α] t in c by [β] E[t]".)
Equational theory The following equations are contextual: equation is the consequence of a linearity restriction that the µ n tp.c binder enforces on the use of µ tp.c, and the equation is not validated here because the restriction is not present in the broader L foc, tp .

E v ::= | E v [ t] | E v [V ] [ tp] µ tp.c = η c µ tp.[e] ((λx.t) (µ tp.c)) = η (λx.µ tp.[e] M ) (µ tp.c) µα.[e] ((λx.t) u) = η (λx.µα.[e] t) u µα.[α] t = η t λx.(V x) = η V (λx.E v [x]) t = η E v [t] . CPS translation from λµ tp v to λ × v CPSv : t → t µ tp.c CPSv def = k c CPSv VALv : V → V V CPSv def = k V VALv x VALv def = x (t u) CPSv def = let k be k in t CPSv CPSv : c → t (λx.t) VALv def = λ(x, k).t CPSv [k/k] λx.u CPSv λ y.x ( y, k) k k ([α] t) CPSv def = t CPSv k α k µα.c CPSv def = let k α be k in c CPSv [ tp] t CPSv def = t CPSv [λx.x/k]
c ::= [x] t | [ tp] t ≃ def = (↔ ∪ = η ) * Reductions (λα.t) u → t [u/α] (µx.c) t → µ y.c [ y] ( t) x ( y fresh) [ y] µx.c → c
Our explanation for the fact that we do not consider the equation [ tp] µ n tp.c = η c is that the λµ tp n calculus is not defined by its CPS semantics but arose as a particular way to solve critical pairs in a non-deterministic λµ tp calculus. But such a syntactic characterisation, as we see, is not devoid of ambiguity if we start looking at extensions of the calculus. Indeed, it is possible to see L foc, tp in particular as one extension of λµ tp n that invalidates the equation.

Proposition 11 (Soundness). If λµ tp

n ⊢ p ≃ p ′ then λ × v ⊢ p CPSn ≃ p ′
CPSn where p is a term or a command. Because of the structural substitution again, and like [HG08], we come close to having a simulation result as well, but do not.

Given t -a negative term and c a command of L foc, tp , we define:

µ n tp.c def = µx. µ tp.c µ(α).〈α || x〉 [ tp] t - def = (t -) tp .
Together with the definitions of Example 3, these definitions canonically induce a translation

The decomposition of type-and-effect systems

Herbelin and Ghilezan give in [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF] type-and-effect systems for λµ tp v and λµ tp n . For λµ tp v , sequents are of the form:

x : A ⊢ t : B T | α : C U ; tp : D
where the connective for implication has two annotations: A T → B U . Now the positive coding of implication yields for A, B, T, U positive formulae of L foc, tp the following positive definition for this connective:

A T → B U def = ´(A ⊥ & B U ) T .
It is related to the positive translation [START_REF] Laurent | Etude de la polarisation en logique[END_REF] through the translation into LLP ! P ? P described in next section. With this definition we find back the type system for λµ tp v as a sub-part of our type system for L foc, tp .

For λµ tp n , sequents are of the form:

A Σ → B def = A ⊥ Σ & B ⊥ def = 0 C • Σ def = ´CΣ
where 0 is the positive false constant. This allows us to retrieve the type-and-effect system of λµ tp n as a sub-part. This coding is related to the negative translation of call-by-name λµ into LLP [START_REF] Laurent | Etude de la polarisation en logique[END_REF].

LLP with annotated exponentials

Laurent's LLP [START_REF] Laurent | Etude de la polarisation en logique[END_REF][START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF] drew attention by giving a fresh view on translations of classical logic. LLP was provided with a theory of proof Such a graphical representation helped in understanding that the (Lafont-Reus-Streicher variant [START_REF] Lafont | Continuation semantics or expressing implication by negation[END_REF] of the) call-by-name CPS translation is very similar [Lau02, CM10] to Girard's translation of call-by-name λ calculus into linear logic, although the former could seem more intricate than the latter.

A key point for this clarification is that LLP decomposes the type of continuations into a co-variant modality "!" and an involutive negation.

We introduce a variant of Laurent's LLP we call LLP ! P ? P . It factors the CPS translation of L foc, tp the following way: 1. • LLP is an extension of the translation of LC into LLP given by Laurent [START_REF] Laurent | Etude de la polarisation en logique[END_REF].

2. • NJ , seen backwards, amounts to a rephrasing of the target of CPS translations, where we emphasise the duality between positives and negatives (in the sense of e.g. Zeilberger [Zei08, Zei09]).

See Fig. 7 for a definition of an untyped term syntax for LLP ! P ? P and Fig. 8 for a typing system. Like for L foc, tp , the equation t + t -= α t -t + is the consequence of our choice to let the involutive negation of LLP implicit.

We write µ(x, y) ⋄ .c def = µz ⋄ . z µ(x, y).c .

Proposition 14 (Confluence). The reduction → is confluent.

Proof. Again, the reduction → 0 is defined by an orthogonal pattern rewrite system, which implies confluence for → (Nipkow [Nip91]).

2.1 From LLP ! P ? P to λ × v In Fig. 9 we translate LLP ! P ? P into λ × v . We observe the following: 1. The translation would identify t + t -and t -t + even if we provided LLP ! P ? P (and consequently L foc, tp ) with an explicit negation, which means that the CPS semantics only provides a coarse description of this negation; 2. A negative term t -is sent onto a context of λ × v , i.e. a term with a hole (written k here), with the type of t -being mapped to the hole. As a consequence, the translation of sequent calculus into natural deduction accounts for the appearance of administrative redexes.

Proposition 15 (Simulation & soundness). If LLP !

P ? P ⊢ c → c ′ then λ × v ⊢ c NJ → i c ′ NJ for some i ≤ 1. If LLP ! P ? P ⊢ c = η c ′ then λ × v ⊢ c NJ = η c ′ NJ .
Proposition 16 (Factoring). For p a command or a term of L foc, tp , we have λ × v ⊢ p LLP NJ = η p CPS and for V a value we have

λ × v ⊢ V LLP+ NJ = η V VAL .
Proof. We have:

(µ tp.c) LLP NJ = let x be k in let y be c LLP NJ in x y = η k c LLP NJ .
In all other cases we have an equality.

Recall that λ ×

v is given a standard system of simple types with connectives →, ×. Formulae and judgements translate as follows:

X NJ def = X (P ⊗ Q) NJ def = P NJ × Q NJ ! P N NJ def = (N ⊥ ) NJ → P NJ ⊢ t : P | Γ Γ ⊥ NJ ⊢ t NJ : P NJ ⊢ t : N | Γ, ⋆ : P Γ ⊥ NJ , k : N ⊥ NJ ⊢ t NJ : P NJ c : (⊢ Γ, ⋆ : P) Γ ⊥ NJ ⊢ c NJ : P NJ with Γ ⊥ NJ = x : (N ) ⊥ NJ whenever Γ = x : N .
2.2 From L foc, tp to LLP ! P ? P In Fig. 10 we translate L foc, tp into LLP ! P ? P . This is an extension to delimited control of the translation of LC into LLP.

For non-delimited control and when negation is explicit, a sequent of LC is translated into a sequent of LLP according to the following pattern [START_REF] Laurent | Etude de la polarisation en logique[END_REF]:

P, N ⊢ LC Q, M P, !N ⊢ LLP ?Q, M
If we restrict to either polarity, this becomes:

P ⊢ LC Q P ⊢ LLP ?Q N ⊢ LC M !N ⊢ LLP M
For the only-positive case, the construction is related to Moggi's description of computations in call-by-value through the Kleisli category for a monad, here the !? monad of LLP. The onlynegative case, by symmetry, is related to the co-Kleisli of the ?! co-monad of LLP. (These two dual "mono-polarised" constructions have been investigated by Selinger [START_REF] Selinger | Control categories and duality: On the categorical semantics of the lambda-mu calculus[END_REF].)

The full translation thus describes a construction which is a generalisation of Kleisli constructions of both a monad and a comonad.

Seen from the proof-theoretic side, the goal of this construction of LC from LLP is to conceal exponentials, such that shifts of LLP ! P ? P Syntax uses positive variables x, y . . . and a distinguished negative variable ⋆.

(values)

V

::= x | (V, V ) | µx ⋄ .c (positive terms) t + ::= V | µ⋆.c (negative terms) t -::= ⋆ | µx.c | µ(x, x).c | V ⋄ (commands) c ::= 〈t + || t -〉 (= α 〈t -|| t + 〉)
Reductions Let → the contextual closure of the following rewrite rules:

V µx.c → 0 c [V /x] (V, V ′ ) µ(x, y).c → 0 c V, V ′ x, y µx ⋄ .c V ⋄ → 0 c [V /x] µ⋆. t + ⋆ t -→ 0 t + t -

Equational theory

The following equations are contextual:

µq. q t -= η t - t + µq. u + µq ′ .c = η u + µq ′ . t + µq.c µx ⋄ . V x ⋄ = η V t + µq. µ⋆.c u -= η µ⋆. t + µq.c u - µ⋆.c ⋆ = η c V µq. µx ⋄ .c u -= η µx ⋄ . V µq.c u -
where q denotes x and (x, y).

P ::= X | P ⊗ P | ! P N (negative) N ::= X ⊥ | N & N | ? P P Implicit negation (X ) ⊥ def = X ⊥ (P ⊗ Q) ⊥ def = P ⊥ & Q ⊥ ! P N ⊥ def = ? P N ⊥ (X ⊥ ) ⊥ def = X (N & M ) ⊥ def = N ⊥ ⊗ M ⊥ ? Q P ⊥ def = ! Q P ⊥ Judgements Γ, ∆ of the form x 1 : N 1 , . . . , x n : N n Π of the form ⋆ : P (Π = always) ⊢ t -: N | Γ, Π ⊢ t + : P | Γ c : (⊢ Γ, Π) Identity (ax + ) ⊢ x : P | x : P ⊥ (ax -) ⊢ ⋆ : N | ⋆ : N ⊥ c : (⊢ x : N , Γ) (µ -) ⊢ µx.c : N | Γ c : (⊢ Γ, ⋆ : P) (µ + ) ⊢ µ⋆.c : P | Γ ⊢ t + : P | Γ ⊢ t -: ⊥ | ∆, Π (cut)
t + t -: ( ⊢ Γ, ∆, Π) Logic ⊢ V : P | Γ ⊢ V ′ : Q | ∆ (⊗) ⊢ (V, V ′ ) : P ⊗ Q | Γ, ∆ c : (⊢ x : N , y : M , Γ, Π) ( & ) ⊢ µ(x, y).c : N & M | Γ, Π Structure c : (⊢ x : N , Γ, ⋆ : P) (prom) ⊢ µx ⋄ .c : ! P N | Γ ⊢ V : P | Γ (der) ⊢ V ⋄ : ? Q P | Γ, ⋆ : Q c : (⊢ Γ, Π) (w) c : (⊢ x : N , Γ, Π) c : (⊢ x : N , y : N , Γ, Π) (c) c x y : (⊢ x : N , Γ, Π)
Plus rules similar to (w) and (c) for t + and t -we do not mention.

Figure 8: A system of simple types for LLP ! P ? P .

NJ : t + → t NJ : t -→ t NJ : c → t x NJ def = x ⋆ NJ def = k t + u -NJ = u -t + NJ (V, V ′ ) NJ def = (V NJ , V ′ NJ ) µx.c NJ def = let x be k in c NJ def = u -NJ t +NJ k (µx ⋄ .c) NJ def = λx.c NJ µ(x, y).c NJ def = let (x, y) be k in c NJ µ⋆.c NJ def = c NJ V ⋄ NJ def = k V NJ Figure 9: The translation of LLP ! P ? P into λ × v LLP+ : V → V LLP : t + → t - x LLP+ def = x (V + ) LLP def = (V + ) LLP+ ⋄ (V, V ′ ) LLP+ def = (V LLP+ , V ′ LLP+ ) µα.c LLP def = µk α .c LLP {t -} LLP+ = t -LLP+ def = t -LLP µ tp.c LLP def = µx. µ⋆.c LLP µ y. y ⋄ x LLP : c → c t + t -LLP def = t +LLP t -LLP t -t + LLP def = t -LLP t +LLP
(κ being x or α in the source, and x or k α in the target.) polarities in LC can be transparent at the level of types, and unobtrusive at the level of terms. The least we can ask of a classical logic is indeed that there be no apparent modality in the system! We reflect this in L foc, tp and its type system: we provide implicit shifts, thanks to which it is possible to write the strict pair of a negative t -: N and a positive V : P and obtain (t -, V ) : N ⊗ P for instance.An exponential is of course introduced in the translation into LLP ! P ? P : !N ⊗ P. But this exponential already belongs to the translation of t -: N . We see that by construction, there is semantically no need in L foc, tp to have a redundant symbol that would represent a shift in this place.

LLP : t -→ V α LLP def = k α tp LLP def = µx ⋄ .〈x || ⋆〉 µx.c LLP def = µx ⋄ .c LLP µ(κ, κ ′ ).c LLP def = µ(κ, κ ′ ) ⋄ .c LLP µ{α}.c LLP def = µk ⋄ α .c LLP
This involved two design choices: 1) dereliction is implicit because positive values and non-values share the same syntactical category; 2) promotion is implicit because we took the convention that negative terms are values.

Proposition 17 (Simulation). If L foc, tp ⊢ c → c ′ then LLP ! P ? P ⊢ c LLP → + c ′ LLP .
Proposition 18 (Soundness).

If L foc, tp ⊢ c ≃ c ′ then LLP ! P ? P ⊢ c LLP ≃ c ′ LLP .
Types and sequents translate as follows:

X LLP def = X ´NP LLP def = ! P LLP N LLP (P * ⊗ Q * ) LLP def = P * LLP ⊗ Q * LLP N P LLP def = ! P LLP N LLP
(and by duality P ⊥ LLP = P LLP ⊥ );

( x : N , α : P Q ) LLP def = x : N LLP , k α : ? Q LLP P LLP tp : P LLP def = ⋆ : P LLP c : (⊢ Γ, T ) c LLP : (⊢ Γ LLP , T LLP ) ⊢ t -: N | Γ, tp : P ⊢ t -LLP : ! P LLP N LLP | Γ LLP ⊢ V : P * | Γ ⊢ V LLP+ : P * LLP | Γ LLP ⊢ t + : P Q | Γ, T ⊢ t +LLP : ? Q LLP P LLP | Γ LLP , T LLP .

Translation into linear logic

In this section we explain the exponential ! P through a translation of LLP ! P ? P into linear logic [Gir87] (LL). Because we miss a of standard acceptation of what would an untyped syntax of LL be (though we proposed one in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]), we restrict ourselves to the typed case (this also makes things simpler since we need to apply η expansion in the translation!). Also, we are volutarily brief: the reader can already refer to Benton & Wadler [START_REF] Benton | Linear logic, monads, and the lambda calculus[END_REF] which establish a correpondence between the call-by-value calculus obtained by the boring translation and Moggi's monadic model for a commutative strong monad (recall that our λ × v is essentially Moggi's calculus plus equations reflecting commutativity of the monad).

In LL, it is possible to take the following definitions:

! P A def = !(A & P) ? P A def = ?(A ⊗ P ⊥ )
This modality enjoys the following rules:

⊢ ?Γ, A, P

(prom P ) ⊢ ?Γ, ! P A ⊢ Γ, A (der P )
⊢ Γ, ? P A, P

The translation is and extension of Laurent and Regnier's reversing translation (ρ) of LLP into LL [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF], which is itself inspired from Quatrini and Tortora de Falco [START_REF] Quatrini | Polarisation des preuves classiques et renversement[END_REF].

The goal of ρ is to confine structural rules to places where they conform to the constraints of LL -thus it takes care that contraction, weakening and the context of promotion are restricted to formulae of the form ?A.

At the level of types, all the translation requires is to replace all the atoms X and X ⊥ respectively by !X and ?X ⊥ . At the level of terms, we can describe such a translation through η-expansion (invertibility) of negative connectives.

Since we are in a typed setting, η-expansion allows us to replace contractions and weakenings on formulae N by the same rules on formulae of the form X ⊥ or ? Q P. Indeed, for instance, if z is not linear in c : (⊢ z : X ⊥ & Y ⊥ , Γ), then it is possible to get rid of structural rules on X ⊥ & Y ⊥ by replacing c by µ(x, y).c (x, y) z z , which is equivalent and only uses structural rules on X ⊥ and Y ⊥ . The negative context of promotion is decomposed similarly so that it only contains formulae of the form X ⊥ or ? Q P -in addition to the positive premise of our modified promotion, which is the main difference with the case of LLP. This promotion and dereliction are replaced by their derivation above.

We are done when we get rid of structural rules on atoms X and X ⊥ by replacing these atoms by !X and ?X ⊥ (the usual exponential, not the annotated one).

Comparison with other works

The polarised analysis of CPS translations

Our analysis of CPS translations remains valid if we restrict to non-delimited control: if we omit the tp part from L foc, tp we essentially get the syntax for Girard's polarised classical logic that we introduced in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]. A simple restriction of our syntax for LLP ! P ? P yields a syntax for LLP. Therefore, the introductory explanation of CPS translations is obtained by restricting λµ tp v and λµ tp n to the λµ part. As we have seen in the details of the proofs, the factorings we obtain:

λµ n/v CPSn/v 1) / / / / LC 2) λ LLP 3) o o
are even plain equalities -and our explanation is still relevant.

Many aspects of existing works are brought together by our account, as non-delimited CPS translations have already been extensively studied from the point of view of proof theory. We do not hope to establish a comprehensive list of contributions in this vast field, therefore we only mention the closest related works.

Beside Curien-Herbelin's λµ μ [CH00], we inherit from Wadler's Dual Calculus [START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF] the idea that abstraction and application can be derived even in a term syntax. There is no polarisation the works of Curien & Herbelin or Wadler, in the sense that call-by-value and call-by-name are conceived as global reduction strategies, and these calculi do not "mix" call-by-value and call-by-name in the same sense as L foc .

Laurent introduced LLP and gave the "positive" translation into LLP for call-by-value λµ calculus and the "negative" one for call-by-name λµ calculus [START_REF] Laurent | Etude de la polarisation en logique[END_REF]. Zeilberger later gave a logical and computational explanation of polarities in terms of values and computations. He described a system [START_REF] Zeilberger | On the unity of duality[END_REF] in which "call-by-value and call-by-name evaluation freely interact" in a "programming language in which evaluation order is explicitly reflected at the level of types", he claims. This allowed him to give a first explanation of CPS translations in terms of polarities [Zei09], based on Laurent's decomposition.

All these works themselves are part of a long series of works in proof theory or programming languages theory (sometimes both), including but not limited to ones of Girard While LLP and Zeilberger's system deal with polarities, they miss the classical polarities of LC and LK η pol . In particular, we incorrectly stated, at the time of [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF], that we shared with Zeilberger a computational interpretation of polarities. We should have looked more carefully, as we believe indeed that demand-driven and data-driven computations are an interpretation of the polarities of LC, and that the difference between these classical polarities and the notion of polarity in systems like LLP or Zeilberger's should not be overlooked.

For instance, Zeilberger described his positives as values while the positives of L foc , like negatives, are computations that may carry effects. Also, the fact that LLP is based on the adjunction ? ⊣ ! (or equivalently ˆ⊣ ´for Zeilberger's [START_REF] Zeilberger | On the unity of duality[END_REF]), but that the shifts in LC and L foc work the other way (ˆis invertible while ís not), makes a definitive distinction in how the two notions of polarity work.

By emphasizing the importance of the classical polarities of LC and LK η pol in the decomposition, we believe that we brought one missing element to the big picture of how polarisation clarifies the contents of CPS translations.

Polarised linear logic and the study of double negation translations

Laurent and Regnier [Lau02, LR03] showed -among other contributions -that double-negation translations are not limited to the CPS translations that we can decompose in the spirit of the present paper. More precisely, they decompose translations of classical logic into linear logic in two steps:

λµ G -→ LLP K -→ LL
where G represents the Girard-Laurent translations (with our definitions, • POS LLP and • NEG LLP ) and K can be the ρ translation or another translation described in [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF] called boxy. They showed that these translations can be performed in the reverse order through a call-by-name λ calculus that they call CLC, to retrieve previous translations:

λµ K ′ -→ CLC G ′ -→ LL
where K ′ denote again double-negation translations. For instance, with G the negative translation (corresponding to the Lafont-Reus-Streicher one [START_REF] Lafont | Continuation semantics or expressing implication by negation[END_REF]), and K the translation ρ, they show that G ′ is Girard's "!A ⊸ B" translation and K ′ is nothing else than the Krivine double-negation translation! We note that while some double-negation translations can be found in both the K ′ and the G steps, like the Lafont-Reus-Streicher translation, we have that Krivine's translation is specific to K ′ , whereas translations that involve recursively defined values, like some CPS translations, are specific to G.

Our explanation of this fact is that the steps K and G answer distinct questions: the K translations answer to "how do we obtain structural rules on negative formulae?" whereas the G translations answer to "how do we obtain structural rules on positive formulae?". It is no surprise that in order to construct classical logic -which requires structural rules on all formulae -from linear logic, both questions have to be answered.

This delineates two families of double negation translations, and also means that it is false to identify double-negation translations in general with CPS translations.

Polarities and delimited control

The first attempt of applying polarisation to the study of delimited control goes back to Shan [Sha03]. Shan introduced an extension of LLP with linear shifts of polarities where he could translate Danvy-Filinski's calculus. He already hinted at a link with Girard's boring translation: his translation of intuitionistic logic into his system "is essentially a polarised variant of Girard's 'boring' translation", he writes. However this translation is more directly related to the CBV CPS translation that corresponds to the second stage of double CPS translations, than the boring translation. As a consequence, Shan's system seems designed to study double-CPS translations of delimited control, while we decompose single CPS translations. Shan does not study any other system with delimited control than Danvy-Filinski's.

Together with Kiselyov, Shan [KS07] later gave a type system and a type checking algorithm for Danvy-Filinski's calculus, whose goal is to be more liberal than the original type system of Danvy and Filinski, while we merely claim that (for the positive part) we retrieve the type system of λµ tp v [START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF]. Kiselyov and Shan use connectives • ↓ T and • ↑ T , which correspond modulo duality to annotated negation modalities (¬ P Q) similar to our exponentials ! P • and ? P •. They note that typing a term amounts to transforming it into continuation-passing style. Our type system for L foc, tp does not improve this aspect, since it anticipates already to some degree the translation into LLP ! P ? P , because we use explicit rules for getting in and out of the stoup that anticipate to some degree the translation into LLP ! P ? P , but which are not reflected in the term syntax. However, "investigating the delimited case" of the duality between call-by-name and call-by-value classical logics was left for "future work" in Kiselyov & Shan [START_REF] Kiselyov | A substructural type system for delimited continuations[END_REF].

More recently, Zeilberger proposed [Zei10] -among other contributions -a "simple account of delimited continuations through a natural generalisation of classical polarised logic" (not to be confused with polarised classical logic, i.e. LC or LK η pol ) and "in continuation-passing style", thus expectedly located at the level of LLP. This work is based on hypotheses that make values returned by delimited continuations affect the structure of the polarity-changing negation.

Our own analysis of the polarised decomposition of CPS translations showed that the continuations are related to the rules for the shifts of LLP rather than to the polarity-changing negation, thanks to which we supposed instead that it is the structure of the shifts -here exponentials -that is affected.

In particular, the hypothesis that the symmetry between positive and negative connectives has to be "broken" does not seem necessary. Our own polarised target for delimited CPS translations (LLP ! P ? P ) contrasts indeed with Zeilberger's by being symmetric. 7Such a difference might find an explanation in the fact that polarisation is given a different meaning in the two works: inspired by a abstract description in the case of Zeilberger's [Zei10], and more faithful to linear logic in our case.

While it is expected that a formal translation of Danvy-Filinski's calculus be given into the positive part of Zeilberger's system, there are no claims of connection with other delimited control calculi of the literature.

The "subtractive" decomposition of delimited continuations

The work of Ariola, Herbelin and Sabry [START_REF] Ariola | A typetheoretic foundation of continuations and prompts[END_REF] presents a study of delimited control calculi through translations into a calculus with a subtraction (see also [START_REF] Herbelin | A uniform approach to call-by-name and call-by-value delimited control[END_REF]). In linear logic, ? P Q = ?(Q ⊗ P ⊥ ) happens to look like a subtraction, and we expect that it is possible, as in Laurent-Regnier [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF], to translate L foc, tp into LL in the reverse order, starting with a reversing translation into a negative intuitionistic logic with a subtraction whose semantics would be inherited from LL's ? P N ⊥ modality. This might relate our decomposition to the one of Ariola et al, but would also yield translations in the style of that do not exist yet.

Perspectives

Our explanation of CPS translations shows the relevance of syntaxes à la λµ μ / system L: their role is that of an interface between programming languages and semantics. On the one hand, they can be closer to the semantics than (idealised) programming languages, because they present computation in its interactive form (here, in interaction with some context). On the other hand, because we accept that the resulting system looks more like abstract machines, we have to devote the role of reflecting traditions of programming languages (such as presenting the features of the system in a functional style) to an additional layer of abstraction. This two-step connection between programming languages and semantics is indeed what we find in our decomposition of CPS translations. Here, step 2) defines a CPS-like semantics. The interactive paradigm is relevant, because making explicit an interaction with some context is indeed the idea behind CPS translations. λ calculi with delimited control operators in callby-value or call-by-name are then retrieved through the syntactic sugar of step 1), which answers the question "How do we get a(n idealised) programming language back from a system such as L foc, tp ?". This question could merit a further development on its own, but is not directly related to denotational semantics. Now this does not speak of the last step. In fact, step 3) seems to have little semantic value: on the contrary, this step necessarily equates commands modulo duality, and needless bureaucracy is introduced with administrative redexes, all of which seem to only serve the cause of obscurity of CPS translations. This suggests that LLP ! P ? P is a more appropriate target than the λ calculus if we want to understand, and be able to question, delimited CPS translations. (And we do not mean our particular syntax for LLP ! P ? P , but more generally the system presented: 1-in sequent calculus style and 2-where the double negation modality is decomposed into two distinct co-variant modalities.) But CPS translations are not the only source of semantics for which we found that system L provided relevant notation: in proof theory already, we found that L foc was the appropriate syntax with which we could define for Girard's LC a polarity-conscious variant of Krivine's classical realisability. (See [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF].)

As far as non-delimited CPS translations are concerned, a stronger result would be to prove the conjecture of Urban and Ratiu [START_REF] Urban | Classical logic is better than intuitionistic logic:a conjecture about double-negation translations[END_REF]. They suggest that regarding computation in classical logic, the tq-protocol of Danos-Joinet-Schellinx [START_REF]A new deconstructive logic: Linear logic[END_REF] is as expressive as double-negation translations, by asking if the normal forms that can be obtained via any kind of doublenegation translation could be obtained as well with the tqprotocol. So far, the result is only established for particular double-negation translations.

Urban and Ratiu mention two obstacles to the proof. One was the lack of an usable presentation of the tq-protocol. We believe that L foc provides an answer, being a rich syntax with a concise equational theory. (We can indeed simulate LK tq in LK η pol , by encoding colours t and q with polarities, by introducing shifts for instance to simulate the lack of η restriction, and if necessary at the cost of replacing some additive connectives with multiplicatives and vice-versa.) The other obstacle is the absence of a positive definition of what a "double-negation translation" is. To this question we provide no answer.

If the one lesson we would retain from the call-by-value CPS translation is the construction by which strong monads describe call-by-value computation with effects, then the equivalent construction we should retain from our polarised decomposition of CPS translations is the one described in step 2).

This construction corresponds to a generalisation of monadic and co-monadic constructions; and therefore it describes how logical connectives and structures of computation that are algebraic can mix and interact with ones that are co-algebraic.

We believe that the question of a categorical account of step 2) is important for semantics of programming languages. Of course, "by duality", LC can be identified with its positive and negative subsystems, and we are back to the case of monads (e.g. [START_REF] Selinger | Control categories and duality: On the categorical semantics of the lambda-mu calculus[END_REF]). But we would request a description of the structure that treats the polarity-changing negation seriously, if only because the perfect symmetry induced by duality might not always be relevant, in particular for computer science. Twenty years after Girard wrote his landmark paper on polarisation [START_REF]A new constructive logic: Classical logic[END_REF], this question still has no answer.

  ).S(λk.λs.([k ()] s)) wr i t e def = λs.S(λk.λ_.

L

  foc with tp Syntax pos. variables x, y, z . . . neg. variables α, β, γ . . . (variables) κ ::= x | α (values) V

Figure 1 :

 1 Figure 1: Syntax, reduction rules and equational theory of one-sided L foc with tp.

Positive and negative formulae P

 formulae ::= X | P * ⊗ P * | ´NP N ::= X ⊥ | N * & N * | ˆPP P * ::= P | N P N * ::= N | P P Judgements Γ, ∆ of the form α : P Q , x : N , . . . T of the form tp : P

Figure 2 :

 2 Figure 2: A simple type-and-effect system for L foc, tp .

Fig. 5

 5 Fig. 5 gives the syntax, equations and CPS semantics of Ariola, Herbelin and Sabry's λµ tp v calculus [AHS04] along the lines of Herbelin and Ghilezan [HG08]. 5

Fig. 6

 6 Fig.6defines the syntax and reduction rules of the λµ tp n calculus along the lines of Herbelin-Ghilezan's[START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF] as well as a CPS translation into λ × v based on the Lafont-Reus-Streicher CPS translation[START_REF] Lafont | Continuation semantics or expressing implication by negation[END_REF].The CPS translation is essentially 6 the one of Herbelin & Ghilezan. However we replaced Herbelin & Ghilezan's target calculus (a call-by-name λ calculus with pairs) by λ × v . We could do so because the image of this CPS translation is indifferent to the evaluation strategy as far as reduction rules are concerned. This is witnessed by the fact that this alternate semantics validates the same rules of reductions.However, with λ × v as a target, the translation no longer validates the equation [ tp] µ n tp.c = η c given in[START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF], in the sense that we do not have [ tp] µ n tp.c CPSn ≃ c CPSn in general. This

  Fig.6defines the syntax and reduction rules of the λµ tp n calculus along the lines of Herbelin-Ghilezan's[START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF] as well as a CPS translation into λ × v based on the Lafont-Reus-Streicher CPS translation[START_REF] Lafont | Continuation semantics or expressing implication by negation[END_REF].The CPS translation is essentially 6 the one of Herbelin & Ghilezan. However we replaced Herbelin & Ghilezan's target calculus (a call-by-name λ calculus with pairs) by λ × v . We could do so because the image of this CPS translation is indifferent to the evaluation strategy as far as reduction rules are concerned. This is witnessed by the fact that this alternate semantics validates the same rules of reductions.However, with λ × v as a target, the translation no longer validates the equation [ tp] µ n tp.c = η c given in[START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF], in the sense that we do not have [ tp] µ n tp.c CPSn ≃ c CPSn in general. This

Figure 5 :

 5 Figure 5: The λµ tp v calculus.

Figure 6 :

 6 Figure 6: The λµ tp n calculus.

α

  : A Σ ⊢ t : B | x : C; tp : Ξ with Σ, Ξ ::= ⊥ | N • Σ, and where the connective for implication has one annotation: A Σ → B. Our coding of λµ tp n yields, for A, B, C denoting negative formulae, the following definition:

L

  foc, tp CPS | | y y y y y y y y y LLP λ × v LLP ! P ? P NJ o o where:

Figure 7 :

 7 Figure 7: Syntax, reduction rules and additional equations of LLP ! P ? P .

Figure 10 :

 10 Figure 10: The translation of L foc, tp into LLP ! P ? P .

  , Danos et al., Laurent et al., Selinger, and others [And92, DJS97, Fil89, Gir87, Gir91, Gir93, Gri90, LRS93, LQdF05, Mog89, Mur92, Par92, QTDF96, Sel01].

  Proposition 13 (Factoring). For p a command or a term of λµ tp n , we have p NEG CPS → * admin p CPSn . NEG CPS = (λx.x) t NEG CPS → admin t NEG CPS µ n tp.c NEG CPS = λx. (λk.k x) c NEG CPS → admin λx.c NEG CPS x .

	Proof. Routine verification for the classical subsystem (without
	tp) where we would even have equality. Thus the property fol-
	lows from:
	[ tp] t

• NEG from terms and commands of λµ tp n to terms and commands of L foc, tp (taking α to α, µx to µx and [x] to | x〉):

λµ tp n • NEG --→ L foc, tp Proposition 12 (Soundness). If λµ tp n ⊢ p ≃ p ′ then L foc, tp ⊢ p NEG ≃ p ′

NEG where p is a term or a command.

We believe that Danos, Joinet and Schellinx[START_REF]A new deconstructive logic: Linear logic[END_REF] already had at least the intuition of this interpretation of the critical pair. However we could find no such formal claim in print.

We would have preferred to write these constructs (•) and µ(•).c since they really read best as unary versions of the pair (•, •). For clarity reasons however, because single parentheses are commonly used for grouping, we chose the notation {•} instead, with no strong preference.

In fact it is slightly more constrained and corresponds more closely to Danos et al's η restriction.

Tradition of having negatives in the stoup goes back to Girard[START_REF]On the unity of logic[END_REF]. An alternative to our concise treatment would be to instantiate each logical rule for all possible combination of polarities of the premises, as in LC or LU[START_REF]A new constructive logic: Classical logic[END_REF][START_REF]On the unity of logic[END_REF]. (Witness the number of rules in these systems!)

We differ from[START_REF] Herbelin | An approach to call-byname delimited continuations[END_REF] in that we applied an η expansion in the case of "µ n tp.c", which leaves the denotational semantics of Herbelin & Ghilezan unchanged for a target in call-by-name. This is possible because c CPSn only reduces to functions.

For instance we are able to formally describe in L foc, tp operators µ tp.c and tp : a dynamic input binder for a special variable. We did not mention them because we do not believe that structures obtained by duality are necessarily useful, but one might expect a completeness result for some co-monadic "effects" dual to the one ofFilinski [Fil94].

Acknowledgements

It was a real chance to benefit from the knowledge of Hugo Herbelin on delimited continuations during the many discussions that we had. I would also like to thank Beniamino Accattoli for discussions related to proof nets for LLP ! P ? P . We did not mention such proof nets here, but they had a capital importance in the design of our decompositions and systems.