Simon Colin

Rodolphe Lepigre
email: rodolphe.lepigre@inria.fr

Gabriel Scherer
email: gabriel.scherer@inria.fr

Unboxing Mutually Recursive Type Definitions in OCaml

In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be "unboxed". This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions.

Introduction

The version 4.04 of the OCaml programming language, released in November 2016, introduced the possibility to unbox single-constructor variants and single-field records. In other words, a value inhabiting such a datatype is exactly represented (at runtime) as the value that it contains, rather than a pointer to a block containing a tag for the constructor and the contained value. The removal of this indirection is called constructor unboxing, or unboxing for short, and it allows for a slight improvement in speed and memory usage.

In the current version of OCaml, unboxing must be explicitly requested with [@@unboxed] as shown in the following example: type uid = UId of int [@@unboxed] One of the main interests of unboxing is that it allows the incorporation of semantic type distinctions without losing runtime efficiency. For example, the elements of uid are distinct from those of int from the point of view of the type-checker, but they have the same runtime representation. As a side-product, unboxing reconciles those that care about software engineering with those that are obsessed with performances.

Unboxing becomes even more interesting when it is combined with advanced features such as existential types (with GADTs) or higher-rank polymorphism (with polymorphic record fields), which are otherwise only accessible in a boxed form.

type 'a data = { name : string ; data : 'a } type any_data = Any_data : 'a data -> any_data [@@unboxed] type proj = { proj : 'a. 'a -> 'a -> 'a } [@@unboxed]

Unboxing and dynamic floating-point checks

OCaml uses a uniform memory representation for all language values, in one machine word. Multi-word data such as floating-point numbers, records or arrays are represented by a (wordsized) pointer to a block on the heap.

For local computations involving floating-point numbers, the compiler tries to optimize by storing short-lived floating-point values directly, without the pointer indirection; this is called floating-point unboxing, a different form of unboxing optimization. The boxing indirection needs to be kept for values passed across function boundaries, or passed through data structures expecting generic OCaml values.

To avoid indirection costs on typical numeric computations, a specific representation exists for floating-point arrays, in which unboxed (two-words) floating-point numbers are stored directly. The compiler uses this optimized representation when an array is statically known to have type float array . It also performs a dynamic optimization when creating a new (non-empty) array: it checks whether its first element is a (boxed) floating-point value, and in that case uses the special floating-point array representation. As a consequence, all writes to such an array need to be unboxed first, and reads produce data in already-unboxed form, which meshes well with the local floating-point unboxing optimizations.

However, this optimization crucially relies on a separability assumption: the inhabitants (i.e., the values) of any given type are either all (boxed) floating-point values, or none of them are. Indeed, if there were types containing both floating-point and non-floating-point values, then this optimization would be unsound. This is demonstrated by the following example, which relies on the unsafe/forbidden casting function Obj.magic . The array of floating point numbers that is constructed here is stored using the optimized representation. As a consequence, its elements must be unboxed prior to being inserted into the actual array. Here, the segmentation fault is precisely triggered when attempting to unbox the value 42 , which is not stored in a block. Recall that values of type int are stored in a memory word, without going through an indirection (i.e., a pointer to a block).

Although the above example requires unsafe features, a similar situation also arises when using a (single-constructor) GADT whose parameter is existentially quantified, and can hence contain both floating-point and non-floating-point values.

type any = Any : 'a -> any

The above datatype is the GADT formulation of the existential type Dα. α: it can contain any OCaml value. However, those values are "boxed" under the Any constructor. In particular, the value Any 0.0 is not directly represented as a floating-point value, but as pointer to a block (stored on the heap) that is tagged with the Any constructor, and that contains two memory words holding the actual floating-point number.

If the any datatype was allowed to be unboxed, we would have constructed a type breaking the separability assumption. The above example of segmentation fault could then be reproduced by a well-typed program as follows.

type any = Any : 'a -> any [@@unboxed] (* The above type is rightfully rejected by OCaml, it cannot be unboxed. *)

let array = [| Any 0.0 ; Any 42 |]
The current implementation correctly rejects this any datatype, but it also rejects valid unboxed definitions (that would not introduce non-separable types) when mutually-recursive datatypes are involved. The following (real-world) example of an interesting definition that is wrongly rejected was given by Markus Mottl. and _ node = Node : ('a, _) tree -> 'a node [@@ocaml.unboxed] (* The above type is incorrectly rejected by OCaml, it could be unboxed. *)

Yet another example of such wrongfully rejected example was encountered by the second author, in the context of the Bindlib library [START_REF] Lepigre | Abstract representation of binders in ocaml using the bindlib library[END_REF]. It resembles the definitions of any_type and 'a data that were given earlier, but it is rejected as the two datatypes are defined mutually-recursively (for more details, see Lepigre and Raffalli, 2018, Section 3.1).

The existing check

The current (legacy) implementation of the compiler check for unboxing was implemented by Damien Doligez in 2016, when constructor unboxing was introduced. It proceeds by inspecting the parameter of every unboxed GADT constructor. If it is an existential variable 'a , the definition is rejected. If it is a type expression whose value representation is known (e.g., a function foo -> bar , a product foo * bar ) and is thus separable, then the definition is accepted. The difficult case arises when the parameter is of the form (foo, bar, ...) t . For example, if the parameter has type 'a t , where 'a is an existential variable, then this definition must be rejected if t is defined as type 'a t = 'a , but it can be accepted if it is defined as type 'a t = int * 'a , for example.

In the current check, (foo, bar, ...) t is expended according to the definition of t , and its expansion is checked recursively. In the case where t is an abstract datatype, the check fails (rightly) as soon as one of the parameter is an existential. If t is part of the same block of mutually-recursive definitions, its definition may not be known yet, and the check fails although it could have succeeded had the definition been known. Finally, it is worth noting that because of recursive datatypes, the expansion process may not terminate. As a consequence, there is a hard limit on the number of expansions.2

Our approach: inference rules for separability

We propose to replace the current check using a "type system" for separability. In other words, we introduce inference rules to approximate the semantic notion of separability: a type is separable if the values it contains are all floating-point numbers, or if none of them are. This approach is very similar to how the variance of datatype parameters is handled in languages with subtyping (including OCaml), both in theory and in practice. In the case of variance, the "types" are annotations such as covariant or contravariant, and the "terms" that are being checked are types and datatype definitions.

Here, the "types" are separability modes indicating whether the corresponding type parameters need to be separable for the whole datatype to be separable. Modes include Sep (separable), the mode of types or parameters that must be separable, and Ind (indifferent), the mode of types or parameters on which no separability constraint is imposed. 3 For example, in the case of type 'a t = 'a * int , the parameter 'a has mode Ind since the values it contains are all pairs, independently of the type used to instantiate 'a . For type ('a, 'b) second = 'b , the parameter 'a has mode Ind, but the parameter 'b has mode Sep. Indeed, if 'b is not instantiated with a separable type, then the whole definition cannot be separable either. The separability behavior of a parametrized datatype is characterized by a mode signature, which gives a choice of mode for the type parameters that guarantees that the whole datatype will be separable. For instance, the previous two examples would have mode signatures ('a:Ind) t and ('a:Ind, 'b:Sep) second .

If a type that is being checked is defined in terms of a type constructor (foo, bar, ...) t , and if the mode signature of t is known, then its definition does not need to be unfolded as in the legacy implementation. Indeed, it is enough to simply check the parameter instances ( foo , bar , ...) against the modes of the signature. For example, if we encounter (foo, bar) second , then we only need to check that bar is separable.

In the case of a block of mutually-recursive datatype definitions, a mode signature must be constructed for each definition of the block. However, this cannot be done separately for each definition due to dependencies. As a consequence, we proceed (like for variance) by computing a fixpoint, iteratively refining an approximation of the mode signatures for the block. The number of possible modes assignments for each parameters being finite, it is immediate that this fixpoint computation terminates. Note that our inference rules do not talk about the fixpoint computation, or about algorithmic aspects in general. It is a simpler, declarative specification for the correctness of mode assignments, from which the checking algorithm can be derived. It can also be used to reason about the semantic correctness of our check.

Contributions

We claim the following three contributions:

• A clear explanation of separability. The notion of separability evidently existed in Damien Doligez's head when unboxed datatypes where implemented in 2016. However, we had to rediscover it to understand the check, and we took this opportunity to document separability and to give it a precise semantic definition.

• A set of inference rules for separability of type expressions and datatype definitions.

• An implementation of a separability check derived from these inference rules, within the OCaml compiler. It is compatible with mutually-recursive definitions, which were previously always rejected. A preliminary version of this work was produced during an internship of the first author [START_REF] Simon | Specifying the unboxability check on mutually recursive datatypes in OCaml[END_REF]. We give here a full treatment of GADTs, while the internship report used first-class existential types, without equations. We also moved from a prototype implementation, separate from the OCaml type-checker and defined on simpler data-structures, to a production-ready implementation of the separability check in (an experimental fork of) the OCaml type-checker.

Type language and separability modes

As mentioned in the introduction, our approach to unboxability checking relies on the notion of separability (of a type), which was already introduced in an intuitive way.

Definition 1 (Separability). A type is said to be separable if and only if its inhabitant contain either only floating-point values, or only non-floating point values.

Intuitively, our final goal is to make sure that all type definitions have a separable body. That is, for all definition type ('a, 'b, ...) t = <type_body> , we want to check that the type <type_body> is separable (under some assumptions on the separability of parameters). Before going into formal definitions, two potential sources of difficulties must be discussed: GADTs, which are the only possible source of non-separability, and the (related) typing constraints, which can be used to extract (possibly non-separable) subcomponents of a type.

GADTs using type equalities and existential quantifiers

Guarded/generalized algebraic datatypes (GADTs for short) extend the usual variant datatypes (with a slightly different syntax). They are parametrized datatypes (_, _, ...) t in which the typing constraints on the parameters may vary depending on the variant constructor. Moreover, existentially quantified type variables may appear in GADT constructors. 4 Examples of GADTs illustrating these features are given below. In the above, we use the new syntax exists 'a. <type_expr> for first-class existential quantification over one or several type variables, and <type_expr> with ('a = <type_expr>) for guarding a type expression with an equality constraint. In our formal description of the separability check, we will use the syntax Dα.τ for existentials, and the syntax τ aepα " κq for equality guards, where α is a type variable, and τ and κ are type expressions.

The semantic intuition behind these two type-formers is the following. An existential type Dα.τ can be understood as the union over all types κ of τ rα :" κs. For example, the values of the type exists 'a. 'a -> 'a contains the values of int -> int , but also the values of bool -> bool and the values of (char -> bool) -> (char -> bool) .6 An equality guard τ aepα " κq exactly corresponds to τ in the case where the constraint pα " κq is satisfied, and it is empty otherwise. Note that we only use guards whose left-hand-side is a type variable, as this suffices to express GADTs: all guards equate a type parameter to its instance in the "return type" of the variant constructor.

Equality guards and deep separability

In the introduction, the parametrized type constructors 'a t that were considered either had mode signature ('a : Ind) t , meaning that 'a t is always separable, no matter what 'a is, or mode signature ('a : Sep) t , meaning that 'a t is separable only if 'a is itself separable. However, these two modes are not always sufficient due to equality guards.

The equality guards used in GADTs7 introduce the ability for parametrized types to "peek" into the definition of their parameters, in ways that affect our separability check. Consider, for example, the unboxed version of the _ first datatype, which is accepted by the current constructor unboxing check.

type _ first = | First : 'b -> ('b * 'c) first [@@unboxed]
Using this definition, ('b * int) first has the same memory representation as 'b , so it is separable if and only if 'b is separable. In other words, the separability of type foo first does not only depend on the separability of type foo , but also on the separability of a subcomponent (in the sense of syntactic inclusion) of type foo .

To account for this situation, we introduce a third separability mode Deepsep (deeply separable). For a closed type expression (i.e., a type expression with no free type variable) to be Deepsep, all its sub-components (including the type expression itself) must be separable.

Formal syntax of types

We define the syntax of the type expressions and datatypes that we consider in the top and middle parts of Figure 1. It is a representative subset of the OCaml grammar of types8 , with first-class existential types Dα.τ and type restrictions τ aepα " κq to represent GADTs with finer-grained rules, as explained in Section 2.1. We also include first-class universal types @α.τ , although they are only allowed in record or method fields in OCaml.

To define deep separability, we need to precise define the syntactic sub-component of a types (see Section 2.2). To this aim, we define a sub-component relation τ Ÿ κ ("τ is a sub-component of κ") at the bottom of Figure 1. The first two rules make the relation reflexive and transitive, and the others give the immediate sub-components for each type-former.

Syntax of type expressions:

τ, κ ::" α, β type variable | float | int | bool builtin types | tpτ 1 , . . . , τ n q (parametrized) type constructor | τ Ñ κ function type | τ 1 ˆ¨¨¨ˆτ n product/record type | @α.τ polymorphic type | Dα.τ existential type | τ aepα " κq equality guard
Syntax of datatypes:

A, B ::" C 1 of τ 1 | . . . | C n of τ n boxed variant | C of τ r@@unboxeds unboxed variant | tl 1 : τ 1 ; . . . ; l n : τ n u boxed record | tl : τ u r@@unboxeds unboxed record | τ type synonym
Sub-component relation on type expressions: The definition of the sub-component relation is careful to preserve the scoping of variables. For example, τ Ÿ @α.κ holds only if α does not occur free in τ , which we write α R τ . In particular, whenever τ Ÿ κ holds, the free type variables of τ are included in those of κ; the sub-components of a closed type expression are also closed types.

τ Ÿ τ τ 1 Ÿ τ 2 τ 2 Ÿ τ 3 τ 1 Ÿ τ 3 i P r1; ns τ i Ÿ tpτ 1 , . . . , τ n q 1 P t1, 2u τ i Ÿ τ 1 Ñ τ 2 i P r1; ns τ i Ÿ τ 1 ˆ¨¨¨ˆτ n τ Ÿ κ α R τ τ Ÿ @α.κ τ Ÿ κ α R τ τ Ÿ Dα.κ i P t1, 2u τ i Ÿ pτ 2 aepα " τ 1 qq

Separability modes

Separability modes m, n, their order structure m ă n and mode composition m ˝n are defined in Figure 2. Modes are (totally) ordered from the less demanding to the more demanding. We may use derived notations such as m ď n, minpm, nq or maxpm, nq for the non-strict ordering, the minimum or the maximum of two modes.

A mode m expresses a requirement on a type expression, which comes from its context: for the whole expression to be valid, some of its sub-component must have the separability property m. The operation m ˝n expresses composition of those requirements in our inference rules (given in the next section). For example, if tpαq requires its parameter α to have mode m for the whole expression to be separable, and upβq requires its parameter β to have mode n for the whole expression to be separable, then tpupβqq is separable when β has mode m ˝n.

Contexts and mode signatures

Our separability judgments in Section 3 make use of contexts Γ, representing separability assumptions on the type variables (like α or β) that are in scope. Moreover, we also rely on mode signatures Σ, representing the separability requirements on the datatype constructors tpαq that are available in the scope. Contexts and mode signatures are defined in Figure 3. This figure also defines the extension of the order on modes to an order on contexts and on mode signatures. The order on context is just a point-wise extension of the mode order, imposing that two comparable contexts have the same type variables. The order on signatures imposes the same datatype constructors on both sides, but it asks their parameter modes to be (pointwise) comparable in the opposite order, pěq rather than pďq: parameters are in contravariant position. For example, we have tpα : Sep, β : Sepq ď tpα : Ind, β : Indq.

Γ ::" H | Γ, α : m Σ ::" H | Σ, tpα : mq Γ ď Γ 1 m ď m 1 Γ, α : m ď Γ 1 , α : m 1 Σ ď Σ 1 α " α 1 m ě m 1 Σ, tpα : mq ď Σ 1 , tpα 1 : m 1 q

Separability inference

The formal deduction rules that we will use to assess the separability of datatype definitions is defined in Figure 4. Type expressions are checked by judgments of the form Σ; Γ $ τ : m, which can intuitively be read in either directions (from Γ to m or conversely):

• If the type variables respect the modes in Γ (for example, if pα : Sepq P Γ is only instantiated with separable types), then the type expression τ has the mode m.

• For the type expression τ to be safe at mode m, then its type variables need to have at least the modes given in Γ.

Type expressions. The rule for parametrized datatypes tpτ 1 , . . . , τ m q uses mode composition; for example, if t is a one-argument type constructor with signature tpα : nq and we want Inference rules at type-expression level:

pα : mq P Γ Σ; Γ $ α : m tpα 1 : m 1 , . . . , α n : m n q P Σ pΣ; Γ $ τ i : m ˝mi q 1ďiďn Σ; Γ $ tpτ 1 , . . . , τ n q : m Σ; Γ $ τ : m ˝Ind Σ; Γ $ κ : m ˝Ind Σ; Γ $ τ Ñ κ : m pΣ; Γ $ τ i : m ˝Indq 1ďiďn Σ; Γ $ τ 1 ˆ¨¨¨ˆτ n : m Σ; Γ, α : n $ τ : m Σ; Γ $ @α.τ : m Σ; Γ, α : Ind $ τ : m Σ; Γ $ Dα.τ : m Σ; Γ $ τ : m m ě n Σ; Γ $ τ : n @Γ 1 ě Γ, Σ; Γ 1 $ pκ 1 " κ 2 q ùñ Σ; Γ 1 $ τ : m Σ; Γ $ τ aepκ 1 " κ 2 q : m @m, Σ; Γ $ τ 1 : m ðñ Σ; Γ $ τ 2 : m Σ; Γ $ pτ 1 " τ 2 q
Inference rules at (single) datatype level:

Σ; Γ $ decl C 1 of τ 1 | . . . | C n of τ n Σ; Γ $ τ : Sep Σ; Γ $ decl C of τ r@@unboxeds Σ; Γ $ decl tl 1 : τ 1 ; . . . ; l n : τ n u Σ; Γ $ τ : Sep Σ; Γ $ decl tl : τ u r@@unboxeds Σ; Γ $ τ : Sep Σ; Γ $ decl τ
Inference rule at the datatype declaration block level:

Dpm i q 1ďiďn , Σ block :" t 1 pα 1 : m 1 q, . . . , t n pα n : m n q pΣ env , Σ block ; α i : m i $ decl A i q 1ďiďn
Σ env $ pt i pα i q :" A i q 1ďiďn % Σ block tpτ q to have mode m, then τ needs to have the mode m ˝n.

The rules for concrete datatypes (functions and products, but also most other OCaml typeformers if we were to add them) use m ˝Ind on their arguments. If m is Sep (or Ind), then m ˝Ind is Ind, which corresponds to not requiring anything of the sub-components: the values at type τ 1 Ñ τ 2 are all functions, never float, no matter what the τ i are. If m is Deepsep, then we do need to check the sub-components, and indeed Deepsep ˝Ind is Deepsep.

A value is at the universal type @α. τ only if it belongs to all the τ rκ{αs for all κ. In particular, it is enough to prove the separability at just one of these τ rκ{αs (the universal type has even less values), so we can assume the (arbitrary) mode n of this particular κ by adding α : n in the context. Conversely, Dα. τ is inhabited by all the τ rκ{αs, so τ has to have the desired mode for all possible modes of κ. Instead of requiring the premise to hold for all possible modes n, we equivalently ask for the most demanding mode Ind.

The conversion rule allows to forget some information about a type τ : m by exporting it at a smaller mode n ď m. For example, all Sep types are also Ind types.

Equality constraints. The rule for equality constraints is by far the most complex rule in the system. A first remark is that κaepτ 1 " τ 2 q always has less elements than κ (it has the same elements when the equality holds, or no elements otherwise), so it should have any given mode m more often. In particular, if κ : m holds in the current context Γ, then κaepτ 1 " τ 2 q : m should also hold in Γ.

When we see an equality constraint, we gain more information, which should allow us to mode-check more types. The way our rules represent this information gain is by moving from the current mode context Γ to a stronger mode context Γ 1 . More precisely, to check κaepτ 1 " τ 2 q : m in Γ, the rule asks to check κ : m in any context Γ 1 ě Γ that is consistent with the assumption pτ 1 " τ 2 q. This corresponds to the Γ 1 $ pτ 1 " τ 2 q hypothesis, which will be explained shortly. For example, if Γ is α : Ind, β : Sep, and we observe the equality pα " βq, then in particular we know that α : Sep also holds (if the two types are equal, they must have the same mode). Our rule will type-check the body type κ in stronger contexts Γ 1 with α : Sep, β : Sep.

A context Γ is valid for a type equality, written Γ $ pτ 1 " τ 2 q, if the two types τ 1 and τ 2 have exactly the same mode in Γ. Remark that it is not enough to ask that, for a given mode m, both types have mode m (trivially, all types have mode Ind). Instead, we ask that for any mode m, either τ 1 and τ 2 have mode m, or neither of them have it. This is equivalent to requiring τ 1 and τ 2 to have the same "best" (i.e., biggest) mode.

In our example where Γ is α : Ind, β : Sep, note that we do not have Γ $ pα " βq: β has mode Sep but α does not. The modes Γ 1 ě Γ that satisfy Γ 1 $ pα " βq are Γ Sep :" α : Sep, β : Sep, and Γ Deepsep :" α : Deepsep, β : Deepsep. To check that κaepα " βq : m holds in Γ, our rule asks us to check that κ : m holds in both Γ Sep and Γ Deepsep . But in fact we, the implementers of the checking algorithm, know that making stronger assumptions in the context makes more mode-checks pass, so it suffices to check in context Γ Sep .9

Finally, it is interesting to consider the derivation of the following judgment, which is represents in our system the key ingredient of the _ first GADT that led to the introduction of Deepsep in Section 2.2. α : m $ Dβγ. βaepα " β ˆγq : Sep

We expect to accept this type declaration only in the case where α : Deepsep, this assumption guaranteeing that β will be separable. Opening the existentials puts β, γ in the context at Ind: α : m, β : Ind, γ : Ind $ βaepα " β ˆγq : Sep Let us now reason by case analysis on m to show that only m " Deepsep has a valid derivation of this judgment.

• If m is Deepsep, then any Γ 1 ě Γ with Γ 1 $ pα " β ˆγq has β : Deepsep, γ : Deepsep since otherwise β ˆγ : Deepsep cannot hold. In particular, Γ 1 $ β : Sep holds as expected, so the judgment is derivable.

• If m is Sep or Ind, then Γ 1 :" α : Sep, β : Ind, γ : Ind satisfies Γ 1 ě Γ and Γ 1 $ pα " βˆγq, but we do not have Γ 1 $ β : Sep: the judgment is not derivable.

Datatypes. The judgment for datatypes is simple: a datatype is accepted if its set of values is separable. Boxed variant or record definitions are always separable, so no premises are required. Unboxed variants/records with parameter type τ , or type synonyms for τ require τ : Sep.

Definition blocks. The judgment for definition blocks has an input signature (Σ env in the rule), which lists assumptions that we make on the datatype constructors provided by the typing environment, and an output signature (Σ blocK in the rule), which is a valid signature for the current block of mutually-recursive definitions. A definition block is valid if each datatype definition it contains is valid. Note that each definition is checked with the full Σ block in the signature context: all mutually-recursive datatype constructors are available in scope.

Meta-theory. The following two lemmas can be (trivially) proved by structural induction on involved typing derivation.

Lemma 1 (Cut elimination). A separability derivation can always be rewritten so that all occurrences of the conversion rule only have axiom rules as their premises.

Lemma 2 (Monotonicity). The following rule is admissible.

Σ ď Σ 1 Γ ď Γ 1 Σ; Γ $ τ : m m ě m 1 Σ 1 ; Γ 1 $ τ : m 1 4 Semantics
Due to space limitations, we moved our sweet-sour presentation of separability semantics to Appendix A.

Integration to OCaml

We are now going to highlight some important points of our implementation in the OCaml type-checker. The corresponding code can be found on GitHub at the following URL, and it shall soon be proposed for integration in the main OCaml repository. https://github.com/gasche/ocaml/tree/recursive-yet-unboxed Our implementation is derived from the type system given in Section 3, by inferring mode signatures for type definitions. It only assign mode signatures that can be justified by our syntactic type system. For example, if ('a : Sep, 'b : Ind) t is assigned to a type definition type ('a, 'b) t = A , then Σ env $ tpα, βq :" A % tpα : Sep, β : Indq must be derivable using the inference rules of Figure 4.

Inferring block signatures with a fixpoint

Our main checking function constructs a block signature Σ block given an environment Σ env and a block of type definitions pt i pα i q :" A i q 1ďiďn : val check : Env.t -> type_definition ConstrMap.t -> mode_signature ConstrMap.t

In this signature, type_definition ConstrMap.t maps datatype constructors t i pαq to datatype definitions A i , and mode_signature ConstrMap.t them to a mode signature t i pα : mq.

It is not possible to directly compute mode signatures for mode definitions, due to (mutually) recursive types: we need to know the mode signature of the type constructors in order to assign them a mode signature. This circularity is solved by using a fixpoint computation: we iteratively refine an approximation of the mode signatures.

The fixpoint computation starts with the most permissive mode signature, which only requires mode Ind for the variables of every type constructors of the block. At each turn, the separability of every type of the block is checked against the current approximation of the mode signatures, accumulating more precise constraints whenever required. If the mode signatures coming from these constraints is more demanding than the current approximation, we define it as the new approximation and continue. Otherwise, we have found a mode signature that validates the judgment -it is sound. In fact, it is the most permissive mode signature that we can find by iteration in this way.

Management of GADTs

As explained in Section 2.1, our type system for separability does not directly account for GADTs: they are encoded using existential quantifiers and equality guards. Our implementation handles only GADTs, which correspond to a very specific/specialized mode of use of existentials and guards within type declarations.

Consider for example type 'a fun = Fun : ('b -> 'c) -> ('b -> 'c) fun . The return type ('b -> 'c) fun determines the equality guard p 1 a " 1 b Ñ 1 cq, and the existential types are the free type variables 1 b, 1 c of the declaration. In general, unboxable GADT types contain existential quantifiers only at the toplevel, immediately followed by one equation for each type parameter, with finally a concrete parameter type τ .

The first thing to note is that all the existential quantification is done at the top level: they exactly correspond to all the free variables of the parameter type. We can infer a mode signature for the parameter type τ , and check that the modes inferred for the (free) existential variables in τ are Ind (according to our rule for existentials) and fail otherwise. Finally, the mode signature for the definition of the GADT is obtained by removing the existential variables from the inferred mode signature.

The delicate matter with the handling of GADTs is unsurprisingly the management of equality guards. Recall that (the parameter of) an unboxed GADT with parameters α is encoded as Dβ.τ aepα " κq (where the κ j do not contain any α i ). The idea of the implementation is to infer a mode context Γ such that Σ; Γ $ τ : Sep, assigning modes to the vecα and the β variables. Equations are then discharged one by one, refining Γ in the process, before the existential variables β are checked to be Ind and eliminated to create the final context for the GADT parameters only -the mode signature. Every equation (taken in any order) is managed according to the following three cases:

• An equation of the form pα i " β j q leads to Γ being updated with tα i Þ Ñ Γpβ j q, β j Þ Ñ Indu.

• An equation of the form pα i " κq with Γ X F V pκq only containing Ind leads to the equation being discarded without any update to Γ.

• Any other equation (i.e., equations pα i " κq with Γ X F V pκq not only containing Ind) leads to Γ being updated with

tα i Þ Ñ Deepsep, F V pκq Þ Ñ Indu.
These transformations respect the following invariant: if the equation pα " κq updates Γ into Γ 0 , then any Γ 1 ě Γ 0 that satisfies Γ 1 $ pα " κq is above the original Γ (Γ 1 ě Γ). In other words, strengthening the resulting context Γ 0 with the equation we just handled would give a context as permissive or more than the original context Γ.

Cyclic types

The OCaml type system accepts equi-recursive types. By default, any cycle in types must go through a polymorphic variant or object type constructor, but the -rectypes option generalizes this to any ground type constructor. A type such as ('a -> 'b) as 'b , for example, gives a cyclic representation to the infinite type 'a -> 'a -> 'a -> ... , and must be supported by our implementation.

To support cyclic types, we extended our checking rules to support a form of coinduction: each time we reduce a judgment to simpler premises (for example from Γ $ τ 1 Ñ τ 2 : m to Γ $ τ i : m ˝Ind), we record in the premises that we have encountered previously the judgment tau 1 Ñ τ 2 : m. If, later, we encounter the same judgment to prove, we terminate immediately with a success.

With this rule, it is possible to prove both α : Ind $ ppα Ñ βq as βq : Sep α : Deepsep $ ppα Ñ βq as βq : Deepsep

Informally, the reason why recursive occurrences of the same judgment can be considered an immediate success is that we "made progress" between the first occurrence of the cyclic type β and its second occurrence in α Ñ β: the second occurrence is "guarded" under a value constructor, and the set of values of β we are classifying as separable, or deeply separable, is not the one we started from (that would be an invalid, cyclic reasoning), but a copy of it occurring deeper in the type structure. However, some cyclic types such as tpαq as α have a less clear status, as the recursive occurrence is not guarded under a computational type constructor (arrow, product...), but under an abbreviation. Is this type well-defined if, for example, tpαq is defined as tpαq :" α? OCaml rejects some of those dubious-looking circular types, but instead of trusting our fate to the rest of the type-checker we decided to account them in our theory. We split our set of co-inductive hypotheses (the list of judgments that we are trying to prove) into a set of "safe" hypotheses Θ safe , which can be used immediately, and a set of "unsafe" hypotheses, which can only be used after a computation type constructor has been traversed.

Here are some rules of the corresponding formal system, extended with coinductive hypotheses, which guided our OCaml implementation:

@i P t1, 2u, Σ; Γ; Θ safe , Θ unsafe , pτ 1 Ñ τ 2 : mq; H $ τ i : m ˝Ind Σ; Γ; Θ safe ; Θ unsafe $ τ 1 Ñ τ 2 : m tpα 1 : m 1 , .
. . , α n : m n q P Σ pΣ; Γ; Θ safe ; Θ unsafe , ptpτ 1 , . . . , τ n q : mq $ τ i : m ˝mi q 1ďiďn Σ; Γ; Θ safe ; Θ unsafe $ tpτ 1 , . . . , τ n q : m pτ : m 1 q P Θ safe m 1 ě m Σ; Γ; Θ safe ; Θ unsafe $ τ : m pτ : mq P Θ unsafe Σ; Γ; Θ safe ; Θ unsafe & τ : m

The arrow rule has its premises under a computational type constructor, so it passes all coinductive hypothesis (including the new assumption on τ 1 Ñ τ 2 ) to its safe set. A datatype constructor may be just an abbreviation, so it adds the new hypothesis to the unsafe set.

Finally, whenever a judgment needs to be proved, it immediately succeeds if a stronger hypothesis is in the safe set. On the other hand, if our hypothesis is already in the unsafe set, then we know that it cannot be proven without recursively assuming itself, and we can in fact fail with an error.

Non-conservativity

We mentioned in Semantics Section A.2 that our judgments are non-principal -Fact 2. In particular, the following OCaml declaration can be given either signatures tpα : Ind, β : Sepq and tpα : Sep, β : Indq. type ('a, 'b) t = K : 'c -> ('c, 'c) t

Our implementation will choose one of the two minimum signatures, depending on the order in which constraints are handled -see Section 5.2. This means that some correct usage of the type will be disallowed: no matter which one is chosen, one of the two following declarations will be rejected: type t1 = T1 : (int, 'a) t -> t1 type t2 = T2 : ('a, int) t -> t2

On the other hand, the current implementation, which expands the definition of t , accepts both definitions.

We have decided to accept these completeness regressions. Our implementation is cleaner, accepts important examples rejected by the current implementer, safer in its handling of cycles (without fuel). In contrast, the counter-examples we could build are fairly esoteric, and we have not found any of them in the current testsuite or user programs. Only time will tell if this assumption is reasonable; we discuss ideas to recover principality (and accept both t1 and t2 ) in Future Work 6.1.

6 Related and future work

Future work

Richer modes The implementation of our unboxability check is satisfactory in the sense that it accepts most valid (unboxed) definitions. There is however room for improvement, especially in the handling of type equality guards, be it in GADTs or in toplevel equality constraints.

For instance, the way we handle equations of GADTS (see the previous section) is in some sense incomplete, and our language of modes is not principal. We considered extending our modes with modes of the form Dpβ : mq. m 1 and maepα " τ q. However, this would sensibly increase the complexity of the theory and the implementation, only to handle corner cases that may not be worth it.

Another, simpler approach to regain an impression of principality would be to support disjunction of modes. In the problematic example tpα, βq :" βaepα " βq, there are two minimum modes tpα : Ind, β : Sepq and tpα : Sep, β : Indq, so this type could be given the principal mode tpα : Ind, β : Sepq _ pα : Sep, β : Indq.

Automatic unboxing Currently, unboxable type declarations are never unboxed automatically, the user has to explicitly ask for it. Automatic unboxing has been considered, but it could break existing code using the foreign function interface. For example, a C function receiving an OCaml value from an unboxable but non-unboxed type currently needs to unbox it explicitly. The same action on an (automatically) unboxed type would fail if the C code is not changed accordingly.

Disjoint GADT unboxing We considered allowing the unboxing of multi-constructor GADTs in the case where typing constraints lead to the mutual exclusion of the different constructors. While each ground instance of this value type has a single possible constructor and could be unboxed, pattern-matching on 'a value would then have to be disallowed: pattern-matching learns the value of 'a from inspecting the GADT constructor, which is not present anymore in the unboxed representation. It seems a bit fishy to only allow pattern-matching on partiallydetermined instances of the type, and we did not investigate further.

Just get rid of the damn float thing

The fairly elaborate sufferings we just went through are caused by the dynamic unboxing optimization for arrays of floating point numbers. If this dynamic optimization was to be removed, we wouldn't need separability anymore and the unboxing check could also be removed. This dynamic check also has consequences on other features: by making a J type (our Dα. α) unsoud, it prevents extending the relaxed value restriction to generalize contravariant variables (Garrigue, 2004, page 11).

Related work

We discussed the existing implementation of the unboxability check in Section 1.2. The approach presented in our work is largely inspired from the way the variance of type declarations is handled in languages with subtyping [START_REF] Abel | Polarised subtyping for sized types[END_REF][START_REF] Scherer | Gadts meet subtyping[END_REF].

The memory representation of values used in OCaml and similar languages finds its origin in Lisp-like languages (for more details, see [START_REF] Leroy | Efficient data representation in polymorphic languages[END_REF] for more details). Despite the advantage of allowing every value to have the same, single-word representation, this approach also has obvious limitations in terms of performances due to the introduction of indirections. As a consequence, ways of lowering (if not eliminating) this overhead in certain scenarios have been investigated, one possibility being to mix tagged and untagged representations [START_REF] Peterson | Untagged data in tagged environments: Choosing optimal representations at compile time[END_REF][START_REF] Leroy | Efficient data representation in polymorphic languages[END_REF][START_REF] Leroy | Unboxed objects and polymorphic typing[END_REF]. Another idea that has been investigated is to consider unboxed values as first-class citizens, although distinguished by their types [START_REF] Simon | Unboxed values as first class citizens in a nonstrict functional language[END_REF].

A Semantics

We give a semantic model of types, datatypes and modes in Figure 5. The general idea is to be able to interpret the judgment Γ $ τ : m as follows: "if we replace each type variable pα : m α q of Γ by a closed/ground type with the correct separability mode m α , then τ will really have the separability mode m".

Ode to semantics. In Section 3 we have given a set of inference rules to prove judgments of the form Σ; Γ $ τ : m, guided by the intuition that this should provide evidence that τ is separable. Inference rules are our key contribution as they can easily be turned into a checking or inference algorithm, but they are also subtle, and may very well be wrong. They are hard to audit by someone else who does not trust us, the authors: there are a lot of details to check.

The point of a semantics is to provide an "obvious" counterpart to inference rules. A formal definition of separability (or whatever property an inference system is trying to capture) that is self-evident, can be easily checked and trusted by other people -in particular, it does not depend on the previous inference rules in any way. It serves as a specification, can use arbitrary mathematical operations, and does not need to be computable or close to an algorithm. Finally, one wishes to prove that the syntactic inference rules and the semantics coincide (in some sense); this implies that we can trust the inference rules as much as we trust the semantics.

Our semantics can also be understood as an idealized "model" of the programming language we are studying: it contains the assumptions that we make about the language and type system, and can be compared to OCaml to ensure that those assumptions are correct.

Ground value semantics.

To define what it means for a closed type τ to have the mode m, we wish to use the set-theoretic intuition we had earlier ("its values are all floating-point numbers, or none of them are"). To do this formally, we introduce a syntax of closed/ground values, and specify which ground values inhabit which ground types.

Our notion of ground/closed values is idealized; in particular, we represent all values at a function type as an opaque function blob, as if all functions were represented in the same way in the programming languages we model. They are not, but the differences in representation are irrelevant to reason about separability.

In the figure we define ground values v (just data, no term variables), ground types τ (no free type variables), ground datatypes (no free type variables or parameters), and blocks of datatype definitions σ, which assign a datatype to each datatype constructor of a signature Σ.

Finally, we define a series of semantic judgments using the symbol p(q. The judgment v ( σ τ specifies when a value inhabits a type, provided a block of definitions σ to interpret type constructors. The judgment v ( σ A specifies when a value inhabits a type parameter; note in particular how the judgments for unboxed datatypes reflect what happens in an implementation.

The judgments τ ( σ m and A ( σ m specifies when a type expression or datatype respect the separability mode m. They are defined in terms of our set-theoretic characterizations, separablepXq. Finally, A ( σ tpα : mq specifies when a (parametrized) datatype A respects a mode signature, and σ ( Σ specifies that a definition block respects a signature block.

In Figure 6, we use those specifications to build a semantic counterpart of each of our syntactic judgments. This lets us easily formulate soundness and (partial) completeness results. For example, Σ; Γ ( τ : m is the semantic counterpart of the judgment Σ; Γ $ τ : m. It captures what it means for the judgment to hold: for any valid definitions σ ( Σ, and any choice of ground types γ valid for Γ (γ ( σ Γ), replacing the variables in τ by the ground types in γ gives a ground type γpτ q at mode m, that is, γpτ q ( σ holds.

Ground/closed values v, type expressions τ , datatypes A, context valuations γ, datatype signature valuations σ v ::" true, false booleans

| intpn P Nq integers | floatpx P Rq float | pv 1 , . . . , v n q tuple | function function | tl 1 : v 1 ; . . . ; l n : v n u record | C i v variant closedpτ q :" @α, α R τ GType :" tτ | closedpτ qu closedpAq :" @τ P A, closedpτ q GDatatype :" tA | closedpAqu γ P PpTypeVar Ñ GTypeq σ P PpTypeConstructor Ñ GDatatypeq Values at a ground type expression v ( σ τ true, false ( σ bool intpnq ( σ int floatpxq ( σ float function ( σ τ 1 Ñ τ 2 `vi ( σ τ i ˘1ďiďn pv 1 , . . . , v n q ( σ pτ 1 ˆ¨¨¨ˆτ n q Dτ P GType, v ( σ κrτ {αs v ( σ Dα.κ @τ P GType, v ( σ κrτ {αs v ( σ @α.κ ptpαq :" Aq P σ v ( σ decl Arτ 1 {α 1 , . . . , τ n {α n s v ( σ tpτ 1 , . . . , τ n q pτ 1 " τ 2 q ùñ v ( σ κ v ( σ κaepτ 1 " τ 2 q
Values at a ground datatype v ( σ decl A v ( σ τ i 1 ď i ď n

C i v ( σ decl C 1 of τ 1 | ¨¨¨| C n of τ 1 v ( σ τ v ( σ
decl C of τ r@@unboxeds `vi ( σ τ i ˘1ďiďn tl 1 : v 1 ; . . . ; l n : v n u ( σ decl tl 1 : τ 1 ; . . . ; l n : τ n u v ( σ τ v ( σ decl tl : τ u r@@unboxeds v ( σ τ v ( σ decl τ

Ground types at a mode τ ( σ m, ground valuations at a context γ ( σ Γ isfloatpvq :" Dx, v " floatpxq separablepXq :" p@v P X, isfloatpvqq _ p@v P X, isfloatpvqq You don't have to trust the inference rules of our syntactic judgment Σ; Γ $ τ : m (which may very well be wrong) to trust that this semantic judgment Σ; Γ ( τ : m captures a good notion of separability. You only have to read the declarative rules of figures 5 and 6. It is now evident what the right statements should be for soundness and completeness of our syntactic inference system: it is sound if the syntactic judgment implies the semantic judgment (all judgments with a syntactic derivation are semantically true), and complete if the converse holds (all true judgments can be established by a syntactic derivation).

A.1 (Maybe-)Soundness and (in-)completeness

In a research paper, the perfect way to evaluate a syntactic system of inference rules is to provide an independent declarative semantics for it, state the corresponding soundness/completeness results, and prove them.

In real-world implementations of a programming language, the syntactic system is rarely written down (often, only the algorithm inspired from the rules is kept), the declarative semantics are only vague intuitions in the mind of the rule designers, and the statements are never formulated precisely enough to dream of a proof.

In this imperfect research paper, we have precise rules, and an independent declarative semantics, and precise statements... but we don't have (many) proofs. In fact, it is fairly nonobvious that proofs exist: as we were doing this precise formalization work we have discovered that completeness does not hold in presence of constraints, and even that the system is not principal -not only the inference rules, but even the semantics.

This subsection contains the best state of our knowledge and hopes about the formal status of our inference rules.

Conjectured Lemma 3 (Type expression soundness). Σ; Γ $ τ : m ùñ Σ; Γ ( τ : m Remark: it is not obvious that the existential rule is sound, for example. It proves Dα. τ : m under a premise α : Ind $ τ : m. The values of Dα. τ are the union of all the τ rσ{αs, and our induction hypothesis tells us that each τ rσ{αs indeed has the mode m. But separability is not at all stable by union: both int and float are separable, but their union is not. One needs to argue that either all τ rσ{αs are inhabited by floating-point numbers only, or that none of them contain floating-point numbers, and this is a subtle property of the structure of algebraic datatypes.

Conjectured Theorem 1 (Soundness). Σ 0 $ σ % Σ ùñ Σ 0 ( σ ) Σ Fact 1 (Incompleteness). There exists a τ such that H; H ( τ : m but H; H & τ : m.

Proof. Consider the two types τ 1 :" Dβ.βaepint " boolq and τ 2 :" Dαβ. βaepα " α ˆintq. They are semantically separable, but our type system cannot prove it. The reason why they are semantically separable is that the equations never hold in our semantic model with finite ground types, so the constrained type is empty and thus trivially separable.

  let despicable : float array = [| 0.0 ; Obj.magic 42 |] (* Produces: "segmentation fault (core dumped)" *)

  type _ data = | Char : char -> char tag | Bool : bool -> bool tag type any_function = Fun : ('a -> 'b) -> any_function type _ first = First : 'c -> ('c * 'd) first As it turns out, GADTs can be decomposed into more primitive components: standard (non-GADT) algebraic datatypes, type equalities and existential types. For instance, the above examples can be encoded as follows, using an imaginary extension of the OCaml syntax explained below. 5 type 'a data = | Char of char with ('a = char) | Bool of bool with ('a = bool) type any_function = Fun of exists 'a 'b. 'a -> 'b type 'a first = First of exists 'b 'c. 'b with ('a = 'b * 'c)

Figure 1 :

 1 Figure 1: Syntax of type expressions, datatypes, and sub-component relation.

  Figure 2: Separability modes and mode operations.

Figure 3 :

 3 Figure 3: Contexts, mode signatures, and their order

Figure 4 :

 4 Figure 4: Inference rules for separability.

τ ( σ Figure 5 :Figure 6 :

 σ56 Figure 5: Ground semantics

https://github.com/ocaml/ocaml/pull/606#issuecomment-248656482

This limit was originally set too high, and it had to be reduced to avoid type-checking slowdowns.

There is actually a third mode Deepsep (deeply separable) that will be explained in the next section.

See the OCaml manual (https://caml.inria.fr/pub/docs/manual-ocaml-4.07/extn.html#sec252) for a more thorough introduction to GADTs.

The translation can be defined in a systematic way, see for example[START_REF] Simonet | A constraint-based approach to guarded algebraic data types[END_REF].

The interpretation of existential quantifiers as unions (and dually, of universal quantifiers as intersections) is very common in realizability semantics, for example.

Constrained datatype definitions such as type 'a t = 'b constraint 'a = 'b * int may also involve equality guards, but we chose to ignore this feature here since it poses exactly the same problem.

For instance, we omit object types and polymorphic variants, but they could be handled just like products.

We could formulate the rule to only check the unique minimal context Γ 1 , but Fact 2 in Section 4 suggests that such a unique context may not always exist.

We could make our syntactic inference rules more complete by adding more equalityreasoning power to the judgment Σ; Γ $ pτ 1 " τ 2 q. For the first case pint " boolq, incompatible type constructors should not be considered equal. In the second case, pα " α ˆintq, one could add an occur-check to rule out these sort of recursive types, but note that this property (true in our model) may not hold in the real world -it doesn't in OCaml when -rectypes is used. This result suggests that equality-reasoning can be fairly subtle and that we should not expect syntactic completeness on types with constraints. We can still hope to have completeness in their absence.

Definition 2 (Constraint-free). A type τ , datatype A or definition block σ is constraint-free if it does not contain any type equality constraint (κaepα " τ 1 q). We write CFpτ q, CFpAq or CFpσq.

Conjectured Lemma 4 (Completeness on constraint-free type expressions).

CFpτ q ^Σ; Γ ( τ : m ùñ Σ; Γ $ τ : m Conjectured Theorem 2 (Completeness on constraint-free signatures).

A.2 Constraint-free principality

Unfortunately, there are more bad news to come for equality constraints.

Fact 2 (Semantic non-principality). There exists a parametrized datatype A with A ( H tpΓ 1 q and A ( H tpΓ 2 q, but A * H tpminpΓ 1 , Γ 2 qq.

Proof. Over two parameters α, β, take A :" αaepα " βq. Both Γ 1 :" α : Ind, β : Sep and Γ 2 :" α : Sep, β : Ind are admissible signatures for A. In particular, our inference rules can verify them: any Γ 1 with Γ 1 $ α " β has pα : Sep, β : Sepq. However, the minimum signature α : Ind, β : Ind is not valid for A.

Note the example in the above proof can be represented as an OCaml datatype as follows.

type (_, _) strange_eq =

| Strange_refl : 'a -> ('a, 'a) strange_eq [@@unboxed] This results shows that some limitations of the system are not due to our typing rules, but a fundamental lack of expressiveness of the current modes and mode signatures as a specification/reasoning language. We would need a richer language of modes, keeping track of equalities between types, to hope to get a principal system. Lemma 5. If Σ; Γ 1 $ τ : m and Σ; Γ 2 $ τ : m and CFpτ q then Σ; minpΓ 1 , Γ 2 q $ τ : m Proof. This proof is done by induction on the two derivations at once, but we need to use the Cut Elimination Lemma 1 first to be able to assume, by inversion/syntax-directedness, that the rules on both sides are the same.

Corollary 1 (Constraint-free principality). If Σ; Γ $ τ : m with CFpτ q, then there exists a minimal context Γ min such that Σ; Γ min $ τ : m. If Σ 0 $ σ % Σ with CFpσq, then there exists a minimal signature Σ min such that Σ 0 $ σ % Σ min .


Dalel Jabri
email: dalel.jabri@yahoo.fr

Djamel E C Belkhiat
email: djamel.belkhiat@univ-setif.dz

Hassen Fourati
email: hassen.fourati@gipsa-lab.grenoble-inp.fr

Design of a decentralized tracking control for a class of switched large-scale systems

Keywords: Output-feedback tracking control, large-scale switched systems, decentralized control, Lyapunov function. 

This paper proposes a new design of a decentralized output-feedback tracking control for a class of switched large-scale systems with external bounded disturbances. The controller proposed herein is synthesized to satisfy the robust H  tracking performance with local disturbance attenuation levels.

Based on multiple switched Lyapunov functions, sufficient conditions proving the existence of the proposed controller are formulated in terms of Linear Matrix Inequalities (LMI). A deep simulation is proposed to illustrate the effectiveness of the obtained results.

INTRODUCTION

During the latter decades, switched interconnected large-scale systems have attracted considerable attention since they provide a convenient modelling approach for many physical systems. Thus, several studies dealing with the stability analysis and stabilization issues for both linear and nonlinear switched interconnected large-scale systems have been explored by [START_REF] Chiou | Stability analysis for a class of switched large-scale time-delay systems via time-switched method[END_REF][START_REF] Belkhiat | Fault Tolerant Control for a Class of Switched Linear Systems using Generalized Switched Observer Scheme[END_REF][START_REF] Jabri | Decentralized stabilization of discrete-time large scale switched systems[END_REF][START_REF] Jabri | Decentralized control for large scale switched Takagi-Sugeno systems[END_REF][START_REF] Mahmoud | Interconnected continuous-time switched systems: Robust stability and stabilization[END_REF][START_REF] Sun | Decentralized control for a class of uncertain switched interconnected large-scale systems[END_REF][START_REF] Thanh | Decentralized stability for switched nonlinear large-scale systems with interval time-varying delays in interconnections[END_REF][START_REF] Wang | Decentralized control design for switched fuzzy large-scale systems with H  performance[END_REF]. Hence, the main challenge in treating such problems consists in determining the conditions ensuring the stability of the whole systems with consideration to the interconnections effects between its subsystems. For example, sufficient stability conditions for a class of switched large-scale time-delay systems have been delivered in [START_REF] Chiou | Stability analysis for a class of switched large-scale time-delay systems via time-switched method[END_REF]. Moreover, the problem of decentralized control for a class of switched interconnected large-scale systems with value-bounded uncertainties has been investigated in [START_REF] Sun | Decentralized control for a class of uncertain switched interconnected large-scale systems[END_REF]. By using Linear Matrix Inequalities (LMI) techniques, decentralized state-feedback controllers and decentralized switching laws have been designed to make this class of system asymptotically stable. In the same way, stabilization issue for discrete-time large-scale switched system has also been studied in [START_REF] Jabri | Decentralized stabilization of discrete-time large scale switched systems[END_REF]. Otherwise, the problem of a low-order H  output-feedback controller design, with a decentralized switching rule, for a class of interconnected continuous-time switched systems subject to disturbances has been treated in [START_REF] Mahmoud | Interconnected continuous-time switched systems: Robust stability and stabilization[END_REF])'s work . The main objective of the work seeks to guarantee the asymptotic stability of the whole system with local disturbance attenuation. Furthermore, the problem of decentralized stabilization for a class of large-scale switched Takagi-Sugeno (T-S) systems has been investigated in [START_REF] Jabri | Decentralized control for large scale switched Takagi-Sugeno systems[END_REF]. To overcome the nonlinearity problem, the large-scale switched nonlinear system was divided into a set of low-order interconnected switched T-S Fuzzy subsystems. Then, in order to stabilize the overall system, a set of switched non-PDC (Parallel Distributed Compensation) controllers has been employed. In the same context, the problem of H  control design, under asynchronous switching, for a class of switched discrete-time T-S Fuzzy large-scale systems has been explored by [START_REF] Wang | Decentralized control design for switched fuzzy large-scale systems with H  performance[END_REF]. Moreover, [START_REF] Thanh | Decentralized stability for switched nonlinear large-scale systems with interval time-varying delays in interconnections[END_REF] have studied the problem of decentralized stability for a class of switched nonlinear large-scale systems with time-varying delays in interconnections. By using a set of Lyapunov-Krasovskii functional, a delay-dependent sufficient condition for designing switching law has been established in terms of LMI. Recently, the design of an adaptive fuzzy output feedback control was developed by [START_REF] Zhang | Adaptive fuzzy output constrained decentralized control for Switched nonlinear large-scale systems with unknown dead zones[END_REF] for a class of switched nonlinear large-scale systems with unknown dead zone. Based on the above, the main advantage of the decentralized control scheme is the tremendous reduction of computational load and the design easiness of locally feedback stabilization.

Likewise, tracking control is one of the most important issues currently under consideration by researchers in linear and nonlinear control theory in [START_REF] Cabecinhas | A nonlinear quadrotor trajectory tracking controller with disturbance rejection[END_REF][START_REF] Guan | Modified tracking performance limitation of unstable linear SIMO feedback control systems[END_REF]. This kind of control has a close relationship with the stability analysis and stabilization issues. Generally, tracking control deal with the stabilization and the minimization of the error between the system output (or state) and the reference signal via designing a controller. As regards the switched systems, few results have been reported on the tracking control problem [START_REF] Belkhiat | Design of a Robust Tracking PD Controller for a Class of Switched Linear Systems with External Disturbances[END_REF][START_REF] Li | Tracking control for switched time-varying delays systems with stabilizable and unstabilizable subsystems[END_REF][START_REF] Lian | Robust H  output tracking control for switched systems under asynchronous switching[END_REF][START_REF] Liu | Exponential L1 output tracking control for positive switched linear systems with timevarying delays[END_REF]Long and Zhoa, 2015;[START_REF] Tong | Observed-based adaptive fuzzy decentralized tracking control for switched uncertain nonlinear large-scale systems with dead zones[END_REF]. For example, the work carried out by [START_REF] Liu | Exponential L1 output tracking control for positive switched linear systems with timevarying delays[END_REF] has focused on performing an exponential 1 L output tracking control for Switched Linear Systems (SLS) with time-varying delays. Similarly, the output tracking control has been studied for a class of switched systems containing stabilizable and unstabilizable subsystems in [START_REF] Li | Tracking control for switched time-varying delays systems with stabilizable and unstabilizable subsystems[END_REF]. Moreover, in [START_REF] Liu | Exponential L1 output tracking control for positive switched linear systems with timevarying delays[END_REF], a controller design approach has been proposed for a class of switched systems with time-varying delay. This one takes into account the effect of the asynchronous switching phenomena and satisfies the robust H  output-feedback tracking performance. In the same context, a robust H  output tracking control for a class of SLS using switched Proportional-Derivative (PD) controller has been designed in the reference [START_REF] Belkhiat | Design of a Robust Tracking PD Controller for a Class of Switched Linear Systems with External Disturbances[END_REF]. Based on the multiple Lyapunov functions and the adaptive fuzzy back-stepping technique, sufficient conditions for the adaptive fuzzy tracking control problem have been derived in (Long and Zhoa, 2015) for a class of switched uncertain nonlinear systems with unstable subsystems. Recently, an adaptive fuzzy decentralized tracking control for a class of switched nonlinear large-scale systems with unknown nonlinear functions has been performed in [START_REF] Tong | Observed-based adaptive fuzzy decentralized tracking control for switched uncertain nonlinear large-scale systems with dead zones[END_REF]. The proposed approach has dealt with the problems related to dead zones and unmeasurable. In a nutshell, it is worth pointing out that the aforementioned results are mainly restricted to the tracking control of lower-dimensional switched systems. Moreover, although some progress have been made in several fields of interconnected switched systems such as the stability and stabilization issues, the tracking control problem of switched interconnected largescale systems subject to external disturbances has rarely been explored so far, that which motivates the present study.

Hence, this paper presents the design of a decentralized tracking controller for a class of switched interconnected large-scale system under synchronous switching and with external bounded disturbances. The considered class consists of set of low-order interconnected subsystems. Each subsystem contains several switching modes which are described by using linear system. As regards the interconnections among different subsystems, two components, combining the state vectors and the external disturbances, are taken into account in the mathematical model representing the considered class. According to the existing literature, the contributions of this paper are the followings:  provides a new synthesis approach to design a decentralized output-feedback tracking control for a class of switched interconnected large-scale systems subject to external disturbances. By using the descriptor redundancy formulation, the proposed approach resolves the crossing terms problem related to using the output-feedback control strategy.  ensure with the designed controller, on the one hand, the stability of the overall switched interconnected large-scale systems and, on the other hand, the robust H  outputfeedback tracking performance with for each low-order subsystem a specific disturbance attenuation level.  provides sufficient conditions to design the proposed controller, formulated in terms of LMI thanks to the multiple switched Lyapunov functions.

The remainder of the paper is organized as follows. Section 2 presents the considered class of switched interconnected large-scale system, followed by the problem statement. The design of the decentralized controller is presented in section 3. A numerical example is proposed to illustrate the efficiency of the proposed approach in section 4. The paper ends with conclusions, appendix and cited references.

SYSTEM'S DESCRIPTION AND PROBLEM STATEMENT

We consider the class of the switched interconnected largescale system S . It is composed of N low-order switched subsystems denoted by i S such that each subsystem i S has its own mode number i M . Thus, the switched interconnected large-scale system S can be represented as follows for 1, , iN   :

          , ,, 1 1, ,, , ,, ij
i ij M N j i ij i ij i w i ii j ij w Axt Bu t B wt xt t Fx tFw t                            (1)    1 ,, M j i ii j i j i yt t Cxt         (2)
where   n i i xt  is the i th state vector,  m i i ut  is the

i th input vector,   m i i wt  is the 2 L -norm
   , , 1
0 ij ij ti f j l ti f j l          (3)
Note that, the mode's evolution of each i th subsystem is independent of the rest of the subsystems. Hence, the global system is represented by Fig. 1. In the sequel, we will deal with the output-feedback tracking problem for the considered class of large-scale system. The tracking control objective is to drive the outputs of the system (1)-( 2 In general, the classical way to write output-feedback dynamics consists on substituting the controller's equation (6)

into the system's equation (1), this leads to, for 1, , iN   :

  1 1 ii i , j i, ,j M N j ,i i i,j i i,j i,j r r i,j i w i ii , j i, ,j w A xB K H x C x Bw x Fx F w                           (7)
Thus, the problem considered in this study can be resumed as follows:

1 The index time (t) will be omitted in the next when there is no ambiguity.

    1 u i th subsystem S i ,, 11 ,, 2, 2 , jj NN w FF x w           Interconnections Disturbances 1 N j N M N 1 i j i M i 1 1 j 1 M 1 i u i y   ,, , , 2,
,

jj ii i N i N w FF x w    
Problem 1: The objective is to design the controllers ( 6) such that the switched interconnected large-scale system (1)-( 2) has a robust H  output-feedback tracking performance.

Definition 1:

The switched interconnected large-scale system (1)-( 2) is said to have a robust H  output-feedback tracking performance, if the following conditions are satisfied:

 Condition 1 (Stability condition): With zero disturbances input condition 0 i w  , for 1, , iN   , the closed-loop dynamics (7) is stable.  Condition 2 (Robustness condition): For all non-zero   2 0 i wL  , under zero initial condition  0 0 i xt  , it holds that for 1, , iN   , 00 1, 2 N i TT T T ii i ii i i i J eed t ww rr ww d t               (8)
By observing the closed-loop dynamics (7), it can be seen that several crossing terms among the gain controllers , ij K and the system's matrices ( ,,,

ij ij ij BKC and ,, i ij ij r BKH, for 1, , iN   , 1, , i jM   ) are present.
Hence, in view of the wealth of interconnections characterizing our system, these crossing terms lead surely to very conservative conditions for the design of the proposed controller. In order to decouple the crossing terms appearing in the equation ( 7) and to provide a LMI conditions, we use an interesting property called the descriptor redundancy (Tanaka et al., 2017). Thus, the equations ( 1)-( 2), ( 4)-( 5) and ( 6) are combined as follows for 1, , iN   :

11 i,j i, ,j M N j, i i i i,j i,j i i,j i w i i, ,j w xA x B u B w F x F w                   1 i ii ii i , N ,i rr rr r r x Ax Br F x         and 0 i ii r i ee y y    
Then, we consider the following augmented variables:

i TT T T ii r i x xxe     , , TT T T ii i ww w r       and TT T T r x xxe        .
Hence, the large-scale system (1)-( 2), the reference model ( 4) -( 5) and the controllers (6) can be reformulated as follows for 1, ,

iN   :   ,, 11 , ,, , ,, , 11 11
i ij M N ji ij i ij i ii ij ij w i A xB u NN Ex Fx B w                         (9)
The controllers are; for 1, , iN   :

1 ,,

M j i ii j i j i u K x       (10)
The tracking errors are given by; for 1, ,

iN   :  1 ,, M j i ii j i j i e Cxt       (11)
with ,, 00

ij ij KK       , ,, 0 i ij ij r CC H      , 00 00 000 i i n in I EI            , , , , 00
00 ij ij i i ij r rp A AA CH I              , , , 0
0 ij ij B B             , ,,
, ,, 00 00 00

0 ij i ij r F FF                ,     ,, , ,, 1 0 1 1 00 1 000 ij i j ij i ww wr BF N B B N                .
Note that the system ( 9) is called switched interconnected descriptor system (

   dim rank E E  ).
By substituting the equation ( 10) into the equation ( 9), the closed-loop dynamics can be written as follows for 1, ,

iN   :    ,, 11 , ,, , , ,, , 1 1
ij M N ji i ij ij ij i ii ij ij w i A BK x N Ex Fx B w                              (12)
At this stage of the work, it is worth pointing out that the output-feedback tracking control problem of the system (1)-( 2) can be converted into the stabilization problem of the augmented system (9). However, it is very complicated to work on the first problem due to the large number of crossing terms. Therefore, we will achieve our study by using the augmented system (9). Thus, the problem 1 can be reformulated as follows:

Problem 2: The objective is to design the controllers (10) such that the closed-loop switched interconnected descriptor systems ( 12) is stable with H  disturbance attenuation performance.

At the end of this section, we introduce the following definition and some mathematical materials needed in the development of our results. Then, based on the works done within the context of the switched linear systems and largescale systems in [START_REF] Zhang | Stability analysis and H  controller design of discrete-time fuzzy large-scale systems based on piecewise Lyapunov functions[END_REF][START_REF] Belkhiat | Design of a Robust Tracking PD Controller for a Class of Switched Linear Systems with External Disturbances[END_REF], we propose the following definition. given in definition 2 by the equation ( 13) is the same one given in definition 1 by equation ( 8).

Moreover, we provide the following lemma which is helpful, in the sequel, in formulating our results in terms of LMI.

Lemma 1: (Zhou and Khagonekar, 1988): Let us consider A and B two matrices with appropriate dimensions, there exists a scalar 0   such that the following inequality holds:

1 TT T T A BB A A A B B     (14)
In the following, we describe the design of the proposed output-feedback tracking control.

ROBUST TRACKING CONTROL DESIGN

The main goal of this work is to propose sufficient LMI conditions in order to determine the gain matrices

, ij K , for 1, , iN   and 1, , i jM  
, so that the robust H  outputfeedback tracking performance is satisfied. The main result is summarized in the following theorem 3 .

2 I  denotes an identity matrix with appropriate dimension.

3 As usual, in a matrix,   indicates a symmetrical transpose quantity.

Theorem 1: Assuming that the current mode is present by j and the up-coming mode by j  . Given positive scalars i  ,

,,

1 ijj    , , i   for 1, , iN   , 1, , N    , i   , 1, , i jM   and 1, , i jM    , jj   , if there exist matrices ,, T ij ij X X  ,   11 ,, 0 T ij ij XX   ,   55 ,, 0 T ij ij XX   , , ij Y and non-singular matrices 9 , ij X ,
such that the LMIs ( 15) and ( 16) hold. Then, the closed-loop switched interconnected descriptor system ( 12) is stable with

H  disturbance attenuation levels 1 2 i  
. Moreover, the controller gains are constructed by

  1 9 ,,, ij ij ij KY X   .   ,, ,, , 0 ij ij ijj ij XX X               (15)     , , , ,,, , 1, 2 1, 2 1, 2
,2 00 0

0 0 0 0 0 0 0 00 0 0 00 0 i ii ii ii ii T TTT T i j ij ij ij ij ij p inp iinp iinp Ni n p XC X X X I I I I I                                                                        (16) with ,, ij   and , ij
X are described below.

Proof: Without loss of generality, we assume that the switched interconnected descriptor system (9) is regular and impulse free in [START_REF] Sajja | Stability of a class of switched descriptor systems[END_REF]. Indeed, the present proof is divided in two parts corresponding to the conditions 1 and 2 are given in the definition 2.

 Condition 1: At this step of the study and according to the definition 2, we assume that we work under zero disturbance input condition , 0 i w    . Then, our objective is to provide sufficient conditions ensuring that the closed-loop dynamics (12) is stable. For this purpose, we consider the following candidate multiple switched Lyapunov functions:

       1,..., 1 , N ii i iN i Vx t tx t        (17) with       ,, 1 ,, i M i i ij ij i i tx t tx t        and        1 ,, , TT ij i i i ij i tx t x t E X x t     
Thus, the closed-loop dynamics ( 12) is stable under arbitrary switching signal if the following conditions ( 18), ( 19) and ( 20) are verified:

      1,..., 0 i iN Vx t    (18)       1,..., 0 i iN Vx t     (19)  There exists, for 1, , iN   , 1, , i jM   , 1, , i jM    , jj   , ,, 1 ijj    such that:       , ,, , ,, ii j i ij j j ijj j j tx t tx t          (20)
where the decreasing rates

ij i T ii i j i ii j T T ii j i i xtE X xt Vx t t x tX E xt                    .
In the sequel, we deal with the stability under arbitrary switching signal of the closed-loop switched interconnected descriptor system in three steps. In the first one, our purpose is to provide the conditions ensuring that the equality ( 18) is satisfied. Thus, we develop the inequality (18) as follows: , are called decision matrices and they can be chosen freely. Moreover, these matrices are necessary to obtain in the sequel the LMI conditions ensuring the robustness of the tracking control.

           1 ,, 1,..., 11 0 i M N TT ii j i i i j i iN ij Vx t txt E X xt          (
    1 0 T T ii , j i , j i EX X E    (22)              , , ,, ,, ,, 1, 1, 1, 1, 11 ,,, , , , , , , 1 ,, ,,, , 55 5 ,, , , 99 ,, 0 1 T
i i ij ij i j i j ii i i i N i NN ii N i T TT ij ij ij ij i i j i j T ij ij ij ij ij TT ww w w TT TT T ij r r ij i r r ij r T ij ij XA A X F F XCB Y BB F F N XA A X F F XH XX                                                          159 ,, , , ij ij ij ij Xd i
In the second step of the stability study of the closed-loop switched interconnected descriptor system, we aim to develop the inequality (19).



                1 ,, , , , 1, , 1 ,, , , ,, 11 1 , 1 1
0 i T TT ii j i j i j i j i ii j iN T TT T ij i j i i i j ij M NN ij i xA X X A x N Vx t xF X x x X F x                              (26) with ,,, , ij ij ij ij A AB K    .
Using lemma 1 and assuming that, for 1, , iN   , , 0

ii   , the inequality (26) becomes:

          1 11 1, 1 ,, , , , 2 , 1 1 , , ,, ,, , 0 ii
N M N p N ij i i T T ij ij ij ij pi n p T ij i i T T ij i i j i j ij AX X A I xx XF F X                                        (27) Inequality (27) is verified,  i x t  , for 1, , iN   , 1, , N    , i   , 1, , ii jM   , if:           1 1, 1 ,, , , , 2 1 1 ,, , , , , , 0 ii N p
N i T T ij ij ij ij pi n p T T ij i i j i j ij AX X A I XF F X                 (28)
Then, multiplying the inequality (28), left by   T i,j X and right by i,j X , it yields:

        1, 1 1 ,, , , , , , , , ,, 2 , 0 ii
N i p T TT ij ij ij ij i i j i j N T ij pi n p ij XA A X F F XI X               (29)
Remark 2: At this step, it should be stressed that the conditions (29) are not LMI and they cannot be resolved with the LMI solvers. To skip to LMI formulation, some mathematical developments should be performed. However, we end the second step of the stability study at this development level. Indeed, this matter will be discussed in greater detail in the sequel, where we will show that the conditions (29), implicitly the conditions (19), will be omitted from the Theorem 1. In the third step of the stability study, we focus on the stability conditions (20). Their aim is to ensure the global behavior of the like-Lyapunov function at the switching time jj t   .

According to the condition (20), we can write:

    1 1 , ,, , ij ij ijj XX      (30) for 1, , iN   , 1, , i jM   , 1, , i jM    , jj   , ,, 1 ijj    .
Left and right multiplying the latter condition (30) by

, ij X , we can obtain:

  1 ,, , ,, , 0 ij ij ij ij ijj XX X X     (31)
Applying Schur's complement, the LMIs (15) presented in the Theorem 1 are provided.

In the next part of the proof, we are focused on dealing with the robustness of the proposed stabilization control according to the condition 2 of the definition 2.

 Condition 2: In this subsection, we provide some sufficient conditions concerning the robustness of the proposed tracking control with local disturbance attenuation levels.

    0 11 , 1 2 ,, , , , , NN ii i TT T ii ii i i ii i ii N ii dt x J ee w w w w d t dt tx                                  (33) Such that   , ii tx   are positive for 1, , iN   , the criterion J is negative, if the following condition is verified:   11 , 2 ,, , , , 0 NN ii TT T ii ii i i ii i ii dt x ee w w w w dt                           (34)
By using the equation ( 12), the latter condition (34) can be reformulated such us:

                  1 1 1 1 ,, , , 1, 2 ,, , , , , , ,, , , ,, , , , , , ,, , 1 1
M j T T T i i ij ij N i TT T T ij i ij ij i i i i i i i i TT ii j i j i j i j i TT T ij i j ij i i ij i j TT T iw i j i i j w xC C x w w w w xA X X A x N xF X x x X F x wB X x x X B                                          , 1 11 , 0 i M N i ji i N w                           (35)
As in the previous parts, one used lemma 1and assuming that, for 1, , iN   , , 0

ii   , the inequality (35) becomes:

              ,, ,, 1 1, 1, 1, 1 ,, , , , 2 , 1 1 ,, , , , , , 2 ,, 1
,, , The latter equation ( 36) can be reformulated such as:

N ii ij i N p N i i i T T ij ij ij ij pi n p T ij i i T TT ij i i i ij ij ij N T ii i i i T TT T i w ij i i ij w AX X A I xx XF F X C C ww wB X x x
   1 ,, 1, 1 1, 11 , , 2 ,, ,, 0 T j ij i N M N i N i i T ij w ii ij ii ii i ij XB x w x w                                             (37) with           1 11 , , , , , 2 1 1 1 , , ,, , ,, 1, ii
N T T ij ij ij ij pi n p p N T TT ij i i i ij ij ij i AX X A I X FF X CC                 
Based on the inequality (37), the global criterion J , given by equation ( 33), is negative if the following sufficient condition is verified for 1, ,

iN   , 1, , N    , i   , 1, , i jM   ; ,, 0 ij T   (38)
In other words, the verification of the inequality ,, 0

ij    , for 1, , iN   , 1, , N    , i   , 1, , i jM   , implies that each local criterion i J , for 1, , iN   , is satisfied
separately as required in the definition 2.

Applying the inverse of Schur's complement, we can write ,,

0 ij   as follows; for 1, , iN   , 1, , N    , i   , 1, , i jM   :              ,, , , 1, 1, 1 ,, , , , , 1 1 ,, 1, 1 1 ,, , , , , 2 1
, 1 0 ij ij ii N ii T TT ij ij ij ij ij ij NN T T ij w i i i w ij i NN T T ij i i i ij pi n p ip AX X A C C XB BX XF F X I                                        (39) with   1 2 ii    .
Multiplying the latter inequality (39), left by   T i,j X and right by i,j X , we obtain the following inequalities for

1, , iN   , 1, , N    , i   , 1, , i jM   :         1 ,, , , 1, 1, 1, 1, 1 ,,, , ,, , , , , , ,, , 1 0
ij ij N i NN N ii i TT TT T ij ij ij ij ij ij ij ij i i i N T T pi ij ij w i i i w p XA A X XC C X F F XX B B                                    (40)
Remark 3: At this step of study, a significant simplification, that relates both inequalities ( 29) and ( 40), can be considered. Indeed, regarding the inequality (29), we can remark that it is bounded by the inequality (40). Then, the inequality (29) will be systematically verified when the inequality (40) is satisfied. For this reason, the inequality ( 29) is omitted from the Theorem 1 as mentioned above in the remark 2. Hence, the Theorem 1 contains only the condition (40) formulated in terms of LMI (readers are referred to the appendix section).

Remark 4: Based on the study above, the design procedure of the switched decentralized tracking control for interconnected switched systems is summarized as follows:

Step.1. Construct the mathematical model of the real system according to equations ( 1) and ( 2)

Step.2. Choose stable interconnected systems as a reference model according to equations ( 4) and (5).

Step.3. Solve the LMI conditions ( 15) and ( 16) of the theorem 1, using LMI solver, in order to obtain the matrices 1 , ij Step.4. Construct the controller gains

  1 9 ,,, ij ij ij KY X   .
Step.5. Implement the obtained switched decentralized controller in the control scheme.

SIMULATION AND RESULTS

In this section, we illustrate the effectiveness of the proposed decentralized tracking control via a numerical simulation. For that, we consider the following switched interconnected large-scale system S composed of three continuous-time switched subsystems 1 S , 2 S and 3 S :

Subsystem 1 S is:             2 1 1 12 13 11 11 1 1 2 2 11 13 3 2 3 j ,j ,, j ,, j ,j ,j w , ,j ,j ,, j w w A xt But B wt F x t xt t Fxt F wt F w t                    2 11 , 1 , 1 1 jj j yt C x t         with,
    1 01 0 2 0 T x  ,     2 01 0 2 0 T x   ,    3 01 5 2 3 T x  .
As stated above, each subsystem has its own mode's evolution independently from other subsystems. Noting that the large-scale system S is unstable.

As mentioned above, we consider the following reference large-scale model to specify the desired trajectory for the overall large-scale system S . This reference model is composed of three subsystems: 2 nd Subsystem:

1 st Subsystem:           1 11 11 1 , 2 2
          2 22 22 2 , 1 2

CONCLUSION

In this paper, the problem of the decentralized outputfeedback tracking control, intended to drive a class of switched interconnected large-scale systems subject to disturbances, has been studied. Two kinds of the interconnections between different subsystems have been considered: interconnections depending on state vector and those depending on unknown disturbances. By effectively using the descriptor redundancy formulation, some new sufficient conditions, which guarantee that the proposed controller had the H  output-feedback tracking performance, have been derived. These conditions have been reformulated in terms of LMI thanks to the multiple switched Lyapunov functions. Some concrete simulations are achieved to illustrate the effectiveness of the proposed approach. Moreover, considering the performances obtained in this work in terms of output-feedback tracking control under synchronous switching, relaxation of this assumption and extension of the proposed approach to general switched systems under asynchronous switching will be the focus of future work.    

,, ,,

ij ij N i NN N ii i T TT T ij ij ij ij i i i ij i ij T wi i i 1, 1, 1, 1, 1 ,, , , , , , ,, 1 0
N i NN ii ij ij i j i j i TT TT T ij ij ij ij ij ij ij TT T ij ij ij T i j ij ij ij i i j i j ij ij ij ij ij 1, , , ,, ,, 17 1 ,, , , , , , 17 ,, , 71 8 ,, , , , , ,, ,, , , , 9 ,,, 5 , 1 T
                          

Fig. 1 .

 1 Fig. 1. System representation.In order to drive our system S and to ensure the H  tracking performance, decentralized switched controller is proposed in this work. The key idea is to synthesize a global controller composed of N local switched controllers. Each local controller is associated to a switched subsystem. The purpose of the local controllers is to ensure the stability and the output-feedback tracking performance of subsystems, while taking into account the problems related to the interconnections among the subsystems. In this work, the local switched controllers and the switched subsystems are synchronously orchestrated. Thus, the set of N local switched controllers are defined as follows for 1, , iN   :   1

  mode j to the up-coming j  and

  using the Matlab LMI toolbox, a solution of the Theorem 1 is obtained and leads to the design of the proposed control. This latter is composed of three local switched controllers of the form (6) and defined as follows:

Fig. 2 .

 2 Fig. 2. The tracking errors evolution, computed between the outputs of the large-scale system S and the reference model, are depicted in Fig. 3. As expected, the outputs   i yt of the

Fig. 3 .

 3 Fig. 3. Evolution of tracking errors. APPENDIX A In this section, we are focused on formulating the inequality (40) in terms of LMI. We recall that 0 ii   , the latter inequality (40) can be written as follows for 1, , iN   , 1, , N    ,

  ), we can obtain the inequality (43).Remark 5: It is important to note that the inequality (43) is not a LMI due to the presence of the quadratic terms ( A way to skip to LMI conditions is to act on decision matrices mentioned in the remark 1. Hence, we choose (for 1

  bounded external disturbance associated to the i th subsystem.

	  n xt     and	  m wt     denote respectively the state
	vector and the 2 L -norm bounded external disturbance of the
	 th subsystem with	1, , N   	and	i   .   p i i yt  is
	the measurement (output) associated to the i th subsystem. j
	denoted the mode of each i th subsystem.	, ij A		nn ii 	,
	, ij B		nm ii 	,	, ij C		p n ii 	are constant matrices,
	,, ij F 		nn i  	and	,, ij w F 		nm i  	are constant matrices
	which describe the influences of the  th subsystem on the i th one. Finally   , ij t  are the switching rules. They are
	assumed to be real time available. The switching rules   , ij t 	are defined that the i th
	subsystem is active in the l th mode, that is to say:

  for mode 1,

													11 , A		01 05 -. .. 1 11    	,	11 , B 	2 0      	,	with, for mode 1, 31 , A		  	14 6 10 5 -. .. 11 12 1    	, 31 , B		  	275 01 . .	  	,
	11 , w B	01 01 . .     	, 121 ,, F		001 02 00 1 .. .   	, 131 ,; F		01 0 01 01 . ..   	,	31 , w B		  	12 01 . . 	  	, 311 ,, F		  	001 07 00 1 .. .    	, 321 ,, F		  	01 10 1 0 . .    	,
	121 ,, w F		001 01 . .   	,	131 ,, w F		01 01 . .   	and	11 , C 		40		311 ,, w F	001 01 . .        	,	321 ,, w F	01 01 . .        	and	 C.  31 265 0 ,	
	and for mode 2 , 12 , A		10 2 5 039 15 -. .-.   	,	12 , B		0 03 .      	,	and for mode 2,	32 , A		15 9 9 2 10 2 13 -. . .-  	,	32 , B		  	0 076 .	  	,
	12 , w B	01 01 . .     	, 122 ,, F		01 0 02 01 . ..   	, 132 ,, F		01 002 01 0 . ..   	,	32 , w B	045 01 . .        	, 312 ,, F		  	001 08 .. 01 01 ..    	, 322 ,, F		  	01 001 20 1 .. .   	,
	122 ,, w F			01 01 . .   	,	132 ,, w F		01 01 . .   		and	12 , C 		03		.	312 ,, w F		001 01 . .      	,	322 ,, w F		01 01 . .      	and	 C.  32 03 4 5 ,		.
	Subsystem 2 S is:																	The	initial	states	are	given	as	follow:
	 22 2 1 j xt     ,j A xt But B wt           2 2 23 21 22 2 2 2 1 1 2 3 3 31 ,j ,, j ,, j ,j ,j w , ,j , ,j ww t F xt F xt Fw tFw t          
	 jj 2 , 2 yt C x t  2 1 22 , j      
	with, for mode 1,			21 , A			46 15 -. .. 2 01    	,	21 , B 	25 0 .      	,
	21 , w B		02 01 . .    	, 211 ,, F		10 2 001 01 . ..   	, 231 ,, F		10 2 001 0 . .   	,
	211 w,, F		1 01 .   		,	231 ,, w F		1 0   	and	 C.  21 35 0 ,		,
	and for mode.2,				22 , A		40 2 12 3 -. .-  	, 22 , B		0 06 .      	,
	22 , w B	02 01 . .     	,	212 ,, F		01 1 05 01 . ..   	, 232 ,, F		04 002 01 1 . ..   	,
	212 ,, w F			01 01 . .   	,	232 ,, w F		04 01 . .   		and		 C.  22 03 2 ,	
	Subsystem 3 S is:
	 33 2 1 j xt     ,j A xt    31 33 3 1 1 12    3 3 3 2 3 3 2 2 ,,j , ,j ,j ,j w , ,j , ,j ww But B wt   3 ,j t F xt F xt Fw tFw t          
	 jj 3 , 3 yt C x t  2 33 , 1 j      

Powered by TCPDF (www.tcpdf.org)