Vincent Andrieu

Christophe Prieur
email: christophe.prieur@gipsa-lab.grenoble-inp.fr

Sophie Tarbouriech

Denis Arzelier
email: arzelier@laas.fr

Global asymptotic stabilization of systems satisfying two different sector conditions

Global asymptotic stabilization for a class of nonlinear systems is addressed. The dynamics of these systems are composed of a linear part to which is added some nonlinearities which satisfy two different sector bound conditions depending on whether the state is near or far from the origin. The proposed approach is based on the uniting of control Lyapunov functions. In this framework, the stabilization problem may be recast as an LMI optimization problem for which powerful semidefinite programming softwares exist. This is illustrated by means of three numerical examples.

Introduction

There is an extensive literature on the design of nonlinear stabilizers providing numerous techniques applicable to specific classes of nonlinear systems. The class of systems considered is the one described by a linear system with an additive memoryless sector-bounded nonlinearity. The nonlinearities under interest in this paper are those satisfying two different sector bound conditions depending on the norm of the state. This class of nonlinearity includes many different memoryless functions (see e.g., [START_REF] Khalil | Nonlinear Systems[END_REF]Chapter 6] for an introduction on this topic) such as saturations (see e.g. [START_REF] Tarbouriech | Advanced strategies in control systems with input and output constraints[END_REF][START_REF] Hu | Stability and performance for saturated systems via quadratic and nonquadratic lyapunov functions[END_REF][START_REF] Hu | Control systems with actuator saturation: analysis and design[END_REF] for design techniques of control system with such nonlinearities). Contrary to what has been done in these papers, two different sector conditions are considered to characterize the nonlinear functions: One sector condition when the state is near the equilibrium and one other sector condition when the state is far from the equilibrium. This distinction between small and large values of the distance from the state to the equilibrium allows us to better describe the nonlinear system. Moreover, we remark that encompassing both sector conditions into one global sector condition may lead to a too conservative synthesis problem which may not have a solution (see the example of Section 5.2 below).

This motivates us to separately consider the local sector condition and the non-local one. In our approach, we design successively:

1. a local stabilizer with a basin of attraction containing a compact set; 2. a non-local controller such that the previous compact set is globally attractive.

In a second step, in order to design a continuous global stabilizer, the local and non-local controllers are merged into one unique and global controller. Different techniques exist to unit a couple of different feedback laws. For instance, provided that the use of discontinuous controllers is allowed, hybrid controllers may be employed to unit them (see [START_REF] Prieur | Uniting local and global controllers with robustness to vanishing noise[END_REF][START_REF] Prieur | Uniting a high performance, local controller with a global controller: the output feedback case for linear systems with input saturation[END_REF][START_REF] Prieur | Quasi-optimal robust stabilization of control systems[END_REF][START_REF] Teel | Uniting local and global controllers[END_REF]).

In the present paper we apply the technique introduced in [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] where a continuous solution to the uniting problem is given through the construction of a uniting control Lyapunov function 1 .

More precisely, in [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] some sufficient conditions are given to provide a global stabilizer from a local and a non-local control Lyapunov function 2 . In the following, we rewrite these sufficient conditions in terms of linear matrix inequalities (LMIs) which, if solved, allow to design a global stabilizer for the control of systems satisfying two different sector conditions.

To be more precise, consider the system defined by its state-space equation:

ẋ = A x + B u + G φ(x) (1)
where the state vector x is in Ê n . (A, B, G) are matrices respectively in Ê n×n , Ê n×m , Ê n×p . Moreover u in Ê m is the control input and φ(x) : Ê n → Ê p is a nonlinear locally Lispchitz function such that φ(0) = 0. One way to design a global stabilizer for system (1) is to use circle and Popov criteria (see [START_REF] Arcak | Circle and Popov criteria as tools for nonlinear feedback design[END_REF]) under the assumption that the nonlinear function φ satisfies some sector bound conditions of the following type 3 :

(φ(x) -Mx) ′ (φ(x) -Nx) ≤ 0 , ∀ x ∈ Ê n , (2)
where M and N are two given matrices in Ê p×n . Following 4 [START_REF] Castelan | Control design for a class of nonlinear continuous-time systems[END_REF][START_REF] Montagner | Robust absolute stability and nonlinear state feedback stabilization based on polynomial Lur'e functions[END_REF], a constructive LMI condition allowing to design a state feedback control law solving the stabilizing problem may be exhibited.

The aim of this paper is to study the case in which the function φ satisfies two different sector conditions depending on the norm of x. The idea of the design is then to apply techniques inspired by [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] to unit local and non-local controllers and to provide a global stabilizer.

Assumptions on the nonlinear function φ introduced in (1) can be given as follows:

Assumption 1. Local sector condition. There exist a positive real number v 0 , two matrices (M 0 , N 0 ) in Ê p×n × Ê p×n such that, for all |x| ≤ v 0 , we have:

(φ(x) -M 0 x) ′ (φ(x) -N 0 x) ≤ 0 . (3)
Assumption 2. Non-local sector condition. There exist a positive real number

v ∞ < v 0 , two matrices (M ∞ , N ∞ ) in Ê p×n × Ê p×n and two vectors (R ∞ , Q ∞ ) in Ê p × Ê p such that, for
all |x| ≥ v ∞ , we have:

(φ(x) -M ∞ x -R ∞ ) ′ (φ(x) -N ∞ x -Q ∞ ) ≤ 0 . ( 4
)
1 see [START_REF] Arststein | Stabilization with relaxed controls[END_REF] for a definition of CLF.

2 see [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] for definitions of local and non-local CLFs. 3 Note that other classes of sector conditions are possible. In particular we may consider the generalized sector conditions written as

(φ(x) -M x) ′ D (φ(x) -N x) ≤ 0 ,
where D is any given diagonal positive definite matrix (as in [START_REF] Da | Anti-windup design with guaranteed regions of stability : an LMI-based approach[END_REF][START_REF] Tarbouriech | Stability analysis and stabilization of systems presenting nested saturations[END_REF]). Despite the fact that considering such generalized sector conditions is possible, we restrict our attention to sector bound condition as [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] to ease the exposition of our results. 4 Note that in [START_REF] Castelan | Control design for a class of nonlinear continuous-time systems[END_REF] is addressed a more involved problem since some saturations on the input are considered.

Systems satisfying both Assumptions 1 and 2 are of interest since local and non-local approximations of nonlinear global dynamics may be found in the literature. For instance, in [START_REF] Andrieu | Homogeneous approximation, recursive observer design and output feedback[END_REF], local and non-local homogeneous approximations of nonlinear systems are studied. Moreover, as shown in the example introduced in Section 5.2 below, it might be useful to split a global sector condition in two pieces (a local and a non-local one) in order to get a solution where the usual LMI-based sufficient conditions obtained from [START_REF] Castelan | Control design for a class of nonlinear continuous-time systems[END_REF][START_REF] Montagner | Robust absolute stability and nonlinear state feedback stabilization based on polynomial Lur'e functions[END_REF] are too conservative. Compared to the preliminary version of this paper presented in [START_REF] Andrieu | Synthesis of a global asymptotic stabilizing feedback law for a system satisfying two different sector conditions[END_REF], two new vectors are involved in the definition of the non local sector condition (i.e. R ∞ and Q ∞ ). This allows to extend the class of considered systems. Note that an illustration of a function satisfying two different sector conditions can be found in Figure 1.

In this paper, the following problem is addressed: Problem: Under Assumptions 1 and 2, is it possible to design a nonlinear control law u = α(x) where α : Ê n → Ê m is a continuous function ensuring global asymptotic stabilization of the origin for the system (1)? Before considering this global stabilization problem, each sector is considered separately in Section 2. Indeed, a local (resp. a non-local) controller u = α 0 (x) (resp. u = α ∞ (x)) is synthesized by employing the local (resp. non-local) sector condition of Assumption 1 (resp. of Assumption 2). After this preliminary step, a new controller, which is equal to the local controller u = α 0 (x) on a neighborhood of the origin and equal to the non-local controller u = α ∞ (x) outside a compact set, is designed. This construction is based on [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] and is considered in Section 3. We then formalize a sufficient condition, expressed in terms of the existence of solutions to LMIs constraints, allowing us to address the global stabilization problem in one step in Section 4. Three numerical examples illustrate the previous results in Section 5. Section 6 contains some concluding remarks.

Notation. The Euclidian norm is denoted by | • |. For a positive real number n, I n (resp. 0 n,m ) denotes the identity matrix (resp. the null matrix) in Ê n×n (resp. in Ê n×m ). The subscripts may be omitted when there is no ambiguity. Moreover, for a vector x the diagonal matrix defined by the entries of x is denoted Diag(x) while for two (or more) matrices A, B, Diag[A, B] is the block diagonal matrix formed by A and B. For a matrix M, He(M) = M +M ′ .

Finally, for each integer q, ½ q denotes the vector in Ê q defined by ½ q = 1 . . . 1

′ . For any symmetric matrix, ⋆ stands for a symmetric term.

Design of local and of non-local controllers

Local case

In this section, we consider Assumption 1 and we design a state feedback ensuring local asymptotic stabilization of the origin for the system [START_REF] Andrieu | Homogeneous approximation, recursive observer design and output feedback[END_REF]. Note that if we introduce:

A 0 = A + GM 0 , φ 0 (x) = φ(x) -M 0 x , S 0 = N 0 -M 0 ,
system (1) can be rewritten as:

ẋ = A 0 x + B u + G φ 0 (x) , (5)
and the local sector condition becomes

φ 0 (x) ′ (φ 0 (x) -S 0 x) ≤ 0 , ∀ |x| ≤ v 0 . (6)
Hence, inspired by [START_REF] Castelan | Control design for a class of nonlinear continuous-time systems[END_REF][START_REF] Montagner | Robust absolute stability and nonlinear state feedback stabilization based on polynomial Lur'e functions[END_REF], we can state a sufficient condition to get local asymptotic stabilization of the origin:

Proposition 2.1. Suppose Assumption 1 is satisfied (hence (6) holds). If there exist a symmetric positive definite matrix W 0 in Ê n×n , two matrices H 0 in Ê m×n , and J 0 in Ê m×p and a positive real number η 0 satisfying the following inequality:

He(A 0 W 0 + BH 0 ) ⋆ J ′ 0 B ′ + η 0 G ′ + S 0 W 0 -2η 0 I p < 0 , (7)
then the control law u = α 0 (x) where

α 0 (x) = K 0 x + η -1 0 J 0 φ 0 (x) , (8)
with K 0 = H 0 W -1 0 makes the origin of the system a locally asymptotically stable equilibrium, with the basin of attraction containing the set

E(W -1 0 , R 0 ) = {x ∈ Ê n , x ′ W -1 0 x ≤ R 0 } where R 0 is any positive real number satisfying R 0 W 0 -v 2 0 I n ≤ 0 . (9)
Proof: Consider the Lyapunov function candidate V 0 (x) = x ′ P 0 x where P 0 = W -1 0 . The satisfaction of relation ( 9) means that the ellipsoid

E(P 0 , R 0 ) = {x ∈ Ê n , x ′ P 0 x ≤ R 0 } is included in the ellipsoidal set {x ∈ Ê n , |x| ≤ v 0 }. Thus, the sector condition (3) is satisfied for any x ∈ E(P 0 , R 0 ).
The time-derivative of V 0 along the trajectories of the system (5) with the control law (8) reads:

V0 (x) = x ′ [(A 0 + BK 0 ) ′ P 0 + P 0 (A 0 + BK 0 )] x + 2x ′ P 0 (B η -1 0 J 0 + G) φ 0 (x)
. Thus, by using the sector condition (3) and with η 0 > 0, it yields for all x ∈ E(P 0 , R 0 ):

V0 (x) ≤ V0 (x) -2η -1 0 φ 0 (x) ′ (φ 0 (x) -S 0 x
) . Hence, this implies, for all x ∈ E(P 0 , R 0 ), that:

V0 (x) ≤ x ′ φ 0 (x) ′ M 0 x φ 0 (x)
,

where M 0 ∈ Ê (n+p)×(n+p) is defined by:

M 0 = He(P 0 (A 0 + BK 0 )) ⋆ (η -1 0 J ′ 0 B + G ′ )P 0 + η -1 0 S 0 -2η -1 0 I p .
By pre-and post-multiplying relation [START_REF] Da | Anti-windup design with guaranteed regions of stability : an LMI-based approach[END_REF] by Diag[W -1 0 , η 0 I p ] = Diag[P 0 , η 0 I p ], it follows that M 0 < 0. Hence, if relation ( 7) is satisfied, one can conclude that V0 (x) < 0, for any x ∈ E(P 0 , R 0 ), x = 0. It follows that the origin of the system (5) closed by the control law ( 8) is locally asymptotically stable, and the ellipsoid E(P 0 , R 0 ) is included in the basin of attraction of the origin.

2

Note that the sufficient condition given by Proposition 2.1 is given in terms of solutions to linear matrix inequalities for which some powerful LMI solvers (see [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF] for instance) may be used as illustrated by the numerical examples given in Section 5. The feasibility of the LMI condition [START_REF] Da | Anti-windup design with guaranteed regions of stability : an LMI-based approach[END_REF] depends upon the matrices A 0 , B, G, S 0 and is independent of the radius v 0 defining the local sector condition. Once W 0 has been computed through the solution of ( 7), v 0 affects the size of the basin of attraction via the radius R 0 of the ellipsoid E(W -1 0 , R 0 ) obtained in (9).

Non-local case

A result similar to Proposition 2.1 can be obtained when considering Assumption 2. Indeed, with:

A ∞ = A + GM ∞ , φ ∞ (z) = φ(x) -M ∞ x -R ∞ , S ∞ = N ∞ -M ∞ , T ∞ = R ∞ -Q ∞ , system (1) becomes: ẋ = A ∞ x + B u + G φ ∞ (x) + GR ∞ , (10)
and the non-local sector condition (i.e. inequality ( 4)) yields:

φ ∞ (x) ′ (φ ∞ (x) -S ∞ x -T ∞ ) ≤ 0 , ∀ |x| ≥ v ∞ . (11)
With these data, a sufficient condition to get global asymptotic stabilization of a set containing the origin can be stated: Proposition 2.2. Suppose Assumption 2 is satisfied (hence (11) holds). If there exist a symmetric positive definite matrix W ∞ in Ê n×n , two matrices H ∞ in Ê m×n , and J ∞ in Ê m×p , two vectors L ∞ and m in Ê m and two positive real numbers η ∞ and τ ∞ satisfying the matrix inequality:

        < 0 , (12)
and the equality

′ m ½ m = τ ∞ (13)
then the control law u = α ∞ (x) where

α ∞ (x) = K ∞ x + η -1 ∞ J ∞ φ ∞ (x) + τ -1 ∞ L ∞ , (14)
with

K ∞ = H ∞ W -1
∞ makes the solutions of the closed-loop system complete and the set

E(W -1 ∞ , r ∞ ) = {x ∈ Ê n , x ′ W -1 ∞ x ≤ r ∞ } ,
globally and asymptotically stable where r ∞ is any positive real number such that

v 2 ∞ I n -W ∞ r ∞ ≤ 0 . ( 15
)
Proof: The Lyapunov function candidate is defined as

V ∞ (x) = x ′ P ∞ x, where P ∞ = W -1 ∞
which is symmetric positive definite. The time-derivative V ∞ along the trajectories of the system (5) with the control law ( 14) reads:

V∞ = x ′ [He(P ∞ A ∞ + P ∞ BK ∞ )]x + 2φ ∞ (x) ′ (Bη -1 ∞ J ∞ + G) ′ P ∞ x + 2(τ -1 ∞ BL ∞ + GR ∞ ) ′ P ∞ x .
Thus, by using the non-local sector condition (3), it follows, for all

x such that |x| ≥ v ∞ , V∞ ≤ x ′ [He(P ∞ A ∞ + P ∞ BK ∞ )]x + 2φ ∞ (x) ′ (Bη -1 ∞ J ∞ + G) ′ P ∞ x + 2τ -1 ∞ (BL ∞ + τ ∞ GR ∞ ) ′ P ∞ x -2 η -1 ∞ φ ∞ (x) ′ (φ ∞ (x) -S ∞ x -T ∞ ) -τ -1 ∞ (v 2 ∞ -x ′ x) . With the equality constraint (13) it yields, V∞ ≤ x ′ [He(P ∞ A ∞ + P ∞ BK ∞ )]x + 2φ ∞ (x) ′ (η -1 ∞ BJ ∞ + G) ′ P ∞ x +2τ -1 ∞ (BDiag(L ∞ )½ m + GR ∞ ′ m ½ m ) ′ P ∞ x -2 η -1 ∞ φ ∞ (x) ′ (φ ∞ (x) -S ∞ x -τ -1 ∞ T ∞ ′ m ½ m ) -τ -1 ∞ (½ ′ m ½ m v 2 ∞ m -x ′ x
) . This can be rewritten in matrix form as,

V∞ ≤   x φ ∞ ½ m   ′ M ∞   x φ ∞ ½ m   (16)
where

M ∞ =   He(P ∞ A ∞ + P ∞ BK ∞ ) + τ -1 ∞ I n ⋆ ⋆ (η -1 ∞ BJ ∞ + G) ′ P ∞ + η -1 ∞ S ∞ -2η -1 ∞ I p ⋆ τ -1 ∞ (Diag(L ∞ )B ′ + m R ′ ∞ G ′ )P ∞ η -1 ∞ τ -1 ∞ m T ′ ∞ -τ -1 ∞ v 2 ∞ m I m   .
The matrix M ∞ obtained by pre-and post-multiplying

M ∞ by Diag[W ∞ , η ∞ I p , τ ∞ I m ]
where

W ∞ = P -1 ∞ , is defined as M ∞ =   He(A ∞ W ∞ + BK ∞ ) + τ -1 ∞ W 2 ∞ ⋆ ⋆ (BJ ∞ + η ∞ G) ′ + S ∞ W ∞ -2η ∞ I p ⋆ Diag(L ∞ )B ′ + m R ′ ∞ G ′ m T ′ ∞ -τ ∞ v 2 ∞ m I m  
Applying Schur complement to inequality [START_REF] Montagner | Robust absolute stability and nonlinear state feedback stabilization based on polynomial Lur'e functions[END_REF] yields that M ∞ < 0. Hence, M ∞ < 0 and with [START_REF] Skelton | A unified approach to linear control design[END_REF], this implies that V∞ < 0 along the trajectories of (10) as long as the trajectories remain in the set {x, |x| ≥ v ∞ }. This implies completeness of the trajectories of system (1) closed by the control law [START_REF] Prieur | Uniting a high performance, local controller with a global controller: the output feedback case for linear systems with input saturation[END_REF]. Moreover, inequality (15) yields:

r ∞ |x| 2 ≥ v 2 ∞ x ′ P ∞ x , ∀ x ∈ Ê n .
Consequently, the set {x, |x| ≥ v ∞ } contains the set E(P ∞ , r ∞ ). Therefore:

V∞ (x) < 0 , ∀ x such that V ∞ (x) ≥ r ∞ ,
and the set E(P ∞ , r ∞ ) is globally asymptotically stable. 2

Design of a globally and asymptotically stabilizing controller

In this section, it is assumed that the local stabilization problem and the non-local one have been solved following Propositions 2.1 and 2.2. Hence, the controllers α 0 and α ∞ defined by ( 8) and ( 14) respectively and the Control Lyapunov Functions (CLF) x → x ′ P 0 x and x → x ′ P ∞ x are available. The problem is to unit these two controllers to get a controller making the origin a global and asymptotic stable equilibrium.

To solve this problem, the uniting strategy introduced in [START_REF] Andrieu | Uniting two control Lyapunov functions for affine Systems[END_REF] is employed. Following this procedure, the first step is to unit the local CLF x → x ′ P 0 x and the non-local one x → x ′ P ∞ x. The first requirement is that the two sets, in which we have a stability property, overlap. Assumption 3. Covering Assumption. There exist two positive real numbers R 0 and r ∞ such that ( 9) and ( 15) are satisfied and such that

r ∞ P 0 -R 0 P ∞ < 0 . (17)
In Figure 2, an illustration of the covering Assumption is presented (using the numerical values of Section 5.1). This assumption implies that we have the following inclusions:

{x, |x| ≤ v ∞ } ⊆ E(P ∞ , r ∞ ) ⊂ E(P 0 , R 0 ) ⊆ {x, |x| ≤ v 0 } .
To get a global stabilizing control law, we have the following result:

numbers (µ 1 , µ 2 , θ 1 , θ 2 , ν 1 , ν 2 , ν 3 , ν 4
) such that the following LMIs are satisfied:

  He(P 0 [A + BK m ]) -ν 1 P 0 + ν 2 P ∞ ⋆ ⋆ (J ′ m B ′ + G ′ )P 0 0 p×p ⋆ Diag(L m ) ′ B ′ P 0 0 m,p ν 1 R 0 -ν 2 r∞ m I m   -µ 1 Q 0 -Q ∞,1 < 0 , (18)
  He(P ∞ [A + BK m ]) + ν 4 P ∞ -ν 3 P 0 ⋆ ⋆ (J ′ m B ′ + G ′ )P ∞ 0 p,p ⋆ Diag(L m ) ′ B ′ P ∞ 0 m,p ν 3 R 0 -ν 4 r∞ m I m   -µ 2 Q 0 -Q ∞,2 < 0 , (19)
where

Q 0 =   He(M ′ 0 N 0 ) ⋆ ⋆ -(M 0 + N 0 ) 2I p ⋆ 0 m,n 0 m,p 0 m,m   , Q ∞,1 =   θ 1 He(M ′ ∞ N ∞ ) ⋆ ⋆ -θ 1 (M ∞ + N ∞ ) 2θ 1 I p ⋆ 1,1 (R ′ ∞ N ∞ + Q ′ ∞ M ∞ ) -1,2 (Q ′ ∞ + R ′ ∞ ) 2θ 1 m R ′ ∞ Q ∞ I m   , Q ∞,2 =   θ 2 He(M ′ ∞ N ∞ ) ⋆ ⋆ -θ 2 (M ∞ + N ∞ ) 2θ 2 I p ⋆ 2,1 (R ′ ∞ N ∞ + Q ′ ∞ M ∞ ) -2,2 (Q ′ ∞ + R ′ ∞ ) 2θ 2 m R ′ ∞ Q ∞ I m   , (20)
with the equality constraint

′ 1,1 ½ m = ′ 1,2 ½ m = θ 1 , ′ 2,1 ½ m = ′ 2,2 ½ m = θ 2 . ( 21
)
then there exists a continuous function α : Ê n → Ê m such that the control law u = α(x) makes the origin a globally asymptotically stable equilibrium for system [START_REF] Andrieu | Homogeneous approximation, recursive observer design and output feedback[END_REF].

Before proving this result, it has to be noticed that this result is not only an existence result but also a design procedure of a stabilizing controller. Indeed, a possible control law ensuring a global asymptotic stabilization of the origin of system (1) is given in [2, Theorem 3.1] and is expressed as:

α(x) = H(x) -k c(x) ∂V ∂x (x)B ′ (22)
with H a continuous function such that

H(x) = α 0 (x) if V ∞ (x) ≤ r ∞ α ∞ (x) if V 0 (x) ≥ R 0 .
The function c is any continuous function such that

c(x) = 0 if V 0 (x) ≥ R 0 or V ∞ (x) ≤ r ∞ > 0 if V 0 (x) < R 0 and V ∞ (x) > r ∞ .
k is a sufficiently large positive real number and finally V is a global CLF for system (1) obtained following the procedure introduced in [2, Theorem 2.1], which enables to unit both CLFs V 0 and V ∞ . Moreover, by solving this uniting problem, we get the existence of a neighborhood of the origin (namely the set {x, V ∞ (x) ≤ r ∞ }) such that all solutions of the closed-loop system with the control law α expressed by ( 22) enter this neighborhood in finite time and are such that, hereafter, along these solutions, the Lyapunov function V 0 is decreasing exponentially fast. Thus, by applying Theorem 3.1, the origin of the closed-loop system with the control law α is globally exponentially stable.

Proof: To prove Theorem 3.1, we apply the procedure introduced in [2, Theorem 2.1] that is based on the uniting of a local and a non-local control Lyapunov function. First, we introduce both functions V 0 (x) = x ′ P 0 x and V ∞ (x) = x ′ P ∞ x. Note that with Assumption 3, we get that both functions V 0 and V ∞ and both positive real numbers R 0 and r ∞ satisfy [2, Assumption 1]. More precisely, P 0 and P ∞ being solutions of Propositions 2.1 and 2.2, we get that the function V 0 satisfies, for all x in {x, V 0 (x) ≤ R 0 },

∂V 0 ∂x (x)[Ax + Bα 0 (x) + Gφ(Lx)] < 0, and V ∞ satisfies, for all x in {x, V ∞ (x) ≥ r ∞ }, ∂V ∞ ∂x (x)[Ax + Bα ∞ (x) + Gφ(Lx)] < 0.
Finally, with the covering assumption, the functions V 0 and V ∞ satisfy

{x, V ∞ (x) > r ∞ } ∪ {x, V 0 (x) < R 0 } = Ê n . and the set {x, V 0 (x) ≤ R 0 } ∪ {x, V ∞ (x) ≥ r ∞ } is a non empty compact subset of Ê n .
Moreover, setting u = K m x + J m φ(x) + L m yields along the trajectories of the system (1), V0

(x) = x ′ [P 0 (A + BK m ) + (A + BK m ) ′ P 0 ] x +2 x ′ P 0 (G + BJ m ) φ(x) + 2 x ′ P 0 B Diag(L m )½ m .
This inequality can be rewritten in matrix form as:

V0 (x) = x ′ φ(x) ′ ½ ′ m   He(P 0 [A + BK m ]) ⋆ ⋆ (J ′ m B ′ + G ′ )P 0 0 ⋆ Diag(L m ) ′ B ′ P 0 0 0     x φ(x) ½ m   . ( 23
)
Note that, for all x such that {x,

V 0 (x) ≤ R 0 } ∪ {x, V ∞ (x) ≥ r ∞ }: x ′ φ(x) ′ ½ ′ m   ν 1 P 0 -ν 2 P ∞ ⋆ ⋆ 0 0 ⋆ 0 0 ν 2 r∞-ν 1 R 0 m I m     x φ(x) ½ m   < 0, (24)
where (ν 1 , ν 2 ) are the positive real numbers given in Theorem 3.1. Moreover, with ( 9) and [START_REF] Prieur | Quasi-optimal robust stabilization of control systems[END_REF] we get that all x in the set {x,

V 0 (x) ≤ R 0 }∪{x, V ∞ (x) ≥ r ∞ } are in the set {x, v ∞ ≤ |x| ≤ v 0 }.
Hence, using both inequalities ( 3) and ( 4), we get, for all x in the set {x,

V 0 (x) ≤ R 0 } ∪ {x, V ∞ (x) ≥ r ∞ }, x ′ φ(x) ′ ½ ′ m [µ 1 Q 0 + Q ∞,1 ]   x φ(x) ½ m   < 0, ( 25
)
where Q 0 and Q ∞,1 are given in [START_REF] Teel | Uniting local and global controllers[END_REF]. Consequently, with inequalities (23), ( 24) and ( 25) and the property [START_REF] Tarbouriech | Advanced strategies in control systems with input and output constraints[END_REF], it yields that

V0 (x) < 0 , ∀x ∈ {x, V 0 (x) ≤ R 0 , V ∞ (x) ≥ r ∞ }.
With [START_REF] Tarbouriech | Stability analysis and stabilization of systems presenting nested saturations[END_REF], the same conclusion holds for V ∞ , i.e.:

V∞ (x) < 0 , ∀x ∈ {x, V 0 (x) ≤ R 0 , V ∞ (x) ≥ r ∞ }.
Consequently, a same control can be designed for both functions V 0 and From the previous results, a design strategy to get a stabilizing control law for system (1) may be described by the following algorithm:

V ∞ for each x in {x, V 0 (x) ≤ R 0 , V ∞ (x) ≥ r ∞ }. With [2,
Design separately a local and a non-local CLF (i.e. P 0 = W -1 0 and P ∞ = W -1 ∞ ) via the LMIs ( 7) and ( 12), and check if 1. they satisfy the covering Assumption [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF] with R 0 and r ∞ satisfying ( 9) and (15); 2. they satisfy the LMIs feasibility conditions ( 18) and ( 19) to be united.

If these two tests are positive then build the stabilizing control law given by (22).

Design in one step

In this section, we investigate the possibility of solving the design problem in one shot. In other words, we wish to find an LMI formulation to prove the existence of matrices P 0 and P ∞ satisfying the conditions in items 1) and 2) of the previous algorithm.

About the covering assumption

Assumption 3 may fail when considering an arbitrary pair of matrices P 0 and P ∞ computed using Propositions 2.1 and 2.2.

Moreover, note that inequality [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF], combined with Propositions 2.1 and 2.2, is not linear in P 0 or P ∞ since R 0 and r ∞ depend on P 0 and P ∞ through the constraints ( 9) and [START_REF] Prieur | Quasi-optimal robust stabilization of control systems[END_REF]

in which W 0 = P -1 0 and W ∞ = P -1 ∞ . Nevertheless, note that, when R 0 = r ∞ = 1
ρ , the covering Assumption can be easily defined as the following LMI:

W 0 -W ∞ > 0 . ( 26
)
Moreover, note that the two matrix inequality constraints ( 9) and ( 15) can be recast as the following LMI constraints:

ρv 2 ∞ I n -W ∞ ≤ 0 , W 0 -ρv 2 0 I n ≤ 0. ( 27
)
Consequently, this feasibility constraint can be added easily in the design of W 0 and W ∞ (i.e. of P 0 and P ∞ ). To summarize, we have: Proposition 4.1. Suppose there exist two positive definite matrices W 0 , W ∞ in Ê n×n and a real number ρ > 0 such that inequalities (26) and ( 27) are satisfied, then the covering assumption (i.e. inequality [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF]) is also satisfied with R 0 = r ∞ = 1 ρ .

About the second feasibility constraint

In this section, in order to ease the presentation, it is assumed that the two matrices Q ∞ and R ∞ , which appear in the definition of the non-local sector condition, are equal to zero. However, all the following results could be extended to the more general case.

To include the feasibility constraints ( 18) and ( 19) into the design of a global asymptotic stabilizer, we need to consider a specific class of matrices W 0 , H 0 , J 0 , W ∞ , H ∞ , and J ∞ solutions of ( 7), ( 12), ( 26), (27).

To be more precise, we consider the subclass of solutions such that the conditions ( 18) and ( 19) are satisfied and read as LMI conditions. Using elimination lemma [START_REF] Skelton | A unified approach to linear control design[END_REF], we get the following result. 4) are such that N 0 = N ∞ = 0 and Q ∞ = R ∞ = 0 and if there exist two symmetric positive definite matrices W 0 and W ∞ in Ê n×n , two matrices J m in Ê m×p and H m in Ê m×n , an invertible matrix F in Ê n×n , satisfying the LMI constraints

  He(AF + BH m ) ⋆ ⋆ -W 0 + F + AF + BH m -2W 0 BJ m + G -W 0 G (M 0 + M ∞ )F + (BJ m + G) ′ + AF + BH m ⋆ -4I p -He(G ′ (BJ m + G))   < 0, (28) 
 He(AF + BH m ) ⋆ ⋆ -W ∞ + F + AF + BH m -2W ∞ BJ m + G -W ∞ G (M 0 + M ∞ )F + (BJ m + G) ′ + G ′ (AF + BH m ) ⋆ -4I p -He(G ′ (BJ m + G))   < 0, (29)
then there exist positive real numbers ν 1 , ν 2 , ν 3 ν 4 , and vectors 1,1 , 1,2 , 2,1 and 2,2 in Ê m such that inequalities ( 18) and ( 19) and the equality (21) hold with

P 0 = W -1 0 , P ∞ = W -1 ∞ , K m = H m F -1 , µ 1 = µ 2 = θ 1 = θ 2 = 1, and L m = 0 m,1 .
Proof: First, note that pre-and post-multiplying inequality (28) respectively by Diag [F 1 , P 0 , I p ] and Diag [F ′ 1 , P 0 , I p ], with

F ′ 1 = F -1 , gives the following inequality.   He(F 1 (A + BK m )) ⋆ ⋆ P 0 -F ′ 1 + P 0 (A + BK m ) -2P 0 P 0 (BJ m + G) -G M 0 + M ∞ + (J ′ m B ′ + G ′ )F ′ 1 + G ′ (A + BK m ) ⋆ -4I p -He(G ′ (BJ m + G))   < 0.
This inequality, can be rewritten as

N 0 +   F 1 P 0 G ′   A + BK m -I n BJ m + G +   A ′ + K ′ m B ′ -I n J ′ m B ′ + G ′   F ′ 1 P 0 G < 0, with, N 0 =   0 ⋆ ⋆ P 0 0 ⋆ M 0 + M ∞ 0 -4I p   .
This implies that

a ′ b ′ c ′ N 0   a b c   < 0, for all (a, b, c) in Ê n × Ê n × Ê p such that A + BK m -I n BJ m + G   a b c   = 0. ( 30
)
Note that setting the matrix in Ê (n+p)×(2n+p)

K 0 =   I n 0 A + BK m BJ m + G 0 I n   ,
the set of points (a, b, c) in Ê 2n+p satisfying the constraint (30) is equal to the image of the matrix K 0 . Consequently, we get K ′ 0 N 0 K 0 < 0. Let ν 1 and ν 2 be such that

K ′ 0 N 0 K 0 + -ν 1 P 0 + ν 2 P ∞ ⋆ 0 n×p 0 p×p < 0, ν 1 R 0 -ν 2 r ∞ m < 0.
Note that this choice is always possible by taking for instance ν 1 = 0 and ν 2 small. This implies that we get

  He(P 0 [A + BK m ]) -ν 1 P 0 + ν 2 P ∞ ⋆ ⋆ (J ′ m B ′ + G ′ )P 0 + M 0 + M ∞ -4I p ⋆ 0 n,m 0 p,m ν 1 R 0 -ν 2 r∞ m I m   < 0.
This matrix inequality is exactly [START_REF] Tarbouriech | Advanced strategies in control systems with input and output constraints[END_REF] in the particular case where

µ 1 = θ 1 = 1, N 0 = N ∞ = 0, Q ∞ = R ∞ = 0 and with L m = 0 m,1 .
The proof that inequality [START_REF] Tarbouriech | Stability analysis and stabilization of systems presenting nested saturations[END_REF] holds with µ 2 = θ 2 = 1 follows the same line. Note that, in the particular case where Q ∞ = R ∞ = 0, the only constraint we have on the matrices 1,1 , 1,2 , 2,1 and 2,2 is the equality constraint (21) which has always a solution (for instance

1,1 = 1,2 = 2,1 = 2,2 1 m ½ m ). 2
By employing a change of variables similar to the one introduced in Sections 2.1 and 2.2, we can also deal with the case where N 0 = N ∞ = 0.

The key point of the previous result is that the constraints (28) and ( 29) are linear in the unknowns W 0 and W ∞ . Consequently, with Propositions 4.1, we are able to give a complete LMI formulation allowing to design a state feedback control law for system (1) making the origin a globally and asymptotically stable equilibrium. This can be summarized as follows.

Theorem 4.3. If the local and the non-local conditions (3) and ( 4) are such that N 0 = N ∞ = 0, Q ∞ = R ∞ = 0 and if there exist two symmetric positive definite matrices W 0 and W ∞ in Ê n×n , three matrices J 0 , J ∞ and J m in Ê m×p three matrices H 0 , H ∞ and H m in Ê m×n , an invertible matrix F in Ê n×n , and a real number ρ > 0 satisfying the matrix inequality ( 7), ( 12), ( 26), ( 27), ( 28) and (29), then the control law u = α(x) with α defined in (22) makes the origin a globally asymptotically stable equilibrium for system [START_REF] Andrieu | Homogeneous approximation, recursive observer design and output feedback[END_REF].

Proof: This proof is a direct consequence of Propositions 4.1 and 4.2 and Theorem 3.1. 2

Numerical examples

To illustrate the proposed procedure and to motivate it, three different examples are presented. The first one is an illustration of the proposed methodology to design a global stabilizing state feedback for a system satisfying Assumptions 1 and 2. The second one exhibits the interest of splitting in two pieces a global sector condition. The third one is an illustration of Theorem 4.3.

Example 1: Illustration of the methodology

In this section, we illustrate the design procedure by applying Theorem 3.1. Consider system (1) described by the following data:

ẋ = Ax + B u + Gφ(x), x ∈ Ê 2 , (31)
with A = 0 5 0 0 , B = 0 1 ′ , G = I 2 , φ is the nonlinear function defined as,

φ(x) = 1 2 [λ(|x|)(N ∞ x + Q ∞ ) + (1 -λ(|x|))N 0 x], with λ(s) =        10 -3 s , s ≤ v 0 20s -10 -3 v 0 20 , s ∈ v 0 , 20+10 -3 v 0 20 2 1 , s ∈ 20+10 -3 v 0 20 2
, +∞ and Q ∞ , N ∞ and N 0 are the matrices defined as

Q ∞ = -1 -6 , N ∞ = 4I 2 , N 0 = 0.1I 2 .
It can be checked that this function satisfies Assumptions 1 and 2 with the data v 0 = 14 and v ∞ = 2, M 0 = M ∞ = 0 and R ∞ = 0. Applying Propositions 2.1 and 2.2, we may compute the controllers α Figures 3 and4 show the behavior of the closed-loop system with the local controller and the non-local one obtained respectively from Propositions 2.1 and 2.2. Note that with the local controller the basin of attraction is a compact subset and that, with the non-local one, the trajectories do not converge toward the origin (but to another equilibrium).

0 : x → K 0 x + η -1 0 J 0 φ(x) and α ∞ : x → K ∞ x + η -1 ∞ J ∞ φ(x) + τ ∞ L ∞ with K 0 = -5.80 -1.23 , J 0 = 0.0130 -0.547 , η 0 = 0.445 , K ∞ = -76.4 -29 , J ∞ = 0.44 -2.4 , η ∞ = 0.93 , τ ∞ = 0.
The covering assumption, namely Assumption 3, is satisfied. This fact is depicted in Figure 2. Moreover, Theorem 3.1 applies and the controller (22) makes the origin a global asymptotically stable equilibrium with parameter k = 1 and the functions c given as:

c(x) = 1 1 + ∂V ∂x (x)B max(0, min((R 0 -x ′ P 0 x)(x ′ P ∞ x -r ∞ ), 1)).
Furthermore, V is obtained from [2, Equation ( 8)] with the parameters R 0 = 190 and r ∞ = 150. Figure 5 depicts the state trajectory of the closed-loop system and it can be checked that the solution converges toward the origin with the uniting controller.

Example 2: Necessity to split in two sector conditions

In this section, we check on an example that it may be necessary to split a sector condition in two sector conditions, and we illustrate the design procedure by applying Theorem 3.1. In this example, system (1) is given with the following data:

ẋ = B u + Gφ(x), x ∈ Ê 3 , (32)
with B = 1 0 0 ′ , G = I 3 . To complete the definition of system (1), it remains to introduce the function φ : Ê 3 → Ê 3 representing the nonlinearity of the system. First consider both matrices M ∞ in Ê 3×3 and N 0 in Ê 3×3 defined as

M ∞ =   0 0 0 0 0 1 1 0 0   , N 0 =   0 0 0 1 0 0 0 1 0   .
The nonlinear function φ is defined as a locally Lipschitz continuous path interpolating M ∞ and N 0 , i.e5 :

φ(x) = λ(|x|)M ∞ x + (1 -λ(|x|))N 0 x, x ∈ Ê 3 , (33)
where λ : Ê + → Ê + is an increasing locally Lipschitz function such that6 :

λ(0) = 0, lim s→+∞ λ(s) = 1.
We wish to find a controller guaranteeing global asymptotic stabilization of the origin.

where the functions g 1 and g 2 are any continuous functions such that:

g 1 (x) ≤ 1 if |x| ≤ v 0 ≤ 2 if |x| ≥ v 0 , g 2 (x) ≤ 1 if |x| ≤ v ∞ ≤ 0.5 if |x| ≥ v ∞ .
Note that this system can be written in the form (1) with A = 0 1 0 0 , B = 0 1 ′ , G = L = I 2 , and with the function φ(x) = x 1 g 1 (x) Hence, we are in the context of Theorem 4.3. Employing YALMIP [START_REF] Löfberg | Yalmip : A toolbox for modeling and optimization in MATLAB[END_REF] with the solver SEDUMI [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF], we check the solvability of LMIs ( 7), ( 12), ( 26), ( 27), (28), and (29). These LMIs are solvable with: and finally ρ = 0.068. Consequently, the conclusion of Theorem 4.3 holds and we obtain a control law making the origin a globally and asymptotic stable equilibrium for the system (36).

Conclusion

In this paper we have introduced the synthesis problem of a nonlinear feedback law for a class of control systems. The control systems under consideration are those with a nonlinearity satisfying a sector condition when the state is close to the equilibrium and a (maybe) different sector condition when the state is distant from the equilibrium. We noted that encompassing both sector conditions into a unique global one may lead to a too conservative synthesis problem. This motivates us to consider both properties of the nonlinearities separately and to design successively 1) a local asymptotic stabilizing nonlinear controller whose basin of attraction contains some compact set and 2) a non-local controller which makes the previous compact set globally attractive. Then, we compute a nonlinear controller which pieces together the local controller with the non-local one, and we obtain a global asymptotic stabilizing controller. We emphasize that the sufficient conditions to solve this design problem are written in terms of LMIs. Three numerical examples motivate and illustrate this approach.

Theorem 3 . 1 .

 31 Assume that Assumptions 1, 2 and 3 hold. If there exist two matrices K m in Ê m×n and J m in Ê m×p , five vectors L m , 1,1 , 1,2 , 2,1 , and 2,2 in Ê m and eight positive real

Proposition 4 . 2 .

 42 If the local and the non-local conditions (3) and (

x 2 g 2

 2 (x) . The function φ(x) satisfies Assumptions 1 and 2 with N 0 = N ∞ = 0 , M 0 = I 2 , M ∞ = Diag[2, 0.5].

J

  ∞ = -1.7 0.68 ,J m = -1.3 0.021 ,H 0 = -2.1 -6.0 , H ∞ = -1.2 -3.4 ,H m = 0.85 -3.7 ,F = 0.73 -0.44 -0.95 1.2 ,

Figure 1 :

 1 Figure 1: Illustration of a nonlinear function satisfying two different sector conditions.

2 Figure 2 : 2 Figure 3 : 2 Figure 4 : 2 Figure 5 :

 22232425 Figure 2: Illustration of the Covering Assumption for numerical Example 1

  Proposition 2.2], we get that [2, Assumption 2] is also satisfied. Consequently, all Assumptions of [2, Theorem 3.1] are satisfied and there exists a control law ensuring global asymptotic stabilization of the origin of system (1).2

  0896 , L ∞ = 0.527 such that the conclusion of Propositions 2.1 and 2.2 holds with

	P 0 =	1.13 0.144 0.144 1.00	, R 0 = 178 , P ∞ =	46.3 15.7 15.7 8.17	, r ∞ = 183.8474.

He(A ∞ W ∞ + BH ∞ ) ⋆ ⋆ ⋆ (BJ ∞ + η ∞ G) ′ + S ∞ W ∞ -2η ∞ I p ⋆ ⋆ Diag(L ∞ )B ′ + m R ′ ∞ G ′ m T ′ ∞ -τ ∞ v 2 ∞ m I m ⋆ W ∞ 0 n,p 0 n,m -τ ∞ I n

This is typically the case when a system is modeled as an interpolation of several linear systems.

For instance λ can be defined by λ(s) = 2 π arctan(s) for all s ≥ 0.

Note that the proof of Proposition 5.1 does not use the expression of the system (1) but only properties of the nonlinearity φ as introduced in (33).

Employing a unique global sector condition

A first strategy to address the stabilization problem for system (32) is to check if the solvability conditions inspired by [START_REF] Castelan | Control design for a class of nonlinear continuous-time systems[END_REF][START_REF] Montagner | Robust absolute stability and nonlinear state feedback stabilization based on polynomial Lur'e functions[END_REF] are satisfied. To this end, let us first prove that the nonlinear function φ satisfies a (global) sector condition 7 : Proposition 5.1. The function φ defined in (33) satisfies the sector condition:

Proof: Note that we have:

This concludes the proof of Proposition 5.1.

2

Following the computations of (the proof of) Proposition 2.1, we may try to compute a global nonlinear feedback law by solving the following LMI optimization problem: Proposition 5.2. If there exist a symmetric positive definite matrices W in Ê 3×3 , and two matrices H in Ê 1×3 , J in Ê satisfying the LMI:

then the control law:

with K = HW -1 makes the origin a globally and asymptotically stable equilibrium for system (32).

Using parser YALMIP [START_REF] Löfberg | Yalmip : A toolbox for modeling and optimization in MATLAB[END_REF] and LMI solver SeDuMi [START_REF] Sturm | Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones[END_REF], this problem is found to be unfeasible on this particular instance. This approach is clearly too conservative and cannot be used in this specific case. This motivates us to split the sector condition in two different sector conditions as done in the following section.

Employing the uniting controller approach

Note however that our uniting controller provides another approach to solve this stabilizing problem. First, we show that the function φ introduced in (33) satisfies Assumptions 1 and 2.

Proposition 5.3. Given two positive real numbers 0 < λ ∞ < λ 0 < 1, Assumptions 1 and 2 are satisfied with

Proof: The proof is similar to the proof of Proposition 5.2. First, note that the function λ being strictly increasing, we have:

Moreover, we have

and consequently, with (35), for all x such that {x, |x| ≤ v 0 }, we have

and Assumption 1 is satisfied. Similarly, we show that Assumption 2 is satisfied. 2 Consequently, we are in the framework of the uniting sector condition. We follow the procedure developed in Sections 3 and 4.1, and we apply Propositions 2.1, 2.2, and 4.1. Therefore we have to check if the LMIs ( 7), ( 12), ( 26) and ( 27) have a solution in W 0 , W ∞ , and ρ (among others variables), and we get that Assumption 3 holds for

ρ . Choosing λ 0 = 0.6 and λ ∞ = 0.4, and assuming that λ is a continuous function such that: Hence, we are in the context of Theorem 3.1 and we can check that, for the two previous matrices P 0 and P ∞ there exist two matrices J m , K m and four scalars µ i satisfying the sufficient conditions ( 18) and [START_REF] Tarbouriech | Stability analysis and stabilization of systems presenting nested saturations[END_REF]. This is indeed the case with

Consequently, the conclusion of Theorem 3.1 holds and we get that the control law (22) makes the origin a globally and asymptotic equilibrium for the system (32).

Example 3: Design of a stabilizing controller in one step

In this section, we apply Theorem 4.3 and we design a stabilizing controller in one step. To this end, let us consider now a second order system defined as: ẋ1 = x 2 + x 1 g 1 (x), ẋ2 = u + x 2 g 2 (x), (36)


The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code Guilhem Jaber 1,2 and Nicolas Tabareau 3

1 ENS Cachan 2 École des Mines de Nantes 3

INRIA

Abstract. Logical relations appeared to be very fruitful for the development of modular proofs of compiler correctness. In this field, logical relations are parametrized by a high-level type system, and are even sometimes directly relating low level pieces of code to high-level programs. All those works rely crucially on biorthogonality to get extensionality and compositionality properties. But the use of biorthogonality in the definitions also complicates matters when it comes to operational correctness. Most of the time, such correctness results amount to show an unfolding lemma that makes reduction more explicit than in a biorthogonal definition. Unfortunately, unfolding lemmas are not easy to derive for rich languages and in particular for assembly code. In this paper, we focus on three different situations that enable to reach step-by-step the assembly code universe: the use of Curry-style polymorphism, the presence of syntactical equality in the language and finally an ideal assembly code with a notion of code pointer.

Logical relations-and more particularly biorthogonal logical relations-have shown to be very fruitful for the development of modular proofs of compiler correctness. Such biorthogonal logical relations are indexed by a high-level type system. When focusing on a particular high level language for compiler correctness, logical relations relate low level pieces of code to high-level programs [START_REF] Benton | Biorthogonality, step-indexing and compiler correctness[END_REF][START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF]. But to give an intrinsic semantics to assembly code, they can also relate directly low level pieces of codes together [START_REF] Benton | Compiling functional types to relational specifications for low level imperative code[END_REF]. In this paper, we will focus on this second line of work. All those works rely crucially on biorthogonality definitions to get extentionality and compositionality properties. Indeed, using it we can define good terms in a logical relation as those which interact well with good contexts, rather than defining them explicitly. More precisely, orthogonality is used to lift relations on values to relations on terms. Indeed, logical relations are defined in three layers. A relation on values V τ is defined for each type τ of the high-level type system, then relations on context

K τ = {(K 1 , K 2 ) | ∀(v 1 , v 2 ) ∈ V τ .O(K 1 [v 1 ], K 2 [v 2 ])}
are obtained by considering contexts that interacts well with values of V τ , which is called the orthogonal of V τ . Orthogonality is defined with respect to an abstract notion of observation O that will be equitermination in this paper. Finally, relations on terms

E τ = {(t 1 , t 2 ) | ∀(K 1 , K 2 ) ∈ K τ .O(K 1 [t 1 ], K 2 [t 2 ])}
are obtained by taking the orthogonal of K τ . But biorthogonality also complicates matters when it comes to operational correctness. Indeed, such results rely on the fact V τ and E τ match on values. Such a result is proved using the intuition that good contexts of type τ has to be seen as tests for type τ . Then, one has to investigate the discriminating power of such contexts. For instance, when contexts are very weak, good terms can be any terms, and to the opposite, when they are very powerful, good terms are only good values.

In this article, we will focus on three different situations related to assembly code. First, we will work in the context of a Curry-style polymorphic λ-calculus, wondering if contexts should be allowed to test terms more than one time with different types. This is an important issue in the assembly code framework, because Church-style polymorphism is hardly expressible at this level. Then we will deal with contexts that can use intentional equality on terms during the test, wondering if in this case contexts are too powerful and discriminate too many terms. Indeed, in assembly code, it is easy to express such contexts using pointer arithmetic. Finally, we will use those two case studies to investigate how to define contexts for an ideal assembly code, with a notion of code pointer. In this case, we have to give up the usual representation of a context as term with an hole. As in [START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF], we will rather define contexts has return addresses. Then, we will see that our two previous results still fit well in this low-level setting.

Biorthogonal Logical Relations for a polymorphic

Curry-style λ-calculus

In this part, we will focus on Curry-style λ-calculus, which is useful in our enterprise to deal with low-level code. Indeed, the main difference between Curry-style and Church-style polymorphism is that there is no explicit values Λα.τ in Currystyle, which is the case for many assembly languages.

The Language

We consider a standard call-by-value λ-calculus with universal polymorphism, noted L. The syntax, typing rules and operational semantics of this language are defined in Figure 1. In each typing rule, ∆ is the context for free type variables, and Γ for free term variables. Figure 2 introduces standard type indexed logical relations for L. The relations K τ and E τ are defined in terms of an abstract notion of observation O, which will be instantiated by the equidivergence relation. Notice that stuck terms which are not values are not in O. Because of universal quantification, we have to deal with open types. This is the purpose of the environment η which associates relations on terms to free type variables. In the definition of V ∀α.τ η , Rel σ1,σ2 is the set of relations on values of types σ 1 and σ 2 .

Syntax Type τ, σ def = Nat | Unit | α | τ → σ | ∀α.τ Val u, v def = n | () | λx.t (where n ∈ Nat) Term t def = v | x | t1t2 Cont K def = • | Kt | vK Operational semantic (λx.t)v → t {v/x} t1 → t2 K[t1] → K[t2]
Typing rules

(x : τ ) ∈ Γ ∆; Γ ⊢ x : τ ∆; Γ ⊢ n : Nat ∆; Γ ⊢ () : Unit ∆; Γ ⊢ t : τ → σ ∆; Γ ⊢ u : τ ∆; Γ ⊢ tu : σ ∆; Γ, x : τ ⊢ t : σ ∆; Γ ⊢ λx.M : τ → σ ∆; Γ ⊢ t : ∀α.τ F V (σ) ⊆ ∆ ∆; Γ ⊢ t : τ {σ/α} ∆, α; Γ ⊢ t : τ ∆; Γ ⊢ t : ∀α.τ

Parametricity

As it is well known, terms in V ∀α.τ and E ∀α.τ have to be parametric, i.e. uniform with respect to the instantiation of α. This is due to the different instantiation of α in the definition of V ∀α.τ η , with σ 1 on the left and σ 2 on the right. This enforces good terms not to adapt their behaviour to the instantiated type. For example, consider the instruction isBool whose semantics is :

isBool u → true if u is a boolean (true or false) false otherwise
isBool has type ∀α.(α → Bool) but has a very different behaviour when used with a boolean or with a term of another type. This means that isBool is not parametric. Indeed, we can prove that (isBool, isBool) / ∈ V ∀α.α → Bool . Consider the relation r ∈ Rel Bool,Nat defined by r = {(true, 0)}, then we should have (isBool true, isBool 0) ∈ E Bool which is false since isBool true → true and isBool 0 → false.

V α η def = {η(α)} ⊥v ⊥ k V Unit η = {((), ())} V Nat η def = {(n, n) | n ∈ Nat} V τ → σ η = {(u1, u2) | ∀(v1, v2) ∈ V τ η .(u1v1, u2v2) ∈ E σ η } V ∀α.τ η = {(v1, v2) | ∀σ1, σ2 : Type, ∀r ∈ Relσ 1 ,σ 2 .(v1, v2) ∈ V τ η,α →r } K τ η def = V τ ⊥ k η E τ η def = K τ ⊥ t η X ⊥ k def = {(K1, K2) | ∀(v1, v2) ∈ X, O(K1[v1], K2[v2])} X ⊥v def = {(v1, v2) | ∀(K1, K2) ∈ X, O(K1[v1], K2[v2])} X ⊥ t def = {(t1, t2) | ∀(K1, K2) ∈ X, O(K1[t1], K2[t2])}

Fundamental property of the logical relation

Let us now prove that terms of types τ are in the diagonal of E τ . To do so, we have to prove the so-called compatibility lemmas-one for each typing rulewhich make the induction on typing derivations possible. But the one about the introduction rule of the of the universal quantifier is problematic in Curry-style, due to the absence of proper values of type ∀α.τ . To be able to prove it, we have to unfold biorthogonality to get a direct definition of E τ in terms of V τ . Lemma 1. For every type τ, σ and every relation r ∈ Rel σ and every environment η,

-V ∀α.τ η ⊆ V τ η•[α →r] -K τ η•[α →r] ⊆ K ∀α.τ η -E ∀α.τ η ⊆ E τ η•[α →r]
Proof. The first inclusion is direct by definition, the other ones come from the basic properties of orthogonality.

Lemma 2 (Adequacy of E and V on values). For every type τ , every map

η s.t. dom(η) = F V (τ ) and every values v 1 , v 2 , (v 1 , v 2 ) ∈ E τ η iff (v 1 , v 2 ) ∈ V τ η
Proof. The proof is done by induction on τ :

-If τ is a type variable α, then E α η = η(α) ⊥t⊥ k ⊥v⊥ k ⊆ η(α) ⊥v⊥ k ⊥v⊥ k = η(α) ⊥v⊥ k = V α η -If τ is ∀α.τ , then Let (v 1 , v 2 ) ∈ E ∀α.τ η , we will prove that (v 1 , v 2 ) ∈
V ∀α.τ η , i.e. for every couple of types (σ 1 , σ 2 ) and every relation r ∈

Rel σ1,σ2 , (v 1 , v 2 ) ∈ V τ η•[α →r]
. By induction hypothesis we can simply show

that (v 1 , v 2 ) ∈ E τ η•[α →r] , i.e. for every (K 1 , K 2 ) ∈ K τ η•[α →r] , O(K 1 [v 1 ], K[v 2 ]).
But from Lemma 1 we know that such (K 1 , K 2 ) are in fact in K ∀α.τ η so we can conclude since (v 1 , v 2 ) ∈ E ∀α.τ η . -The proof of other cases are classic, see [?].

Lemma 3 (Unfolding of biorthogonality). Let t 1 , t 2 be two terms, then (t 1 , t 2 ) ∈ E τ η iff t 1 , t 2 both diverge or there exists two values

(v 1 , v 2 ) ∈ V τ η s.t. t i → * v i .
Proof. -Direct side : If (t 1 , t 2 ) ∈ E τ η do not both diverge, then they both normalize since the empty context is in the diagonal of K τ η . So from Lemma 2, there exists values

(v 1 , v 2 ) ∈ V τ η s.t. t i → * v i . -Reverse side : Let (K 1 , K 2 ) ∈ K τ η , then from (K 1 [v 1 ], K 2 [v 2 ]) ∈ O we get (K 1 [t 1 ], K 2 [t 2 ]) ∈ O, i.e. (
, (v 1 , v 2 ) ∈ V τ η•α →r and t i → * v i , i.e. (v 1 , v 2 ) ∈ V ∀α.
τ η , and we conclude using the reverse side of lemma 3.

Thanks to this lemma, we can prove the desired theorem.

Theorem 1 (Fundamental property). Let t be a term such that ∆, Γ ⊢ t : τ , then for every environment γ and η compatible respectively with Γ and ∆, we get (γt, γt) ∈ E τ η

Proof. The proof is done by induction on the typing proof, using compatibility lemmas.

Finally, here is an example of what kind of operational correctness results we can get.

Theorem 2 (Operational correctness for the type Nat). If (t 1 , t 2 ) ∈ E Nat then t 1 and t 2 both diverges or there exists n ∈ Nat such that t 1 and t 2 both normalize to n.

Proof. Straightforward using lemma 3 and the definition of V Nat .

Addition of mutable states

To deal with the problem of program equivalence for a language with mutable states, the so-called Kripke logical relations have been developed [START_REF] Pitts | Operational reasoning for functions with local state[END_REF]. The idea is to use a notion of world to represent relations on heaps. Building such worlds in presence of higher-order references is difficult, since there is circularity problems in the definition. To overcome this problem, it is now common to use step-index

Syntax Type τ, σ def = Nat | Unit | α | τ → σ | ∀α.τ | ref τ Val u, v def = n | () | λx.t | l (where n ∈ Nat and l ∈ Loc) Term t def = v | x | t1t2 | ref τ t | t1 := t2 | !t Cont K def = • | Kt | vK | ref τ K | K := t | v := K | !K Operational semantic ((λx.t)v, h) → (t {v/x} , h) (ref v, h) → (l, h • [l → v]) (l := v, h) → ((), h[l → v]) (!l, h) → (h(l), h) (t1, h1) → (t2, h2) (K[t1], h1) → (K[t2], h2)
New typing rules

Υ (l) = T ∆; Γ ; Υ ⊢ l : ref T ∆; Γ ; Υ ⊢ t : τ ∆; Γ ; Υ ⊢ ref t : ref τ ∆; Γ ; Υ ⊢ t1 : ref τ ∆; Γ ; Υ ⊢ t2 : τ ∆; Γ ; Υ ⊢ t1 := t2 : Unit ∆; Γ ; Υ ⊢ t : ref τ ∆; Γ ⊢!t : τ Fig. 3. The Extention L ref .
method [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF] which induces a stratification on worlds. However, it is possible to hide completely such technicalities in the definition, as it is shown in [START_REF] Jaber | Decomposing Logical Relations with Forcing[END_REF].

In fact here we only want to prove the fundamental lemma, i.e. to prove (t, t) ∈ E τ , so we can work with really simple world, which are predicates on heaps, specifying the free locations l of t. More precisely, from a typing environment Υ of free location one associate the world

w def = {(l, v, w ′ ) | l ∈ dom(Υ ), v is in the diagonal of V Υ (l) w ′ ,η }
We will call such worlds "simple predicative". In the following, we will note h ∈ w as a shortcut for dom(h) = dom(w) ∧ ∀l ∈ dom(h), (l, h(l), w) ∈ w. Such worlds can be useful only if the type system ensure weak updates of heap (i.e. type preserving one).

Lemma 5 (Weak updates). If

∆; Γ ; Υ ⊢ t : τ and h is a heap satisfying Υ and (t, h) → * (t ′ , h ′ ), then h ′ satisfies Υ .
Proof. This property is ensure by the restriction of monomorphic types for references.

Then we will have to consider only typable terms in our logical relations to get this property.

Lemma 6 (One-Step Unfolding of biorthogonality). Let t be a typable term which is not a value and w a simple predicative world, then (t, t) ∈ E τ w,η iff for all heaps h ∈ w, there exists a simple predicative world

w ′ ⊒ w, a term t ′ s.t. (t ′ , t ′ ) ∈ E τ w ′ ,η and a heap h ′ ∈ w ′ s.t. (t, h) → (t ′ , h ′ ).
Proof. -Direct side : For every heap h ∈ w there exists a unique term t ′ and heap h ′ such that (t, h) → (t ′ , h ′ ). We are going to build the world w ′ ⊒ w by case analysis on this reduction step :

• If h ′ = h then we can simply take w ′ = w.

• If t can be written as K[ref τ v] and t ′ as K[l] then then one can take

w ′ = w ∪ {((l, w ′′ , v) | (v, v) ∈ V τ w ′′ ,η ]} • If If t can be written as K[l := v],
then from lemma 5, h ′ will be in w so we take w ′ = w. -Reverse side : Let (K 1 , K 2 ) ∈ K τ w,η then we have to show

((K 1 [t], h), (K 2 [t], h)) ∈ O.
To do so we will just prove that ((K

1 [t ′ ], h ′ ), (K 2 [t ′ ], h ′ )) ∈ O,
which comes from the fact that (t ′ , t ′ ) ∈ E τ w ′ ,η and by monotonicity of K τ with respect to worlds, (K 1 , K 2 ) ∈ K τ w ′ ,η .

Lemma 7 (Adequacy of E and V on values). For every type τ , every map η s.t. dom(η) = F V (τ ), every values v 1 , v 2 and every world w,

(v 1 , v 2 ) ∈ E τ w,η iff (v 1 , v 2 ) ∈ V τ w,η
Proof. Same as for lemma 2.

Lemma 8 (Unfolding of biorthogonality). Let t be a typable term and w a simple predicative world, then (t, t) ∈ E τ w,η iff for all heaps h ∈ w, (t, h) diverges or there exists a simple predicative world w ′ ⊒ w, a value v in the diagonal of V τ w,η and a heap h ′ ∈ w ′ s.t. (t, h) → * (v, h ′ ).

Proof. -Direct side : The proof is done combining lemmas 6 and 7.

-Reverse side : Let (K 1 , K 2 ) ∈ K τ w,η then we have to show

((K 1 [t 1 ], h 1 ), (K 2 [t 2 ], h 2 )) ∈ O.
To do so we will just prove that ((K

1 [v 1 ], h ′ 1 ), (K 2 [v 2 ], h ′ 2 )) ∈ O, which comes from the fact that (v 1 , v 2 ) ∈ V τ w ′ ,η and by monotonicity of K τ with respect to worlds, (K 1 , K 2 ) ∈ K τ w ′ ,η .
Notice that this lemma is too weak to be useful to get operational correctness from (t 1 , t 2 ) ∈ E τ , since it talks only about the diagonal of E τ . It seems hard to extend this result to the whole relation, since we do not know how to build w ′ ⊒ w when worlds are relations on heaps and terms t 1 and t 2 do not modify their heap in the same way. This seems to be a weakness of Kripke logical relations, since worlds are only preconditions and there is no postconditions which assert the way the heap is modified by the terms. We plan to further investigate this point using the language of separation logic, more precisely Hoare Type Theory [START_REF] Nanevski | Polymorphism and Separation in Hoare Type Theory[END_REF], to extend logical relations with postconditions. Nevertheless, it is enough to prove the compatibility lemma for the introduction rule of the universal quantifier.

Lemma 9 (Compatibility lemma for the polymorphic introduction rule). Let t 1 , t 2 be two typable terms such that for every type σ 1 , σ 2 and every relation

r ∈ Rel σ1,σ2 , (t 1 , t 2 ) ∈ E τ w,η•α →r then (t 1 , t 2 ) ∈ E ∀α.τ w,η Γ ⊢ t : σ Γ ⊢ σ<:τ Γ ⊢ t : τ Γ ⊢ t : σ Γ ⊢ t : τ Γ ⊢ t : σ ∩ τ
Then we define V σ ∩ τ = V σ ∩ V τ while K σ ∩ τ and E σ ∩ τ are defined as usual by orthogonality. We can easily check that the previous proof of the various lemmas are still working.

Lemma 10. For every types σ, τ , σ<:τ implies E σ η ⊆ E τ η .

Proof. By induction on the proof of σ<:τ :

-If σ = α → β and τ = α ′ → β ′ with α ′ <:α and ⊢ β<:β ′ , then we have to prove that for all (t

1 , t 2 ) ∈ E α → β and (v 1 , v 2 ) ∈ V α ′ , (t 1 v 1 , t 2 v 2 ) ∈ E β .
By induction hypothesis, (v 1 , v 2 ) ∈ E α , and using lemma 2 we get that (v 1 , v 2 ) ∈ V α , so we can easily conclude.

-If σ = α ∩ τ and τ = α then one has to unfold biorthogonality using lemma 3, following the same proof than lemma 4.

However, compared to values in V ∀α.τ , those in V σ ∩ τ does not have to have the same behaviour for σ and τ . For example the function λn.if n > 0 then n else Ω is in the diagonal of V (Nat 0 → Nat 0 ) ∩ (Pos → Pos) . In comparison, terms in V ∀α.τ equidiverge regardless of the instantiation of α. In fact one can even prove that isBool is in the diagonal of V (Nat → Bool) ∩ (Bool → Bool) .

Notice that all these results are still true when we add an implicit depend types ∀n : Nat.τ n as in [START_REF] Benton | Compiling functional types to relational specifications for low level imperative code[END_REF], with the following subtyping rule Γ ⊢ ∀n : Nat.τ n <:τ n Then V ∀n : Nat.τ n η is defined as

n∈N V τ n 2 Intentional

equality

Like in [START_REF] Benton | Step-indexing: the good, the bad and the ugly[END_REF], we consider a language with an intentional equality, and we are going to investigate the discriminating power of contexts in this setting. More precisely, consider the language L α where we add to L the relation ≃ α encoding α-equivalence: t 1 ≃ α t 2 iff t 1 and t 2 are α-equivalent.

We will note Val α and Term α the corresponding syntactical classes of L α .

Adding such an intentional equality, contextual equivalence collapses to syntactical equality, so one should not seek correctness of logical relations anymore. But if we consider our previous logical relation E, this relation collapse to V on basic types. Indeed let K = if • ≃ α n then Ω else (), then we have (K, K) ∈ K Nat and (K, K) will be able to discriminate between a term t which reduces to n and the value n, so E Nat = V Nat .

To avoid this problem we have to restrict contexts to the form

Cont α = {let x = • in M | M ∈ Term α }
Then we force the evaluation of the term to happen first, and only the value we get as the result can be tested. As we will see later, this is in fact the shape of low-level contexts. The addition of ≃ α breaks the rule

t 1 → t 2 K[t 1 ] → K[t 2 ] .
which provides an up-to context reasoning for operational semantics. But if we know that K 1 , K 2 are in this restricted shape, this rule is true again, so does the unfolding of biorthogonality.

Consider

K α τ def = {(K 1 , K 2 ) ∈ Cont α .∀(v 1 , v 2 ) ∈ V τ , (K 1 [v 1 ], K 2 [v 2 ]) ∈ O} and
E α τ = {(t 1 , t 2 ) ∈ Term.∀(K 1 , K 2 ) ∈ K α τ , (K 1 [t 1 ], K 2 [t 2 ]) ∈ O}.
Here V τ corresponds to the previous relation on Val, and not on Val α , while E τ is restricted to elements of Term and not of Term α . Indeed, we are only interested in the logical relations on elements of L, and we just want to see if extending the power of contexts changes something, which is not the case :

Theorem 3. For every type τ and every environment η, E α τ η = E τ η .

Proof. First we prove E τ ⊆ E α τ . Let (e 1 , e 2 ) ∈ E τ , then unfolding biorthogonality we know that (e 1 , e 2 ) both diverge or there exists

(v 1 , v 2 ) ∈ V τ such that e i → * v i . But since K α τ = V τ ⊥ , taking (K 1 , K 2 ) ∈ K α τ we get (v 1 , v 2 )⊥(K 1 , K 2 )
, so (e 1 , e 2 )⊥(K 1 , K 2 ), i.e. (e 1 , e 2 ) ∈ E α τ .

Finally, K τ ⊆ K α τ , because they are orthogonal of the same set of values -not with the same notion of orthogonality, but Cont ⊆ Cont α -so E α τ ⊆ E τ .

Looking carefully at the proof, we see that it does not depend on the new added instruction-here ≃ α -but relies only on the possibility to unfold biorthogonality. Of course, it is not always the case, even with restricted shapes of contexts, as one can see by considering the call/cc instruction.

Logical Relations for Assembly code

Now we will investigate previous results in the setting of low-level code.

A variant of the SECD

We will work with an ideal assembly code, represented by a variant of the SECD machine. Compared to previous articles [START_REF] Jaber | Krivine realizability for compiler correctness[END_REF], [START_REF] Benton | Biorthogonality, step-indexing and compiler correctness[END_REF], we use a machine with an explicit code pointer. Indeed, while with λ-calculus or usual abstract machines we can define contexts as code with an hole (and possibly an environment and a stack), this is no more possible when we have an explicit code pointer, since code has to be constant. The machine is defined in Figure 1.

Notice that the instruction Stop has no reduction rule. Indeed, it is here to indicate final configurations. Then, the whole compiled program associate to a term t will be compile (t, 0)++ [Stop], where compile is defined in Figure 2. But to prove operational correctness for compile (t, 0), this is in fact compile (t, 0)++[Return] which will be used, to force context in the dump to be evaluated.

We keep O as the equidivergence, but one has to define what it means to be a good final configuration, to avoid stuck configurations. (l, e, s, d) is a good final configuration with respect to c if :

-l = size(c) + 1 -s = [v] -d = []

Fig. 1 .

 1 Fig. 1. The Language L.

Fig. 2 .

 2 Fig. 2. Logical relations for L

  t 1 , t 2 ) ∈ E τ η . Lemma 4 (Compatibility lemma for the polymorphic introduction rule). Let t 1 , t 2 be two terms such that for every types σ 1 , σ 2 and every relation r ∈ Rel σ1,σ2 , (t 1 , t 2 ) ∈ E τ η•α →r then (t 1 , t 2 ) ∈ E ∀α.τ

η Proof. By Lemma 3, there are two cases. Either t 1 and t 2 both diverge then they are trivially in E ∀α.τ η . Otherwise there exists (v 1 , v 2 ) s.t. for every types σ 1 , σ 2 and every relation r ∈ Rel σ1,σ2

Proof. Same as for lemma 4.1.5 Intersection typesFor the time, we have only work with a parametric quantification, which implies a uniform behaviour of programs. We will now add intersection types τ ∩ σ with a subtyping rule <: defined by the following rule :Γ ⊢ σ ′ <:σ Γ ⊢ τ <:τ ′ Γ ⊢ σ → τ <:σ ′ → τ ′ Γ ⊢ σ ∩ τ <:σ Γ ⊢ σ ∩ τ <:τand new typing rules :

Syntax

Table 1. A Variant of the SECD with code pointer

where

where

where k = size(compile (tc, l)) and i = size(compile (t1, l + k + 1))

One also define the orthogonality between configuration inf Conf and contexts in Cont :

Contexts have to be seen as return addresses, as in [START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF]. Just like the restricted contexts in part 2, such contexts can only test values and not full configurations, since they are evaluated by an instruction Return.

The fact that the code c is constant induces some conceptual changes. Indeed, the syntactic duality between terms and values blurs to a duality on the control flow between a result and its computation. But since we still want to consider contexts as tests, we have to allow to extend c to add tests of results in it. We could also imagine, as in [START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF], to use Kripke logical relations with worlds describing code c 1 , c 2 . This is in fact closer to the spirit to low-level language since code is in fact stocked in the memory, and can modify itself.

Then, we defined our logical relation :

) in the definition of K τ (c1,c2),η and E τ (c1,c2),η , to allow contexts K 1 , K 2 to be extended so that they can test configurations.

Unfolding biorthogonality

As we have seen before, writing E τ directly in term of V τ is crucial to prove fact about E ∀α.τ , just like to get operational results from (t 1 , t 2 ) ∈ E τ .

However, to adapt this result to our low-level machine is not straightforward, because code c is fixed so one cannot replace a value v by a term t in a context. What we rather want to express is that a configuration is going to reduce to a value v, and that the context behave the same way with respect to this value and to this configuration.

To prove this result, we have to adapt the usual rule Proof. By case analysis on the instructions and their transitions.

implies that for all

) and c ′ i (size(c i ) + 1) = Return so we get the configuration (l i , e i , v i ::

Proof. -Direct side : If (Φ 1 , Φ 2 ) ∈ E τ (c1,c2),η do not both diverge, then they both normalize to good final configurations since the empty context, which corresponds here to the code pointer to the instruction Stop, is in the

2 ),η . So from the previous theorem there exists values

Then, using this result on can again prove our fundamental lemma for our language with Curry-style polymorphism and intersection types : Theorem 5 (Fundamental property). Let t be a term such that ∆, Γ ⊢ t : τ , then for every environment γ and η compatible respectively with Γ and ∆, and

As said in part 1.5, this result also extend to implicit dependent types, and so it solves one of the open problems of [START_REF] Benton | Compiling functional types to relational specifications for low level imperative code[END_REF].

Code pointer equality

Finally, we are going to adapt results of Section 2 to our low-level setting. We are not going to try to compile our α-equivalence, since we are working directly with De Bruijn indices. We will rather add a new instruction EqPoint which is able to test code pointer equality in closures. Then just like in Section 2 one has to make the distinction between the two set of instructions, to forbid values to use EqPoint . However we cannot do that syntactically on the code c, otherwise we would also forbid contexts to use it, which is definitely not what we want to do (or the result would be trivial). So we have to define it semantically : C(l, e) ∈ Val good,c iff every reduction made from the configuration (l, e, s, d) with code c does not use the instruction EqPoint . Then logical relations V τ c1,c2 are defined restricted to Val good,c1 × Val good,c2 .

In the same way, one define what is a good context (l, e, s) in Cont good,c and a good configuration (l, e, s, d) ∈ Conf good,c . Then one can easily show the equality of Theorem 3, defining K τ (c1,c2),η restricted to Cont good,c1 × Cont good,c2 , E τ (c1,c2),η as Proof. The proof of E τ η ⊆ E α τ η is the same than in Theorem 3. The other side is proved using the fact that Cont good,c ⊆ Cont.


Dr Birgitta Söder
email: birgitta.soder@ki.se

Maha Yakob

Jukka H Meurman

Leif C Andersson

Per-Östen Björn Klinge

M Söder

B Yakob

P-Ö Klinge

Söder

L C Anderssson

Periodontal disease may associate with breast cancer

Keywords: Breast cancer, Periodontitis, Missing molar teeth,

Purpose

The main purpose was to evaluate the association between periodontal disease and the incidence of breast cancer in a prospective study of 3273 randomly-selected subjects aged 30-40 years at baseline.

Methods

Breast cancer incidence was registered from 1985 to 2001 according to the WHO International Classification of Diseases criteria. At baseline, 1676 individuals also underwent a clinical oral examination (Group A) whereas 1597 subjects were not clinically examined but were registered (Group B). The associations between breast cancer, periodontal disease and missing molars were determined using multiple logistic regression models with several background variables and known risk factors for cancer.

Results

In total 26 subjects in group A and 15 subjects in group B had breast cancer. The incidence of breast cancer was 1.75 % in subjects who had periodontal disease and/or any missing molars, and 0 in subjects who had periodontal disease but had no missing molars. For periodontally healthy subjects with no missing teeth the breast cancer incidence was 1%. For Group B the respective incidence was 0.94%. Female gender (odds ratio [OR] 13.08) and missing any molar in the mandible (OR 2.36) were explanatory variables for breast cancer. Of the subjects with periodontal disease and any missing molars in the mandible 5.5% had breast cancer in comparison to 0.5% of the subjects who had periodontal disease but no missing molars in the mandible (p<0.02).

Conclusions Chronic periodontal disease indicated by missing molars seemed to associate statistically with breast cancer.

Introduction

Inflammation is a key feature in many chronic diseases including cancer [START_REF] Coussens | Inflammation and cancer[END_REF][START_REF] Mantovani | Cancer-related inflammation[END_REF]. Inflammation caused by infections seems to be one of the most important preventable causes of cancer in humans [START_REF] Kuper | Infections as a major preventable cause of human cancer[END_REF]. Periodontal disease is characterized by chronic infection and inflammation leading to destruction of the bone surrounding the teeth. The disease may take decades to develop and it ultimately leads to tooth loss [START_REF] Page | Advances in the pathogenesis of periodontitis: summary of developments, clinical implications and future directions[END_REF][START_REF] Pihlstrom | Periodontal diseases[END_REF]. An estimated 15-35% of the adult population in industrialized countries suffers from this multifactor disease [START_REF] Albandar | Periodontal diseases in North America[END_REF][START_REF] Gjermo | Periodontal diseases in Central and South America[END_REF][START_REF] Sheiham | Periodontal diseases in Europe[END_REF]. Periodontal disease involves complex interactions of host defence, bacteria, and virus. Periodontal disease is initiated by a biofilm of bacteria on the teeth which triggers an immune-inflammatory response in the adjacent host tissues [START_REF] Page | Advances in the pathogenesis of periodontitis: summary of developments, clinical implications and future directions[END_REF][START_REF] Socransky | Dental biofilms: difficult therapeutic targets[END_REF] . Numerous oral bacterial species have been associated with periodontal disease [START_REF] Haffajee | Microbiology of periodontal diseases: introduction[END_REF][START_REF] Socransky | Periodontal microbial ecology[END_REF] .

Human cytomegalovirus (HCMV), Epstein-Barr virus (EBV) and HCMV-EBV co-infection seems to be closely associated with disease-active periodontitis. [START_REF] Grenier | Detection of herpetic viruses in gingival crevicular fluid of patients suffering from periodontal diseases: prevalence and effect of treatment[END_REF][START_REF] Slots | Update on human cytomegalovirus in destructive periodontal disease[END_REF][START_REF] Slots | Herpesviruses, the missing link between gingivitis and periodontitis?[END_REF] . Infection by HCMV or EBV seems to inhibit the macrophages to respond to bacterial challenge, and thus have pathogenic role in the development of periodontal disease. [START_REF] Lin | Human cytomegalovirus and Epstein-Barr virus inhibit oral bacteria-induced macrophage activation and phagocytosis[END_REF] The associations between infectious agents of putative bacterial pathogens, herpes viruses, Epstein-Barr virus (EBV) type 1, cytomegalovirus (CMV) seems to play an important synergistic role in the pathogenesis of chronic periodontitis. [START_REF] Botero | Subgingival Human Cytomegalovirus Correlates With Increased Clinical Periodontal Parameters and Bacterial Coinfection in Periodontitis[END_REF][START_REF] Chalabi | Periodontopathic bacteria and herpesviruses in chronic periodontitis[END_REF][START_REF] Saygun | Quantitative analysis of association between herpesviruses and bacterial pathogens in periodontitis[END_REF] .

Breast cancer is the most common malignancy in women worldwide and it is the leading cause of cancer-related mortality [START_REF] Murray | Mortality by cause for eight regions of the world: Global Burden of Disease Study[END_REF]. Incidence rates are high in developed countries and are also increasing in the developing world [START_REF] Igene | Global health inequalities and breast cancer: an impending public health problem for developing countries[END_REF]. National income and health expenditures are known to affect breast cancer incidence but these factors only partly explain variations in mortality rates [START_REF] Igene | Global health inequalities and breast cancer: an impending public health problem for developing countries[END_REF]. Viral infections such as human papilloma virus infections seem to associate with breast cancer as shown in a recent meta-analysis [START_REF] Li | Human papillomavirus infection and sporadic breast carcinoma risk: a meta-analysis[END_REF] In general, persistent and prevalent infections in populations appear to link with malignancies [START_REF] Glaser | Epstein-Barr virus and breast cancer: state of the evidence for viral carcinogenesis[END_REF]. In Sweden breast cancer represents 29% of all cancers in the female [START_REF] Boström | The development and Distribution of Public Health[END_REF]. Breast cancer also has a hereditary component [START_REF] Trichopoulos | Early life events and conditions and breast cancer risk: from epidemiology to etiology[END_REF].

The results of an epidemiological study 2001, from our group, showed that fairly young individuals with periodontal disease and missing molars are at increased risk of premature death caused by life threatening diseases such as malignant neoplasm, cardiovascular diseases, and diseases of the digestive system [START_REF] Soder | Periodontitis and premature death: a 16-year longitudinal study in a Swedish urban population[END_REF]. Recently, periodontal disease was also found to associate with head and neck cancer in patients who never smoked or consumed alcohol [START_REF] Tezal | Chronic periodontitis and the incidence of head and neck squamous cell carcinoma[END_REF]. Poor oral health has been statistically associated with the prevalence of many types of cancer such as pancreatic and gastrointestinal cancer [START_REF] Meurman | Oral microbiota and cancer[END_REF]. Consequently, the hypothesis for the present study was that a low degree chronic inflammation such as seen in periodontal disease is involved in carcinogenesis.

For that reason the specific aim of the present investigation was to study the incidence of breast cancer from 2001 in subjects with periodontal disease and characteristic tooth loss in our 16-year prospective investigation.

Materials and Methods

Study population

In 1985 we undertook this longitudinal prospective study, which comprised a random sample cohort of 3273 individuals aged 30-40 years. The subjects were selected from a registry database of all inhabitants (n = 105,798) of Stockholm County born on the 20th of any month from 1945 to 1954 inclusive. They were informed about the purpose of the study and offered a clinical oral examination. In total, 1676 individuals (51.2%; 838 men and 838 women) underwent a detailed clinical oral examination (Group A). The remaining 1597 subjects (849 men and 748 women) did not have the clinical examination and constituted Group B. Figure 1 shows the study profile.

Clinical examination

For all subjects of the clinically examined Group A the following parameters were recorded: the number of remaining teeth excluding third molars; gingival inflammation around every tooth as assessed using the gingival index [START_REF] Silness | Periodontal Disease In Pregnancy. Ii. Correlation Between Oral Hygiene And Periodontal Condtion[END_REF]; and oral hygiene status as determined by using both the dental plaque [START_REF] Löe | Periodontal Disease In Pregnancy. I. Prevalence And Severity[END_REF] and the calculus indices to assess all six surfaces of six representative teeth. Pocket depth was determined using a periodontal probe and recorded to the nearest higher millimetre for six sites of each tooth. Presence or absence of each tooth was recorded. The prevalence of periodontal disease was determined in each age group year by year from 31 years of the age to 40. All subjects in Group A also filled in a structured questionnaire containing questions about factors such as regular dental visits and the use of tobacco. Smoking was divided into smokers and former smoker categories. The smokers reported the number of cigarettes per day, and the number of years of smoking. Former smokers reported when they had quit smoking and also the number of cigarettes per day and years of smoking. Smoking was then further analyzed as pack-years. The Ethics Committee of the Karolinska Institute and Huddinge University Hospital, Sweden, approved the study protocol. The study is in accordance with the Declaration of Helsinki.

Cancer and socio economic data

The data for cancer (malignant neoplasm) and causes of death were obtained from the Centre of Epidemiology, Swedish National Board of Health and Welfare, Sweden. The data were classified according to the WHO International Statistical Classification of Diseases and Related Health Problems ICD-7, ICD-9 and ICD-10. Socio-economic data were obtained from the National Statistics Centre, Örebro, Sweden.

Statistical analyses

Analysis of variance, chi-square test, Fisher´s exact t-test and multiple logistic regression analyses were applied when appropriate. Multiple logistic regression analysis was used to compare the incidence of cancer, according to the state of oral health at baseline, while simultaneously controlling for confounding variables. The confounding variables included age, gender, education, income, socioeconomic status, smoking habits, and dental visits.

Smoking habits were dichotomized into the number of smokers (ever smokers) and the number of never smokers. The model with the confounders was correlated to the incidences of cancer. A backwards elimination method was used to control for multicollinearity (correlation between confounders). The statistical model was tested according to Cox & Snell [START_REF] Cox | On test statistics calculated from residuals[END_REF] and Nagelkerke [START_REF] Nagelkerke | A note on a general definition of the cefficient of determination[END_REF].

Results

In the total cohort of 3273 subjects, 41 subjects (1.3 %) were diagnosed as having breast cancer; comprising 39 women and 2 men. Breast cancer had been diagnosed at the mean age of 45.8 ± 6.8. In the clinically examined Group A comprising 1676 subjects, 26 persons (1.6%) had breast cancer; 24 women and two men; whereas in Group B with 1597 subjects, 15 women (0.9 %) had breast cancer.

6

The prevalence of periodontal disease in Group A significantly increased year by year, in women from 9.8 % at the age of 31 to 25.6 % at the age of 40 (p<0.001) and in men from 8.5% at the age of 31 to 35.0 % at the age of 40 (p<0.001). In total 17.1% had periodontal disease diagnosed at the 1985 baseline examination.

Of the subjects with breast cancer 12 subjects were smokers (42.8%); 5 were former smokers (17.9%), whereas 11 had never smoked (39.3%). Of the remaining 1648 subjects with no breast cancer 605 were smokers (37.7%), 432 were former smokers (26.2%), and 611 had never smoked (37.1%). For the subjects with breast cancer, a mean of 2411.3 ± 2811.4 S.D. pack-years of smoking was calculated; for those with no breast cancer the respective packyears were 3643.0 ± 5195.7 S.D. The difference between the groups was statistically not significant (NS).

The demographic and oral health data at baseline in 1985 for subjects with and without periodontal disease are shown in Table 1. The demographic data and oral health data in 1985 for subjects with or without breast cancer in 2001 are shown in Table 2. In the multiple logistic regression model with breast cancer as the dependent variable, female gender appeared to be the principal independent predictor associated with 13.08-fold the risk for breast cancer. Those subjects with any missing molar had 2.36-fold the risk for breast cancer.

The results are given in Table 3. The incidence figures for breast cancer for the clinically examined Group A showed that 1.75% of those with any missing molar had breast cancer whereas only 0 % of the subjects with no missing molar had cancer (Table 4). The difference in the prevalence of breast cancer for subjects with periodontal disease and with or without any missing molar in the mandible was significant (p<0.02), see Table 5.

Discussion

This study addressed the issue of chronic dental infections, and periodontal disease in particular, as a risk factor for breast cancer. Our results clearly identified periodontal disease and loss of any molar from the mandible as an independent predictor for breast cancer.

Consequently, our study hypothesis based on the paradigm of chronic infection/inflammation vs. breast cancer was confirmed. Some comments should be made concerning the reliability of the results. Our subjects were randomly chosen to avoid selection bias. The large subject pool was representative of the ethnically homogenous Swedish adult population, with an age range of 10 years to limit the influence of age differences. The study had a longitudinal prospective design with a cohort of subjects of whom many had periodontal disease documented at baseline [START_REF] Botero | Subgingival Human Cytomegalovirus Correlates With Increased Clinical Periodontal Parameters and Bacterial Coinfection in Periodontitis[END_REF] Further comments should be made about the missing molars which in this study were used as a proxy for chronic dental infections. The first permanent teeth to erupt are the first and second permanent molars [START_REF] Ekstrand | Time and duration of eruption of first and second permanent molars: a longitudinal investigation[END_REF]. The newly erupted molars can be infected by oral bacteria from the primary dentition or by intra-familial transmission [START_REF] Kulekci | Salivary detection of periodontopathic bacteria in periodontally healthy children[END_REF][START_REF] Umeda | The distribution of periodontopathic bacteria among Japanese children and their parents[END_REF]. Our study subjects who had lost their molars already by 1985 had most probably been suffering from periodontal disease for many years. Namely, the reason for molar tooth extraction is either due to dental caries or periodontal disease. The reason could not be identified in our data. However, dental caries is also a chronic infectious disease leading to pulp infections and periapical abscesses with subsequent systemic spread of micro-organisms. Thus the end result of both periodontal disease and caries is a systemic infection burden and often leading to tooth extraction. Hence we felt justified to use missing molars as a proxy for long-lasting dental infections in our analyses.

The inevitable increase of periodontal disease with age poses a threat to large patient groups who then will be exposed to chronic infections with systemic consequences. Hence, periodontal disease may indeed contribute to the increasing incidence of breast cancer in middle aged and older people. The development of cancer obviously depends on differences in the characteristic carcinogenesis and thus the impact of the role infection and inflammation depends on the etiopathogenesis of the neoplasm in question.

Our findings may nevertheless have importance in the ongoing discussion about life style and the risk of cancer. The results also have public health consequences. There is a well warranted basis for prophylactic measures against the prevalence and outcome of periodontal disease in addition to the costs it incurs to societies. Even if periodontal disease is only one contributor to the carcinogenic process a strategy to remove this burden might reduce the incidence of breast cancer worldwide.

Conclusions

This is to our knowledge the first study presenting data about the eventual risk that longstanding dental infections may present risk for breast cancer. Chronic periodontal disease indicated by missing molars seemed to associate statistically with breast cancer. If our results will be confirmed in future studies the finding should have clinical consequences in advising the patients.

. Plaque index [28] 0.67 ± 0.47 0.99 ± 0.53 <0.001

Fig. 1 Study profile

Gingival inflammation [29] 1. Plaque index [28] 0.90 ± 0.537 0.87 ± 0.61 NS Gingival inflammation [29] 1.76 ± 0.54 2.12 ± 0.

  years earlier. The participants were born on the 20 th of any month between 1945 and 1954 and therefore it was possible to get the diagnosis of breast cancer for each participant up to the year 2001 from the National Cancer Registry Centre of Epidemiology, Swedish National Board of Health and Welfare. This registry collects cancer data from all subjects in Sweden born on the 20 th of any month.

Table 1

 1 Demographic clinical oral health data of subjects of Group A with or without diagnosed periodontal disease at the baseline examination in 1985.

		No periodontal disease	Periodontal disease	p*
		(n =1390 )	(n = 286 )
		number, mean ± SD	number, mean ± SD
	Gender (female/male)	159/825	127/851	<0.05
	Age in 1985 (years)	35.6 ± 2.8	36.5 ± 2.8	<0.001
	Education (compulsory/higher)	218/1172	73/286	<0.001
	Smoking (pack-year)	3315.5 ± 5041.2	5060.5 ± 5455.7	<0.001
	Income (Swedish Crowns x 1000)	188.5 ± 102.9	186.4 ± 89.3	NS

Table 2

 2 Demographic and clinical oral data for subjects with periodontitis 1985, with and without breast cancer 2001

		Periodontitis 1985 Periodontitis 1985	p*
		without	with
		breast cancer 2001	breast cancer 2001
		(n = 281)	(n = 5 )
		number, mean ± SD number, mean ± SD
	Gender (male/female)	0/161	5/125	= 0.01
	Age in 1985 (years)	35.7 ± 2.9	± 2.5	NS
	Education (compulsory/higher)	70/281	3/5	NS
	Smoking (pack-year)	5107.1 ± 5482.6	2445.5 ± 2814.3	NS
	Income (Swedish Crowns x 1000)	178.7 ± 92.2	150.2 ± 53.0	NS

Table 3

 3 Results of the multiple logistic regression analysis. Breast cancer was the dependent variable and age, gender, education level, socio economic status, working history, yearly income, smoking in pack-years, dental appointments, dental plaque index, gingival bleeding index, and loss of any molar tooth in the mandible were used as explanatory variables.

	Odds 95% confidence

Table 4

 4 Percentage of breast cancer 2001 † for subjects in A with periodontitis and periodontitis with missing any molar as well as subjects with no periodontitis and no missing teeth and subjects in B. According to International Classification of Diseases, ICD-8, ICD-9 in1985-1996 and ICD-10 in 1997-2000.

	A

†

Table 5

 5 Percentage of breast cancer in subjects with periodontal disease with or without any missing molar teeth.

		Missing molars in the mandible	No missing molars in the mandible	p
		(n=73)	(n=213)
	Percent	5.48	0.47	<0.02

Cox & Snell R 2 = 0.017; Nagelkerke R 2 = 0.11

Acknowledgements

The Swedish Heart-Lung Foundation, the AFA Insurance, Sweden, Philips Oral Health Care, Sweden and the Karolinska Institutet, Stockholm, Sweden, and by grant TI020Y0003 from the Helsinki University Central Hospital, Finland. Grant from The Medical Society of Finland.