Joris Van Der Hoeven

Grégoire Lecerf
email: lecerf@lix.polytechnique.fr

Evaluating Straight-Line Programs over Balls

Keywords: ball arithmetic, polynomial evaluation, software implementation

research documents, whether they are published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Interval arithmetic is a classical tool for making numerical computations reliable, by systematically computing interval enclosures for the desired results instead of numerical approximations [START_REF] Alefeld | Introduction to interval analysis[END_REF][START_REF] Jaulin | Applied interval analysis[END_REF][START_REF] Kulisch | Computer Arithmetic and Validity. Theory, Implementation, and Applications[END_REF][START_REF] Moore | Interval Analysis[END_REF][START_REF] Moore | Introduction to Interval Analysis[END_REF][START_REF] Neumaier | Interval methods for systems of equations[END_REF][START_REF] Rump | Verification methods: rigorous results using floating-point arithmetic[END_REF]. Interval arithmetic has been applied with success in many areas, such as the resolution of systems of equations, homotopy continuations, reliable integration of dynamical systems, etc. There exist several variants of interval arithmetic such as ball arithmetic, interval slope arithmetic, Taylor models, etc. Depending on the context, these variants may be more efficient than standard interval arithmetic and/or provide tighter enclosures.

In this paper, we will mainly focus on ball arithmetic (also known as midpoint-radius interval arithmetic), which is particularly useful for reliable computations with complex numbers and multiple precision numbers [START_REF] Van Der Hoeven | Ball arithmetic[END_REF]. One of our main motivations is the implementation of reliable numerical homotopy methods for polynomial system solving [START_REF] Bates | Bertini: software for numerical algebraic geometry[END_REF][START_REF] Beltrán | Certified numerical homotopy tracking[END_REF][START_REF] Van Der Hoeven | Reliable homotopy continuation[END_REF][START_REF] Sommese | The Numerical Solution of Systems of Polynomials Arising in Engineering and Science[END_REF][START_REF] Verschelde | Homotopy continuation methods for solving polynomial systems[END_REF][START_REF] Verschelde | PHCpack: a general-purpose solver for polynomial systems by homotopy continuation[END_REF]. One basic prerequisite for this project concerns the efficient and reliable evaluation of multivariate polynomials represented by so called straight-line programs (SLPs).

Two classical disadvantages of interval arithmetic and its variants are the additional computational overhead and possible overestimation of errors. There is a trade-off between these two evils: it is always possible to reduce the overestimation at the expense of a more costly variant of interval arithmetic (such as high order Taylor models). For a fixed variant, the computational overhead is usually finite, but it remains an important issue for high performance applications to reduce the involved constant factors as much as possible. In this paper, we will focus on this "overhead problem" in the case of basic ball arithmetic (and without knowledge about the derivatives of the functions being evaluated). About ten years ago, we started the implementation of a basic C++ template library for ball arithmetic in the Mathemagix system [START_REF] Van Der Hoeven | [END_REF]. However, comparing speed of operations over complex numbers in double precision and over the corresponding balls was quite discouraging. The overhead comes from extra computations of radii, but also from changes of rounding mode, and the way the C++ compiler generates executable code from C99 portable sources. For our application to reliable homotopies, the critical part to be optimized concerns the evaluation of input polynomials using ball arithmetic. The goal of the present work is to minimize the overhead of such evaluations with respect to their numeric counterparts.

Our contributions

In this article we investigate various strategies to reduce the overhead involved when evaluating straight-line programs over balls. Our point of view is pragmatic and directed towards the development of more efficient implementations. We will not turn around the fact that the development of efficient ball arithmetic admits a quite technical side: the optimal answer greatly depends on available hardware features. We will consider on the following situations, encountered for modern processors:

• Without specific IEEE 754 compliant hardware (which is frequently the case for GPUs), we may only assume faithful rounding, specifying a bound on relative errors for each operation, and that errors can be thrown on numerical exceptions.

• For recent Intel-compatible processors (integrating SSE or AVX technologies) it is recommended to perform numerical computations using SIMD (single instruction, multiple data) units. Programming must be done mostly at the assembly code level with specific builtin instructions called intrinsics. Dynamically switching the rounding mode involves a rather small overhead.

• Recent AVX-512 processors propose floating point instructions which directly incorporate a rounding mode, thereby eliminating all need to switch rounding modes via the status register and all resulting delays caused by broken pipelines.

As a general rule, modern processors have also become highly parallel. For this reason, it is important to focus on algorithms that can easily be vectorized. The first contribution of this paper concerns various strategies for ball arithmetic as a function of the available hardware. From the conceptual point of view, this will be done in Section 2, whereas additional implementation details will be given in Section 4.

Our second main contribution is the introduction of transient ball arithmetic in Section 2.5 and its application to the evaluation of SLPs in Section 3. The idea is to not bother about rounding errors occurring when computing centers and radii of individual balls, which simplifies the implementation of the basic ring operations. Provided that the radii of the input balls are not too small and that neither overflow nor underflow occur, we will show that the cumulated effect of the ignored rounding errors can be bounded for the evaluation of a complete SLP. More precisely, we will show that the relative errors due to rounding are essentially dominated by the depth of the computation. Although it is most convenient to apply our result to SLPs, much of it can be generalized to arbitrary programs, by regarding the trace of the execution as an SLP. For such generalizations, the main requirement is to have an a priori bound for the (parallel) depth of the computation. Most of our strategies have been implemented inside the Multimix and Justinline libraries of Mathemagix [START_REF] Van Der Hoeven | [END_REF], in C++ and in the Mathemagix language. In Section 4, we compare costs for naive, statically compiled, and dynamically compiled polynomial evaluations. Using our new theoretical ideas and various implementation tricks, we managed to reduce the overhead of ball arithmetic to a small factor between two and four. We also propose SSE and AVX based functions for arithmetic operations on balls. Dynamic compilation, also known as just in time (JIT) compilation, is implemented from scratch in our Runtime library, and turns out to reach high performance for large polynomial functions.

Related Work

In the context of real midpoint-radius interval arithmetic, and for specific calculations, such as matrix products, several authors proposed dedicated solutions that mostly perform operations on centers and then rely on fast bounds on radii [START_REF] Ogita | Fast inclusion of interval matrix multiplication[END_REF][START_REF] Ozaki | Tight and efficient enclosure of matrix multiplication by using optimized BLAS[END_REF][START_REF] Ozaki | Fast algorithms for floating-point interval matrix multiplication[END_REF][START_REF] Rump | Fast and parallel interval arithmetic[END_REF][START_REF] Rump | Fast interval matrix multiplication[END_REF]. In this case, the real gain comes from the ability to exploit HPC (high performance computing) solutions to linear algebra, and similar tricks sometimes apply to classical interval methods [START_REF] Diep | Efficient algorithms for verified scientific computing: numerical linear algebra using interval arithmetic[END_REF][START_REF] Revol | Parallel implementation of interval matrix multiplication[END_REF].

The use of SIMD instructions for intervals started in [START_REF] Von Gudenberg | Interval arithmetic on multimedia architectures[END_REF], and initially led to a rather modest speed-up, according to the author. Changing the rounding mode for almost each arithmetic operation seriously slows down computations, and might involve a serious stall of a hundred of cycles by breaking FPU pipelines of some hardware such as Intel x87.

To avoid switching rounding modes, the author of [START_REF] Stolte | Arbitrary 3D resolution discrete ray tracing of implicit surfaces[END_REF] uses different independent rounding modes on the x87 and SSE units. Specific solutions to diminish the swap of rounding modes also rely on the opposite trick in internal computations or directly in the representation [START_REF] Goualard | Fast and correct SIMD algorithms for interval arithmetic[END_REF][START_REF] Lambov | Interval arithmetic using SSE-2[END_REF][START_REF] Von Gudenberg | Interval arithmetic on multimedia architectures[END_REF]. Modern wide SIMD processors tend to handle roundings more efficiently and AVX-512 even features instructions that directly integrate a rounding mode.

Different types of ball arithmetic

Machine arithmetic

Throughout this paper, we denote by R the set of machine floating point numbers. We let p 16 be the machine precision (which corresponds to the number of fractional bits of the mantissa plus one), and let E min and E max be the minimal and maximal exponents (included). For IEEE 754 double precision numbers, this means that p = 53, E min = -1022 and E max = 1023. We enlarge R with symbols -∞, +∞, and NaN, with their standard meaning.

For our basic arithmetic, we allow for various rounding modes written ↓, ♮, ↑, . The first three rounding modes correspond to IEEE arithmetic with correct rounding (downwards, to the nearest and upwards). The rounding mode corresponds to faithful rounding without any well specified direction. For x ∈ R, we write x • ∈ R for the approximation of x in R with the specified rounding mode • ∈ {↓, ♮, ↑, }. The quantity ε • (x) := |x • -x| stands for the corresponding rounding error, that may be +∞. Given a single operation * ∈ {+, -, ×, ...}, it will be convenient to write x * • y for (x * y) • . For compound expressions ϕ, we will also write •[ϕ] for the full evaluation of ϕ using the rounding mode •. For instance,

•[x y + a 2 b] = x • × • y • + • (a • × • a • ) × • b • .
Modern processors usually support fused-multiply-add (fma) and fused-multiply-subtract (fms) instructions, both for scalar and SIMD vector operands: fma • (x, y, z) and fms • (x, y, z) represent the roundings of x y + z and x yz according to the mode •. For generalities about these instructions, we refer the reader to the book [START_REF] Muller | Handbook of Floating-Point Arithmetic[END_REF] for instance.

We will denote by ε ¯• any upper bound function for ε • that is easy to compute. In absence of underflows/overflows, we claim that we may take ε ¯

•(x) = |x • | ǫ • , with ǫ • = 2 -p+1
for • = / ♮ and ǫ ♮ = 2 -p . Indeed, given x, y ∈ R and * ∈ {+, -, ×}, let e be the exponent of x • , so that 2 e |x • | < 2 e+1 and E min e E max . Then ε • (x) < 2 e-p+1 |x • | 2 -p+1 for all rounding modes, and ε ♮ (x) 2 e-p |♮(x)| 2 -p .

If we want to allow for underflows during computations, we may safely take ε ¯

•(x) = |x • | ǫ • + 2 E min -p+1
, where 2 E min -p+1 is the smallest positive subnormal number in R. Notice that if x, y ∈ R, then we may still take ε ¯•(x ± y) = |x ± • y | ǫ • since no underflow occurs in that special case. Underflows and overflows will be further discussed in Section 3.3.

Complex arithmetic and generalizations

In order to describe our algorithms in a flexible context, A denotes a Banach algebra over R, endowed with a norm written • . The most common examples are A = R and A = C with z = |z | for all z ∈ A.

For actual machine computations, we will denote by A the counterpart of R when R is replaced by A. For instance, if A = C, then we may take A = R[i]. In other words, if R is the C++ type double, then we may take complex<double> for A, where complex represents the template type available from the standard C++ library, or from the Numerix library of Mathemagix.

For any rounding mode •∈{↓, ♮, ↑, }, the notations from the previous section naturally extend to A. For instance, ε

• (x) := x • -x . Similarly, if A = C, then (x + y i) • = x • + y • i.
For complex arithmetic we consider the following implementation:

(a + b i) ± • (c + d i) := •[a ± c] + •[b ± d] i (1)
(a + b i) × • (c + d i) := •[a c -b d] + •[a d + b c] i (2) a + b i • := • a 2 + b 2 √ . (3)
As for ε ¯• we may clearly take ε ¯•(x) = x • ǫ • in absence of underflows/overflows, and

ε ¯•(x) = x • ǫ • + 2 √ • 2 E min -p+1 in general.
Remark 1. For applications to the case when A = C, it is sometimes interesting to replace computations of norms x by computations of quick and rough upper bounds ⌈⌈x⌉⌉ x . For instance, on architectures where square roots are expensive, one may use

⌈⌈a + b i⌉⌉ = min 2 √ max (|a|, |b|), |a| + |b| .

Exact ball arithmetic

Given a ∈ A and r ∈ R := {x ∈ R: x 0}, we write B(a, r) = {x ∈ A: xa r} for the closed ball with center a and radius r. The set of such balls is denoted by B(A, R). One may lift the ring operations +, -, × in A to balls in B(A, R), by setting:

B(a, r) ± B(b, s) := B(a ± b, r + s) B(a, r) × B(b, s) := B(a b, ( a + r) s + b r).
These formulas are simplest so as to satisfy the so called inclusion principle: given * ∈ {+, -, ×}, x ∈ B(a, r) and y ∈ B(b, s), we have x * y ∈ B(a, r) * B(b, s). This arithmetic for computing with balls is called exact ball arithmetic. It extends to other operations that might be defined on A, as long as the ball lifts of operations satisfy the inclusion principle. For instance, we may implement fused-multiply-add and fused-multiply-subtract using fma(B(a, r), B(b, s), B(c, t)) := B(fma(a, b, c), fma( a + r, s, fma( b , r, t)).

Certified machine ball arithmetic

We will denote by B(A, R) the set of balls with centers in A and radii in R. In order to implement machine ball arithmetic for B(A, R), we need to adjust formulas from the previous section so as to take rounding errors into account. Indeed, the main constraint is the inclusion principle, which should still hold for each operation in such an implementation. The best way to achieve this depends heavily on rounding modes used for operations on centers and radii.

On processors that feature IEEE 754 style rounding, it is most natural to perform operations on centers using any rounding mode • (and preferably rounding to the nearest), and operations on radii using upward rounding. This leads to the following formulas:

B(a, r) ± • B(b, s) := B(a ± • b, ↑[r + s + ε ¯•(a ± b)]) B(a, r) × • B(b, s) := B(a × • b, ↑[( a + r) s + b r + ε ¯•(a b)]) fma • (B(a, r), B(b, s), B(c, t)) := B(fma • (a, b, c), ↑[R]) R ≡ fma( a + r, s, fma( b , r, t + ε ¯•(fma • (a, b, c)))).
For instance, when using ε ¯•(x) of the form x • ǫ + η in the last case of fma/fms, this means that three additional instructions are needed with respect to the exact arithmetic from the previous subsection:

C := fma • (a, b, c) ↑ C ′ := fma ↑ (C , ǫ, η) radius ′ := radius + ↑ C ′ .
In practical implementations, unless A = R, the radius computations involve many roundings. The correctness of the above formulas is justified by the fact that we systematically use upward rounding for all bound computations; the rounding error for the single operation on the centers is captured by ε ¯•. Remark 2. Unfortunately, dynamically switching rounding modes may be expensive on some processors. In that case, one approach is to reorganize computations in such a way that we first perform sufficiently many operations on centers using one rounding mode, and next perform all corresponding operations on radii using upward rounding.

Another approach is to use the same rounding mode for computations on centers and radii. If we take • = ↑ as the sole rounding mode, then we may directly apply the above formulas, but the quality of computations with centers degrades. If we take • = / ↑, then we have to further adjust the radii so as to take into account the additional rounding errors that might occur during radius computations. For instance, if A = R, in the cases of addition and subtraction, and in absence of underflows/overflows, we may use

B(a, r) ± • ′ B(b, s) := B(a ± • b, •[(r + s + ε ¯•(a ± b)) × (1 + 8 • 2 -p+1 )]), since we have (r + • s + • ε ¯•(a ± b)) × • (1 + 8 • 2 -p+1 ) r + s + ε ¯•(a ± b).
This arithmetic, sometimes called rough ball arithmetic, fits one of the main recommendations of [START_REF] Revol | Numerical reproducibility and parallel computations: issues for interval algorithms[END_REF]: "Get free from the rounding mode by bounding, roughly but robustly, errors with formulas independent of the rounding mode if needed."

Transient ball arithmetic

The adjustments which where needed above in order to counter the problem of rounding errors induce a non trivial computational overhead, despite the fact that these adjustments are usually very small. It is interesting to consider an alternative transient ball arithmetic for which we simply ignore all rounding errors. In the next Section 3, we will see that it is often possible to treat these rounding errors at a more global level for a complete computation instead of a single operation.

For any rounding mode •, we will denote by • ˜the corresponding "rounding mode" for transient ball arithmetic; the basic operations are defined as follows:

B(a, r) ± • ˜B(b, s) := B(a ± • b, •[r + s]) B(a, r) × • ˜B(b, s) := B(a × • b, •[( a + r) s + b r]) fma • ˜(B(a, r), B(b, s), B(c, t)) := B(fma • (a, b, c), •[fma(( a + r), s, fma( b , r, t)]).
Of course, these formulas do not satisfy the inclusion principle. On processors that allow for efficient switching of rounding modes, it is also possible to systematically use upward rounding for radius computations, with resulting simplifications in the error analysis below.

Let us fix a rounding mode • ∈ {↓, ♮, ↑, }. We assume that we are given a suitable floating point number ǫ in R ∩ (N 2 -p+1 ) such that ǫ 1/16 and

a * • b -a * b a * • b ǫ | a • -a | a • ǫ,
hold for all a, b ∈ A and * ∈ {+, -, ×}, in absence of underflows and overflows. If A = R, then we may take ǫ = ǫ • . If A = C, and assuming that complex arithmetic is implemented using (1-3), then it can be checked that we may take ǫ = 4 ǫ • (see Appendix A). The following lemma provides an error estimate for the radius computation of a transient ball product.

Lemma 3. For all a, b ∈ A and r, s ∈ R such that the computation of

R = •[( a + r) s + b r]
involves no underflow or overflow, we have

( a + r) s + b r R (1 + ǫ) 4 .
Proof. We have

( a • + • r) × • s + • b • × • r (( a • + • r) × • s + b • × • t) (1 + ǫ) -1 (( a • + • r) s + b • r) (1 + ǫ) -2 (( a • + r) s + b • r) (1 + ǫ) -3 (( a + r) s + b r) (1 + ǫ) -4 .

Evaluation of SLPs

Straight-line programs

A straight-line program Γ over a ring A is a sequence Γ 1 , ..., Γ l of instructions of the form

Γ k ≡ X k := C k or Γ k ≡ X k := Y k * Z k ,
where X k , Y k , Z k are variables in a finite ordered set V, C k constants in A, and * ∈ {+, -, ×}. Variables that appear for the first time in the sequence in the right-hand side of an instruction are called input variables. A distinguished subset of the set of all variables occurring at the left-hand side of instructions is called the set of output variables. Variables which are not used for input or output are called temporary variables and determine the amount of auxiliary memory needed to evaluate the program. The length l Γ = l of the sequence is called the length of Γ.

Let I 1 , ..., I m be the input variables of Γ and O 1 , ..., O n the output variables, listed in increasing order. Then we associate an evaluation function E Γ : A m → A n to Γ as follows: given (a 1 , ..., a m ) ∈ A m , we assign a i to I i for i = 1, ..., m, then evaluate the instructions of Γ in sequence, and finally read off the values of O 1 , ..., O n , which determine E Γ (a 1 , ..., a m ).

To each instruction Γ k , one may associate the remaining path lengths q k as follows. Let q l = 1, and assume that q k+1 , ..., q l have been defined for some k ∈ {1, ..., l}. Then we take

q k = max (q i 1 , ..., q i n ) + 1, where i 1 > ••• > i n are those indices i > k such that Γ i is of the form X i := Y i op Z i with X k ∈ {Y i , Z i } and X k ∈ / {X k+1 , ..., X i-1 }.
If no such indices i exist, then we set q k = 1. Similarly, for each input variable I k we define q I k = max (q i 1 , ..., q i n ) + 1, where i 1 > ••• > i n are those indices such that Γ i is of the form X i := Y i op Z i with I k ∈ {Y i , Z i } and I k ∈ / {X 1 , ..., X i-1 }. We also define q Γ = max (q I 1 , ..., q I m , q i 1 , ..., q i n ), where I 1 , ..., I m are the input variables of Γ and i 1 , ..., i n all indices i such that Γ i is of the form X i := C i .

Example 4.

Let us consider Γ = (x 1 := 5, x 2 := a 1 × a 2 , x 1 := x 1 × x 2 , x 3 := x 1 + a 1 ), of length l = 4. The input variables are a 1 and a 2 , and we distinguish x 3 as the sole output variable. This SLP thus computes the function 5 a 1 a 2 + a 1 . The associated computation graph, together with remaining path lengths are as pictured:

a 1 a 2 × × + 5 q 2 = 3 q 1 = 3 q 3 = 2 q 4 = 1

Transient evaluation

Consider the "semi-exact" ball arithmetic in which all computations on centers are done using a given rounding mode • and all computations on radii are exact. More precisely, we take

B(a, r * ) ± * B(b, s * ) = B(a + • b, r * + s * + ε ¯•(a + b)) B(a, r * ) × * B(b, s * ) = B(a × • b, ( a + r * ) s * + a s * + ε ¯•(a b)),
for any a, b ∈ A and r * , s * ∈ R . We wish to investigate how far the transient arithmetic from Section 2.5 can deviate from this idealized arithmetic (which satisfies the inclusion principle). We will write

H k = 1 1 + ••• + 1 k
for the k-th harmonic number and H k,l = H l -H k for all l k. Theorem 5. Let Γ be a SLP of length l as above and let α > 0 be an arbitrary parameter such that 1 + α > (1 + ǫ) 4 q Γ . Consider two evaluations of Γ with two different ball arithmetics. For the first evaluation, we use the above semi-exact arithmetic with ε ¯•(x) = x • ǫ. For the second evaluation, we use transient ball arithmetic with the same arithmetic for centers, and the additional property that any input or constant ball B(a, r * ) is replaced by a larger ball B(a, r) with

r max ( a ((1 + ǫ) βq Γ -1), (1 + α) r * ),
where

β max 3, 1 + α α γ , γ H q Γ (1 + ǫ) 4q Γ α 1 + α 1 - (1 + ǫ) 4q Γ 1 + α -1
.

If no underflow or overflow occurs during the second evaluation, then for all B(c, t * ) in the output of the first evaluation with corresponding entry B(c, t) for the second evaluation, we have t * t.

Proof. It will be convenient to systematically use the star superscript for the semi-exact radius evaluation and no superscript for the transient evaluation.

Let B(c k , t k ) be the ball value of the variable X k just after evaluation of Γ 1 , ..., Γ k using transient ball arithmetic. Let us show by induction over k that

t k c k ((1 + ǫ) βq k -1).
So assume that the hypothesis holds for all strictly smaller values of k. If Γ k is of the form X k := C k , then we are done by assumption since q k q Γ . If Γ k is of the form X k := Y k * Z k , then we claim that Y k contains a ball B(a, r) with r a ((1 + ǫ) β(q k +1) -1).

Indeed, this holds by assumption if Y k is an input variable. Otherwise, let i < k be largest with X i = Y k . Then q i q k + 1 by the construction of q i , whence our claim follows by the induction hypothesis. In a similar way, Z k contains a ball B(b, s) with s b ((1 + ǫ) β(q k +1) -1). Having shown our claim, let us first consider the case when * ∈ {+, -}. Then we get

r + s ( a + b ) ((1 + ǫ) β(q k +1) -1) a ± b ((1 + ǫ) β(q k +1) -1).

Using the inequalities ((1 + ǫ)

A -1) (1 + ǫ) -1 (1 + ǫ) A-1 -1, 1 -ǫ (1 + ǫ) -2
, and the fact that β 3, we obtain:

t k = r + • s (r + s) (1 + ǫ) -1 (4) a ± b ((1 + ǫ) β(q k +1) -1) (1 + ǫ) -1 c k ((1 + ǫ) β(q k +1) -1) (1 -ǫ) (1 + ǫ) -1 (5)
c k ((1 + ǫ) βq k -1),
as desired. In the same way, if * = ×, then

( a + r) s + b r a s + b r 2 a b ((1 + ǫ) β(q k +1) -1),
whence, using Lemma 3, and the fact that 2/(1 + ǫ) -4 > 1/(1 + ǫ),

t k = ( a • + • r) × • s + • b • × • r (( a + r) s + b r) (1 + ǫ) -4 (6) 2 a b ((1 + ǫ) β (q k +1) -1) (1 + ǫ) -4 c k ((1 + ǫ) β(q k +1) -1) (1 -ǫ) (1 + ǫ) -1 c k ((1 + ǫ) βq k -1), (7)
which completes our claim by induction. For all k ∈ {1, ..., l}, we introduce

γ k = 1 1 + α + α γ (1 + α) H q k ,q Γ (1 + ǫ) 4(q Γ -q k ) , so that (1 + α) -1 γ k 1.
Using a second induction over k, let us next prove that

t k * γ k t k .
Assume that this inequality holds up until order k -1. If Γ k is of the form X k := C k , then we are done by the fact that

γ k (1 + α) -1 . If Γ k is of the form X k := Y k ± Z k , then let i, j < k be largest with X i = Y k and X j = Z k .
Then min (q i , q j ) q k + 1, and max (γ i , γ j )

1 1 + α + α γ (1 + α) H q k +1,q Γ (1 + ǫ) 4(q Γ -(q k +1)) , η k := c k ǫ t k ǫ ((1 + ǫ) βq k -1) 1 β q k α q k γ (1 + α) .
In particular, (max (γ i , γ j ) + η k ) (1 + ǫ) 4 γ k . With r and s as above, it follows that

t k * = r * + s * + c k ǫ ((r + s) max (γ i , γ j ) + η k t k ) (max (γ i , γ j ) + η k ) t k (1 + ǫ) (8)
γ k t k . If Γ k is of the form X k := Y k × Z k
, then thanks to Lemma 3, a similar computation yields

t k * = ( a + r * ) s * + b r * + c k ǫ (( a + r) s + b r) max (γ i , γ j ) + η k t k (max (γ i , γ j ) + η k ) t k (1 + ǫ) 4 (9)
γ k t k .
This completes the second induction and the proof of this theorem.

For fixed α and q Γ = o(1/ε), we observe that (1 + ǫ) βq Γ -1 = O(ǫ q Γ log q Γ ). The value of the parameter α may be optimized for given SLPs and inputs. Without entering details, α should be taken large when inputs are accurate, and small when inputs are rough, as encountered for instance within subdivision algorithms.

Managing underflows and overflows

In Theorem 5, we have assumed the absence of underflows and overflows. There are several strategies for managing such exceptions, whose efficiencies heavily depend on the specific kind of hardware being used.

One strategy to manage exceptions is to use the status register of an IEEE 754 FPU. The idea is to simply clear the underflow and overflow flags of the status register, then perform the evaluation, and finally check both flags at the end. Whenever an overflow occurred during the evaluation, then we may set the radii of all results to plus infinity, thereby preserving the inclusion principle. If an underflow occurred (which is quite unlikely), then we simply reevaluate the entire SLP using a more expensive, fully certified ball arithmetic.

When performing all computations using the IEEE 754 rounding-to-nearest mode ♮, we also notice that consulting the status register can be avoided for managing overflows. Indeed, denoting by H the largest positive finite number in R, we have x ♮ = -∞ for all x < -H and x ♮ = +∞ for all x > H. Consequently, whenever a computation on centers overflows, the corresponding radius will be set to infinity.

From now on, we assume the absence of overflows and we focus on underflows. In addition to the constant ǫ, we suppose given an other positive constant η in R such that

ε ¯•(x) = x • ǫ + η (10) a × • b -a b a × • b ǫ + η (11) | a • -a | a • ǫ + η (12)
for all x ∈ A and a, b ∈ A. For instance, if A = R, then we may take η = 2 E min -p+1 . If A = C, and assuming the arithmetic from Section 2.2, then it is safe to take η = 8 • 2 (E min -p+1)/2 (see Appendix A). In addition to the method based on the status register, the following strategies can be used for managing underflows.

Using upward rounding for radii. If it is possible to use different rounding modes for computations on centers and radii, then we may round centers to the nearest and radii upwards. In other words, we replace the transient arithmetic from Section 2.5 by

B(a, r) ± • ˘B(b, s) := B(a ± • b, ↑[r + s]) B(a, r) × • ˘B(b, s) := B(a × • b, ↑[( a + r) s + b r]).
This arithmetic makes Theorem 5 hold without the assumption on the absence of underflows, and provided that

3 η ((1 + ǫ) βq Γ -1) 2 E min -p+1 . ( 13
)
Indeed, inequalities ( 5), [START_REF] Van Der Hoeven | Mathemagix User Guide[END_REF], and ( 9) immediately hold, even without extra factors (1 + ǫ).

It remains to prove that (6) also holds. From

a × • b -a b a × • b ǫ + η we have a × • b ( a b + η) (1 -ǫ) -1 . Therefore, if a b η (1 -2 ǫ) -1 , then a × • b 2 a b holds, whence inequality (6). Otherwise a × • b η (1 + (1 -2 ǫ) -1 ) (1 -ǫ) -1
3 η, and the extra assumption (13) directly implies t k c k ((1 + ǫ) βq k -1) because t k 2 E min -p+1 always holds by construction.

Adding corrective terms to the radii. Another strategy is to manually counter underflows by adding corrective terms to the radii. This yields the following arithmetic which is half way between transient and certified:

B(a, r) ± • ˇB(b, s) := B(a ± • b, r + • s) B(a, r) × • ˇB(b, s) := B(a × • b, •[max (( a + r) s + b r, 2 η /ǫ)])
No corrections are necessary for additions and subtractions which never provoke underflows. As to multiplication, Lemma 3 admits Lemma 6 below as its analogue in the case when A = R. Using this, it may again be shown that Theorem 5 holds without the assumption on the absence of underflows, and provided that

3 ǫ ((1 + ǫ) βq Γ -1) 2. ( 14
)
Indeed, inequalities ( 5), [START_REF] Van Der Hoeven | Mathemagix User Guide[END_REF], and (9) immediately hold. It remains to prove that (6) also holds. The case a b η (1 -2 ǫ) -1 is handled as for the previous strategy. Otherwise, we have a ×

• b η (1 + (1 -2 ǫ) -1 ) (1 -ǫ) -1
3 η, and the extra assumption ( 14) directly implies

t k c k ((1 + ǫ) βq k -1) because t k 2 η /ǫ holds by construction. Lemma 6. For all a, b ∈ R and r, s ∈ R, letting R ˇ= •[max ((|a| + r) s + |b| r, 2 η /ǫ)] and R = (|a| + r) s + |b| r, we have R R ˇ(1 + ǫ • ) 4 .
Proof. We have

(|a| + • r) × • s + • |b| × • r ((|a| + • r) × • s + |b| × • t) (1 + ǫ • ) -1 ((|a| + • r) s + |b| r -2 η) (1 + ǫ • ) -2 ((|a| + r) s + |b| r) (1 + ǫ • ) -3 -2 η. It follows that R ˇ R (1 + ǫ • ) -3 -ǫ R ˇ.

Remark 7.

If A = / R, then the above method still applies under the condition that all norm computations are replaced by reliable upper bounds. In other words, assuming that ⌈⌈x⌉⌉ ∈ R satisfies ⌈⌈x⌉⌉ x for all x ∈ A, we may take

B(a, r) × • ˇB(b, s) := B(a × • b, •[max ((⌈⌈a⌉⌉ + r) s + ⌈⌈b⌉⌉ r, 2 η /ǫ)]).
Subnormal numbers. On some processors, computations with subnormal numbers incur a significant performance penalty. Such processors often support a "fast math" mode in which subnormal numbers in input and output are set to zero, which does not comply with the IEEE 754 standard. For instance, SSE and AVX technologies include two flags in the MXCSR control register dedicated to this purpose, namely denormal-are-zero and flush-to-zero. When setting these two flags together, we must take ε ¯

•(x) = |x • | ǫ • + 2 E min
over R as a protection against this additional error, 2 E min being the smallest positive normal number in R. Roughly speaking, the above strategies may be adapted by replacing E min by E min + p in the proofs.

Implementation

Our new algorithms have been implemented in Mathemagix. The source code, tests, and benchmark files are freely available from the SVN server of Mathemagix via http://gforge.inria.fr/projects/mmx/, from revision 10356. In this section, we briefly present our implementation. We first describe the implemented strategies for evaluations over the standard numeric types double and complex<double>. We next consider balls over these types, and finally say a few words about vectorized variants.

Software overview

Our implementation is divided into C++ and Mathemagix libraries. Import/export mechanisms between these two languages are rather easy, as described in [START_REF] Van Der Hoeven | Interfacing Mathemagix with C++[END_REF][START_REF] Van Der Hoeven | Mathemagix User Guide[END_REF]. The C++ library Multimix contains several implementations of multivariate polynomials, including SLPs (type slp_polynomial defined in slp_polynomial.hpp), naive interpreted evaluation (slp_polynomial_naive.hpp), compilation into dynamic libraries loaded via dlopen (slp_polynomial_compiled.hpp), and fast JIT compilation. JIT compilation, is a classical technique, traditionally used in scientific computing: when an expression such as a SLP needs to be evaluated at many points, it pays off to compile the expression and then perform the evaluations using fast executable code. When allowed by the operating system, it suffices to compile SLPs into executable memory regions, without temporary files. Since SLPs are very basic programs, there is no special need to appeal to general purpose compilers. In Multimix, such a compilation is supported for double coefficients, for SSE2 enabled CPU, and System V amd64 application binary interface (ABI), which covers most 64-bit Unix-like platforms.

To develop a confortable JIT library dedicated to SLPs, we turned to the Mathemagix language [START_REF] Van Der Hoeven | Mathemagix User Guide[END_REF], from which we benefit of extensible union types and fast pattern matching. Our Runtime library provides basic facilities to produce JIT executable code from assembly language. On the top of it, our Justinline library defines a templated SLP data type with additional JIT facilities. This includes common subexpression simplification, constant simplification, register allocation, and vectorization. Recall that vectorization is the ability to transform a SLP over a given ring type R to a SLP over vectors of R. This is especially useful in order to exploit SIMD technologies.

Timings for numeric types

In order to estimate the concrete overhead of ball arithmetic, we first focus on timings for double and complex<double>. In the rest of this article, timings are measured on a platform equipped with an Intel(R) Core(TM) i7-4770 CPU at 3.40 GHz and 8 GB of 1600 MHz DDR3, which includes AVX2 and FMA technologies. The platform runs the Jessie GNU Debian operating system with a 64 bit Linux kernel version 3.14. Care has been taken for avoiding CPU throttling and Turbo Boost issues while measuring timings. We compile with GCC [31] version 4.9.2 with options -O3 -mavx2 -mfma -mfpmath=sse.

In Table 1, column "double" displays timings for evaluating a multivariate polynomial over double, with 10 variables, made of 100 terms, built from random monomials of partial degrees at most 10. We build the SLP using a dedicated algorithm implemented in multimix/dag_polynomial.hpp. Support for this specific coefficient type may be found in multimix/slp_polynomial_double.hpp. This example, with the corresponding functions to reproduce these timings are available in multimix/bench/slp_polynomial_bench.cpp. The evaluation of this SLP takes 1169 products and 100 sums.

The first row corresponds to using the naive interpreted evaluation available by default from Multimix. In the second row, the SLP is printed into a C++ file, which is then compiled into a dynamic library with options -O3 -fPIC -mavx2 -mfma -mfpmath=sse. The compilation and dynamic loading take 260ms, which corresponds to about 10 4 naive evaluations.

The third row concerns JIT compilation from Multimix, which achieves compilation for SSE2 legacy scalar instructions in 50ms, with no optimization and no register allocation. Notice that this only corresponds to less than 30 naive evaluations. However the lack of optimization implies a loss of a factor more than two with respect to GCC.

The fourth row is for our JIT implementation in the Justinline library. Compilation performs register allocation as sole optimization, and takes about 8ms: this is much faster than with GCC, but still higher than in Multimix. Nevertheless, the integration of more powerful optimization features in the Mathemagix compiler should progressively reduce this gap. The implementation of additional optimizations in the Justinline library should also make it possible to get closer to the evaluation performance via GCC.

The second column of Table 1 shows similar timings for the complex<double> type from the Numerix library. We did not implement the JIT strategy in Multimix. Of course, the performance ratio between compiled and interpreted strategies is much lower than for double.

Timings for balls

We are now interested in measuring the speed-up of our evaluation strategies over balls.

The first column of Table 2 shows timings for balls over double (i.e. A = R). Early versions of the Mathemagix libraries already contained a C99 portable implementation of ball arithmetic in the Numerix library (see numerix/ball.hpp and related files). The first row of Table 2 is obtained with naive evaluation over this portable arithmetic when rounding centers to the nearest and radii upwards. We observe rather high timings involved by the compiler and the mathematical library. The second row is similar but concerns the rough ball arithmetic of Remark 2. The row "Naive, transient" is the interpreted transient ball arithmetic from Multimix. The next three rows correspond to dynamic compilation via GCC and Justinline; they reveal the gain of the JIT strategy. Notice that we carefully tuned the assembly code generated by our SLP compiler. For instance, if ymm0 contains -0.0 and if ymm1 contains a center a, then -a is obtained as vxorpd ymm0 ymm1 ymm2, and |a| as vandnpd ymm0 ymm1 ymm2. The latency and throughput of both these instructions are a single cycle and no branchings are required to compute |a|. In this way, each transient addition/subtraction takes 2 cycles, and each product 6 cycles. For rough arithmetic this increases to 5 and 9 cycles respectively. The gain of the transient arithmetic is thus well reflected in practice, since our example essentially performs products. Comparing to Table 1, we observe that transient arithmetic is just about 4 times slower than numeric arithmetic. This turns out to be competitive with interval arithmetic, where each interval product usually requires 8 machine multiplications and 6 min/max operations.

The second column of timings in Table 2 is similar to the first one, but with balls over complex<double>. The computation of norms is expensive in this case because the scalar square root instruction takes 14 CPU cycles. In order to reduce this cost, we rewrite SPLs so that norms of products are computed as products of norms. Taking care of using or simulating upwards rounding, this involves a slight loss in precision but does not invalidate the results. At the end, comparing to

Vectorization

In order to profit from SIMD technologies, we also implemented vectorization in our Justinline library, in the sense that the executable code runs over SSE or AVX hardware vectors. The expected speed-up of 2 or 4 is easily observed for double, complex<double>, and balls over double. For balls over complex<double>, a penalty occurs, because the vectorial square root instruction is about twice slower than its scalar counterpart. For instance, the evaluation of a univariate polynomial in degree 1000 with Hörner's method takes about 5000 CPU cycles over double (each fma instruction takes the expected latency), 13000 cycles over complex<double>, and 16000 cycles for transient balls of double, with both scalar and vectorial instructions. As for transient balls over complex<double>, scalar instructions amount to about 17000 cycles, while vectorial ones take about 28000 cycles.

Conclusion

In this paper, we have shown how to implement highly efficient ball arithmetic dedicated to polynomial evaluation. In the near future, we expect significant speed-ups in our numerical system solvers implemented within Mathemagix.

It is interesting to notice in Table 2 that the code generated by our rather straightforward JIT compiler for SLPs is more efficient than the code produced by GCC. This suggests that it might be worthwhile to put more efforts into the development of specific JIT compilers for SLPs dedicated to high performance computing.

We also plan to adapt the present results to standard intervals, that are useful for real solving. In that case, we replace input and constant intervals [x, y] by intervals of the form [xδ, y + δ], where δ = κ max (|x|, |y |, |y -x|) ǫ for suitable κ. We next proceed as usual, but without any assumption on the rounding mode.

We finally notice that interval arithmetic benefits from hardware accelerations on many current processors, as soon as IEEE 754 style rounding is integrated in an efficient manner. An interesting question is whether ball arithmetic might benefit from similar hardware accelerations. In particular, is it possible to integrate rounding errors more efficiently into error bounds (the radii of balls)? This might for instance be achieved using an accumulaterounding-error instruction for computing a guaranteed upper bound for r + κ ε ¯•(x) as a function of r, κ, x ∈ R.

[31] GCC, the GNU Compiler Collection. Software available at http://gcc.gnu.org, from 1987.

Appendix A Rounding errors for complex arithmetic

Let x = a + b i and y = c + d i be two complex numbers in R[i]. We will show that

x ± • y -x ± y x ± • y ǫ • (15)
x × • yx y x × • y 4 ǫ • + 5 • 2 E min -p+1 (16)

| x • -x | x • 3 ǫ • + 3 • 2 (E min -p+1)/2 . ( 17
)
In addition, in absence of underflows, the terms in 2 E min -p+1 may be discarded.

For short we set ι := 2 E min -p+1 , and we shall freely use the assumption ε • 2 -16 . The first bound (15) is immediate. As for the second one, it will be convenient to use the norm a + b i 1 = |a| + |b|, that satisfies a + b i a + b i 1 2 √ a + b i . We begin with combining

|a × • c -• b × • d -(a c -b d)| |a × • c -• b × • d| ǫ • + (|a × • c| + |b × • d|) ǫ • + 2 ι and |a × • d + • b × • c -(a d + b c)| |a × • d -• b × • c| ǫ • + (|a × • d| + |b × • c|) ǫ • + 2 ι into x × • y -x y 1 x × • y 1 ǫ • + x 1 y 1 ǫ • (1 -ǫ • ) -1 + (4 + 8 ǫ • ) ι.
We deduce that It follows that

|•[a 2 + b 2 ] -(a 2 + b 2 )| |•[a 2 + b 2 ] -(a × • a + b × • b)| + |a × • a + b × • b -(a 2 + b 2 )| •[a 2 + b 2 ] ǫ • + |a × • a + b × • b| ǫ • + 2 ι •[a 2 + b 2 ] ǫ • + (a 2 + b 2 + 2 ι) ǫ • (1 -ǫ • ) -1 + 2 ι •[a 2 + b 2 ] ǫ • + (a 2 + b 2 ) 1.1 ǫ • + 2.1 ι,
from which we extract

a 2 + b 2 (•[a 2 + b 2 ] (1 + ǫ • ) + 2.1 ι) (1 -1.1 ǫ • ) -1 •[a 2 + b 2 ] (1 + 2.2 ǫ • ) + 2.2 ι.

x × • y -x y x × • y 2 √

 2 ǫ • + x y 2 ǫ • (1ǫ • ) -1 + (4 + 8 ǫ • ) ι, whence x y x × • y 1 + 2 √ ǫ • + (4 + 8 ǫ • ) ι /(1 -2 ǫ • (1ǫ • ) -1 ), which simplifies into x y x × • y (1 + 4 ǫ • ) + (4 + 11 ǫ • ) ι. It follows that x × • yx y x × • y 2 √ ǫ • + 2 ǫ • (1 + 4 ǫ • ) (1ǫ • ) -1 + (4 + 17 ǫ • ) ι,which simplifies into[START_REF] Diep | Efficient algorithms for verified scientific computing: numerical linear algebra using interval arithmetic[END_REF].As to[START_REF] Neumaier | Interval methods for systems of equations[END_REF], we begin with|a × • aa 2 | |a × • a| ǫ • + ι and |b × • bb 2 | |b × • b| ǫ • + ι, that give |a × • a + b × • b -(a 2 + b 2 )| |a × • a + b × • b| ǫ • + 2 ι.

Table 1 .

 1 Polynomial evaluation with 100 terms of degree 10 in 10 variables, in ms.

		double complex<double>
	Multimix, naive	2.1	3.4
	Multimix, compiled 0.29	1.3
	Multimix, JIT	0.84	N/A
	Justinline, JIT	0.43	1.4

Table 1 ,

 1 we are glad to observe that our new transient arithmetic strategy is only about twice as expensive as standard numeric evaluations.

		Ball over	Ball over
		double	complex<double>
	Naive, rounded, C99	62	130
	Naive, rough, C99	66	200
	Naive, transient	14	18
	Compiled, transient	2.0	4.0
	JIT, rough	3.2	4.5
	JIT, transient	1.8	3.1

Table 2 .

 2 Polynomial evaluation with 100 terms of degree 10 in 10 variables, in ms.

Evaluation of SLPs

Bibliography

We thus obtain that

We distinguish the two following cases:

since the square root does not provoke underflows, we obtain

which means that both products a × • a and b × • b involve underflows. We restart the analysis from

Rounding errors for complex arithmetic


Shahid Rahman

A Very Brief Introduction to Standard Classical and Intuitionistic Dialogical Logic

The present paper, that provides an introduction to standard dialogical logic, has mainly didactic purposes. Thus, the study of the metalogical properties has been left totally by side. However, two sections have been added for those readers willing to go through a technically more demanding material. The first one contains a technically rigorous presentation of standard dialogical logic the second one presents, some very recent work towards a logic with content, applied to modal logic, where modal logic is developed in a purely dialogical way: instead of worlds, we have contexts, constituted by hypothetical assertions and where transitions between worlds are understood as extending contexts by the means of questions.

1

Introduction:

Dialogical logic developed by Paul Lorenzen and Kuno Lorenz, was the result of a solution to some of the problems that arouse in Lorenzen' Operative Logik (1955). 1 We can not discuss here thoroughly the passage from the operative to the dialogical approach, though as pointed out by Peter Schroeder-Heister, the insights of Operative logic had lasting consequences in the literature on proof-theory and still deserve attention nowadays. 2 Moreover, the notion of harmony formulated by the antirealists and particularly by Dag Prawitz has been influenced by Lorenzen's notions of admissibility; eliminability and inversion. However, on my view, the dialogical tradition is rather a rupture than a continuation of the operative project and it might be confusing to start by linking conceptually both projects together. Dialogical Logic was suggested at the end of the 1950s by Paul Lorenzen and then worked out by Kuno Lorenz. 3 Inspired by Wittgenstein's meaning as use the basic idea of the dialogical approach to logic is that the meaning of the logical constants is given by the norms 1 Cf. Lorenz 2001. 2 Schröder-Heister 2008. 3 The main original papers are collected in Lorenzen/Lorenz (1978). For an historical overview see Lorenz (2001). Other papers have been collected more recently in Lorenz (2008Lorenz ( , 2010a,b),b). A detailed account of recent developments since Rahman (1993), can be found in Rahman/Keiff (2005

or rules for their use. This feature of its underlying semantics quite often motivated the dialogical approach to be understood as a pragmatist semantics. 4The point is that those rules that fix meaning may be of more than one type, and that they determine the kind of reconstruction of an argumentative and/or linguistic practice that a certain kind of language games called dialogues provide. As mentioned above the dialogical approach to logic is not a logic but a semantic rule-based framework where different logics could developed, combined or compared. However, for the sake of simplicity and exemplification I will introduce only to the dialogical version of classical and intuitionist logics.

In a dialogue two parties argue about a thesis respecting certain fixed rules. The player that states the thesis is called Proponent (P), his rival, who puts into question the thesis is called Opponent (O). In its original form, dialogues were designed in such a way that each of the plays end after a finite number of moves with one player winning, while the other loses. Actions or moves in a dialogue are often understood as utterances5 or as speech-acts 6 . The point is that the rules of the dialogue do not operate on expressions or sentences isolated from the act of uttering them. 7 . The rules are divided into particle rules or rules for logical constants (Partikelregeln) and structural rules (Rahmenregeln). The structural rules determine the general course of a dialogue game, whereas the particle rules regulate those moves (or utterances) that are requests (to the moves of a rival) and those moves that are answers (to the requests).

Crucial for the dialogical approach are the following points 1. The distinction between local (rules for logical constants) and global meaning (included in the structural rules) 2. The player independence of local meaning 3. The distinction between the play level (local winning or winning of a play) and the strategic level (existence of a winning strategy). 4. A notion of validity that amounts to winning strategy independently of any model instead of winning strategy for every model. 5. The notion of winning in a formal play instead of winning strategy in a model.

Dialogical Logic and Meaning

Local Meaning

Particle rules:

In dialogical logic, the particle rules are said to state the local semantics: what is at stake is only the request and the answer corresponding to the utterance of a given logical constant, rather than the whole context where the logical constant is embedded.

• The standard terminology makes use of the terms challenge or attack and defence. 8However let me point out that at the local level (the level of the particle rules) this terminology should be devoid of strategic underpinning.

• Declarative utterances involve the use of formulae, interrogative utterances do not involve the use of formulae

The following table displays the particle rules, where X and Y stand for any of the players O or P:

X: α [x/k] X: ∃xα Y ?∃ X: α [x/k] (X chooses)
In the diagram, α[x/k] stands for the result of substituting the constant k for every occurrence of the variable x in the formula A.

One interesting way to look at the local meaning is as rendering an abstract view (on the semantics of the logical constant) that distinguishes between the following types of actions:

a) Choice of declarative utterances (=:disjunction and conjunction). b) Choice of interrogative utterances involving individual constants (=: quantifiers). c) Switch of the roles of defender and challenger (=: conditional and negation). As we will discuss later on we might draw a distinction between the switches involved in the local meaning of negation and the conditional).

Let us briefly mention two crucial issues to which we will come back later on

• Player independence: The particle rules are symmetric in the sense that they are player independent -that is why they are formulated with the help of variables for players. Compare with the rules of tableaux or sequent calculus that are asymmetric: one set of rules for the true(left)-side other set of rules for the false(right)-side. The symmetry of the particle rules provides, as we will see below, the means to get rid of tonk-like-operators.

• Sub-formula property: If the local meaning of a particle # occurring in φ involves declarative utterances, these utterances must be constituted by sub-formulae of φ.9

Global Meaning

Structural rules:

(SR 0) (starting rule):
The initial formula is uttered by P (if possible). It provides the topic of the argumentation. Moves are alternately uttered by P and O. Each move that follows the initial formula is either a request or an answer.

Comment:

The proviso if possible relates to the utterance of elementary propositione. See formal rule (SR 2) below.

(SR 1) (no delaying tactics rule):

Both P and O may only make moves that change the situation.

Comments: This rule should assure that plays are finite (though there might an infinite number of them). There are several formulations of it with different advantages and disadvantages. The original formulation of Lorenz made use of ranks; other devices introduced explicit restrictions on repetitions. Ranks seem to be more compatible with the general aim of the dialogical approach of distinguishing between the play level and the strategic level. Other non-repetition rules seem to presuppose the strategic level. In fact, if we take meaning to be constituted by interaction we need a way to ensure finiteness of plays because there is no such thing as an infinite interaction. That is to say, finiteness is an essential property of interaction. The potential infinity of plays required by proofs involving infinite domains is accounted for at the level of strategies (see [START_REF] Clerbout | First-order dialogical games and tableaux[END_REF][START_REF] Clerbout | Etude sur quelques sémantiques dialogiques: Concepts fondamentaux et éléments de metathéorie[END_REF]. . Let us describe here the rule that implements the use of ranks.

• After the move that sets the thesis players O and P each choose a natural number n and m respectively (termed their repetition ranks). Thereafter the players move alternately, each move being a request or an answer.

• In the course of the dialogue, O (P) may attack or defend any single (token of an) utterance at most n (or m) times.

(SR 2) (formal rule): 10 P may not utter an elementary proposition unless O uttered it first. Elementary propositione can not be challenged.

The dialogical framework is flexible enough to define the so-called material dialogues, that assume that elementary propositione have a fixed truth-value:

(SR *2) (rule for material dialogues):

Only elementary propositione standing for true propositions may be uttered. Elementary propositione standing for false propositions can not be uttered.

(SR 3) (winning rule): X wins iff it is Y's turn but he cannot move (either challenge or defend).

Global meaning

These rules determine the meaning of a formula where a particle occurs as a main operator in every possible play.

(SR 4i) (intuitionist rule): 11

In any move, each player may challenge a (complex) formula uttered by his partner or he may defend himself against the last challenge that has not yet been defended.

or (SR 4c) (classical rule):

In any move, each player may challenge a (complex) formula uttered by his partner or he may defend himself against any challenge (including those challenges that have already been defended once).

• Notice that the dialogical framework offers a fine-grained answer to the question: Are intuitionist and classical negation the same negations? Namely: The particle rules are the same but it is the global meaning that changes.

In the dialogical approach validity is defined via the notion of winning strategy, where winning strategy for X means that for any choice of moves by Y, X has at least one possible move at his disposal such that he (X) wins:

Validity (definition):

A formula is valid in a certain dialogical system iff P has a formal winning strategy for this formula.

Thus, • α is classically valid if there is a winning strategy for P in the formal dialogue Dc(α). • α is intuitionistically valid if there is a winning strategy for P in the formal dialogue Dint (α).

Comments on the dialogical notion of validity:

Helge Rückert pointed out, and rightly so, that the formal rule triggers a novel notion of validity. Validity, is not being understood as being true in every model, but as having a winning strategy independently of any model or more generally independently of any material grounding claim (such as truth or justification). The copy-cat strategy implicit in the formal rule is not copy cat of groundings but copy-cat of declarative utterances involving elementary propositione. Moreover one should add that there is the notion of formal play, that does not seem to correspond to nothing in model-theoretic approach: a formal play is not playing in a model.

In fact, one could see the formal rule as a process the first stage of which starts with what Laurent Keiff called contentious dialogues.12 Contentious dialogues are dialogues where a player X utters one or more elementary propositione that are dependent upon a given ground and X is not prepared to put this ground into question -one can think of it as a claim of having some kind of ground (or a claim of truth) for it. Moreover, the antagonist is willing to concede this ground for the sake of the argument. 13 Now, if we would like to avoid to have the result that an elementary proposition is true by the only reason that the player X stated it -that is, if we want to find a way out of contentious dialogues, then there are two possible ways:

• either we accept some principle of grounding external to the dialogue itself (and thus external to the interaction of the players) or • we look for a player principle of grounding that is internal to the dialogue and dependent on the interaction of the players.

The first ways leads to material dialogues the second to formal ones If we are willing to accept something like material truth, then we can think that the grounds upon which the elementary propositione depend are facts of the world and a grounded elementary propositione is a way to say that it is true. However, something more general might be thought too, such as true in virtue of some players' independent ground. This is the basis on which the rule for material dialogues has been formulated

Rückert pointed out that the formal rule establishes a kind of game where one of the players must play without knowing what the antagonist's justifications of the elementary propositione are. Thus, according to this view, the passage to formal dialogues relates to the switch to some kind of games with incomplete information. Now, if the ultimate grounds of a dialogical thesis are elementary propositione and if this is implemented by the use of a formal rule, then the dialogues are in this sense necessarily asymmetric. Indeed, if both contenders were restricted by the formal rule no elementary proposition can ever be uttered. Thus, we implement the formal rule by designing one player, called the proponent, whose utterances of elementary propositione are, at least, at the start of the dialogue restricted by this rule.

Apparently, the formal rule introduces an asymmetry in relation to the commitments of O and P particularly so in the case of the utterance of the conditional. Indeed, if O utters a conditional, then P' challenge commits him to a declarative utterance that must at the end be based on atomic moves of O. If it is O that challenges a conditional no such commitment will be triggered. But it would be a mistake to draw from this fact the conclusion that the local meaning of the conditional is not symmetric. The very point of player independence is that it is a property of the meaning of the logical particles not of the dialogue as a whole where P is committed to a thesis. Furthermore the asymmetry of the winning strategy is triggered by the semantic asymmetry of the formal rule. It is the possibility to isolate local meaning from validity commitments that allows dialogicians to speak of the symmetry of the logical constants and this prevents tonk-like operators from being introduced in the dialogical framework.

Examples

In the following examples, the outer columns indicate the numerical label of the move, the inner columns state the number of a move targeted by an attack. Expressions are not listed following the order of the moves, but writing the defence on the same line as the corresponding attack, thus showing when a round is closed. Recall, from the particle rules, that the sign "-" signalises that there is no defence against the attack on a negation.

For the sake of a simpler notation we will not record in the dialogue the rank choices but assume the uniform rank O: n=1 P: m=2:

Ex. 1: Classical and intuitionistic rules

In the following dialogue played with classical structural rules P' move 4 answers O's challenge in move 1, since P, according to the classical rule, is allowed to defend (once more) himself from the challenge in move 1. P states his defence in move 4 though, actually O did not repeat his challenge -we signalise this fact by inscribing the not repeated challenge between square brackets.

O P p∨¬p 0 1 ? ∨ 0 ¬p 2 3 p 2 - [1] [? ∨ ] [0 ] p 4
Classical rules. P wins.

In the dialogue displayed below about the same thesis as before, O wins according to the intuitionistic structural rules because, after the challenger's last attack in move 3, the intuitionist structural rule forbids P to defend himself (once more) from the challenge in move 1.

O P p∨¬p 0 1 ? ∨ 0 ¬p 2 3 p 2 - Intuitionist rules. O wins.

Ex. 2:

The following example shows that P wins double negation if he plays with the classical rule but loses if it is the intuitionistic one

O P ¬¬p→p 0 1 ¬¬p 0 p 4 - 1 ¬p 2 3 p 2 -
Classical rules. P wins P will not win with the intuitionistic rule since he must answer to last challenge. The defensive move 4 is then forbidden since the last challenge was move 3 and 4 answers the challenge brought forward by O in his move 1:

O P ¬¬p→p 0 1 ¬¬p 0 - 1 ¬p 2 3 p 2 -

Intuitionistic rules.O wins

P cannot win since O challenges with move 3 and P has no more legal move at his disposal. O wins since he has the last word.

Ex. 3:

In the following example the Proponent can win the double negation of the third excluded, despite the fact that he is playing with intuitionistic rules. Recall -form the preceding example -that intuitionist logic double negation is not equivalent as the positive version of expression. Here P makes use of the repetition rank 2. That he is allowed to challenge twice the same move of his antagonist. The rank 2 forbids P to start again with a new challenge. However it should be clear that even if the rank would be higher O will always win. The second following branch that the clever opponent can finish the affair wihout involveing higher ranks. It is sufficient for him to chose the same individual constant. Thus, unless it has been conceded that A,xy is reflexive before starting the play O wins (in this branch) by making the choice of not changing the individual constant introduced by P. . Let L be a first-order language built as usual upon the propositional connectives, the quantifiers, a denumerable set of individual variables, a denumerable set of individual constants and a denumerable set of predicate symbols (each with a fixed arity).

O P ¬¬(p∨¬p) 0 1 ¬(p∨¬p) 0 - - 1
We extend the language L with two labels O and P, standing for the players of the game, and the question mark `?'. When the identity of the player does not matter, we use variables X or Y (with X≠Y). A move is an expression of the form `X-e', where e is either a formula ϕ of L or the form `?[ϕ 1 ,..., ϕ n ]'. We now present the rules of dialogical games. There are two distinct kinds of rules named particle (or local) rules and structural rules. We start with the particle rules.

Previous move

X-ϕ∧ψ X-ϕ∨ψ X-ϕ→ψ X-¬ϕ

Challenge Y-?[ϕ] or Y-?[ψ] Y-?[ϕ,ψ] Y-ϕ Y-ϕ Defence X-ϕ resp. X-ψ X-ϕ or X-ψ X-ψ -- Previous move X-∀xϕ X-∃xϕ Challenge Y-?[ϕ(a/x)] Y-?[ϕ(a 1 /x),...,ϕ(a n /x)] Defence X-ϕ(a/x) X-ϕ(a i /x) with 1≤ i ≤n
In this table, the a i s are individual constants and ϕ(a i /x) denotes the formula obtained by replacing every occurrence of x in ϕ by a i . When a move consists in a question of the form `?[ϕ 1 ,...,ϕ n ]', the other player chooses one formula among ϕ 1 ,...,ϕ n and plays it. We can thus distinguish between conjunction and disjunction on the one hand, and universal and existential quantification on the other hand, in terms of which player has a choice. In the cases of conjunction and universal quantification, the challenger chooses which formula he asks for. Conversely, in the cases of disjunction and existential quantification, the defender is the one 14

The following brief presentation of standard dialogical logic has been extracted from Nicolas [START_REF] Clerbout | First-order dialogical games and tableaux[END_REF][START_REF] Clerbout | Etude sur quelques sémantiques dialogiques: Concepts fondamentaux et éléments de metathéorie[END_REF]. who can choose between various formulas. Notice that there is no defence in the particle rule for negation.

Particle rules provide an abstract description of how the game can proceed locally: they specify the way a formula can be challenged and defended according to its main logical constant. In this way we say that these rules govern the local level of meaning. Strictly speaking, the expressions occurring in the table above are not actual moves because they feature formulas schemata and the players are not specified. Moreover, these rules are indifferent to any particular situations that might occur during the game. For these reasons we say that the description provided by the particle rules is abstract. The words "challenge" and "defence" are convenient to name certain moves according to their relationship with other moves. Such relationships can be precisely defined in the following way. Let Σ be a sequence of moves. The function p Σ assigns a position to each move in Σ, starting with 0. The function F Σ assigns a pair [m,Z] to certain moves N in Σ, where m denotes a position smaller than p Σ (N) and Z is either C or D, standing respectively for "challenge" and "defence". That is, the function F Σ keeps track of the relations of challenge and defence as they are given by the particle rules. A play (or dialogue) is a legal sequence of moves, i.e., a sequence of moves which observes the game rules. The rules of the second kind that we mentioned, the structural rules, give the precise conditions under which a given sentence is a play. The dialogical game for ϕ, written D(ϕ), is the set of all plays with ϕ as the thesis (see the Starting rule below). The structural rules are the following: SR0 (Starting rule) Let ϕ be a complex formula of L. For every π∈D(ϕ) we have:

-p π (P-ϕ)=0, -p π (O-n:=i)=1, -p π (P-m:=j)=2
In other words, any play π in D(ϕ) starts with P-ϕ. We call ϕ the thesis of the play and of the dialogical game. After that, the Opponent and the Proponent successively choose a positive integer called repetition rank. The role of these integers is to ensure that every play ends after finitely many moves, in a way specified by the next structural rule.

SR1 (Classical game-playing rule)

-Let π∈D(ϕ). For every M in π with p π (M)>2 we have F π (M)=[m',Z] with m'<p π (M) and Z∈{C,D} -Let r be the repetition rank of player X and π∈D(ϕ) such that -the last member of

π is a Y move, -M 0 is a Y move of position m 0 in π, -M 1 ,...,M n are X moves in π such that F π (M 1 )=...=F π (M n )=[m 0 ,Z]. Consider the sequence 15 π' =π * N where N is an X move such that F π' (N)=[m 0 ,Z]. We have π'∈D(ϕ) only if n < r.
The first part of the rule states that every move after the choice of repetition ranks is either a challenge or a defence. The second part ensures finiteness of plays by setting the player's repetition rank as the maximum number of times he can challenge or defend against a given move of the other player.

SR2 (Formal rule)

Let ψ be an elementary sentence, N be the move P-ψ and M be the move O-ψ . A sequence π of moves is a play only if we have: if N∈π then M∈π and p π (M)<p π (N).

A play is called terminal when it cannot be extended by further moves in compliance with the rules. We say it is X terminal when the last move in the play is an X move.

SR3 (Winning rule) Player X wins the play π only if it is X terminal.

Consider for example the following sequences of moves: P-Qa→Qa, O-n:=1, P-m:=12, O-Qa, P-Qa . We often use a convenient table notation for plays. For example, we can write this play as follows:

O P Qa→Qa 0 1 n:=1 m:=12 2 3 Qa (0) Qa 4
The numbers in the external columns are the positions of the moves in the play. When a move is a challenge, the position of the challenged move is indicated in the internal columns, as with move 3 in this example. Notice that such tables carry the information given by the functions p and F in addition to represent the play itself.

However, when we want to consider several plays together -or example when building a strategy -such tables are not that perspicuous. So we do not use them to deal with dialogical games for which we prefer another perspective. The extensive form of the dialogical game D(ϕ) is simply the tree representation of it, also often called the game-tree. More precisely, the extensive form E ϕ of D(ϕ) is the tree (T,l,S) such that: i) Every node t in T is labelled with a move occurring in D(ϕ)

ii) l: T→ N iii) S⊆T 2 with:

-There is a unique t 0 (the root) in T such that l(t 0 )=0, and t 0 is labelled with the thesis of the game.

-For every t≠t 0 there is a unique t' such that t'St.

-For every t and t' in T, if tSt' then l(t')=l(t)+1.

-Given a play π in D(ϕ) such that p π (M')=p π (M)+1 and t, t' respectively labelled with M and M', then tSt'.

A strategy for Player X in D(ϕ) is a function which assigns an X move M to every non terminal play π with a Y move as last member such that extending π with M results in a play. An X strategy is winning if playing according to it leads to X's victory no matter how Y plays.

A strategy can be considered from the viewpoint of extensive forms: the extensive form of an X strategy σ in D(ϕ) is the tree-fragment E ϕ,σ =(T σ , l σ , S σ ) of E ϕ such that:

i) The root of E ϕ,σ is the root of E ϕ .

ii) Given a node t in E ϕ labelled with an X move, we have that tS σ t' whenever tSt'.

iii) Given a node t in E ϕ labelled with a Y move and with at least one t' such that tSt', then there is a unique σ(t) in T σ where tS σ σ(t) and σ(t) is labelled with the X move prescribed by σ.

Here are some examples of results which pertain to the level of strategies. 16 -Winning P strategies and leaves. Let w be a winning P strategy in D(ϕ). Then every leaf in E ϕ,w is labelled with a P signed atomic sentence.

-Determinacy. There is a winning X strategy in D(ϕ) if and only if there is no winning

Y strategy in D(ϕ).
-Soundness and Completeness of Tableaux. Consider first-order tableaux and firstorder dialogical games. There is a tableau proof for ϕ if and only if there is a winning

P strategy in D(ϕ).
By soundness and completeness of the tableau method with respect to modeltheoretical semantics, it follows that existence of a winning P strategy coincides with validity: There is a winning P strategy in D(ϕ) if and only if ϕ is valid.

EXAMPLES OF EXTENSIVE FORMS

Extensive forms of dialogical games and of strategies are infinitely generated trees (trees with infinitely many branches). Thus it is not possible to actually write them down. But an illustration remains helpful, so we add Figures 1 and2 below.

Figure 1 partially represents the extensive form of the dialogical game for the formula

∀x(Q(x) → Q(x)).
Every play in this game is represented as a branch in the extensive form: we have given an example where the leftmost branch represents one of the simplest and shortest plays in the game. The root of the extensive form is labelled with the thesis. After that, the Opponent has infinitely many possible choices for her repetition rank: this is represented by the root's having infinitely many immediate successors in the extensive form.

The same goes for the Proponent's repetition rank, and for every time a player is to choose an individual constant.

16

These results are proven, together with others, in [START_REF] Clerbout | First-order dialogical games and tableaux[END_REF]. But since all the possible ways for the Opponent to play must be taken into account by a strategy, the other ramifications are kept. In our example, the strategy prescribes choosing the same repetition rank as the Opponent. Of course there are infinitely many other strategies available for P.

A dialogical approach to Modal Logic: Worlds as hypotheses 17

In fact there is already some work on dialogical modal logic (such as Rahman/Rückert (2001), Redmond/Fontaine (2011), Clerbout (2013a)). However, this approach that makes use of labels is too close to the model-theoretical approach of Kripke's modal logic: in such a setting, labels are names of model-theoretic worlds after all. What we need is a conception where worlds are introduced at the object-language level and have genuine dialogical rather than metaphysical nature. Fortunately, A. [START_REF] Ranta | Constructing possible worlds[END_REF][START_REF] Ranta | Type-Theoretical Grammar[END_REF] provided one half of the task by developing a CTT version of possible world-semantics. What we need now is to combine it with the dialogical approach to CTT recently developed (see Appendix). Let us start with the CTT approach to possible worlds as developed by [START_REF] Ranta | Type-Theoretical Grammar[END_REF]. The main idea of Ranta is that an assertion relativized to a possible world W amounts to a hypothetical where that assertion is brought forward provided the hypothesis W and this is expressed at the level of the object-language. In other words, the modal assertions are reduced to hypotheticals. Thus, one might say that, in some way, Leibniz's (metaphysical) notion of possible world is placed into Kant's conception of hypotheticals. Thus, what we need is not labels for worlds but assertions that are brought forward during a play provided some open assumptions. Accordingly, hypotheses take the place of worlds and arbitrary elements (variables) of the hypotheses the proposition is dependent on, take the place of world-labels.

More generally, and independently of the dialogical setting, this yields the following correspondences -pointed out by [START_REF] Ranta | Constructing possible worlds[END_REF]Ranta ( , 1983)):

A : set in W means A(x) : set (x : W) A = B : set in W means A(x) = B(x) : set ( x : W) a : A in W means a(x) : A(x) (x : W) a = b: A in W means a(x) = b(x): A(x) (x : W)
The CTT take on hypotheses is that when making the hypothesis A, we consider that there is an arbitrary proof of A. We use a variable x for such a proof in the same way as we make use of variable when considering an arbitrary element of a set. In the case of the dialogical approach to CTT, proof-objects only occur at the level of strategies, however, at the play level, play-objects provide the ontology suitable for that level. More precisely, while bare play-objects provide the ontology of categorical moves, functions provide the play-objects of hypotheticals.

Let us now make use of the translation proposed by Ranta in order to formulate in the context of dialogical logic the local meaning of quantifiers brought forward by hypothetical movesand so doing, introduce its modal structure at the level of the object-language:

In order to avoid a heavy notation we will not write the world variable in proposition but we will assume that it occurs free in in it; for instance the expression b(y) : The quantification that results from these rules corresponds to what in standard modal logic is known as actualist quantification -i.e., the scope of the quantifiers is circumscribed by the objects that "inhabit" W. In our setting this means that the players must choose for their moves the suitable hypothetical objects, i.e. those functions defined on the hypothesis W. This yields a new approach to free logic in general and of dialogical free logic in particular: One can infer Something is a vampire from Nosferatu is a vampire only if the existential is relativized to the same world W, upon which Nosferatu is dependent. We cannot, for example, infer b(y) : (∃x : A) Βx(y) (y : W), neither from the hypothetical a(z) : Bk(z) (z : V) nor from the categorical expression a : Bk. From the dialogical perspective; the point is that because of the formal rule, in order to win P can only choose those play objects that O has chosen before.

Thus, since during the plays involving our examples, O brings forward a(z) : Bk(z) (z : V) (in the first example) and a : Bk, in the second, P will not be able to make a suitable choice that yields a copy-cat of those moves of O -the closest move that P can obtain is a(y) : Bk(y) (y : W) -that will yield a P-win for the first example iff V=W and a win in the second examples iff there is no (more) hypothesis. Moreover, the following tautological hypothetical implications are valid (there is winning strategy for P) : b(y) : Bk → (∃x : A) Βx (y : W) and b(y) : (∀x : A)Bx →Bk (y : W) only if the formation rules for Bk : prop presuppose a set such that this set is dependent upon W.

However we have not still tackled the following questions:

What corresponds to the accessibility relation of standard modal logic?

What is a set W?

How do we understand fictional objects as Holmes? The answer to these questions takes us to the next sections.

Epistemic alternatives, Accessibility and the Dialogical perspective. 18One way to see the relation between a world W 1 and world W 2 is to see it as an epistemic alternative, where W 2 is an extension of W 1 in the sense that W 2 adds information in such a way that every proposition that is true under the hypothesis W 1 is also true under the hypothesis W 2 . More generally we express this situation in the following way: d(y) : W 1 (y : W 2 ). Thus, if W 2 is accessible from W 1 , then there is a function f from W 2 to W 1 -see Ranta (1994, p. 147). But certainly there might many such functions, that express not only that W 2 from W 1 but also that, say, V and U are accessible too from W 1 , though W 2 , V, U are not accessible between them. The whole yields a tree structure with W 1 as root. In the dialogical frame the point is that if it is the case that a(b(y)) : A (b(y) : W (y : V)), and a(x)) : A (x : W), then players can bring forward b(y) : A ( y : V). Interesting is the fact that one way to understand a(b(y)) is the variant of the object a(x) when 'transferred' to the world V. If the language contains modal operators, the relation between W and V, can also be brought dynamically into the play by the choices of the players as usual in dialogical modal logic -see Rahman/Rückert (2001), however, for the purpose of the study of hypothetical objects such operators are not needed.

Worlds as Contexts

Still we do not know exactly what the sets W are and in what sense they can be seen as expressing the idea of "possible world". Recall that in this context each world W, V, U is a set -, and this set is a hypothesis. What we need to elucidate is what are the elements of this set and in what sense we can say that is captures the idea of possible. Let us start with the latter. From the epistemic point of view possible means, different alternatives of adding knowledge provided full knowledge is not achieved. A. Ranta (1991, p. 78) Here we are then, in such a frame, possible means an alternative ways of completing not yet achieved full knowledge. Moreover, this means that possible is always an approximation to full knowledge: if the approximation were to end, then possibility will not be any more there, but full knowledge. Possible is that what always can be completed. But how to express this notion formally and how to link it with the dialogical approach? Formally speaking, a possible world is itself a set constituted by a sequence of hypothetical assertions with a dependence defined between them (this structure is called a context). Let us call Γ the sequence that approximates a world, then we have a :

A in Γ means a(x 1 , …, x n ) : A(x 1 , …, x n ) (x 1 : A 1 , …, x n : A n (x 1 …, x n-1 ))
and similar applies to: A : set in Γ, A = B : set in Γ, and a = b : A in Γ As mentioned above, if contexts should capture the notion of possible world, it is important that the approximations never end. Thus, as pointed out by Ranta (1991, p. 93) worlds are a kind of limits of sequences of hypothetical assertions further and further specified -without ever reaching full specification. In fact there are two ways to extend a context by adding information to it, and one by reducing uncertainty into it, namely:

(1) By adding a further hypothesis. It may happen that the new proposition, say, A(x 1 , …,

x n ) be potentially true in Γ (that is, when the new proposition can be inferred from the original context -then there in growth only on actual knowledge ), but it could also add a new information (2) By introducing a definition for some variables and achieving in this way a reduction of uncertainty. For instance, the context Γ = (x 1 : A 1 , ... x n : A n ) is extended to the extension Γ, x k = c : A k So that in the new context every occurrence of x k is substituted by a. The new context is obtained from Γ by removing the hypothesis x k : A k by c(x 1 ... x n ). Thus the new context is shorter than the original. Still, this operation furnishes not only the knowledge of the original context but the value of the one variable reduces the uncertainty within the context.

(3) By presenting a new context ∆ such that there is function f from ∆ to Γ as explained in II.2.1a

As observed by Ranta (1994, p. 146-47) 1) and 2) can be seen as special cases of 3). Thus (3) provides the most general case of extension and, at the same time deploys the constructive meaning of the notion of accessibility. Dialogically speaking, extensions of contexts are to be understood as answers to questions of specification -recall that we are dealing with a fully interpreted language. Assume that one player brings forward the hypothetical that there is a play object for A(y), provided x is a living being, y is a human(x). Then the first kind of extension will the triggered by a question such as is (s)he European or Asian?. The second kind of extension will be triggered by a wh-question (that is a who, what or when question.

The third kind of extension can thought as asking the defender to establish a link between the variables between the first and the new context. Assume for instance that the initial context Γ contains the disjunction A ∨ Β the hypothetical play object of which is the variable x. Assume further on that the new context ∆ contains y : A. In such a case the player that claims that ∆ is an extension of Γ must produce the definition L ∨ (x) = y : A ∨ B, and similar must happen in relation to every component of Γ. Summing up, from the dialogical perspective modality can be seen as a dialogue where moves involved questions and answers in relation to underlying contexts.

Appendix III The Dialogical Approach to CTT 19

The Formation of Propositions Before delving into the details about play-objects, let us first discuss the issue of the formation of expressions, and in particular of propositions, in the context of dialogical logic. In standard dialogical systems there is a presupposition that the players use well-formed formulas (wff's). One can check well-formedness at will, but only via the usual metareasoning by which one checks that the formula indeed observes the definition of wff. The first addendum we want to make is to allow players to question the status of expressions, in particular to question the status of something as actually standing for a proposition. Thus we start with rules giving a dialogical explanation of the formation of propositions. These are local rules added to the particle rules which give the local meaning of logical constants (see next section).

Let us make a remark before displaying the formation rules. Because the dialogical theory of meaning is based on argumentative interaction, dialogues feature expressions which are not posits or sentences. They also feature requests used as challenges, as illustrated by the formation rules below and the particle rules in the next section. Now, by the No entity without type principle, the type of these actions, which type we shall write "formation- By definition the falsum symbol ⊥ is of type prop. Therefore the formation of a posit of the form ⊥ cannot be challenged. The next rule is not a formation rule per se but rather a substitution rule.20

Posit-substitution

There are two cases in which Y can ask X to make a substitution in the context x i : A i . The first one is when in a standard play a variable (or a list of variables) occurs in a posit with a proviso. Then the challenger posits an instantiation of the proviso:

Posit Challenge Defence X ! π(x 1 , …, x n ) (x i : A i ) Y ! τ 1 : A 1 , …, τ n : A n X ! π(τ 1 …τ n )
The second case is in a formation-play. In such a play the challenger simply posits the whole assumption as in Move 7 of the example below:

Posit Challenge Defence X ! π(τ 1 , …, τ n ) (τ i : A i ) Y ! τ 1 : A 1 , …, τ n : A n X ! π(τ 1 , …, τ n )
Play objects/ The idea is now to design dialogical games in which the players' posits are of the form "p : ϕ" and acquire their meaning in the way they are used in the game -i.e., how they are challenged and defended. This requires, among others, to analyse the form of a given play-object p, which depends on ϕ, and how a play-object can be obtained from other, simpler, play-objects. The standard dialogical semantics for logical constants gives us the needed information for this purpose. The main logical constant of the expression at stake provides the basic information as to what a play-object for that expression consists of:

A play for X ϕ∨ψ is obtained from two plays p 1 and p 2 , where p 1 is a play for X ϕ and p 2 is a play for X ψ. According to the particle rule for disjunction, it is the player X who can switch from p 1 to p 2 and vice-versa.

A play for X ϕ∧ψ is obtained similarly, except that it is the player Y who can switch from p 1 to p 2 .

A play for X ϕ→ψ is obtained from two plays p 1 and p 2 , where p 1 is a play for Y ϕ and p 2 is a play for X ψ. It is the player X who can switch from p 1 to p 2 .

The standard dialogical particle rule for negation rests on the interpretation of ¬ϕ as an abbreviation for ϕ→⊥, although it is usually left implicit. It follows that a play for X ¬ϕ is also of the form of a material implication, where p 1 is a play for Y ϕ and p 2 is a play for X ⊥, and where X can switch from p 1 to p 2 .

As for quantifiers, we are dealing with quantifiers for which the type of the bound variable is always specified. We thus consider expressions of the form (Qx : A)ϕ, where Q is a quantifier symbol.

Posit

Figure 2

 2 Figure 2 partially represents the extensive form of a strategy for the Proponent in this game. It is a fragment of the tree of Figure 1 where each node labelled with an O-move has at most one successor. We do not keep track of all the possible choices for P any more: every time the Proponent has a choice in the game, the strategy selects exactly one of the possible moves.

  (∃x : A)ϕ (y : W) should be read as b(y) : [(∃x : A)ϕ](y) (y : W): (b(y)) : ϕ(L(b(y))) (y : W) Y ? prop X (∀x : A)ϕ : prop, A, W : set X b(y) : (∀x : A)ϕ (y : W) Y L ∀ (b(y)) : A (y : W) X R ∀ (b(y)) : ϕ(L(p(y))))ϕ (y : W)

  links this notion of possibility with Husserl's (Cart. Med., p. 62) conception of different ways of completing what I know.

  has the choice] X R {...} (p) : ϕ(L(p)) Y ? prop X (∀x : A)ϕ : prop X p : (∀x : A)ϕ Y L ∀ (p) : A X R ∀ (p) : ϕ(L(p))

  In the following example. we separated two branches or subdialogues only because of didactic aims not because this separation is intrinsical to the development of a dialogue . Each of the branches is motivated by a possible choice of O. In one subdialogue he chooses to defend himself by bringing forward the left part of the disjunction (it is his choice anyway) and in the other the right one. However, he looses in both. In fact these plays, build what[START_REF] Clerbout | First-order dialogical games and tableaux[END_REF][START_REF] Clerbout | Etude sur quelques sémantiques dialogiques: Concepts fondamentaux et éléments de metathéorie[END_REF] calls the core of the winning strategy. That is P wins independently of O's choices and that is why these plays build the core of the a proof of the validity of the thesis brought forward by P. Notice that P will win irrespectively if intuitionistic or classical rules are used.In the following examples we leave the reader to check if the thesis is winnable by P with both intuitionistic and classical rules

			5	?-ki	4		7	1	p	Aki	5 ?-kz	?-∨	10	6
			9 7	O Aki∨Bki Aki	7 1					¬¬(¬¬p→p) ? ∨ P 3 ?-ki →∞	p☺	0	8
	Option 2:		1	¬(¬¬p→p) -	0 Branch2 1	-¬¬p→p	2
	Ex. 6:	1 3 5	3 5 1 ∀x(Ax∨Bx) 0 ¬¬p p Branch 1 2 4 ∀x(Ac∨Bc) → ( ∀xAx∨∀xBx) 3 ¬p -1 ¬¬p→p (∀xAx∨∀xBx) 3 2 ∀xAx O P ?-∨ 5 ?-ki 4 ∀x(∀xAx→Ax)→∀xAx 7 ¬¬p 6 p ☺ O P ∃x (Px∨Qx) →∃x (Px∨Qx) ∃x (Px∨Qx) 0 ∃x (Px∨Qx) ?-∃ 2 Pki∨Qki Pki ∨Qki 1 ?-∃ 7 1 ?-ki 1 ∀x(∀xAx→Ax) 0 ∀xAx Aki∨Bki 9 Bki 7 3 ?-ki 2 Aki☺ ? ∨ 5 ∀xAx→Aki 1 ?-ki ∀xBx 11 ?-kj 7 Aki 5 ∀xAx 10 Branch 2 O P	4 6 8 0 2 6 10 4
	Ex. 8:		Branch 1 1 ∀x(∀xAx→Ax) 0 O 3 ?-ki 2 1 ∃x (Px∨Qx) O 5 ∀xAx→Aki 0 3 ?-∃ 2 5 Pki∨Qki 1 ∀x(∀xAx→Ax) 0 7 ?-ki 6 7 ?-∨ 6 3 ?-ki 2 9 ∀xAx→Aki 9 Qki 5 ∀xAx→Aki 11 ?-ki 10	1 5 1 9 5	1 5	∀x(∀xAx→Ax) → ∀xAx ∀xAx P ∃x (Px∨Qx) →∃x (Px∨Qx) P ?-ki ∃x (Px∨Qx) ∀x(∀xAx→Ax)→∀xAx ∀xAx Pki ∨Qki ∀xAx ?-∃ Qki ☺ ?-ki ?-ki ∀xAx ?-∨ ∀xAx	10	10
					Branch 2
				O								P
	Ex. 5: Option 1: Ex. 9:		1	∃x(Px∨Qx)	0			∃x(Px∨Qx) →∃x(Px∨Qx) ∃x(Px∨Qx)
	Ex. 7:	O [(p∨q)∧¬p] ¬p p∨q ?-∃ Pki ∨Qki O ?-∨ Branch 1 0 2 6 Pki O 1 ∀x∃xAxy 0 3 ∃xAxki 1 ∀x(∀xAx→Ax) 0 1 3 5 3 5 7 9 3 ?-ki 2 5 ∀xAx→Aki Branch 1	1 1 1 5 1 3 5 1	P [(p∨q)∧¬p]→q ?-∧2 ?-∧1 Pki ∨Qki P ?-∃ ¬∀x∃xAxy 0 Pki ☺ ?-∨ P ?-ki 2 ∀x(∀xAx→Ax)→∀xAx 0 2 ?-∃ 4 ∀xAx 4 ?-∨ 6 Aki☺ ?-ki	10
			7	Aki O			5	P		∀xAx
				O			¬∀x∃xAxy	P	0
	O 1 [(p∨q)∧¬p] 0 3 ¬p 5 p∨q 7' q	p∨¬p ¬p -p∨¬p p ☺ ∀x(Ac∨Bc) → ( ∀xAx∨∀xBx) 0 2 2 4 4 1 6 6 8 O P 2 P 1 ?-ki 2 (∀xAx∨∀xBx) ∀xAx ∀x(∀xAx→Ax)→∀xAx 3 ?-∃ 4 4 1 ∀x(∀xAx→Ax) 0 ?-∨ p ?-∨ P [(p∨q)∧¬p]→q 0 q☺ 8' ?-∧2 2 ?-∧1 4 ?-∨ 6 Branch 2 1 ∀x∃xAxy 0 1 ∀x(Ax∨Bx) 0 3 5 7 1 1 5 O 3 ∃xAxki 3 ?-∨ 2 5 Akjki 5 ?-ki ∀xAx 7 ∃xAxkj 1 ?-kj 6 4 7 Aki∨Bki 1 ?-ki 3 ?-ki 2 9 Akzkj 7 ?-∃ 8 6 7 ? ∨ ∀xAx 5 8 5 ∀xAx→Aki 1 ?-ki 1
	Ex. 4: Similar applies to the following 7 9 ∀xAx→Akj ?-kj 1 ∀x(Ax∨Bx) 0 3 ?-∨ 2 11 ?-kz	[(p∨q)∧¬p]→q 0 ?-∧2 2 ?-∧1 4 ∀x(Ac∨Bc) → ( ∀xAx∨∀xBx) 0 1 [(p∨q)∧¬p] 0 3 ¬p 1 5 p∨q 1 6 Branch1 1 ?-kj 2 9 ∀xAx 10 (∀xAx∨∀xBx) ∀xAx 4 10

  request", should be specified during a dialogue

	Posit	Challenge	Defence
		[when different challenges are
		possible, the challenger chooses]
	X ! Γ : set	Y ? c Γ,	X ! a 1 : Γ, X ! a 2 : Γ, …
		or	X gives the canonical elements of Γ; provides
			a generation method a i : Γ ⇒ a j : Γ, provides
			the equality rules
		Y ? F∨1	X ! ϕ : prop
	X ! ϕ ∨ ψ : prop	or
	(similar applies for the rest of	Y ? F∨2	X ! ψ : prop
	the propostional connectives)
		Y ? F∀1	X ! A : set
	X ! (∀x : A) ϕ(x) : prop	or
		Y ? F∀2

X ! ϕ(x) : prop (x : A) Y ? F∃1 X ! A : set X ! (∃x : A) ϕ(x) : prop or Y ? F∃� X ! ϕ(x) : prop (x : A)

Quite often it has said that dialogical logics has a pragmatic approach to meaning. I concede that the terminology might be misleading and induce one to think that the theory of meaning involved in dialogic is not semantics at all. Helge Rückert proposes the more appropriate formulation pragmatistische Semantik (pragmatist semantics), perhaps even better: pragmatist theory of meaning.

Cf.Rahman/Rückert 2001, 111 and Rückert 2001, chapter 1.2.

Cf. Keiff 2007.

Tulenheimo 2010.

See Keiff 2007, Rahman/Clerbout/Keiff 2009. Tero Tulenheimo pointed out that this might lead the reader to think that already at the local level there are strategic features and that this contravenes a crucial feature of the dialogical framework. Indeed, LaurentKeiff [2007] introduced the terminology requests and answers. However the dialogical vocabulary has been established with the former choice and it would be perhaps confusing to change it once more.

This has been pointed out by Laurent Keiff and by Helge Rückert in several communications.

In the standard literature on dialogues, there is an asymmetric version of the intuitionist rule, called E-rule since Felscher[1985]. For a discussion of this see appendices 1 and 2.

Cf. Clerbout/Keiff/Rahman 209 and in Keiff/Rahman 2010.

Cf.Keiff/Rahman 2010 (156-157), where this is linked to some specific passages of Plato's Gorgias (472b-c).

We use π * N to denote the sequence obtained by adding move N to the play π.

For the CTT approach to the notion of possible worlds in the present and the following sections we follow[START_REF] Ranta | Constructing possible worlds[END_REF]

1994).

The present overview on the dialogical approach to CTT is based onRahman/Clerbout (2013,

2014).

It is an application of the original rule from CTT given inRanta (1994, p. 30).


Clermont

Y Coulier

A Lowe

J-Y Coxam

K Ballerat-Busserolles

Liquid-liquid equilibriums in aqueous solutions of demixing amines loaded with gas for CO 2 capture processes

Liquid-liquid equilibriums in aqueous solutions of demixing amines loaded with gas for CO 2 capture processes

Y Coulier, A Lowe, Jean Yves Coxam, Karine Ballerat-Busserolles

Aqueous solutions of amines are selective carbon dioxide (CO 2 ) absorbents [1,2] . They are used in CO 2 capture processes working on absorption/desorption cycles.

Demixing amines may be valuable for new capture processes [START_REF] Bouillon | IFP.Energies nouvelles[END_REF].

These amines demonstrate a liquid-liquid phase separation [START_REF] Coulier | [END_REF] which can be used to reduce energy costs of desorption (absorbent regeneration).

Aim of this paper : presentation of a method developed in the laboratory to study precisely the LLE in the binary solutions water + amines and the ternary mixtures water+amine+CO 2 , as a function of the pressure and the CO 2 loading charge.

Amines : N-methylpiperidine 2-methylpiperidine

The objective of the project, co-supported by ANR in France and NSERC in Canada, is to analyze the structure-properties relationships for different substituted piperidines.

Results and Conclusions

ANR -NSERC joint program DACOOTA

Thermodynamic properties (enthalpies, heat capacities, volumes, phase equilibriums) are measured in Clermont-Ferrand (France). [6] Speciation in solution using Raman spectroscopy at high temperature and pressure are determined in Guelph (canada).

Modeling using activity coefficient models and molecular simulation will complete the program.

Hastelloy cell : THAR SPM20 Sapphire Cell

a = 0. 2 a

 2 = 0* w 2MP = 20% (x 2MP ~0.05) w 2MP = 40% (x 2MP ~0.1)

-Uncertainties -composition :

-Pressure : ± 0.1 bar , -Temperature : ± 0.3 K Temperatures of liquid-liquid phase separation for solutions of water + N-methylpiperidine (NMP) + CO 2 (figure 1) and for solutions of water + 2-methylpiperidine (2MP) + CO 2 (figure 2) versus composition of the binary mixture water + methylpiperidine at different loading charges a. For 2MP, data at a = 0 are from reference [5] -Good agreement between the two methods -LCST is strongly influenced by the presence of the dissolved gas -N-methylpiperidine cannot be used in a process at high concentration (40%wt) as the CO 2 drastically lowered the LCST; 2-methylpiperidine is a better candidate.

Temperatures of liquid-liquid phase separation for solutions of water + N-methylpiperidine (NMP) + CO 2 (figure 3) and for solutions of water + 2-methylpiperidine (2MP) + CO 2 (figure 4) versus loading charge a at different compositions of the binary mixture water + methylpiperidine. Open symbols : Thar Inst. Cell; full symbol : Sapphire cell