Gian Carlo Cardarilli
email: g.cardarilli@uniroma2.it

Alberto Nannarelli

Marco Re
email: marco.re@uniroma2.it

On the Comparison of Different Number Systems in the Implementation of Complex FIR Filters

Introduction

In modern electronic systems, complex arithmetic computation plays an important role in the implementation of different Digital Signal Processing (DSP) and scientific computation algorithms [START_REF] Oppenheim | Digital Signal Processing[END_REF], [START_REF] Mitra | Handbook for Digital Signal Processing[END_REF]. Most of the interest in complex signal processing is related to the implementation of wireless communication systems based on new concepts and architectures [START_REF] Brodersen | Digital Complex Signal Processing Techniques for Impulse Radio[END_REF]. A very interesting tutorial paper on complex signal processing and its applications has been presented recently in [START_REF] Martin | Complex signal processing is not complex[END_REF]. In [START_REF] Martin | Complex signal processing is not complex[END_REF], the importance of the use of complex signal processing in wireless communications systems has been shown. Regarding communication systems, one of the most critical computation to be implemented in hardware is complex FIR filtering. In fact, FIR filters are generally characterized by a high order (number of taps) to obtain sharp transition bands that, in case of high speed real time computation, require a many resources and have high power dissipation. In particular, for complex FIR filters, the hardware complexity is mostly determined by the number of complex multipliers (i.e. each complex multiplication is actually implemented with four scalar multiplications). Different solutions have been proposed to lower the hardware complexity of the complex multiplication either at algorithmic level (Golub Rule) [START_REF] Moharir | Extending the scope of Golub's method beyond complex multiplication to binary converters[END_REF], or by using different number systems such as the Quadratic Residue Number System (QRNS) [START_REF] Sodestrand | Residue Number System Arithmetic: Modern Applications in Digital Signal Processing[END_REF], [START_REF] Mitra | Handbook for Digital Signal Processing[END_REF] and the Quater-Imaginary Number System (QINS) [START_REF] Knuth | The Art of Computer Programming 2: Seminumerical Algorithms[END_REF].

The aim of this work is to compare in terms of performance, area and power dissipation, the implementations of complex FIR filters based on the traditional Two's Complement System (TCS), the QRNS and the QINS (or radix-2j) implemented in the Redundant Complex Number Systems (RCNS) [START_REF] Aoki | Real/Complex Reconconfigurable Arithmetic using Redundant Complex Number Systems[END_REF].

Previous work was done on both the QRNS ( [START_REF] Sodestrand | Residue Number System Arithmetic: Modern Applications in Digital Signal Processing[END_REF], [START_REF] D'amora | Reducing Power Dissipation in Complex Digital Filters by using the Quadratic Residue Number System[END_REF]) and on the radix-2j and the RCNS ( [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF], [START_REF] Ohi | Redundant Complex Number Systems[END_REF], [START_REF] Aoki | Redundant Complex Number Arithmetic for High-Speed Signal Processing[END_REF]). In this work, we compare for a specific application, the complex FIR filter, the performance and the tradeoffs of TCS, QRNS and RCNS. The results of the implementations show that the complex filter implemented in QRNS has the lowest power dissipation and the smallest area with respect to filters implemented in TCS and RCNS.

The work is organized as follows: in Section II a background on the QRNS and the radix-2j number systems is given; the FIR filter architectures for the three number systems are described in Section III; the synthesis results and the comparisons are discussed in Section IV. Finally, the conclusions are drawn in Section V.

The Quadratic Residue Number System

A Residue Number System (RNS) is defined by a set of P relatively prime integers {m 1 , m 2 , . . . , m P } which identify the RNS base. Its dynamic range is given by the product

M = m 1 • m 2 • . . . • m P .
Any integer X ∈ {0, 1, 2, . . . M -1} has a unique RNS representation given by: X

RN S → ( X m1 , X m2 , . . . , X mP )
where X mi denotes the operation X mod m i [START_REF] Szabo | Residue Arithmetic and its Applications in Computer Technology[END_REF]. Operations on different m i (moduli) are done in parallel

Z = X op Y RN S →        Z m1 = X m1 op Y m1 m1 Z m2 = X m2 op Y m2 m2 . . . . . . . . . Z mP = X mP op Y mP mP (1)
As a consequence, operations on large wordlengths can be split into several modular operations executed in parallel and with reduced wordlength [START_REF] Szabo | Residue Arithmetic and its Applications in Computer Technology[END_REF].

The conversion of the RNS representation of Z can be accomplished by the Chinese Remainder Theorem (CRT):

Z = P i=0 m i • m i -1 mi • Z mi M with m i = M m i (2)
and m i -1 obtained by m i • m i -1 mi = 1. To better explain the CRT, we show an example in which we convert the RNS representation {3, 6, 5}, with RNS base { 5, 7, 8 }, to integer. The dynamic range of the RNS base { 5, 7, 8 } is M = 280. We start by computing the values

m i = M mi m 1 = 280 5 = 56 m 2 = 280 7 = 40 m 3 = 280 8 = 35
To compute m i -1 , we have to find a number x such that

m i • x mi = 1 (3)
For this reason, x is called the multiplicative inverse of m i and indicated as m i -1 . By computer iterations, we find

m 1 -1 = 1 m 2 -1 = 3 m 3 -1 = 3
Finally, applying (2) to the set of residues {3, 6, 5} we get

3 i=1 m i • m i -1 mi • Z i 280 = 56 • 1 • 3 + 40 • 3 • 6 + 35 • 3 • 5 280 = 1413 280 = 13
We can easily verify that 13 5 = 3, 13 7 = 6, 13 8 = 5

In the complex case, we can transform the imaginary term into an integer if the equation q 2 + 1 = 0 has two distinct roots q 1 and q 2 in the ring of integers modulo M (Z M ). A complex number x R + jx I = (x R , x I ) ∈ Z M × Z M , with q root of q 2 + 1 = 0 in Z M , has a unique Quadratic Residue Number System representation given by

(x R , x I ) QRN S → (X i , Xi ) i = 1, 2, . . . , P X i = x R + q • x I mi Xi = x R -q • x I mi (4)
The inverse QRNS transformation is given by

(X i , Xi ) RN S → (X Ri , X Ii ) i = 1, 2, . . . , P X Ri = 2 -1 (X i + Xi ) mi X Ii = 2 -1 • q -1 (X i -Xi ) mi (5)
where 2 -1 and q -1 are the multiplicative inverses of 2 and q, respectively, modulo m i : 2 • 2 -1 mi = 1 and q • q -1 mi = 1 . Then, by applying the CRT we get

(X R1 , X R2 , . . . , X RP ) CRT → x R (X I1 , X I2 , . . . , X IP ) CRT → x I (6)
Moreover, it can be proved that for all the prime integers which satisfy

p = 4k + 1 k ∈ N
the equation q 2 + 1 = 0 has two distinct roots q 1 and q 2 . As a consequence, the product of two complex numbers x R + jx I and y R + jy I is in QRNS

(x R + jx I )(y R + jy I ) QRN S → ( X i Y i mi , Xi Ŷi mi ) ( 7
)
and it is realized by using two integers multiplications instead of four.

We illustrate an example of QRNS multiplication in the ring modulo 13. The complex multiplication to perform is

(x R + jx I )(y R + jy I ) = (3 + j)(2 + j2) = 4 + j8
For m = 13 the root is q = q 1 = 5 ↔ 5 • 5 13 = -1. The conversion to QRNS according to (4) gives

X = 3 + 5 • 1 13 = 8 Y = 2 + 5 • 2 13 = 12 X = 3 -5 • 1 13 = 11 Ŷ = 2 -5 • 2 13 = 5
The two QRNS multiplications (modulus 13) are:

X • Y = 8 • 12 13 = 5 X • Ŷ = 11 • 5 13 = 3
And finally, the conversion QRNS to integer according to [START_REF] Moharir | Extending the scope of Golub's method beyond complex multiplication to binary converters[END_REF] gives

z R = 7(5 + 3) 13 = 4 being 2 -1 = 7 z I = 7 • 8(5 -3) 13 = 8
and q -1 = 8

The Radix-2j Number System

It is well known that an integer x can be represented by a digit-vector

X = (x n-1 , . . . , x 1 , x 0 ) r such that x = n-1 i=0 x i • r i
where r is the radix of the representation. By choosing r = 2j, we obtain a Quater-Imaginary Number System (QINS) [START_REF] Knuth | The Art of Computer Programming 2: Seminumerical Algorithms[END_REF]. Complex numbers can be represented in QINS by vectors with the non-redundant digit set {0, 1, 2, 3}. Therefore, a complex number a + jb is represented in QINS as: Table 1. Representation of real and imaginary integers in QINS.

a + jb = x n-1 (2j) n-1 + x n-2 (2j) n-2 + . . . + +x 3 (-8j) + x 2 (-4) + x 1 (2j) + x 0 (1) = (x n-1 , . . . , x 1 , x 0 ) 2j (8)
The above expression, shows that the real part is represented by the digits of even weight, while the imaginary one by the digits of odd weight. Furthermore, the sign is embedded in the representation. The imaginary number j cannot be represented by [START_REF] Aoki | Real/Complex Reconconfigurable Arithmetic using Redundant Complex Number Systems[END_REF]. To represent j, we need the power -1, which corresponds to -1 2 j, that in the conventional number systems (e.g. binary) is only needed to represent fractional numbers. Table 1 shows how the real and imaginary numbers, in the range [-8, 8] and [-8j, 8j] respectively, are represented in QINS. Every complex number x R + jx I can be obtained by overlapping the real and imaginary parts. For example, according to Table 1, 4 -5j is represented by the digit vector 11320.2.

From Table 1 we can notice that for a given number of digits the representation is not symmetric with respect to the zero. For example, in the two's complement binary system with 8 digits we can represent the dynamic range {-128, 127}. In the QINS, for the real part, with 3 digits (equivalent to 64 different values) the dynamic range representable is {-12, 51}.

Addition

The addition of two QINS numbers can be performed by changing the carry rule according to [START_REF] Aoki | Real/Complex Reconconfigurable Arithmetic using Redundant Complex Number Systems[END_REF]. First, because the even weight digits represent the real part and the odd weight the imaginary one, the carry is propagated by skipping a digit. Second, because two adjacent even (or odd) weight digits have opposite sign, the carry propagated acts as a borrow. For example, if a positive weight digit generates a carry, this positive value will decrement the next digit with negative weight, and vice-versa. In addition, the propagation of borrows can generate negative digits (e.g. -1). Therefore, because of the quaternary representation of the QINS, the negative digits are converted into positive (modulo operation) and an always positive carry propagated. Summarizing the addition algorithm is implemented as:

x i , y i , s i ∈ {0, 1, 2, 3} c i ∈ {1, 0, 1} s i = (x i + y i + c i ) mod 4 c i+2 =    1 if (x i + y i + c i ) ≥ 4 1 if (x i + y i + c i ) < 0 0 otherwise
For example, if we wnat to add x R = 1 and y R = 3 in QINS we get:

X: 0 0 0 0 3. 0 + Y : 0 0 0 0 1. 0 + c: 1 0 1 0 0. 0 = S: 1 0 3 0 0. 0 → s R = 4

The Redundant Complex Number Systems

The implementation of the basic arithmetic operators in radix-2j can take advantage of the Signed-Digit (SD) representation [START_REF] Avizienis | Signed-Digit Number Representations for Fast Parallel Arithmetic[END_REF], which allows carry free addition. The combination of radix-2j and SD representation, resulted in the Redundant Complex Number Systems (RCNS), which is described in [START_REF] Aoki | Real/Complex Reconconfigurable Arithmetic using Redundant Complex Number Systems[END_REF], [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF], [START_REF] Ohi | Redundant Complex Number Systems[END_REF], [START_REF] Aoki | Redundant Complex Number Arithmetic for High-Speed Signal Processing[END_REF] and [START_REF] Nielsen | Borrow-Save Adders for Real and Complex Number Systems[END_REF].

We now briefly recall the characteristics of the RCNS. The RCNS is a redundant positional number system based on the radix rj where its digits can assume the 2α + 1 values: A α = {α, • • • , 1, 0, 1, • • • , α} where α = -α. . In the case of the radix 2j, two possible RCNSs [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF] are:

1. RCNS 2j, 2 with digit set A 2 = {2, 1, 0, 1, 2} 2. RCNS 2j, 3 with digit set A 3 = {3, 2, 1, 0, 1, 2, 3}
In this work, RCNS 2j, 2 is used to recode the multiplier, and RCNS 2j, 3 is used for the signed-digit additions, as illustrated next.

FIR Filter Architecture

A complex FIR filter of order N is expressed by

y(n) = N -1 k=0 a k x(n -k) (9)
Z -1 where x, y and a k denote complex numbers. We consider the implementation of a FIR filter in transposed form because its structure is more regular with respect to the filter order N and it does not require a tree of adders. The filter in transposed form (Fig. 1) can be regarded as the sequence of groups, often referred as taps, composed of:

+ + Z -1 + + Z -1 + + + a 0 a 1 a a n-1 y(t) x(t) n-2
• a complex multiplier;

• a complex adder implemented with one adder for the real part, and one for the imaginary part; • a register to store the real and imaginary parts.

We perform our design space exploration for programmable N-tap complex FIR filters with input and coefficients size of 10 bits for both the real part and imaginary parts. The 20 bit dynamic range of the filter guarantees error free operations3 .

TCS FIR Filter

A single tap of the The programmable N-tap TCS complex FIR filter is realized as sketched in Fig. 2. It is composed of two branches: the real branch (top part of Fig. 2) and the imaginary branch (bottom part of Fig. 2). The real and imaginary products are both realized with two Booth multipliers each, and the resulting partial products are accumulated in a Wallace's tree structure which produces a carry-save (CS) representation of the product at each side of the filter. We chose to keep the product in carry-save (CS) format to speed-up the operation, and delayed the assimilation of the CS representation to the last stage of the filter. In both branches (real and imaginary) of each tap we need to add the CS representation of the product to the value stored in the register (previous tap). Again, to avoid the propagation of the carry, we can store the CS representation. For this reason, we need to implement the addition with an array of 4:2 carry-save adders (CSA), as shown in Fig. 2. We convert the CS representation of y Re and y Im with two carry-propagate adders at the filter output.

CSA 4:2 REG CSA 4:2 CSA 4:2 X X X X REG CSA 4:2 X RE X IM A RE A RE A IM -A IM COMPLEX FILTER TAP CSA 4:2 REG CSA 4:2 CSA 4:2 X X X X REG CSA 4:2 X RE X IM A RE A RE A IM -A IM COMPLEX FILTER TAP

QRNS FIR Filter

The architecture of the QRNS filter, is a direct consequence of (1), ( 7) and [START_REF] D'amora | Reducing Power Dissipation in Complex Digital Filters by using the Quadratic Residue Number System[END_REF], and it can be realized by two RNS filters in parallel as shown in Fig. 3. Each RNS filter is then decomposed into P filters working in parallel, where P is the number of moduli used in the RNS representation. In addition, the RNS filter requires both binary to QRNS and QRNS to binary converters.

In order to have a dynamic range of 20 bits, as required by the specifications, we chose the following set of moduli:

m i = {5, 13, 17, 29, 41} such that log 2 (5 • 13 • 17 • 29 • 41) > 20 .
For each path mod m i , we have to build a FIR filter with a structure similar to that of Fig. 1. Therefore, we need to implement modular multiplication and addition.

Implementation of modular addition

The modular addition a 1 + a 2 m can be implemented by two additions. If the result of a 1 + a 2 exceeds the modulo (it is larger than m -1), we have to subtract the modulo m. In order to speed-up the operation we can execute in parallel the two operations:

(a 1 + a 2 ) and (a 1 + a 2m).

If the sign of the three-term addition is negative, it means than the sum (a 1 + a 2 ) < m and the modular sum is a 1 + a 2 , otherwise the modular ad-

n w q w m = n 0 N/A 1 0 2 0 5 = 1 2 1 2 1 5 = 2 3 3 2 3 5 = 3 4 2 2 2 5 = 4 Table 2. Example of isomorphic transformation for m = 5 (q = 2).
dition is the result of the three-term addition. The above algorithm can be implemented with two binary adders as shown in Fig. 4.

Implementation of modular multiplication by isomorphism

Because of the complexity of modular multiplication, it is convenient to implement the product of residues by the isomorphism technique [START_REF] Vinogradov | An Introduction to the Theory of Numbers[END_REF] . By using isomorphisms, the product of the two residues is transformed into the sum of their indices which are obtained by an isomorphic transformation. According to [START_REF] Vinogradov | An Introduction to the Theory of Numbers[END_REF], if m is prime there exists a primitive radix q such that its powers modulo m cover the set [1, m -1]:

n = q w m with n ∈ [1, m -1] and w ∈ [0, m -2].
An example of isomorphic transformation is shown in Table 2 for m = 5. In this case, the primitive radix is q = 2.

Both transformations n → w and w → n can be implemented with m -1 entries look-up tables, if the moduli are not too large (less than 8-bit wide). Therefore, the product of a 1 and a 2 modulo m can be obtained as:

a 1 • a 2 m = q w m where w = w 1 + w 2 m-1
with a 1 = q w1 m and a 2 = q w2 m In order to implement the modular multiplication the following operations are performed:

1) Two Direct Isomorphic Transformations (DIT) to obtain w 1 and w 2 ;

2) One modulo m -1 addition w 1 + w 2 m-1 ;

3) One Inverse Isomorphic Transformations (IIT) to obtain the product.

The architecture of the isomorphic multiplier is shown in Fig. 5. Special attention has to be paid when one of the two operands is zero. In this case there exists no isomorphic correspondence and the modular adder has to be bypassed. For example, for the modular multiplication 3 • 4 5 = 2 using the isomorphic transformation of Table 2, we have

1) 3 = 2 3 5 DIT → w 1 = 3 4 = 2 2 5 DIT → w 2 = 2 2) 2 + 3 4 = 1 3) 1 IIT → 2 1 5 = 2
Implementation of FIR filter modulo m By using the isomorphism technique, the product of the two residues is transformed into the sum of their indices which are obtained by an isomorphic transformation. As a result, in each tap, the modular multiplication is reduced to a modular addition followed by an access to table (inverse isomorphism).

The two input DIT tables of Fig. 5 do not need to be replicated in every tap. By observing that in computing the product A k X(nk) the term X is common to all taps and it can be converted once in the input conversion unit, and that the term A k can be stored directly as the index of the isomorphism. Therefore, the structure of each modular tap can be simplified as shown in Fig. 6.

Radix-2j Filter (RCNS)

Because of the radix-2j representation, the filter tap is simply implemented with a multiplier and an adder. We implement the multiplier as described in [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF]. The complex x and a k are converted in non-redundant QINS and then a k is recoded into RCNS 2j, 2. The partial products (PPs) are then accumulated by a tree of arrays of signed-digit full-adders (SDFA) which operates in RCNS 2j, 3.

In RCNS 2j, 3, the complex number

X = (X n-1 , . . . , X i , . . . , X 1 , X 0 , X -1 )
has digits in the set X i = {3, 2, 1, 0, 1, 2, 3}, which encoded in binary as Both x 1 i and x 0 i are then encoded with two bits each as shown in Table 3. Therefore, the resulting binary encoding of X i is illustrated in Table 4. For bits are necessary to represent each RCNS 2j, 3 digit. With the encoding of Table 4 the SDFA of Fig. 7 can be derived.

X i = 2x 1 i + x 0 i with x 1 i , x 0 i ∈ {1, 0, 1} (10)
x 1 i x P 1 i x M 1 i x 0 i x P 0 i x M 0 i 1 0 1 1 0 1 0 0 0 0 0 0 0 1 1 0 1 1 1 1 0 1 1 0
Table 3. Binary encoding of x 1 i and x 0 i .

By arranging the SDFAs in a tree the 10 PPs are reduced to 2 as shown in Fig. 8. An extra array of SDFAs adds the product x • a k to the partial sum coming from the previous tap. As for the TCS case, we keep the carry-save representation of the digits until the last stage of the filter where we perform the conversion from RCNS 2j, 3 to radix-2 (binary) integers. Due to the CS representation of digits we need to store 8N bits in the tap's registers.

Filters Implementation

The filters are implemented in the 90 nm STM library of standard cells [START_REF]CMOS090 Design Platform[END_REF] and they have been synthesized by Synopsys Design Compiler. All the filters Xi can be clocked at f max = 300 M Hz. By interpolating the results obtained by synthesis on filters of different order (number of taps), we obtain the trends shown in Fig. 9 for the area and Fig. 10 for the power. The values of area and power dissipation for the single tap (Fig. 2, Fig. 6 and Fig. 8) determine the slopes of the curves in the figures. The conversions from the TCS to the other number systems (and vice versa) are a constant contribution that does not depend on the number of taps, but only on the dynamic range of the filters. Table 5 reports the data for tap and conversion contribution for the three number systems.

x 1 i x 0 i x P 1 i x M 1 i x P 0 i x M 0 i 0 Table 4. Binary encoding of Xi. Booth's Recoding & PP Generator REG SDFA x(n) A k N N 8N 8N Booth's Recoding & PP Generator REG SDFA x(n) A k N N 8N 8N
The results show that complex filters implemented in QRNS consume significantly less power than the corresponding ones in TCS and RCNS. The expression for the power dissipated dynamically [START_REF] Weste | Principles of CMOS VLSI Design[END_REF] in a system composed of n cells is

P dyn = V 2 DD f • n i=1 C Li a i (11)
where V DD is the power supply voltage; f is the clock frequency; C Li is the load connected to the i-th cell (both active load and interconnections); a i is the activity factor of the i-th cell, which is the measure of how many transitions occur at its output. The activity factor is normally related to the clock a i ∈ [0, 1].

The lower power dissipation in the QRNS filter is due to the combination of two factors:

1. As clearly shown in Fig. 9, the smaller area results in a global reduced capacitance n i=1 C Li (including shorter interconnections). 2. The work in [START_REF] Stouraitis | Considering the alternatives in low-power design[END_REF] showed that the number of transitions, i.e. the switching activity, for vectors of the same number of bits k, in RNS is lower than in TCS Therefore, the switched capacitance n i=1 C Li a i , and by ( 11) the power consumption, in QRNS is smaller than in TCS and RCNS.

Conclusions

In this work, the use of different number representations for the implementation of complex FIR filters has been investigated.

Complex multipliers determine the performance, area and power dissipation of complex filters. Previously in [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF], complex multipliers in TCS and RCNS were evaluated, while in [START_REF] D'amora | Reducing Power Dissipation in Complex Digital Filters by using the Quadratic Residue Number System[END_REF], complex filters in QRNS and TCS were compared. Here we extended the comparison to complex filters implemented in TCS, QRNS and RCNS.

The experimental results on complex filters with 20 bit dynamic range show that for the TCS and the RCNS the area and power dissipation are similar and confirms the findings of [START_REF] Aoki | Reduntant Complex Arithmetic and its Application to Complex Multiplier Design[END_REF]. As for the QRNS, the results presented here, confirm those of [START_REF] D'amora | Reducing Power Dissipation in Complex Digital Filters by using the Quadratic Residue Number System[END_REF], based on the implementation of TCS and QRNS complex filters in a 0.35 µm technology.

To summarize, this work shows that for complex high order FIR filters implementations based on QRNS offer significant advantages in area and power dissipation without any performance degradation.

Fig. 1 .

 1 Fig. 1. Structure of FIR filter in transposed form.

Fig. 2 .

 2 Fig. 2. Structure of tap in TCS complex FIR filter.

Fig. 3 .

 3 Fig. 3. QRNS FIR Filter architecture

Fig. 4 .

 4 Fig. 4. Architecture of the modular adder.

Fig. 6 .

 6 Fig. 6. Structure of RNS tap for filter in transposed form.

Fig. 7 .

 7 Fig. 7. Implementation of SD full-adder (SDFA).

Fig. 8 .

 8 Fig. 8. Structure of RCNS tap.

  Fig. 9. Trends in area for increasing N.

Fig. 10 .

 10 Fig. 10. Trends in power dissipation (at 100 MHz) for increasing N.

Table DIT Table a

 DITa

	1	a 2
	Fig. 5. Structure of isomorphic multiplication.

Table 5 .

 5 Trends in area for increasing N. Values of area and power dissipation.

		Area	P at 100 MHz
		tap conv. tap	conv.
	TCS	21.8K	2.0K 1.00	0.10
	QRNS 9.6K 12.0K 0.25	1.20
	RCNS 23.9K	8.0K 1.05	0.30
		[µm 2 ]	[mW ]

These wordlengths are derived from the specification of an actual digital filter for satellite TV broadcasting.


Yves Martinez-Maure
email: yves.martinez-maure@imj-prg.fr

Plane Lorentzian and Fuchsian hedgehogs

Keywords: 2010 MSC: 52A40, 52A55, 53A04, 53B30; Fuchsian and Lorentzian hedgehogs, evolute, duality, convolution, reversed isoperimetric inequality, reversed Bonnesen inequality

Introduction

Our main results consist in the Fuchsian analogues of some classical geometrical inequalities. These new results will be presented in Subsection 1.3. For the convenience of the reader, we begin by recalling brie ‡y some de…nitions and results concerning plane Euclidean hedgehogs in Subsection 1.1. Finally, Subsection 1.2 is devoted to a short introduction of plane Lorentzian hedgehogs and …rst results concerning evolutes and duality in the Lorentz-Minkowski plane L 2 .

Plane Euclidean hedgehogs

In the Euclidean plane R 2 , a hedgehog is the envelope of a family of cooriented lines L ( ) parametrized by the oriented angle 2 S 1 ' R=2 Z from e 1 = (1; 0) to their coorienting normal vector u ( ) = (cos; sin ). These cooriented lines L ( ) have equations

hx; u ( )i = h ( ) , (1)
where h:; :i is the usual inner product on R 2 and where h 2 C 1 (S 1 ; R). Partial di¤erentiation of (1) yields hx; u 0 ( )i = h 0 ( ) :

(2)

From (1) and (2), the parametrization of the corresponding hedgehog is

x h : S 1 ! R 2 , 7 ! h ( ) u ( ) + h 0 ( ) u 0 ( ) .
This envelope H h := x h (S 1 ) is called the (Euclidean) hedgehog with support function h. If h is only C 1 then H h may be a fractal curve [Y1].

In this paper, we shall be mainly interested in C 2 -hedgehogs, that is, hedgehogs with a C 2 -support function. Note that regular C 2 -hedgehogs of R 2 are strictly convex smooth curves and that C 2 -hedgehogs can be regarded as the Minkowski di¤erences of two such convex curves [Y6]. H. Geppert was the …rst to introduce hedgehogs in R 2 and R 3 (under the German names stützbare Bereiche in R 2 and stützbare Flächen R 3 ) in an attempt to extend certain parts of the Brunn-Minkowski theory [G]. Many classical inequalities for convex curves …nd their counterparts in the setting of hedgehogs. Of course, a few adaptations are necessary. In particular, lengths and areas have to be replaced by their algebraic versions. For instance, Theorem 1 extends the classical isoperimetric inequality and gives an upper bound of the isoperimetric de…cit in terms of signed area of the evolute.

Theorem 1 ( [START_REF] Martinez-Maure | De nouvelles inégalités géométriques pour les hérissons[END_REF]Prop. 6]). For any h 2 C 3 (S 1 ; R) , we have:

0 l(h) 2 4 a(h) 4 a(h 0 ), (3)
where l (h) and a (h) are respectively the signed length and area of H h and where a(h 0 ) is the area of its evolute. In each inequality of (3), the equality holds if, and only if, H h is a circle.

For a recent study of hedgehogs in the Euclidean plane, we refer the reader to [Y6].

Plane Lorentzian hedgehogs

In this paper, we shall undertake a similar study replacing the Euclidean plane R 2 by the Lorentzian plane L 2 and the unit circle S 1 of R 2 by the hyperbolic line H 1 . In the Lorentzian plane L 2 , a spacelike hedgehog is similarly de…ned to be the envelope of a family of cooriented spacelike lines L (t) parametrized by the oriented hyperbolic angle t 2 H 1 ' R from e 2 = (0; 1) to their coorienting normal vector v (t) = (sinh t; cosh t), (see Section 2). These cooriented lines L (t) have equations

hx; v (t)i L := h (t) , (4)
where hx; yi L := x 1 y 1 x 2 y 2 is the Lorentzian inner product of the vectors x = (x 1 ; x 2 ) and y = (y 1 ; y 2 ) in L 2 , and where h 2 C 1 (R; R). Note that h (t) is the signed distance from the origin to the support line with coorienting unit normal v (t). Partial di¤erentiation of (4) yields hx; v 0 (t)i L := h 0 (t) .

(5)

From (4) and (5), the parametrization of the corresponding hedgehog is

x h : H 1 ! L 2 , t 7 ! h 0 (t) v 0 (t) h (t) v (t) .
This envelope

S h := x h (H 1 ) is called the spacelike hedgehog of L 2 with support function h 2 C 1 (H 1 ; R).
As in the Euclidean case, we shall generally restrict to C 2 -hedgehogs (i.e., with a C 2 -support function). In Section 3, we shall give a study of their evolutes. In particular, we shall prove the following.

Theorem. For any h 2 C 3 (R; R), the second evolute of S h is the spacelike hedgehog with support function h 00 :

D (D (S h )) = S h 00 ,
where D (C) denotes the evolute of a curve C L 2 with no in ‡exion or lightlike point:

In Section 3, we shall also introduce timemike hedgehogs of L 2 and, in Section 4, we shall show that there is a duality relationship between spacelike hedgehogs and timelike hedgehogs.

Plane Fuchsian hedgehogs

Of course, a spacelike hedgehog S h L 2 has no reason to be a compact curve. So, in order to develop a Brunn-Minkowski theory, we are going to replace H 1 by its quotient by a Fuchsian group : In other words: (i) we identify

SO (1; 1) = M = x 2 x 1 x 1 x 2 2 M 2 (R) x 2 2 x 2 1 = 1
with the hyperbola

H = (x 1 ; x 2 ) 2 L 2 x 2 2
x 2 1 = 1 ; (ii) we take the subgroup of SO (1; 1) generated by (sinh T; cosh T ) 2 H 1 = f(x 1 ; x 2 ) 2 H jx 2 > 0 g for some T 2 R + ; and (iii) we replace H 1 by H 1 = ' R=T Z. In practice, any h 2 C 1 (H 1 = ; R) will be regarded as a T -periodic funtion h : R 7 ! R of class C 1 . The -hedgehog with support function h 2 C 1 (H 1 = ; R) is then de…ned to be the curve h parametrized by h : R ! L 2 , t 7 ! h 0 (t) v 0 (t) h (t) v (t) . Note that, for any t 2 R, we have h (t + T ) = g (T ) [ h (t)], where g (T ) denotes the linear isometry of L 2 whose matrix in the canonical basis is

cosh T sinh T sinh T cosh T . For every h 2 C 2 (H 1 = ; R), the C 1 -curve h : [0; T ] ! L 2 = , t 7 ! h 0 (t) v 0 (t) h (t) v (t)
is recti…able and its length is given by

L (h) := Z T 0 kx 0 h (t)k L dt,
where kxk L := p jhx; xij L for all x 2 L 2 . Note that x 0 h = R h v 0 , where R h := h 00 h is the so-called curvature function of h . Therefore

L (h) := Z T 0 jR h (t)j dt:
If in this last integral we remove the absolute value to take into account the sign of the curvature function of h , we obtain the so-called algebraic (or signed) length of h , which is thus given by l (h) :=

Z T 0 R h (t) dt = Z T 0 h (t) dt.
Given any h 2 C 2 (H 1 = ; R), let h be the oriented closed curve of L 2 consisting of the oriented line segment joining the origin to h (0), followed by the oriented curve h and …nally the oriented line segment joining h (T ) to the origin. Denote by ( h ) the curve obtained from h by taking the opposite orientation (see Figure 1). De…ne the algebraic (or signed) area of the -hedgehog h to be the algebraic area bounded by ( h ) that is,

a (h) := Z L 2 i h (x) d (x),
where the Lebesgue measure; i h (x) the winding number of x with respect to ( h ) for x 2 L 2 ( h ) , and i h (x) = 0 for x 2 ( h ) . An easy straightforward calculation gives

a (h) = 1 2 Z ( h ) x 1 dx 2 x 2 dx 1 = 1 2 Z T 0 h (t) R h (t) dt = 1 2 Z T 0 h 2 + (h 0 ) 2 (t) dt. h T h 0 h 0 x 1 x 2 Figure 1. The oriented closed curve ( h ) when h (t) := 1 + cos (2 t)
In the Fuchsian case, many geometric inequalities will be reversed. A …rst example is given by the following obvious result.

Proposition. The map p a : C 2 (H 1 = ; R) ! R + ; h 7 ! p a(h) is a norm associated with a scalar product (h; k) 7 ! a (h; k). In particular, for any (h; k) 2 C 2 (H 1 = ; R) 2 , we have p a(h + k) p a(h) + p a(k) (6) and a(h; k) 2 a(h) a(k); (7)
with equalities if, and only if, h and k are homothetic (here,"homothetic" means that there exists ( ;

) 2 R 2 f(0; 0)g such that h + k = 0).
Indeed, Inequality (6) (resp. ( 7)) has to be compared with the Brunn-Minkowski inequality (resp. Minkowski inequality) in R 2 (e.g., see [S, Section 7]): for any pair (H; K) of convex bodies of R 2 , we have

p a(H + K) p a(H) + p a(K) (8) and a(H; K) 2 a(H) a(K); (9)
where a(L) (resp. a(H; K)) is the area (resp. the mixed area) of L (resp. (H; K)). By taking k = 1 (that is, k = H 1 ) in (7), we obtain the following reversed isoperimetric inequality

a (h) l (h) 2 2T , ( 10
)
with equality if, and only if, h and H 1 are homothetic (that is, h is constant). In Section 6, we shall prove an other reversed geometric inequality given by the following analogous of Theorem 1 for Fuchsian hedgehogs.

Theorem 2. Let T 2 ]0; 2 ]. For any T -periodic function h : R ! R of class C 3 , we have:

0 2T a(h) l(h) 2 2T a (h 0 ) , ( 11
)
where l (h) and a (h) are respectively the signed length and area of h and a(h 0 ) the area of its evolute.

Note that 2T a(h) l(h) 2 provides a measure of how far h deviates from a -hedgehog given by a spacelike branch of a hyperbola. A lower bound of the isoperimetric excess a(h) l(h) 2 =2T is given by the following reversed Bonnesen inequality, which we shall prove in Section 7.

Theorem 3 (Reversed Bonnesen inequality). For any T -periodic function h : R ! R of class C 2 , we have:

1 2T (R r) 2 a (h) l (h) 2 2T ,
where l (h) and a (h) are respectively the signed length and area of h and where r := min

0 t T ( h (t)) and R := max 0 t T ( h (t))
. Furthermore, the equality holds if and only if R = r.

Recall that Bonnesen's sharpening of the isoperimetric inequality for a convex body K with non-empty interior in R 2 reads as follows:

L 2 4 A 2 (R r) 2 ,
where L and A are respectively the perimeter and the area of K and where r and R stand respectively for the inradius and the circumradius of K (e.g., see [E, pp. 108-110]).

Acknowledgement. I would like to thank F. Fillastre for sending me a preliminary version of his paper [F]. It did not contain any notion of hedgehog but I immediately understood that existence of Fuchsian hedgehogs was a direct by-product of Fillastre's work and I made him the remark in an e-mail dated 2011-11-17. I would like also thank F. Fillastre for stimulative conversations during the preparation of this paper.

Preliminaries

The Lorentzian plane L 2 is the vector space R 2 endowed with the pseudoscalar product hx; yi L := x 1 y 1 x 2 y 2 , for any x = (x 1 ; x 2 ) and y = (y 1 ; y 2 ). For any x 2 L 2 , de…ne the norm of x by kxk L = p jhx; xi L j and the sign of x by " (x) = sgn (hx; xi L ), where sgn denotes the sign function: sgn (t) is 1, 0, or 1 if t is positive, zero, or negative, respectively. A nonzero vector x 2 L 2 is said to be spacelike if " (x) = 1, lightlike if " (x) = 0 and timelike if " (x) = 1. Let e 2 = (0; 1). A timelike vector x = (x 1 ; x 2 ) 2 L 2 is said to be a future vector if hx; e 2 i L < 0, that is, if x 2 > 0. We shall denote by F the set of all future timelike vectors:

F = x = (x 1 ; x 2 ) 2 L 2 jhx; xi L < 0 and x 2 > 0 .
The hyperbolic line H 1 is the set of all unit future timelike vectors:

H 1 := x = (x 1 ; x 2 ) 2 L 2 jhx; xi L = 1 and x 2 > 0 .
In other words, H 1 is the upper branch of the hyperbola x 2 2 = x 2 1 + 1. It will play in L 2 the same role as the one the unit circle S 1 plays in the Euclidean plane R 2 . For any t 2 R, let g (t) be the linear isometry of the Lorentzian plane whose matrix in the canonical basis of R 2 is cosh t sinh t sinh t cosh t These isometries g (t) constitute the group G of hyperbolic translations of L 2 . Note that G is an abelian subgroup of O (1; 1) and that g : R ! G, t 7 ! g (t) is a group isomorphism: g (s + t) = g (s) g (t) for all s; t 2 R. The hyperbolic line H 1 can be regarded as the orbit of e 2 under the action of G. Any v (t) = (sinh t; cosh t) 2 H 1 is identi…ed with the unique t 2 R such that g (t) (e 2 ) = v (t). For any x; y 2 H 1 , the oriented hyperbolic angle from x to y is the unique t such that g (t) (x) = y:

A (smooth) curve of L 2 is a di¤erentiable map c : I R ! L 2
, where I is an open interval. A curve c : I ! L 2 is said to be regular at t if c 0 (t) 6 = 0. The curve is said to be regular if it is regular at every t 2 I. A curve c : I ! L 2 is said to be spacelike (resp. lightlike, timelike) at t if c 0 (t) is a spacelike (resp. null or lightlike, timelike) vector. The curve is said to be spacelike (resp. timelike) if it is spacelike (resp. timelike) at every t 2 I.

Let be the anti-isometric involutive operator of L 2 that is given by (x 1 ; x 2 ) = (x 2 ; x 1 ) for all (x 1 ; x 2 ) 2 L 2 . For any nonzero vector x of L 2 , let x ? := " (x) (x). Note that, for any x 2 L 2 f(0; 0)g, x; x ? is a positively oriented basis of L 2 endowed with the orientation of the canonical basis of R 2 .

Let c : I ! L 2 be a spacelike (resp. timelike) curve of class C 2 . At any point of c : I ! L 2 , we can de…ne the oriented Frenet frame (T (t) ; N (t)) consisting of Frenet vectors

T (t) := c 0 (t) kc 0 (t)k L
and N (t) := T (t) ? .

If c : I ! L 2 is parametrized by the pseudo arc length s (that is, if kc 0 (s)k L = 1 for all s 2 I), then the algebraic curvature of c is de…ned to be the function such that T 0 (s) = (s) N (s). If it is not the case, a straightforward computation using the fact that ds=dt = kc 0 (t)k L shows that the algebraic curvature is given by

(t) := hc 0 (t) ; (c 00 (t))i L kc 0 (t)k 3 L . If c : I ! L 2 is a spacelike hedgehog x h : H 1 ! L 2 with support function h 2 C 3 (R; R), then c 0 = x 0 h = R h v 0
, where R h := h 00 h is the so-called curvature function of S h . In this case, we hence obtain

T = sgn (R h ) v 0 , N = sgn (R h ) v and (t) = 1 jR h j . 3 Evolute 3.1 Evolute of a spacelike hedgehog S h of L 2
In this subsection, h will denote any C 3 -function from R to R. As in the Euclidean case, the evolute of the spacelike hedgehog S h can be de…ned in two di¤erent but equivalent ways: as an envelope or as a locus.

Evolute of S h as the envelope of its normal lines

For every t 2 R, the support line L h (t), with coorienting unit normal vector v (t) := (sinh t; cosh t), has equation hx; v (t)i L := h 0 (t) .

(5)

Let N h (t) be the line through x that is orthogonal to L h (t) in L 2 . We shall say that N h (t) is a normal line to H h at x h (t). This normal line N h (t) has equation hx; v (t)i L := h 00 (t) .

De…ne the evolute D (S h ) of the spacelike hedgehog S h L 2 to be the envelope of the family (N h (t)) t2R of its normal lines. This evolute D (S h ) is thus the curve of L 2 parametrized by c h : R ! L 2 ; t 7 ! c h (t) , where c h (t) is the unique solution of the system hx; v (t)i L := h 0 (t) hx; v (t)i L := h 00 (t) , that is, c h (t) = h 0 (t) v 0 (t) h 00 (t) v (t).

Evolute of S h as the locus of its centers of curvature

The evolute D (S h ) of the spacelike hedgehog S h L 2 can also be de…ned as the locus of all its centers of curvature. First note that

x 0 h (t) = R h (t) v 0 (t) , for all t 2 H 1 ' R. Since S h := x h (H 1
) is an envelope parametrized by its coorienting unit normal vector …eld, the center of curvature of S h at x h (t) is de…ned to be

c h (t) := x h (t) R h (t) v (t) , that is c h (t) = h 0 (t) v 0 (t) h 00 (t) v (t) , for all t 2 H 1 ' R. Of course, if x h is regular at t then c h (t) = x h (t) N (t) (t) , but the center of curvature c h (t) is well-de…ned even if x 0 h (t) = 0.
3.2 Timelike hedgehogs of L 2 and their evolutes

De…nitions

We can also de…ne timelike hedgehogs of L 2 . The timelike hedgehog with support function h 2 C 1 (R; R) is de…ned to be the envelope T h of the family (L 0 h (t)) t2R of cooriented timelike lines with equation

hx; v 0 (t)i L := h (t) , (7)
v 0 (t) = (cosh t; sinh t) being the unit coorienting normal vector of L 0 h (t). Partial di¤erentiation of (7) yields hx; v (t)i L := h 0 (t) . ( 8) From ( 7) and ( 8), the parametrization of the timelike hedgehog T h is

y h : R ! L 2 , t 7 ! h (t) v 0 (t) h 0 (t) v (t) .
Note that for every t 2 R, we have

y 0 h (t) = R h (t) v (t) . The evolute D (T h ) of a timelike hedgehog T h
L 2 is de…ned to be the envelope of the family of its normal lines (i.e., the envelope of the family of lines with equation hx; v (t)i L := h 0 (t)) or, equivalently, the locus of its centers of curvature

d h (t) := y h (t) ( R h (t) v 0 (t)) = h 00 (t) v 0 (t) h 0 (t) v (t) , (t 2 R).

Relationship between S

h = x h (R) and T h = y h (R)

Let

be the anti-isometric involutive operator of L 2 that is given by

(x) = (x) for all x 2 L 2 . Note that v = v 0 and v 0 = v.
Proposition. For any h 2 C 1 (R; R), the spacelike hedgehog S h and the timelike hedgehog T h are related by

T h = (S h ) and S h = (T h ) .
Proof. Indeed, their respective parametrizations x h := h 0 v 0 hv and y h := hv 0 h 0 v are such that y h = x h and x h = y h .

Second evolute

Proposition. For any h 2 C 2 (R; R), the evolute of the spacelike hedgehog S h (resp. of the timelike hedgehog T h ) can be given by

D (S h ) = (S h 0 ) (resp. D (T h ) = (T h 0 ))
and hence by

D (S h ) = T h 0 (resp. D (T h ) = S h 0 )
from the previous proposition.

Proof. Indeed, c h := h 0 v 0 h 00 v (resp.

d h := h 00 v 0 h 0 v) satis…es c h = h 0 v + h 00 v 0 = x h 0 (resp. d h = h 00 v + h 0 v 0 = y h 0 ) and hence c h = x h 0 (resp. d h = y h 0 ).
See Figure 2 for an illustration.

Figure 2. S h and its evolute T h 0 if h (t) := cosh(2t)

A straightforward consequence is the following.

Corollary. For any h 2 C 3 (R; R), the second evolute of the spacelike hedgehog S h (resp. of the timelike hedgehog T h ) is simply the spacelike (resp. timelike hedgehog) with support function h 00 :

D 2 (S h ) := D (D (S h )) = S h 00 resp. D 2 (T h ) = D (D (T h )) = T h 00 .

Duality

Let c : I R ! L 2 be a spacelike or timelike curve of L 2 and let p c : I ! L 2 be its pedal curve: for any t 2 I, p c (t) is the foot of the perpendicular from the origin to the tangent line to c at c (t). Note that, replacing tangent lines by support lines, we can de…ne the pedal curve of a spacelike (resp. timelike) hedgehog even if x h (resp. y h ) is not regular. Assume that kc (t)k L : kp c (t)k L 6 = 0 for all t 2 I. De…ne the star curve of c to be the curve c : I R ! L 2 given by c := i p C , where i (x) := " (x)

x kxk 2 L for all x 2 L 2 such that kxk L 6 = 0, (recall that " (x) := sgn (hx; xi L )). If c : R ! L 2 is a spacelike hedgehog x h (resp. a timelike hedgehog y h ), then p c = hv (resp. p c = hv 0 ) and, assuming that h: kx h k L 6 = 0 (resp. h: ky h k L 6 = 0), we can de…ne its star curve in the same way.

Proposition. If c : R ! L 2 is a spacelike hedgehog x h (resp. a timelike hedgehog y h ), then (c ) = c.

Proof. If c = x h (resp. c = y h ), then p c = hv (resp. p c = hv 0 ). Thus x h = v h resp. y h = v 0 h .

Di¤erentiation gives

(x h ) 0 = y h h 2 resp. (y h ) 0 = x h h 2 . Now x h = h 0 y h hx h h h 2 (h 0 ) 2 resp. y h = hy h h 0 x h h h 2 (h 0 ) 2 ! . Therefore p x h = x h (h 0 ) 2 h 2 resp. p y h = y h h 2 (h 0 ) 2 ,
and hence

(x h ) = x h (resp. (y h ) = y h ) . De…nition. For any h 2 C 1 (R; R) such that h (t) : kx h (t)k L 6 = 0 (resp. h (t) : ky h (t)k L 6 = 0) for all t 2 R, we shall say that S h := x h (R) (resp. T h := y h (R))
is the dual curve of the spacelike (resp. timelike) hedgehog S h (resp. T h ).

Convolution

Di¤erences of convex bodies of the Euclidean plane R 2 do not only constitute a real vector space (H 2 ; +; :) but also a commutative and associative R-algebra. Indeed, as noticed by H. Görtler [G1, G2], we can de…ne the convolution product of two hedgehogs H f and H g of R 2 as the hedgehog whose support function is given by

(f g) ( ) = 1 2 Z 2 0 f ( ) g ( ) d ,
for all 2 S 1 ' R=2 Z and we can check at once that (H 2 ; +; :; ) is then a commutative and associative algebra. The interest is, of course, that the convolution product of two Euclidean hedgehogs inherits many properties of the factors [START_REF] Martinez-Maure | Geometric study of Minkowski di¤erences of plane convex bodies[END_REF]Section 6]. In particular, H. Görtler noticed that the convolution product of two plane convex bodies is still a plane convex body. The purpose of the present section is to give a similar result for Fuchsian hedgehogs.

Let h 2 C 2 (H 1 ; R). Recall that, for all t 2 H 1 ' R, we have:

x 0 h (t) = R h (t) v 0 (t)
, where R h := h 00 h. Therefore, the spacelike hedgehog S h = x h (H 1 ) is a regular curve if, and only if, its curvature function R h is everywhere nonzero. In that case, S h will be said to be convex.

De…nition. Let h 2 C 2 (H 1 ; R). The spacelike hedgehog S h is said to be convex if its curvature function R h := h 00 h is everywhere nonzero on H 1 . It is said to be future convex (resp. past convex) if its curvature function is everywhere positive (resp. negative) on H 1 .

De…nition. Let h 2 C 2 (H 1 = ; R). The -hedgehog h is said to be a - hedgehog of class C 2 + of F = fx = (x 1 ; x 2 ) 2 L 2 jhx; xi L < 0 and x 2 > 0 g if h < 0 and R h > 0:
Remark. A -hedgehog of class C 2 + of F can indi¤erently be regarded as a convex curve of F or as a convex closed curve of F= .

De…nition. Let f and g be -hedgehogs whose respective support functions f and g are in C 1 (H 1 = ; R). The convolution of f and g is the -hedgehog f g whose support function is de…ned by

(f g) (t) = Z T 0 f (t s) g (s) ds for all t 2 [0; T ] .
The operation of convolution of -hedgehogs is of course commutative, associative and distributive over addition. Here is an analogous result of Görtler's theorem.

Proposition. Let f and g be -hedgehogs whose respective support functions f and g are in

C 2 (H 1 = ; R). If f is a -hedgehog of class C 2 + of F and if g is negative, then f g is a -hedgehog of class C 2 + of F .
Proof. If f < 0, g < 0 and R h > 0, then (f g) < 0 and R f g > 0.

Indeed, the …rst inequality is trivial and

R f g (t) = (f g) 00 (t) (f g) (t) = (f g 00 ) (t) (f g) (t) = (f (g 00 g)) (t) = (f R g ) (t) = R T 0 f (t s) R g (s) ds is positive for all t 2 [0; T ] since f < 0 and R g > 0.
6 Isometric excess and area of the evolute

Let us prove the following analogous of Theorem 1 for Fuchsian hedgehogs.

Theorem 2. Let T 2 ]0; 2 ]. For any T -periodic function h : R ! R of class C 3 , we have:

0 2T a(h) l(h) 2 2T a (h 0 ) ,
where l (h) and a (h) are respectively the signed length and area of h and a(h 0 ) the area of its evolute.

Proof. The …rst inequality is simply the isoperimetric inequality (10).

Let us prove the second one. First note that:

a (h) a (h 0 ) = 1 2 Z T 0 h 2 dt Z T 0 (h 00 ) 2 dt .
Let a n (f ) and b n (f ) denote the Fourier coe¢cients of a T -periodic differentiable function f : R ! R:

a 0 (f ) := 1 T Z T 0 f (t) dt, a n (f ) := 2 T Z T 0 f (t) cos n!t dt and b n (f ) := 2 T Z T 0 f (t) sin n!t dt
where ! := 2 =T and n 2 N . Recall that a n (h 00 ) = (n!) 2 a n (h) and b n (h 00 ) = (n!) 2 b n (h) for all n 2 N . By applying the Parseval equality, we thus obtain

1 2 Z T 0 h 2 (h 00 ) 2 (t) dt = T 2 a 0 (h) 2 + T 4 +1 X n=1 1 (n!) 4 a n (h) 2 + b n (h) 2 .
Since the sum in the right-hand side is obviously nonpositive, we deduce that 1 2

Z T 0 h 2 (h 00 ) 2 (t) dt T 2 a 0 (h) 2 = l (h) 2 2T . Therefore a (h) l (h) 2 2T a (h 0 ) ,
which achieves the proof.

Remarks. 1. For T 2 ]0; 2 [, the equality 2T a(h) l(h) 2 = 2T a (h 0 ) holds if, and only if, h is constant.

2. For T = 2 , the equality 2T a(h) l(h) 2 = 2T a (h 0 ) may hold for nonconstant h 2 C 3 (H 1 = ; R). Consider for instance h (t) := cos t.

3.

The assumption T 2 ]0; 2 ] is necessary even if we restrict tohedgehogs that are -hedgehogs of class C 2 + of F . Consider for instance h (t) := 2 + cos 2 7 t , which is such that h < 0 and R h > 0.

Reversed Bonnesen inequality

Let K be a convex body with non-empty interior in R 2 . In the 1920s, T. Bonnesen gave various sharpening of the classical isoperimetric inequality

A L 2 4 ,
where L and A denote respectively the perimeter and the area of K.

In particular, he proved the inequality

L 2 4 A 2 (R r) 2 , ( 12
)
where r and R are respectively the inradius and the circumradius of K (i.e., the radii of the largest inscribed and the smallest circumscribed circles of the boundary of K, respectively). He further proved that the equality holds in (12) if and only if R = r, i.e., if K is a disc. The proof by Bonnesen is reproduced in [E, pp. 108-110]. For a survey of Bonnesentype inequalities in Euclidean spaces, we refer the reader to [O]. Let us prove the following reversed Bonnesen inequality for Fuchsian hedgehogs.

Theorem 3. For any T -periodic function h : R ! R of class C 2 , we have:

1 2T (R r) 2 a (h) l (h) 2 2T ,
where l (h) and a (h) are respectively the signed length and area of h and where r := min 0 t T ( h (t)) and R := max 0 t T ( h (t)). Furthermore, the equality holds if and only if R = r.

Proof. Since h : R ! R is continuous, there exists (t 0 ; t 1 ) 2 [0; T ] 2 such that r = h (t 0 ) and R = h (t 1 ). We have thus

(R r) 2 = (h (t 1 ) h (t 0 )) 2 = Z t 1 t 0 h 0 (t) dt 2 .
By the Cauchy-Schwarz inequality, we deduce that (R r) 2 jt 1 t 0 j : Z max(t 0 ;t 1 ) min(t 0 ;t 1 ) Finally, considering equality cases at each step of the reasoning, we immediately see that the equality holds if, and only if, h is constant, which completes the proof.

  t) 2 dt = 2a (h) ) 2 2T a (h) l (h) 2 ,which achieves the proof of the reversed Bonnesen inequality.


Pierre-Louis Curien

The duality of computation under focus

Keywords:

We review the relationship between abstract machines for (call-byname or call-by-value) λ-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on the way Curien-Herbelin's syntactic kit of the duality of computation. We provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and we transcribe cut elimination as (non confluent) rewriting. A key slogan, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules. We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author's focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for a synthetic presentation of classical logic, that provides a quotient on (focalised) proofs, abstracting out the order of decomposition of negative connectives.

).

Here is Krivine machine, a simple device for call-by-name λ-calculus [13]:

A state of the machine is thus a pair M | E where M is "where the computation is currently active", and E is the stack of things that are waiting to be done in the future, or the continuation, or the evaluation context. In λ-calculus litterature, contexts are more traditionally presented as terms with a hole: with this tradition,

or "fill the hole of E with M (resp. []M )". How can we type the components of this machine? We have three categories of terms and of typing judgements: Expressions

Introduction

This paper on one hand has an expository purpose and on the other hand pushes further the syntactic investigations on the duality of computation undertaken in [START_REF] Curien | The duality of computation[END_REF].

Section 2 discusses the relation between abstract machines for the λ-calculus (extended with control) and (classical) sequent calculus. Section 3 presents a language (with a one-to-one correspondence between well-typed terms and proof trees) for a version of LK in which we choose to give a dissymetric presentation for the conjunction on the left and for the disjunction on the right, anticipating a key ingredient of focalisation. We recall the non-confluence of unconstrained classical cut-elimination.

In Section 4, we present the focalised proof search discipline (for classical logic), and adapt the syntactic framework of Section 3 to get a confluent system whose normal forms are precisely the terms denoting (cut-free) focalised proofs. The system we arrive at from these proof-search motivations is (a variant of) the second author's focalising system L (L foc ) [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF] We prove the completeness of L foc with respect to LK for provability. In Section 5, we define some simple encodings having L foc as source or target, indicating its suitability as an intermediate language.

Finally, in Section 6, further reinforcing of the focalisation discipline leads us to synthetic system L (L synth ), a logic of synthetic connectives in the spirit of Girard's ludics and Zeilberger's CU, for which we offer a syntactic account based on a simple game of patterns and counterpatterns. We show that the synthetic system L is complete with respect to focalising system L. Notation. We shall write t{v/x} the result of substituting v for x at all (free) occurrences of x in t, and t[v/x] for an explicit operator (as in [START_REF] Abadi | Explicit Substitutions[END_REF]) added to the language together with rules propagating it.

Then it is natural to associate continuation variables with the formulas in ∆: a term will depend on its input variables, and on its output continuations. With this in mind, we can read the operational rule for C(M ) as " C(M ) is a map E → M | E * • [ ] ", and write it with a new binder (that comes from [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF]):

C(M ) = µβ. M | β * • [ ] ,
where [ ] is now a continuation variable (of "top-level" type R). Likewise, we synthesise E * = λx.µα. x | E , with α, x fresh, from the operational rules for E * and for λx.M .

The typing judgements are now:

(Γ ⊢ M : A | ∆), (Γ | E : A ⊢ ∆), c : (Γ ⊢ ∆).
The two relevant new typing rules are (axiom, right activation):

Γ | α : A ⊢ α : A, ∆ c : (Γ ⊢ α : A, ∆) Γ ⊢ µα.c : A | ∆ plus a reduction rule: µα.c | E → c{E/α}.
Note that in this setting, there is no more need to "reify" a context E into an expression E * , as it can be directly substituted for a continuation variable.

Similarly, we can read off a (call-by-name) definition of M N from its operational rule: M N = µβ. M | N.β . Hence we can remove application from the syntax and arrive at a system in sequent calculus style only (no more elimination rule). This yields Herbelin's λµ-calculus [START_REF] Herbelin | Séquents qu'on calcule[END_REF]:

Expressions Contexts Commands

M ::= x | λx.M | µα.c E ::= α | M • E c ::= M | E
which combines the first two milestones above: "sequent calculus", "classical".

Let us step back to the λ-calculus. The following describes a call-by-value version of Krivine machine:

M N | e → N | M ⊙ e V | M ⊙ e → M | V • e
(the operational rule for λx.M is unchanged) 1 . Here, V is a value, defined as being either a variable or an abstraction (this goes back to [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF]). Again, we can read M ⊙ e as "a map Finally, we get from the rule for M N a call-by-value definition of application:

V → M | V • e ",
M N = µα. N μx. M | x • α .
We have arrived at Curien and Herbelin's λµμ Q -calculus [START_REF] Curien | The duality of computation[END_REF]:

Expressions

Values Contexts Commands

M ::= V ♦ | µα.c V ::= x | λx.M e ::= α | V • e | μx.c c ::= M | e Γ ⊢ M : A | ∆ Γ ⊢ V : A ; ∆ Γ | e : A ⊢ ∆ c : (Γ ⊢ ∆)
with a new judgement for values (more on this later) and an explicit coercion from values to expressions. The syntax for contexts is both extended (μx.c) and restricted (V • e instead of M • e). The reduction rules are as follows:

(λx.M ) ♦ | V • e → M {V /x} | e µα.c | e → c{e/α} V ♦ | μx.c → c{V /x}
1 The reason for switching notation from E to e will become clear in Section 5.

A language for LK proofs

In this section, we use some of the kit of the previous section to give a term language for classical sequent calculus LK, with negation, conjunction, and disjunction as connectives. Our term language is as follows:

Commands c ::= x | α | v | α | x | e | µα.c | μx.c Expressions v ::= (μx.c) • | (µα.c, µα.c) | inl (µα.c) | inr (µα.c) Contexts e ::= μα • .c | μ(x 1 , x 2 ).c | μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ] (In v | α (resp.
x | e ), we suppose α (resp. x) fresh for v (resp. e).) A term t is a command, an expression, or a context. As in section 2, we have three kinds of sequents:

(Γ ⊢ ∆), (Γ ⊢ A | ∆), and
(Γ | A ⊢ ∆).
We decorate LK's inference rules with terms, yielding the following typing system (one term construction for each rule of LK):

2. Still in the λ-calculus tradition, weakening is "transparent". If c : Γ ⊢ ∆ is welltyped, then c : (Γ, Γ ′ ⊢ ∆, ∆ ′ ) is well-typed (idem v, e). (Also, we recall that all free variables of c are among the ones declared in Γ, ∆.) 3. More importantly, we have adopted irreversible rules for right introduction of disjunction. On the other hand, we have given a reversible rule for left introduction of conjunction: the premise is derivable from the conclusion. This choice prepares the ground for the next section on focalisation. 3The relation between our typed terms and LK proofs is as follows.

-Every typing proof induces a proof tree of LK (one erases variables naming assumptions and conclusions, terms, the distinction between the three kinds of sequents, and the application of the deactivation rules).

-

µα. µα ′ .c μx ′ . x ′ | α μx.d → µα. µα ′ .c | μx.d μx.d (duplication) µα. y | β μx.d → y | β (erasing)
Commutative rules (going "up right", redexes of the form µα.c μx. y | e ): similar.

The (only?) merit of this syntax is its tight fit with proof trees and traditional cut elimination defined as transformations of undecorated proof trees. If we accept to losen this, we arrive at the following more "atomic" syntax:

Commands c ::= v | e | c[σ] Expressions v ::= x | µα.c | e • | (v, v) | inl (v) | inr (v) | v[σ] Contexts e ::= α | μx.c | μα • .c | μ(x 1 , x 2 ).c | μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ] | e[σ]
where σ is a list v 1 /x 1 , . . . , v m /x m , e 1 /α 1 , . . . , e n /α n . In this syntax, activation becomes "first class", and two versions of the axiom are now present (x, α, which give back the axiom of the previous syntax by deactivation). The typing rules are as follows

Γ ⊢ v1 : A1 | ∆ Γ ⊢ inl (v1) : A1 ∨ A2 | ∆ Γ ⊢ v2 : A2 | ∆ Γ ⊢ inr (v2) : A1 ∨ A2 | ∆ c : (Γ, x1 : A1, . . . , xm : Am ⊢ α1 : B1, . . . , αn : Bn) . . . Γ ⊢ vi : Ai | ∆Γ | ej : Bj ⊢ ∆ . . . c[v1/x1, . . . , vm/xm, e1/α1, . . . , en/αn] : (Γ ⊢ ∆) (idem v[σ], e[σ])
Note that we have now explicit substitutions t[σ], which feature a form of (multi-)cut where the receiver t's active formula, if any, is not among the cut formulas, in contrast with the construct v | e where the cut formula is active on both sides. It is still the case that, by erasing, a well-typed term of this new syntax induces a proof of LK, and that all proofs of LK are reached (although not injectively anymore), since all terms of the previous syntax are terms of the new syntax. The rewriting rules divide now in three groups:

(control) µα.c | e → c[e/α] v | μx.c → c[v/x] (logical) e • | μα • .c → c[e/α] (v 1 , v 2 ) | μ(x 1 , x 2 ).c → c[v 1 /x 1 , v 2 /x 2 ] inl (v 1 ) | μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ] → c 1 [v 1 /x 1 ] (idem inr ) (commutation) v | e [σ] → v[σ] | e[σ] x[σ] → x (x not declared in σ) x[v/x, σ] → v (idem α[σ]) (µα.c)[σ] → µα.(c[σ]) (idem (μx.c)[σ]) (capture avoiding) (etc, no rule for composing substitutions)
The control rules mark the decision to launch a substitution (and, in this section, of the direction in which to go, see below). The logical rules provide the interesting cases of cut elimination, corresponding to cuts where the active formula has been just introduced on both sides. The commutative cuts are now accounted for "trivially" by means of the explicit substitution machinery that carries substitution progressively inside terms towards their variable occurrences. Summarising, by liberalising the syntax, we have gained considerably in readability of the cut elimination rules 4Remark 1. In the "atomic" syntax, contractions are transcribed as terms of the form v | β (resp. x | e ) where β (resp. x) occurs free in v (resp. e). If β (resp. x) does not occur free in v (resp. e), then the command expresses a simple deactivation.

The problem with classical logic viewed as a computational system is its wild non confluence, as captured by Lafont's critical pair [START_REF] Girard | Proofs and Types[END_REF][START_REF] Danos | A new deconstructive logic: linear logic[END_REF], for which the µμ kit offers a crisp formulation. For any c 1 , c 2 both of type (Γ ⊢ ∆), we have (with α, x fresh for c 1 , c 2 , respectively):

c 1 * ← µα.c 1 | μx.c 2 → * c 2 .
So, all proofs are identified... Focalisation, discussed in the next section, will guide us to solve this dilemma.

A syntax for focalised classical logic

We adapt the focalisation discipline (originally introduced by [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] in the setting of linear logic) to LK. A focalised proof search alternates between right and left phases:

-Left phase: Decompose (copies of) formulas on the left, in any order. Every decomposition of a negation on the left feeds the right part of the sequent. At any moment, one can change the phase from left to right.

-Right phase: Choose a formula A on the right, and hereditarily decompose a copy of it in all branches of the proof search. This focusing in any branch can only end with an axiom (which ends the proof search in that branch), or with a decomposition of a negation, which prompts a phase change back to the left. Etc. . . Note the irreversible (or positive, active) character of the whole right phase, by the choice of A, by the choice of the left or right summand of a disjunction. One takes the risk of not being able to eventually end a proof search branch with an axiom. In contrast, all the choices on the left are reversible (or negative, passive). This strategy is not only complete (see below), it also guides us to design a disciplined logic whose behaviour will not collapse all the proofs.

To account for right focalisation, we introduce a fourth kind of judgement and a fourth syntactic category of terms: the values, typed as (Γ ⊢ V : A ; ∆) (the zone between the turnstyle and the semicolon is called the stoup, after [START_REF] Girard | A new constructive logic: classical logic[END_REF]). We also make official the existence of two disjunctions (since the behaviours of the conjunction on the left and of the disjunction on the right are different) and two conjunctions, by renaming ∧, ∨, ¬ as ⊗, ⊕, ¬ + , respectively. Of course, this choice of linear logic like notation is not fortuitous. Note however that the source of distinction is not based here on the use of resources like in the founding work on linear logic, which divides the line between additive and multiplicative connectives. In contrast, our motivating dividing line here is that between irreversible and reversible connectives, and hopefully this provides additional motivation for the two conjunctions and the two disjunctions. Our formulas are thus defined by the following syntax:

P ::= X | P ⊗ P | P ⊕ P | ¬ + P
These formulas are called positive. We can define their De Morgan duals as follows:

P 1 ⊗ P 2 = P 1 P 2 P 1 ⊕ P 2 = P 1 P 2 ¬ + P = ¬ -P
These duals are negative formulas:

N ::= X | N N | N N | ¬ -N .
They restore the duality of connectives, and are implicit in the presentation that follows (think of P on the left as being a P in a unilateral sequent ⊢ Γ , ∆).

P1 ⊗ P2 ⊢ ∆ c1 : (Γ, x1 : P1 ⊢ ∆) c2 : (Γ, x2 : P2 ⊢ ∆) Γ | μ[inl (x1).c1|inr (x2).c2] : P1 ⊕ P2 ⊢ ∆ c : (Γ . . . , q : P, . . . ⊢ ∆, . . . , α : Q, . . .) . . . Γ ⊢ V : P ; ∆ . . . Γ | e : Q ⊢ ∆ . . . c[. . . , V /q, . . . , e/α] : (Γ ⊢ ∆) (idem v[σ], V [σ], e[σ])
We are now ready to give the syntax of our calculus, which is a variant of the one given by the second author in [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF] 5 .

Commands c ::= v | e | c[σ] Expressions v ::= V ♦ | µα.c | v[σ] Values V ::= x | (V, V ) | inl (V ) | inr (V ) | e • | V [σ] Contexts e ::= α | μx.c | μα • .c | μ(x 1 , x 2 ).c | μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ] | e[σ]
The typing rules are given in Figure 1. Henceforth, we shall refer to the calculus of this section (syntax + rewriting rules) as L foc , and to the typing system as LKQ (after [START_REF] Danos | A new deconstructive logic: linear logic[END_REF]).

Here are examples of proof terms in LKQ.

Example 1.

(⊢ (μ(x, α • ). x ♦ | α ) • : ¬ + (P ⊗ ¬ + P ) ; ), where μ(x, α • ).c is an abbreviation for μ(x, y). y

♦ | μα • .c . inr ((μx. inl (x) ♦ | α ) • ) ♦ α : (⊢ α : P ⊕ ¬ + P ). ( | μ(x 2 , x 1 ). (x 1 , x 2 ) ♦ | α : P 2 ⊗ P 1 ⊢ α : P 1 ⊗ P 2 ). Proposition 1. If Γ ⊢ ∆ is provable in LK, then it is provable in LKQ. Fig. 2. Cut eliminition in Lfoc (control) µα.c | e → c[e/α] V ♦ | μx.c → c[V /x] (logical) (e • ) ♦ | μα • .c → c[e/α] (V1, V2) ♦ | μ(x1, x2).c → c[V1/x1, V2/x2] inl (V1) ♦ | μ[inl (x1).c1|inr (x2).c2] → c1[V1/x1] (idem inr ) (commutation) v | e [σ] → v[σ] | e[σ] etc . . .
PROOF. We translate the syntax given in section 3 into the focalised one. All cases are obvious except for the introduction of ⊗ and ⊕ on the right. We define (µα 1 .c 1 , µα 2 .c 2 )

as (Γ ⊢ µα. µα 2 .c 2 μx 2 . µα 1 .c 1 μx 1 . (x 1 , x 2 ) ♦ | α : P 1 ⊗ P 2 | ∆). ⊓ ⊔
We make two observations on the translation involved in the proof of Proposition 1.

Remark 2. The translation introduces cuts: in particular, a cut-free proof is translated to a proof with cuts. It also fixes an order of evaluation: one should read the translation of right and introduction as a protocol prescribing the evaluation of the second element of a pair and then of the first (the pair is thus in particular strict, as observed independently in [START_REF] Zeilberger | On the unity of duality[END_REF] and [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]). An equally reasonable choice would have been to permute the two μs: that would have encoded a left-to-right order of evaluation. This non-determinism of the translation has been known ever since Girard's seminal work [START_REF] Girard | A new constructive logic: classical logic[END_REF].

We move on to cut elimination, which (cf. Section 3) is expressed by means of three sets of rewriting rules, given in Figure 2. Note that we now have only one way to reduce µα.c 1 | μx.c 2 (no more critical pair). As already stressed in Section 3), the commutation rules are the usual rules defining (capture-avoiding) substitution. The overall operational semantics features call-by-value by the fact that variables x receive values, and features also call-by-name (through symmetry, see the logic LKT in Section 5) by the fact that continuation variables α receive contexts.

The reduction system presented in Figure 2 is confluent, as it is an orthogonal system in the sense of higher-order rewriting systems (left-linear rules, no critical pairs) [START_REF] Nipkow | Orthogonal higher-order rewriting systems are confluent[END_REF]. However, using such an encoding would mean to shift from a direct to an indirect style for terms of the form µβ.c.

Proposition 2. Cut-elimination holds in LKQ.

PROOF. This is an easy consequence of the following three properties: 1) Subject reduction. This is checked as usual rule by rule.

2) Weak normalisation. As for LK, or for simply typed λ-calculus.

3) Characterisation of normal forms. A command in normal form has one of the following shapes (all contractions):

V ♦ | α x ♦ | μα • .c x ♦ | μ(x 1 , x 2 ).c x ♦ | μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ] ⊓ ⊔ Corollary 1.
Every sequent Γ ⊢ ∆ that is provable in LK admits a (cut-free) proof respecting the focalised discipline.

PROOF. Let π be a proof of Γ ⊢ ∆. By Propositions 1 and 2, one obtains a term denoting a focalised, cut-free proof of Γ ⊢ ∆.

⊓ ⊔

We can add η-equivalences (or expansion rules, when read from right to left) to the system, as follows (where all mentioned variables are fresh for the mentioned terms):

µα. v | α = v μ(x 1 , x 2 ). (x 1 , x 2 ) ♦ | e = e μx. x ♦ | e = e μ[inl (x 1 ). inl (x 1 ) ♦ | e |inr (x 2 ). inr (x 2 ) ♦ | e ] = e μα • (α • ) ♦ | e = e
The rules on the left column allow us to cancel a deactivation followed by an activation (the control rules do the job for the sequence in the reverse order), while the rules in the right column express the reversibility of the negative rules.

We end the section with a lemma that will be useful in Section 6.

Lemma 1. -If Γ, x : ¬ + P | e : Q ⊢ ∆, then Γ | e{α • /x} : Q ⊢ α : P, ∆. -If Γ, x : P 1 ⊗ P 2 | e : Q ⊢ ∆, then Γ, x 1 : P 1 , x 2 : P 2 | e{(x 1 , x 2 )/x} : Q ⊢ ∆. -If Γ, x : P 1 ⊕ P 2 | e : Q ⊢ ∆, then Γ, x 1 : P 1 | e{inl (x 1 )/x} : Q ⊢ ∆ and Γ, x 2 : P 2 | e{inr (x 2 )/x} : Q ⊢ ∆.
(and similarly for c, V, v).

Encodings

Encoding CBV λ(µ)-calculus into LKQ. We are now in a position to hook up with the material of Section 2. We can encode the call-by-value λ-calculus, by defining the following derived CBV implication and terms:

P → v Q = ¬ + (P ⊗ ¬ + Q) λx.v = ((μ(x, α • ). v | α ) • ) ♦ v 1 v 2 = µα. v 2 μx. v 1 | ((x, α • ) ♦ )
where μ(x, α • ).c is the abbreviation used in Example 1 and where V stands for μα • . V ♦ | α . The translation extends to (call-by-value) λµ-calculus [START_REF] Ong | A Curry-Howard foundation for functional computation with control[END_REF], and factors though λµμ Q -calculus (cf. Section 2), defining V • e as (V, e • ) . The translation makes also sense in the untyped setting, as the following example shows.

Example 2. Let ∆ = λx.xx. We have [[∆∆]] + v = µγ.c, and c → * c, with c = (e • ) ♦ μz. (e • ) ♦ | (z, γ • ) and e = μ(x, α • ). x ♦ μy. x ♦ | (y, α • )
Encoding CBN λ(µ)-calculus. What about CBN? We can translate it to LKQ, but at the price of translating terms to contexts, which is a violence to our goal of giving an intuitive semantics to the first abstract machine presented in Section 2. But keeping the same term language, we can type sequents of the form (. . . , α : N, . . . ⊢ . . . , x : N, . . .), giving rise to a dual logic LKT, renaming the metavariables for expressions, values, and contexts as e (now contexts), E (now covalues, also called applicative contexts in [START_REF] Curien | The duality of computation[END_REF]),

v | e cps = (vcps)(ecps) (V ♦ )cps = λk.k(Vcps) (µα.c)cps = λkα.(ccps) = μα • .ccps xcps = x (V1, V2)cps = ((V1)cps, (V2)cps) inl (V1)cps = inl ((V1)cps) (e • )cps = ecps αcps = kα (μx.c)cps = λx.(ccps) (μ(x1, x2).c)cps = λz.(ccps[fst(z)/x1, snd (z)/x2]) (μ[inl (x1).c1|inr (x2).c2])cps = λz.case z [inl (x1) → (c1)cps, inr (x2) → (c2)cps]
and v (now expressions). For example the rules for left introduction of and of right introduction for are as follows:

Γ ; E1 : N1 ⊢ ∆ Γ ; inl (E1) : N1 N2 ⊢ ∆ Γ ; E2 : N2 ⊢ ∆ Γ ; inr (E2) : N1 N2 ⊢ ∆ c : (Γ ⊢ x1 : N1 , x2 : N2 , ∆) Γ ⊢ μ(x1, x2).c : N1 N2 | ∆
In what follows, it will be handier (and closer to the tradition of CBN λµ-calculus) to use x (resp. α) instead of a negative variable α (resp. continuation variable x).

We would have arrived to this logic naturally if we had chosen in Section 3 to present LK with a reversible disjunction on the right and an irreversible conjunction on the left, and in Section 4 to present a focalisation discipline with focusing on formulas on the left. In LKT we can define the following derived CBN implication and terms:

M → n N = (¬ -M ) N λx.v = μ(x • , α). v | α♦ v 1 v 2 = µ α. v 1 | (v • 2 , α)
The translation extends to λµ-calculus [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF] and factors though the λµμ T -calculus of [START_REF] Curien | The duality of computation[END_REF], defining v • E as (v • , E). Note that the covalues involved in executing call-by-name λ-calculus are just stacks of expressions (cf. Section 2).

Translating LKQ into NJ. Figure 3 presents a translation from LKQ to intuitionistic natural deduction NJ, or, via Curry-Howard, to λ-calculus extended with products and sums. In the translation, R is a fixed target formula (cf. Section 2). We translate (¬ + ) as " implies R" (cf. [START_REF] Krivine | Lambda-calcul, types et modèles[END_REF][START_REF] Lafont | Continuation Semantics or Expressing Implication by Negation[END_REF]). We write B A for function types / intuitionistic implications. The rules of L foc are simulated by β-reductions. One may think of the source L foc terms as a description of the target ones "in direct style" (cf. [START_REF] Danvy | Back to direct style[END_REF]).

Proposition 3. Let Γ cps = {x : P cps | x : P ∈ Γ }, R ∆cps = {k α : R Pcps | α : P ∈ ∆}.

We have:

C : (Γ ⊢ ∆) ⇒ Γ cps , R ∆cps ⊢ C cps : R Γ ⊢ V : P ; ∆ ⇒ Γ cps , R ∆cps ⊢ V cps : P cps Γ ⊢ v : P | ∆ ⇒ Γ cps , R ∆cps ⊢ v cps : R R Pcps Γ | e : P ⊢ ∆ ⇒ Γ cps , R
∆cps ⊢ e cps : R Pcps Moreover, the translation preserves reduction: if t → t ′ , then t cps → * (t ′ ) cps .

In this section we pursue two related goals.

1. We want to account for the full (or strong) focalisation (cf. [START_REF] Quatrini | Polarisation des preuves classiques et renversement[END_REF]), which consists in removing the use of contractions in the negative phases and carrying these phases maximally, up to having only atoms on the left of the sequent. The positive phases are made also "more maximal" by allowing the use of the axiom only on positive atoms X. This is of interest in a proof search perspective, since the stronger discipline further reduces the search space. 2. We would like our syntax to quotient proofs over the order of decomposition of negative formulas. The use of structured pattern-matching (cf. Example 1) is relevant, as we can describe the construction of a proof of (Γ, x : (P 1 ⊗P 2 )⊗(P 3 ⊗P 4 ) ⊢ ∆) out of a proof of c : (Γ, x 1 : P 1 , x 2 : P 2 , x 3 : P 3 , x 4 : P 4 ⊢ ∆) "synthetically", by writing x ♦ | μ((x 1 , x 2 ), (x 3 , x 4 )).c , where μ((x 1 , x 2 ), (x 3 , x 4 )).c stands for an abbreviation of either of the following two commands:

x ♦ μ(y, z). y ♦ μ(x1, x2). z ♦ | μ(x3, x4).c x ♦ μ(y, z). z ♦ μ(x3, x4). y ♦ | μ(x1, x2).c
The two goals are connected, since applying strong focalisation will forbid the formation of these two terms (because y, z are values appearing with non atomic types), keeping the synthetic form only... provided we make it first class.

We shall proceed in two steps. The first, intermediate one, consists in introducing first-class counterpatterns and will serve goal 1 but not quite goal 2:

Simple commands c ::

= v | e Commands C ::= c | [C q,q C] Expressions v ::= V ♦ | µα.C Values V ::= x | (V, V ) | inl (V ) | inr (V ) | e • Contexts e ::= α | μq.C Counterpatterns q ::= x | α • | (q, q) | [q, q]
The counterpatterns are to be thought of as constructs that match patterns (see below). In this syntax, we have gained a unique μ binder, but the price to pay is that now commands are trees of copairings [ q1,q2 ] whose leaves are simple commands.

The typing discipline is restricted with respect to that of Figure 1 (and adapted to the setting with explicit counterpatterns). Let Ξ = x 1 : X 1 , . . . , x n : X n denote a left context consisting of atomic formulas only. The rules are as follows:

Ξ , x : X ⊢ x : X ; ∆ C : (Ξ , q : P ⊢ ∆) Ξ | μq.C : P ⊢ ∆ C : (Ξ ⊢ α : P , ∆) Ξ ⊢ µα.C : P | ∆ C : (Γ ⊢ α : P , ∆) C : (Γ , α • : ¬ + P ⊢ ∆) C : (Γ , q1 : P1 , q2 : P2 ⊢ ∆) C : (Γ , (q1, q2) : P1 ⊗ P2 ⊢ ∆) C1 : (Γ , q1 : P1 ⊢ ∆)C2 : (Γ , q2 : P2 ⊢ ∆) [C1 q 1 ,q 2 C2] : (Γ , [q1, q2] : P1 ⊕ P2 ⊢ ∆)
(all the other rules as in Figure 1, with Ξ in place of Γ )

Our aim now (second step) is to get rid of the tree structure of a command. Indeed, if c ij : (Γ, x i : P i , x j : P j ⊢ S ∆) (i = 1, 2, j = 3, 4), we want to identify

[[c13 x 3 ,x 4 c14] x 1 ,x 2 [c23 x 3 ,x 4 c24]] and [[c13 x 1 ,x 2 c23] x 3 ,x 4 [c14 x 1 ,x 2 c24]] .
To this effect, we need a last ingredient. We introduce a syntax of patterns, and we redefine the syntax of values, as follows:

V ::= x | e • V ::= p V i /i | i ∈ p p ::= x | α • | (p, p) | inl (p) | inr (p)
where i ∈ p is defined by:

x ∈ x α • ∈ α • i ∈ p 1 i ∈ (p 1 , p 2 ) i ∈ p 2 i ∈ (p 1 , p 2 ) i ∈ p 1 i ∈ inl (p 1 ) i ∈ p 2 i ∈ inr (p 2 )
Moreover, V i must be of the form y (resp. e • ) if i = x (resp. i = α • ).

Patterns are required to be linear, as well as the counterpatterns, for which the definition of "linear" is adjusted in the case [q 1 , q 2 ], in which a variable can occur (but recursively linearly so) in both q 1 and q 2 .

We can now rephrase the logical reduction rules in terms of pattern/counterpattern interaction (whence the terminology), resulting in the following packaging of rules: V = p . . . y/x, . . . , e • /α • , . . . C[p/q] → * c V ♦ | μq.C → c{. . . , y/x, . . . , e/α, . . .} where c{σ} is the usual, implicit substitution, and where c (see the next proposition) is the normal form of C[p/q] with respect to the following set of rules: C[(p 1 , p 2 )/(q 1 , q 2 ), σ] → C[p 1 /q 1 , p 2 /q 2 , σ] C[β • /α • , σ] → C[β/α, σ] [C 1 q1,q2 C 2 ][inl (p 1 )/[q 1 , q 2 ], σ] → C 1 [p 1 /q 1 , σ] (idem inr )

Logically, this means that we now consider each formula as made of blocks of synthetic connectives.

Example 3. -Patterns for P = X ⊗ (Y ⊕ ¬ + Q). Focusing on the right yields two possible proof searches:

Γ ⊢ x ′ {V x ′ } : X ; ∆ Γ ⊢ y ′ {V y ′ } : Y ; ∆ Γ ⊢ (x ′ , inl (y ′ )){V x ′ , V y ′ } : X ⊗ (Y ⊕ ¬ + Q) ; ∆ Γ ⊢ x ′ {V x ′ } : X ; ∆ Γ ⊢ α ′ • {V α ′ • } : ¬ + Q ; ∆ Γ ⊢ (x ′ , inr (α ′ • )){V x ′ , V α ′ • } : X ⊗ (Y ⊕ ¬ + Q) ; ∆ -Counterpattern for P = X ⊗ (Y ⊕ ¬ + Q).
The counterpattern describes the tree structure of P : c 1 : (Γ , x : X , y : Y ⊢ ∆) c 2 : (Γ , x : X , α

• : ¬ + Q ⊢ ∆) [c 1 y,α • c 2 ] : (Γ , (x, [y, α • ]) : X ⊗ (Y ⊕ ¬ + Q) ⊢ ∆)
We observe that the leaves of the decomposition are in one-to-one correspondence with the patterns p for the (irreversible) decomposition of P on the right:

[c 1 y,α • c 2 ][p 1 /q] = c 1 {x ′ /x, y ′ /y} [c 1 y,α • c 2 ][p 2 /q] = c 2 {x ′ /x, α ′ /α}
where q = (x, [y, α • ]) , p 1 = (x ′ , inl (yk ′ )) , p 2 = (x ′ , inr (α ′• )).

  or, introducing a new binder μ (binding now ordinary variables): M ⊙ e = μx. M | x • e . The typing rule for this operator is (left activation): c : (Γ, x : A ⊢ ∆) Γ | μx.c : A ⊢ ∆ , and the operational rule is V | μx.c → c{V /x} (V value).

  µα. (μx.c) • | α μy. y | μα • .d → µα.d | μx.c (similar rules for conjunction and disjunction) Commutative rules (going "up left", redexes of the form µα. v | β μx.c ): µα. (μy.c) • | β μx.d → µβ ′ . (μy. µα.c | μx.d ) • β ′ μy. y | β (¬ right) (similar rules with the other right introduction rules and with the left introduction rules) µα. µβ. y | β μy ′ .c μx.d → µβ. y | β μy ′ . µα.c | μx.d (contraction right) µα. µβ ′ .c μy. y | β μx.d → µβ ′ . µα.c | μx.d μy. y | β (contraction left)

Fig. 1 .

 1 Fig. 1. System LKQ

Remark 3 .

 3 About µ: we note that µβ.c is used only in a command µβ.c | e , and in such a context it can be expressed as (e • ) ♦ | μβ • .c , which indeed reduces to c[e/β].

Fig. 3 .

 3 Fig. 3. Translation of LKQ into the λ-calculus / NJ Translation of formulas: Xcps = X (¬ + P )cps = R Pcps (P ⊗ Q)cps = (Pcps) × (Qcps) P ⊕ Qcps = Pcps + Qcps Translation of terms:

Fig. 4 .

 4 Fig. 4. The syntax and reduction semantics of Lsynth

  If bound variables are explicitly typed (which we shall refrain from doing in the sequel), then every provable typing judgement, say Γ | e : A ⊢ ∆, has a unique typing proof, i.e. all information is in Γ , A, ∆, e.-If Π is an LK proof tree of (A 1 , . . . , A m ⊢ B 1 , . . . , B n ), and if names x 1 , . . . , x m , α 1 , . . . , α n are provided, then there exists a unique command c : (x 1 : A 1 , . . . , x m : A m ⊢ α 1 : B 1 , . . . , α n : B n ), whose (unique) typing proof gives back Π by erasing.With this syntax, we can express the cut-elimination rules of LK as rewriting rules: Logical rules (redexes of the form µα. v | α μx. x | e ):

(Γ | E : A ⊢ R) c : (Γ ⊢ R)where R is a (fixed) type of final results. The type of an expression (resp. a context) is the type of the value that it is producing (resp. expecting). The typing rules for contexts and commands are as follows:Γ | [ ] : R ⊢ R Γ ⊢ M : A Γ | E : B ⊢ R Γ | M • E : A → B ⊢ R Γ ⊢ M : A Γ | E : A ⊢ R M | E : (Γ ⊢ R)and the typing rules for expressions are the usual ones for simply typed λ-calculus.Stripping up the term information, the second and third rules are rules of sequent calculus (left introduction of implication and cut). We next review Griffin's typing of Felleisen's control operator C. As a matter of fact, the behaviour of this constructor is best expressed at the level of an abstract machine:C(M ) | E → M | E * • [ ] E * | N • E ′ → N | EThe first rule explains how the continuation E gets captured, and the second rule how it gets restored. Griffin[START_REF] Griffin | A formulae-as-types notion of control[END_REF] observed that the typing constraints induced by the well-typing of these four commands are met when C(M ) and E * are typed as follows:

(axiom and cut/contraction) x | α : (Γ, x : A ⊢ α : A, ∆) c : (Γ ⊢ α : A, ∆) d : (Γ, x : A ⊢ ∆) µα.c | μx.d : (Γ ⊢ ∆) (right)c : (Γ, x : A ⊢ ∆) Γ ⊢ (μx.c) • : ¬A | ∆ c1 : (Γ ⊢ α1 : A1, ∆) c2 : (Γ ⊢ α2 : A2, ∆) Γ ⊢ (µα1.c1, µα2.c2) : A1 ∧ A2 | ∆ c1 : (Γ ⊢ α1 : A1, ∆) Γ ⊢ inl (µα1.c1) : A1 ∨ A2 | ∆ c2 : (Γ ⊢ α2 : A2, ∆) Γ ⊢ inr (µα2.c2) : A1 ∨ A2 | ∆ (left) c : (Γ ⊢ α : A, ∆) Γ | μα • .c : ¬A ⊢ ∆ c : (Γ, x1 : A1, x2 : A2 ⊢ ∆) Γ | μ(x1, x2).c : A1 ∧ A2 ⊢ ∆ c1 : (Γ, x1 : A1 ⊢ ∆) c2 : (Γ, x2 : A2 ⊢ ∆) Γ | μ[inl (x1).c1|inr (x2).c2] : A1 ∨ A2 ⊢ ∆ (deactivation) Γ ⊢ v : A | ∆ v | α : (Γ ⊢ α : A, ∆) Γ | e : A ⊢ ∆ x | e : (Γ, x : A ⊢ ∆)Note that the activation rules are packaged in the introduction rules and in the cut rule. As for the underlying sequent calculus rules, we have made the following choices:1. We have preferred additive formulations for the cut rule and for the right introduction of conjunction (to stay in tune with the tradition of typed λ-calculi) over a multiplicative one where the three occurrences of Γ would be resp. Γ 1 , Γ 2 , and (Γ 1 , Γ 2 ) (idem for ∆). An important consequence of this choice is that contraction is a derived rule of our system, whence the name of cut/contraction rule above 2 :Γ, A ⊢ A, ∆ Γ, A, A ⊢ ∆ Γ, A ⊢ ∆ Γ ⊢ A, A, ∆ Γ, A ⊢ A, ∆ Γ ⊢ A, ∆2In usual syntactic accounts of contraction, one says that if, say t denotes a proof of Γ, x :A, y : A ⊢ ∆, then t[z/x, z/y] denotes a proof of Γ, z : A ⊢ ∆. Note that if this substitution is explicit, then we are back to an overloading of cut and contraction.

For the same reason, we have three connectives instead of just, say, ∨ and ¬, because in the focalised setting ¬(¬A ∨ ¬B) is only equivalent to A ∧ B at the level of provavility.(we omit the rules for μx.c, μα • .c, μ(x 1 , x 2 ).c, μ[inl (x 1 ).c 1 |inr (x 2 ).c 2 ], which are unchanged):Γ , x : A ⊢ x : A | ∆ Γ | α : A ⊢ α : A , ∆ Γ ⊢ v : A | ∆ Γ | e : A ⊢ ∆ v | e : (Γ ⊢ ∆) c : (Γ , x : A ⊢ ∆) Γ | μx.c : A ⊢ ∆ c : (Γ ⊢ α : A , ∆) Γ ⊢ µα.c : A | ∆ Γ | e : A ⊢ ∆ Γ ⊢ e • : ¬A | ∆ Γ ⊢ v1 : A1 | ∆ Γ ⊢ v2 : A2 | ∆ Γ ⊢ (v1, v2) : A1 ∧ A2 | ∆

The precise relation with the previous rules is as follows: for all s1, s2 such that s1 → s2 in the first system, there exists s such that s1 → * s and s2 → * s in the new system.

Γ ⊢ v : P | ∆ Γ | e : P ⊢ ∆ v | e : (Γ ⊢ ∆) c : (Γ , x : P ⊢ ∆) Γ | μx.c : P ⊢ ∆ c : (Γ ⊢ α : P , ∆) Γ ⊢ µα.c : P | ∆ Γ ⊢ V : P ; ∆ Γ ⊢ V ♦ : P | ∆ Γ | e : P ⊢ ∆ Γ ⊢ e • : ¬ + P ; ∆ Γ ⊢ V1 : P1 ; ∆ Γ ⊢ V2 : P2 ; ∆ Γ ⊢ (V1, V2) : P1 ⊗ P2 ; ∆ Γ ⊢ V1 : P1 ; ∆ Γ ⊢ inl (V1) : P1 ⊕ P2 ; ∆ c : (Γ ⊢ α : P, ∆) Γ | μα • .c : ¬ + P ⊢ ∆ c : (Γ, x1 : P1, x2 : P2 ⊢ ∆)

The main differences with the system presented in[START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF] is that we have here an explicit syntax of values, with an associated form of typing judgement, while focalisation is dealt with at the level of the reduction semantics in[START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF]. Also, the present system is bilateral but limited to positive formulas on both sides, it thus corresponds to the positive fragment of the bilateral version of Lfoc as presented in[START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF][long version, Appendix A].

(μ + ) (p . . . , y/x, . . . , e • /α • . . . ) ♦ | μq.{p → cp | q ⊥ p} → cp {. . . , y/x, . . . , e/α, . . . } (µ) µα.c | e → c{e/α} Typing rules: the old ones for α, x, e • , c, plus the following ones: . . . Γ ⊢ Vi : Pi ; ∆ ((i : Pi) ∈ Γ (p, P )) . . . Γ ⊢ p Vi/i | i ∈ p : P ; ∆ . . . cp : (Γ , Γ (p, P ) ⊢ ∆) (q ⊥ p) . . . Γ | μq.{p → cp | q ⊥ p} ⊢ ∆

See also[START_REF] Murthy | A computational analysis of Girard's translation and LC[END_REF] for an early analysis of the computational meaning of LC from a programming language perspective.

where Γ (p, P ) must be successfully defined as follows:

This correspondence is general. We define two predicates c ∈ C and q ⊥ p ("q is orthogonal to p") as follows:

We can now state the correspondence result. Proposition 4. Let C : (Ξ , q : P ⊢ ∆) (as in the assumption of the typing rule for μq.C), and let p be such that q is orthogonal to p. Then the normal form c of C[p/q] is a simple command, and the mapping p → c (q, C fixed) from {p | q ⊥ p} to {c | c ∈ C} is one-to-one and onto.

Thanks to this correspondence, we can quotient over the "bureaucracy" of commands, and we arrive at the calculus described in Figure 4, together with its typing rules, which we call synthetic system L, or L synth . The μ construct of L synth is closely related to Zeilberger's higher-order abstract approach to focalisation in [START_REF] Zeilberger | On the unity of duality[END_REF]: indeed we can view {p → c | q ⊥ p} as a function from patterns to commands. We actually prefer to see here a finite record whoses fields are the p's orthogonal to q. There are only two reduction rules in L synth . the µ-rule now expressed with implicit substitution and the μ+rule, which combines two familiar operations: select a field p (like in object-oriented programming), and substitute (like in functional programming). The next proposition relates L synth to L foc . Proposition 5. The typing system of L synth is complete with respect to LKQ.

PROOF. The completeness of L synth with respect to the intermediate system above is an easy consequence of Proposition 4. In order to prove the completeness of the intermediate system, we define the following rewriting relation between sets of sequents:

(Γ, x : ¬ + P ⊢ ∆), S (Γ ⊢ α : P, ∆), S (Γ, x :

(Γ, x 1 : P 1 ⊢ ∆), (Γ, x 2 : P 2 ⊢ ∆), S (where α, x 1 , x 2 are fresh). One proves the following properties together: 1) if c : (x 1 : P 1 , . . . , x m : P m ⊢ ∆), then there exist q 1 , . . . , q m and C such that C : (q 1 : P 1 , . . . , q m : P m ⊢ S ∆), 2) if Ξ | e : P ⊢ ∆, then there exists e ′ such that Ξ | e ′ : P ⊢ S ∆ (and similarly for expressions v), where ⊢ S (resp. ⊢) refers to the intermediate system (resp. to L foc ). The proof of 1) goes as follows. Using Lemma 1 and induction, we get simple commands c i proving all the sequents in the normal form of (x 1 : P 1 , . . . , x m : P m ⊢ ∆) w.r.t. the above rewriting rules. One can then assemble the c i 's to form a command C as in the statement.

⊓ ⊔ Putting together Propositions 1 and 5, we have proved that L synth is complete with respect to LK for provability. Remark 4. In the multiplicative case (no C, inl (V ), inr (V ), [q 1 , q 2 ]), there is a unique p such that q ⊥ p, namely q, and the syntax boils down to:

Conclusion

We believe that Curien-Herbelin's syntactic kit, which we could call system L for short, provides us with a robust infrastructure for proof-theoretical investigations, and for applications in formal studies in operational semantics. Thus, the work presented here is faithful to the spirit of Herbelin's Habilitation Thesis [START_REF] Herbelin | C'est maintenant qu'on calcule, au coeur de la dualité[END_REF], where he advocated an incremental approach to connectives, starting from a pure control kernel.

The good fit between abstract machines and our syntax L foc makes it a good candidate for being used as an intermediate language appropriate to reason about the correctness of abstract machines (see also [START_REF] Levy | Call-by-push-value. A functional/imperative synthesis[END_REF]). In this spirit, in order to account for languages with mixed call-by-value / call-by-name features, one may give a truly bilateral presentation of L foc that freely mixes positive and negative formulas like in Girard's LC [START_REF] Girard | A new constructive logic: classical logic[END_REF]. 6 Such a system is presented in the long version of [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF].

We wish to thank R. Harper, H. Herbelin, and O. Laurent for helpful discussions.