S Salvati

I Walukiewicz

Using models to model-check recursive schemes

We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, λY -calculus, is equivalent to schemes, we propose to use a model of λY to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. We provide a construction of such a model for every property expressed by automata with trivial acceptance conditions and divergence testing. We argue that having a model capable of recognizing terms satisfying a given property has other benefits than just providing decidability of the model-checking problem. We show a very simple construction transforming a scheme to a scheme reflecting a given property.

Introduction

Recursive schemes are abstract forms of programs where the meaning of constants is not specified. In consequence, the meaning of a scheme is a potentially infinite tree labeled with constants obtained from the unfolding of the recursive definition. Recursive schemes can be also represented in the λY -calculus: simply typed λ-calculus with fixpoint combinators. In this context the meaning of a scheme is just the Böhm tree of a term.

We consider the model checking problem: given a λY -term decide if the Böhm tree it generates is accepted by a given tree automaton with trivial acceptance conditions. The main novelty of the present work is to solve this problem using models for λY -calculus. For a given automaton we construct a finitary model such that the value of a term in this model tells us if the automaton accepts the Böhm tree of the term. The principal technical challenge we address here is that we allow automata to detect if a term has a head normal form. We call such automata insightful as opposed to Ωblind automata that are insensitive to divergence. For example, the models studied by Aehlig [START_REF] Aehlig | A finite semantics of simply-typed lambda terms for infinite runs of automata[END_REF] or Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF] are Ω-blind.

As the name suggests automata with trivial acceptance conditions (TAC automata for short) are a very special case of tree automata. In terms of expressive power they can recognize precisely the safety properties. It has been found by Aehlig [Aeh07] that for recursive schemes the model checking problem is conceptually much easier if restricted to automata with trivial conditions. Subsequently Kobayashi has presented a type system for this variant of the model checking problem. This system has been a basis of a successful implementation and application effort [START_REF] Kobayashi | Model-checking higher-order functions[END_REF][START_REF] Lester | Model checking liveness properties of higher-order functional programs[END_REF][START_REF] Kobayashi | A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes[END_REF]. Recall that the decidability of the general case of the model-checking problem has been shown by Ong [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF], and then reproved several times using a number of different methods [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF][START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF][START_REF] Salvati | Krivine machines and higher-order schemes[END_REF]. Yet none of them is as simple as the case of automata with trivial conditions, and none of them has been implemented.

In this paper we look closer at the issue that has been somehow pushed aside in previous works. The semantics of a recursive scheme says that if the scheme gets into an infinite computation without producing a new head symbol then in the resulting tree we get a special symbol Ω. Yet this is not how this issue is treated in all known solutions to the modelchecking problem. There, instead of reading Ω the automaton is let to run on the infinite sequence of unproductive reductions. In case of automata with trivial conditions, this has an immediate consequence that such an infinite computation is accepted by the automaton. So, for example, with this approach to semantics the language of schemes that produces at least one head symbol is not definable by automata with trivial conditions. Let us note that this problem disappears once we consider Büchi conditions as they permit to detect an infinite unproductive execution. So here we look at the particular class of properties expressible by a Büchi condition.

In our opinion solving the model-checking problem using models for λYcalculus is important. First, models need to handle all the constructions of the λ-calculus while, for example, the type systems proposed so far by Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF], and by Kobayashi and Ong [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF] do not cater for λ-abstraction. In consequence the model-based approach gives more insight into the solution while, from algorithmic point of view, offering the same advantages as typing [START_REF] Salvati | Loader and Urzyczyn are logically related[END_REF]. To substantiate we present a straightforward transformation of a scheme to scheme reflecting a given property [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF]. More importantly, the model based approach opens a new bridge between λ-calculus and model-checking communities. In particular the model we construct for insightful automata brings into the front stage particular nonextremal fixpoints. To our knowledge these were not much studied in λcalculus literature.

The main result of the paper is a construction of a finitary model from a given insightful automaton with trivial acceptance conditions. The meaning of a term in this model determines if the Böhm tree of the term is accepted by the automaton. In this model the fixpoint operator is neither the greatest nor the least one. Indeed, and this is the second result of the paper, models with extremal fixpoints correspond exactly to boolean combinations Ω-blind automata with trivial acceptance conditions. The third result is a transformation of a term into a term reflecting a given property in a sense of [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF]. Roughly, a scheme reflects some property when during its execution it knows if the tree generated from the current point satisfies the property or not. This is a very useful technical property [START_REF] Broadbent | The Limits of Decidability for First Order Logic on CPDA Graphs[END_REF], that can also be used in program transformation. The known solutions to this problem are based on a translation to collapsible pushdown automata, so the obtained scheme has no resemblance to the initial one. With the help of models we get a simple and direct translation.

Related work

The model checking problem for schemes with respect to monadic second-order logic has been solved by Ong [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF] and subsequently revisited in a number of ways [HMOS08, [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF][START_REF] Salvati | Krivine machines and higher-order schemes[END_REF]. Much simpler proof for the same problem in the case of automata with trivial conditions have been given by Aehlig [START_REF] Aehlig | A finite semantics of simply-typed lambda terms for infinite runs of automata[END_REF]. In his influential work, Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF][START_REF] Kobayashi | Higher-order program verification and languagebased security[END_REF][START_REF] Kobayashi | Types and recursion schemes for higher-order program verification[END_REF] has shown that many interesting properties of higher-order recursive programs can be analyzed with recursive schemes and automata with trivial conditions. He has also proposed an intersection type system for the model-checking problem. The method has been applied to verification of higher-order programs. In a recent work Ong and Tsukada [START_REF] Ong | Two-level game semantics, intersection types, and recursion schemes[END_REF] provide a game semantics model corresponding to Kobayashi style proof system. Their model can handle only Ω-blind automata, but then it is fully complete. We cannot hope to have full completeness in our approach using simple models. In turn, as we mention in [START_REF] Walukiewicz | Simple models for recursive schemes[END_REF] and show here, handling Ω-blind automata with simple models is straightforward. Reflection property for schemes have been proved by Broadbent et. al. [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF]. Haddad gives a direct transformation of a scheme to an equivalent scheme without divergent computations [START_REF] Haddad | IO vs OI in higher-order recursion schemes[END_REF].

Organization of the paper We find that the richer syntax of λY -calculus offers more freedom than that of schemes. Yet the two formalism are closely related and there are direct translations between them (cf. [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF]). The next section introduces objects of our study: λY -calculus and automata with trivial acceptance conditions (TAC automata). In the following section we present the correspondence between models of λY with greatest fixpoints and boolean combinations of Ω-blind TAC automata. In Section 4 we give the construction of the model for insightful TAC automata. The last section presents a transformation of a term into a term reflecting a given property.

Preliminaries

We introduce two basic objects of our study: λY -calculus and TAC automata. We will look at λY -terms as mechanisms for generating infinite trees that then are accepted or rejected by a TAC automaton. The definitions we adopt are standard ones in the λ-calculus and automata theory. The only exceptions are the notions of a tree signature used to simplify the presentation and of Ω-blind/insightful automata that are specific to this paper.

λY -calculus and models

The set of types T is constructed from a unique basic type 0 using a binary operation →. Thus 0 is a type and if α, β are types, so is (α → β). The order of a type is defined by: order (0) = 1, and order (α → β) = max(1 + order (α), order (β)).

A signature, denoted Σ, is a set of typed constants, that is symbols with associated types from T . We will assume that for every type α ∈ T there are constants ω α , Ω α and Y (α→α)→α . A constant Y (α→α)→α will stand for a fixpoint operator. Both ω α and Ω α will stand for undefined, but we will need two such constants in Section 4. Of special interest to us will be tree signatures where all constants other than Y , ω and Ω have order at most 2. Observe that types of order 2 have the form 0 i → 0 for some i; the latter is a short notation for 0 → 0 → • • • → 0 → 0, where there are i + 1 occurrences of 0.

Proviso: To simplify the notation we will suppose that all the constants in a tree signature are either of type 0 or of type 0 → 0 → 0. So they are either a constant of the base type or a function of two arguments over the base type. This assumption does not influence the results of the paper.

The set of simply typed λ-terms is defined inductively as follows. A constant of type α is a term of type α. For each type α there is a countable set of variables x α , y α , . . . that are also terms of type α. If M is a term of type β and x α a variable of type α then λx α .M is a term of type α → β. Finally, if M is of type α → β and N is a term of type α then M N is a term of type β.

The usual operational semantics of the λ-calculus is given by β-contraction. To give the meaning to fixpoint constants we use δ-contraction (→ δ ).

(λx.M )N → β M [N/x] Y M → δ M (Y M ).
We write → * βδ for, the βδ-reduction, the reflexive and transitive closure of the sum of the two relations (we write → + βδ for its transitive closure). This relation defines an operational equality on terms. We write = βδ for the smallest equivalence relation containing → * βδ . It is called βδ-conversion or βδ-equality. Given a term M = λx 1 . . . x n .N 0 N 1 . . . N p where N 0 is of the form (λx.P )Q or Y P , then N 0 is called the head redex of M . We write M → βδh M when M is obtain by βδ-contracting the head redex of M (when it has one). We write → * βδh and → + βδh respectively for the reflexive and transitive closure and the transitive closure of → βδh . The relation → * βδh is called head reduction. A term with no head redex is said in head normal form.

Thus, the operational semantics of the λY -calculus is the βδ-reduction. It is well-known that this semantics is confluent and enjoys subject reduction (i.e. the type of terms is invariant under computation). So every term has at most one normal form, but due to δ-reduction there are terms without a normal form. A term may not have a normal form because it does not have head normal form, in such case it is called unsolvable. Even if a term has a head normal form, i.e. it is solvable, it may contain an unsolvable subterm that prevents it from having a normal form. Finally, it may be also the case that all the subterms of a term are solvable but the reduction generates an infinitely growing term. It is thus classical in the λ-calculus to consider a kind of infinite normal form that by itself is an infinite tree, and in consequence it is not a term of λY [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF][START_REF] Amadio | Domains and Lambda-Calculi[END_REF].

A Böhm tree is an unranked, ordered, and potentially infinite tree with nodes labelled by terms of the form λx 1 . . . . x n .N ; where N is a variable or a constant, and the sequence of λ-abstractions is optional. So for example x 0 , Ω 0 , λx 0 .ω 0 are labels, but λy 0 . x 0→0 y 0 is not.

Definition 1 A Böhm tree of a term M is obtained in the following way.

• If M → * βδ λ x.N 0 N 1 . . . N k with N 0 a variable or a constant then BT (M ) is a tree having root labelled by λ x.N 0 and having BT (N 1 ), . . . , BT (N k ) as subtrees.

• Otherwise BT (M ) = Ω α , where α is the type of M .

Observe that a term M without the constants Ω and ω has a βδ-normal form if and only if BT (M ) is a finite tree without the constants Ω and ω. In this case the Böhm tree is just another representation of the normal form. Unlike in the standard theory of the simply typed λ-calculus we will be rather interested in terms with infinite Böhm trees.

Recall that in a tree signature all constants except of Y , Ω, and ω are of type 0 or 0 → 0 → 0. A closed term without λ-abstraction and Y over such a signature is just a finite binary tree, where constants of type 0 are in leaves, and constants of type 0 → 0 → 0 are in the internal nodes. The same holds for Böhm trees:

Lemma 2 If M is a closed term of type 0 over a tree signature then BT (M ) is a potentially infinite binary tree.

We will consider finitary models of λY -calculus. In the first part of the paper we will concentrate on those where Y is interpreted as the greatest fixpoint (those with least fixpoints are just dual to these ones).

Definition 3 A GFP-model of a signature Σ is a tuple S = {S α } α∈T , ρ where S 0 is a finite lattice, and for every type α → β ∈ T , S α→β is the lattice mon[S α → S β ] of monotone functions from S α to S β ordered coordinatewise. The valuation function ρ is required to satisfy certain conditions:

• If c ∈ Σ is a constant of type α then ρ(c) is an element of S α .
• For every α ∈ T , both ρ(ω α ) and ρ(Ω α ) are the greatest elements of S α .

• Moreover, ρ(Y (α→α)→α ) is the function assigning to every function f ∈ S α→α its greatest fixpoint.

Observe that every S α is finite, hence all the greatest fixpoints exist without any additional assumptions on the lattice. A variable assignment is a function υ associating to a variable of type α an element of S α . If s is an element of S α and x α is a variable of type α then υ[s/x α ] denotes the valuation that assigns s to x α and that is identical to υ otherwise.

The interpretation of a term M of type α in the model S under the valuation υ is an element of

S α denoted [[M ]] υ S .
The meaning is defined inductively:

• [[c]] υ S = ρ(c) • [[x α ]] υ S = υ(x α ) • [[M N ]] υ S = [[M ]] υ S ([[N ]] υ S ) • [[λx α .M ]] υ S is a function mapping an element s ∈ S α to [[M ]] υ[s/x α ] S
that by abuse of notation we may write λs.

[[M ]] υ[s/x α ] S .
As usual, we will omit subscripts or superscripts in the notation of the semantic function if they are clear from the context.

Of course a GFP model is sound with respect to βδ-conversion. Hence two βδ-convertible terms have the same semantics in the model. For us it is important that a stronger property holds: if two terms have the same Böhm trees then they have the same semantics in the model. For this we need to formally define the semantics of a Böhm tree.

The semantics of a Böhm tree is defined in terms of its truncations. For every n ∈ N, we denote by BT (M ) ↓ n the finite term that is the result of replacing in the tree BT (M ) every subtree at depth n by the constant ω α of the appropriate type. Observe that if M is closed and of type 0 then α will always be the base type 0. This is because we work with a tree signature. We define

[[BT (M )]] υ S = {[[BT (M ) ↓ n ]] υ S | n ∈ N}.
The above definitions are standard for λY -calculus, or more generally for PCF [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]. In particular the following proposition, in a more general form, can be found as Exercise 6.1.8 in op. cit.

Proposition 1 If S is a finite GFP-model and M is a closed term then:

[[M ]] S = [[BT (M )]] S .

TAC Automata

Let us fix a tree signature Σ. Recall that this means that apart from ω, Ω and Y all constants have order at most 2. According to our proviso from page 4 all constants in Σ have either type 0 or type 0 → 0 → 0. In this case, by Lemma 2, Böhm trees are potentially infinite binary trees. Let Σ 0 be the set of constants of type 0, and Σ 2 the set of constants of type 0 → 0 → 0.

Definition 4 A finite tree automaton with trivial acceptance condition (TAC automaton) over the signature

Σ = Σ 0 ∪ Σ 2 is A = Q, Σ, q 0 ∈ Q, δ 0 : Q × (Σ 0 ∪ {Ω}) → {ff , tt}, δ 2 : Q × Σ 2 → P(Q 2 )
where Q is a finite set of states and q 0 ∈ Q is the initial state. The transition function of TAC automaton may be the subject to the additional restriction: Ω-blind: δ 0 (q, Ω) = tt for all q ∈ Q.

An automaton satisfying this restriction is called Ω-blind. For clarity, we use the term insightful to refer to automata without this restriction.

Automata will run on Σ-labelled binary trees that are partial functions t : {1, 2} * → Σ∪{Ω} such that their domain is a binary tree, and t(u) ∈ Σ 0 ∪{Ω} if u is a leaf, and t(u) ∈ Σ 2 otherwise.

A run of A on t is a mapping r : {1, 2} * → Q with the same domain as t an such that:

• r(ε) = q 0 , here ε is the root of t.

• (r(u1), r(u2)) ∈ δ 2 (t(u), r(u)) if u is an internal node.
A run is accepting if δ 0 (r(u), t(u)) = tt for every leaf u of t . A tree is accepted by A if there is an accepting run on the tree. The language of A, denoted L(A), is the set of trees accepted by A.

Observe that TAC automata have acceptance conditions on leaves, expressed with δ 0 , but do not have acceptance conditions on infinite paths.

As underlined in the introduction, all the previous works on automata with trivial conditions rely on Ω-blind restriction. Let us give some examples of properties that can be expressed with insightful automata but not with Ω-blind automata.

• The set of terms not having Ω in their Böhm tree. To recognize this set we take the automaton with a unique state q. This state has transitions on all the letters from Σ 2 . It also can end a run in every constant of type 0 except for Ω: this means δ 0 (q, Ω) = ff and δ 0 (q, c) = tt for all other c.

• The set of terms having a head normal form. We take an automaton with two states q and q . From q automaton accepts every tree.

From q it has transitions to q on all the letters from Σ 2 , on letters from Σ 0 it behaves as the automaton above.

• Building on these two examples one can easily construct an automaton for a property like "every occurrence of Ω is preceded by a constant err".

It is easy to see that none of these languages is recognized by Ω-blind automaton since if such an automaton accepts a tree t then it accepts also every tree obtained by replacing a subtree of t by Ω. This observation also allows to show that those languages cannot be defined as boolean combinations of Ω-blind automata.

GFP models and Ω-blind TAC automata

In this section we show that the recognizing power of GFP models coincides with that of boolean combinations of Ω-blind TAC automata. For every automaton we will construct a model capable of discriminating the terms accepted by the automaton. For the opposite direction, we will construct a collection of TAC automata from a model. We start with the expected formal definition of a set of λY -terms recognized by a model. We now give some notations that we shall use in the course of the proofs. Given a closed term M of type 0, the tree BT (M ) can be seen as a binary tree t : {1, 2} * → Σ. For every node in the domain of t, we write M v for the subtree of t rooted at node v. The tree BT (M ) ↓ k is a prefix of this tree containing nodes up to depth k, denote it t k . Every node v in the domain of t k corresponds to a subterm of BT (M ) ↓ k that we denote M k v .

Proposition 2 For every Ω-blind TAC automaton A, the language of A is recognized by a GFP model.

Proof

For the model S A in question we take a GFP model with S 0 = P(Q). This defines S α for every type α. It remains to define the interpretation of constants other than ω, Ω, or Y . A constant c of type 0 is interpreted as a set {q | δ 1 (q, c) = tt}. A constant a of type 0 → 0 → 0 is interpreted as a function whose value on (S 0 , S 1 )

∈ P(Q) 2 is {q | δ 2 (q, a) ∩ S 0 × S 1 = ∅}.
Finally, for the set F A used to recognize L(A) we will take {S | q 0 ∈ S};

recall that q 0 is the initial state of A. We want to show that for every closed term M of type 0:

BT (M ) ∈ L(A) iff [[M ]] ∈ F A .
For the direction from left to right, we take a λY -term M such that BT (M ) ∈ L(A), and show that

q 0 ∈ [[BT (M )]]. This will do as [[BT (M )]] = [[M ]] by Proposition 1. Recall that [[BT (M )]] = {[[BT (M ) ↓ k ]] | k = 1, 2, . . . }. So it is enough to show that q 0 ∈ [[BT (M ) ↓ k ]] for every k.
Let us assume that we have an accepting run r of A on BT (M ). By induction on the height of v in the domain of

BT (M ) ↓ k we show that r(v) ∈ [[M k v ]].
The desired conclusion will follow by taking v = ε; that is the root of the tree. If v is a "cut leaf" then

M k v is ω 0 . So r(v) ∈ Q = [[ω 0 ]]. If v is a "normal" leaf then M k v is a constant c of type 0. We have r(v) ∈ {q : δ(q, c) = tt}. If v is an internal node then M k v = aM k v1 M k v2 . By induction assumption r(v1) ∈ [[M k v1 ]] and r(v2) ∈ [[M k v2 ]]. Hence by definition of ρ(a) we get r(v) ∈ [[M v ]] = ρ(a)([[M k v1 ]], [[M k v2 ]]
) . For the direction from right to left we take a term M and a state q ∈ [[M ]]. We construct a run of A on BT (M ) that starts with the state q. So we put r(ε) = q. By Proposition 1, we know that q ∈ [[BT (M ) ↓ k ]] for all k. There is a letter a such that every term BT (M ) ↓ k is of the form ω or aM k 1 M k 2 . Since δ(q, a) is a finite set of pairs, there is a pair (q 1 , q 2 ) ∈ δ(q, a) such that

q 1 ∈ [[M k 1 ]] and q 2 ∈ [[M k 2 ]
] for infinitely many k. We repeat the argument with the state q 1 from nodes 1 and with the state q 2 from node 2. It is easy to see that this gives an accepting run of A.

We are now going to see that the power of GFP models is characterized by Ω-blind TAC automata. We will show that every language recognized by a GFP model is a boolean combination of languages of Ω-blind TAC automata. For the rest of the subsection we fix a tree signature Σ and a GFP model S = {S α } α∈T , ρ over Σ.

We construct a family of automata that reflect the model S. We let Q be equal to the set S 0 . We define δ 0 : Q × Σ 0 ∪ {Ω} → {ff , tt} and δ 1 : Q × Σ 2 → P(Q 2 ) to be the functions such that:

δ 0 (q, a) =tt iff q ≤ ρ(a)
(in the order of S 0 ) δ 1 (q, a) ={(q 1 , q 2 ) | q ≤ ρ(a)(q 1 , q 2 )}.

For q in Q, we define A q to be the automaton with the starting state q and the other components as above:

A q = Q, Σ, q, δ 0 , δ 1
We have the following lemma:

Lemma 6 Given a closed λ-term M of type 0:

BT (M ) ∈ L(A q ) iff q ≤ [[M ]].

Proof

We start by showing that if

A q accepts BT (M ) then q ≤ [[M ]]. Proposition 1 reduces this implication to proving that q ≤ [[BT (M )]]. Since [[BT (M )]] = {[[BT (M ) ↓ k ]] | k ∈ N}, we need to show that for every k > 0, q ≤ [[BT (M ) ↓ k ]]
. Fix an accepting run r of A q on BT (M ). We are going to show that for every v in the domain of

BT (M ) ↓ k , r(v) ≤ [[M k v ]]. This will imply that r(ε) = q ≤ [[BT (M )]] ↓ k .
We proceed by induction on the height of v.

In case v is a "cut leaf" then M k v is ω 0 and [[M k v ]] is the greatest element of S 0 so that r(v) is indeed smaller than [[M k v ]].
In case v is a "normal leaf" then M k v is a constant c of type 0. Since r is an accepting run, we need to have, by definition,

r(v) ≤ ρ(c) = [[M k v ]]. In case v is an internal node then M k v = aM k v1 M k v2
, and, by induction, we have that r

(vi) ≤ [[M k vi ]].
Moreover, because r is a run, we need to have r(v) ≤ ρ(a)(r(v1))(r(v2)), but since ρ(a) is monotone, and

r(vi) ≤ [[M k vi ]], we have ρ(a)(r(v1))(r(v2)) ≤ ρ(a)([[M k v1 ]])([[M k v2 ]]) = [[M k v ]]. This proves, as expected, that r(v) ≤ [[M k v ]]. Now given q ≤ [[M ]
] we are going to construct a run of A q on BT (M ). For a node v of BT (M ) let M v denote the subtree rooted in this node. Take r defined by r(v) = [[M v ]] for every v. We show that r is a run of the automaton A

[[M ]] . Since q ≤ [[M ]]
, by the definitions of δ 0 andδ 1 , this run can be easily turned into a run of A q .

By definition

r(ε) = [[M ]] = [[BT (M )]].
In case v is a leaf c, then r(v) = ρ(c) and we have δ 0 (c, ρ(c)) = tt. In case v is an internal node labeled by a, then, by definition

[[M v ]] = ρ(a)([[M v1 ]], [[M v2 ]]), so ([[M v1 ]], [[M v2 ]]) is in δ 1 (a, [[M v ]]).
This lemma and Proposition 2 allow us to infer the announced correspondence.

Theorem 7 A language L of λ-terms is recognized by a GFP-model iff it is a boolean combination of languages of TAC automata.

Proof

For the left to right direction take a model S and p ∈ S 0 . By the above lemma we get that the language recognized by {p} is

L p = L(A p ) -{L(A q ) | q ≤ p}
So given F included in S 0 , the language recognized by F is p∈F L p .

For the other direction we take an automaton for every basic language in a boolean combination. We make a product of the corresponding GFP models given by Proposition 2, and take the appropriate F defined by the form of the boolean combination of the basic languages.

Using the results in [START_REF] Salvati | Loader and Urzyczyn are logically related[END_REF], it can be shown that typings in Kobayashi's type systems [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF] give precisely values in GFP models.

A model for insightfull TAC automata

The goal of this section is to present a model capable of recognizing languages of insightful TAC automata. Theorem 7 implies that the fixpoint operator in such a model can be neither the greatest nor the least fixpoint. In the first subsection we will construct a model containing at the same time a model with the least fixpoint and a model with the greatest fixpoint. We cannot just take the model generated by the product of the base sets of the two models as we will need that the value of a term in the least fixpoint component influences the value in the greatest fixpoint component. In the second part of this section we will show how to interpret insightful TAC automata in such a model.

Model construction and basic properties

In this section we build a model K intended to recognize the language of a given insightful TAC automaton. This model is built on top of the standard model D for detecting if a term has a head-normal form.

Consider a family of sets {D α } α∈T ; where D 0 = {⊥, } is the two elements lattice, and D α→β is the set of monotone functions from D α to D β . So for every α, D α is a finite lattice. We shall refer to the minimal and maximal element of D α respectively with the notations ⊥ α and α .

Consider the model D = {D α } α∈T , ρ where ω and Ω are interpreted as the least elements, and Y is interpreted as the least fixpoint operator. So D is a dual of a GFP model as presented in Definition 3. The reason for not taking a GFP model here is that we would prefer to use the greatest fixpoint later in the construction. To all constants other than Y , ω, and Ω the interpretation ρ assigns the greatest element of the appropriate type. The following theorem is well-known (cf [AC98] page 130).

Theorem 8 For every closed term M of type 0 without ω we have:

BT (M ) = Ω iff [[M ]] D = ⊥.
We fix a finite set Q and Q Ω ⊆ Q. Later these will be the set of states of a TAC automaton, and the set of states from which this automaton accepts Ω, respectively. To capture the power of such an automaton, we are going to define a model K(Q, Q Ω ) of the λY -calculus with a non-standard interpretation of the fixpoint. Roughly, this model will live inside the product of D and the GFP model S for an Ω-blind automaton. The idea is that every set K α will have a projection on D but not necessarily on S. This allows to observe whether a term converges or not, and at the same time to use this information in computing in the second component.

Definition 9 For a given finite set Q and

Q Ω ⊆ Q we define a family of sets K Q,Q Ω = (K α ) α∈T that is defined by mutual recursion together with a relation L = (L α ) α∈T such that L α ⊆ K α × D α : 1. we let K 0 = {( , P ) | P ⊆ Q} ∪ {(⊥, Q Ω )} with the order: (d 1 , P 1 ) ≤ (d 2 , P 2 ) iff d 1 ≤ d 2 in D 0 and P 1 ⊆ P 2 . (cf. Figure 1) 2. L 0 = {((d, P ), d) | (d, P ) ∈ K 0 }, 3. K α→β = {f ∈ mon[K α → K β ] | ∃d ∈ D α→β .∀(g, e) ∈ L α .(f (g), d(e)) ∈ L β }, 4. L α→β = {(f, d) ∈ K α→β × D α→β | ∀(g, e) ∈ L α .(f (g), d(e)) ∈ L β }. ( , {1; 2}) ( , {1}) ( , {2}) ( , ∅) (⊥, {1}) Figure 1: The order K 0 for Q = {1, 2} and Q Ω = {1}
Note that every K α is finite since it lives inside the standard model constructed from D 0 × P(Q) as the base set. Recall that a TAC automaton is supposed to accept unsolvable terms from states Q Ω . So the unsolvable terms of type 0 should have Q Ω as a part of their meaning. This is why ⊥ of D 0 is associated to (⊥, Q Ω ) in K 0 via the relation L 0 . This also explains why we needed to take the least fixpoint in D. If we had taken the greatest fixpoint then the unsolvable terms would have evaluated to and the solvable ones to ⊥. In consequence we would have needed to relate with ( , Q Ω ), and we would have been forced to relate ⊥ with (⊥, Q). But since ( , Q Ω ) and (⊥, Q) are incomparable in K 0 we would not have obtained an order preserving injection from D 0 to K 0 .

The following lemma shows that for every type α, K α is a join semilattice.

Lemma 10 Given (f 1 , d 1 ) and (f 2 , d 2 ) in L α , then f 1 ∨ f 2 is in K α and (f 1 ∨ f 2 , d 1 ∨ d 2 ) is in L α .

Proof

We proceed by induction on the structure of the type. For the base type the lemma is immediate from the definition. For the induction step consider a type of a form α → β and two functions f 1 and

f 2 in mon[K α → K β ].
Since, by induction, K β is a join semilattice, we have that

f 1 ∨ f 2 is also in mon[K α → K β ].
By assumption of the lemma, for every (p, e) in L α we have that (f 1 (p), d 1 (e)) and (f 2 (p), d 2 (e)) are in L β . The induction hypothesis implies that (f 1 (p)∨f 2 (p), d 1 (e)∨d 2 (e)) is in L β . As by induction hypothesis K β is a join semilattice, we get (

f 1 ∨ f 2 )(p) = f 1 (p) ∨ f 2 (p) is in K β . Thus ((f 1 ∨ f 2 )(p), (d 1 ∨ d 2 )(e)
) is in L β . Since (p, e) ∈ L α was arbitrary this implies that

f 1 ∨ f 2 is in K α→β and (f 1 ∨ f 2 , d 1 ∨ d 2 ) is in L α→β .
A consequence of this lemma and of the finiteness of K α is that K α has a greatest element that we denote α . Observe that ( α , α ) is in L α . The lemma also implies existence of certain meets.

Corollary 11 For every type α and f 1 , f 2 in K α . If there is g ∈ K α such that g ≤ f 1 and g ≤ f 2 then f 1 and f 2 have a greatest lower bound

f 1 ∧ f 2 . Moreover if (f 1 , d 1 ) and (f 2 , d 2 ) are in L α then (f 1 ∧ f 2 , d 1 ∧ d 2 ) is in L α . Proof Just take f = {g ∈ K α | g ≤ f 1 ∧ g ≤ f 2 }.
Element f exists by Lemma 10 and the fact that K α is finite.

We are now going to show that every constant function of mon[K α → K β ] is actually in K α→β .

Lemma 12 For every q in K β , the function c q of mon[K α → K β ] such that for every p in K α , c q (p) = q is in K α→β .

Proof

To show that c q is in K α→β , we need to find h q in D α→β such that for every (p, e), (c q (p), h q (e)) is in L β . Since q is in K β , there is d such that (q, d) is in L β . It suffices to take h q to be the function of D α→β such that for every e in D α , h q (e) = d.

This lemma allows us to define inductively on types the family of constant functions (⊥ ⊥ α ) α∈T as follows:

1. ⊥ ⊥ 0 = (⊥, Q Ω ), 2. ⊥ ⊥ α→β (h) = ⊥ ⊥ β for every h in K α .
Notice that ⊥ ⊥ α is a minimal element of K α , but that K α does not have a least element in general.

For every d in D α , we denote by L d the set of elements of K α that are related to it:

L d = {p ∈ K α | (p, d) ∈ L α }. Definition 13 A type α is D-complete if, for every d in D α : 1. L d is not empty, 2. ⊥ ⊥ α ≤ L d , 3. for every (f, e) in L α : f ≤ L d iff e ≤ d.
Later we will show that every type is D-complete, but for this we will need some preparatory lemmas. We now define an operation (•) ↑ that, as we will show later, is an embedding for D into K. But for this we need the notion of co-step functions: give two partial orders L 1 and L 2 where L 2 has a greatest element , p in L 1 and q in L 2 , we write p q for the function of mon[L 1 → L 2 ] such that for r in L 1 , (p q)(r) is equal to q when r ≤ p and to otherwise.

Lemma 14 If α is a D-complete type and d is in D α then ( L d , d) is in L α . Proof Since α is D-complete, L d is
Definition 16 Let α, β be D-complete types. For every h ∈ D α→β and every d ∈ D α we define two monotone functions and the element h ↑ :

f h,d = L d L h(d) , f h,d = d h(d), h ↑ = d∈D f h,d .
For h in D 0 , we write h ↑ for (⊥, Q Ω ) when h = ⊥ and for ( , Q) when h = .

The next lemma summarizes all essential properties of the model K.

Lemma 17 For all D-complete types α, β, for every h ∈ D α→β and every

d ∈ D α : 1. (f h,d , f h,d ) is in L α→β ; 2. ⊥ ⊥ α→β ≤ f h,d ; 3. h ↑ is an element of K α→β and (h ↑ , h) ∈ L α→β ; 4. if (p, e) ∈ L α then h ↑ (p) = L h(e) ; 5. h ↑ = L h .

Proof

For the first item we take (p, e) ∈ L α , and show that (f h,d (p), f h,d (e)) ∈ L β . This will be sufficient by the definition of L α→β . Lemma 14 gives (

L d , d) ∈ L α and ( L h(d) , h(d)) ∈ L β . By D-completeness of α: p ≤ L d iff e ≤ d. We have two cases. If p ≤ L d then f h,d (p) = L h(d) and f h,d (e) = h(d). Otherwise, p L d that gives f h,d (p) = β and f h,d (e) = β .
With the help of Lemma 14 in both cases we have that the result is in L β , and we are done.

For the second item, by D-completeness of β we have L h(d) ≥ ⊥ ⊥ β . In the proof of the first item we have seen that

f h,d (p) ≥ L h(d) for every p ∈ K α . Since ⊥ ⊥ α→β (p) = ⊥ ⊥ β we get ⊥ ⊥ α→β ≤ f h,d .
In order to show the third item we use the first item telling us that (f h,e , f h,e ) is in L α→β for every e ∈ D α . Since by the second item ⊥ ⊥ α ≤ f h,e , Corollary 11 shows that ( e∈Dα f h,e , e∈Dα f h,e ) is in L α→β . Directly from the definition of co-step functions we have e∈Da e h(e) = h. This gives, as desired, ( e∈Dα f h,e , h) in L α→β .

For the fourth item, take an arbitrary (p, e) ∈ L α . We show that h For the last item we want to show that h ↑ = L h . We know that h ↑ ∈ L h = {g ∈ K α→β : (g, h) ∈ L α } since (h ↑ , h) ∈ L α→β by the third item. We show that for every g ∈ L h , g ≤ h ↑ . Take some (p, e) ∈ L α . We have (g(p), h(e)) ∈ L β , hence g(p) ≤ L h(e) by definition of L h(e) . Since h ↑ (p) = L h(e) by the fourth item, we get g ≤ h ↑ .

Lemma 18 Every type α is D-complete. Let us now suppose that f ≤ L d . The D-completeness of α tells us that for every e in D α there is p in K α so that (p, e ) is in L α . Then Lemma 17 gives that (

L d ) (p) = L d(e ) . We have thus f (p) ≤ ( L d ) (p) = L d(e ) .
Using Lemma 15 and the fact that (f (p), e(e )) ∈ L β we get e(e ) ≤ d(e ). As e was arbitrary we obtain that e ≤ d.

The proposition below sums up the properties of the embedding (•) ↑ from Definition 16.

Proof

We proceed by induction on the structure of the types. The case of the base type follows by a straightforward inspection. For the induction step take f ≤ g in K α→β . For an arbitrary d ∈ D α we have f (d ↑ ) ≤ g(d ↑ ). By induction hypothesis on type β we get f (d ↑ ) ≤ g(d ↑ ). By Lemma 21 we obtain f We are now going to give the definition of the interpretation of the fixpoint combinator in K. This definition is based on that of the fixpoint operator in D. As a shorthand, we write fix α for the operation in D (α→α)→α that maps a function of D α→α to its least fixpoint.

(d ↑ ) = f (d ↑ ) = f (d).
Lemma 23 Given f in K α→α , we have f (fix α (f ) ↑ ) ≤ fix α (f ) ↑ . Proof By Proposition 3, we have that (fix α (f ) ↑ , fix α (f )) is in L α . Moreover, (f, f ) is in L α→α , therefore, we have (f (fix α (f ) ↑ ), f (fix α (f ))) = (f (fix α (f ) ↑ ), fix α (f )) is in L α . Then by Proposition 3 we have f (fix α (f ) ↑ ) ≤ fix α (f ) ↑ .
The above lemma guarantees that the sequence f n (fix α (f ) ↑ ) is decreasing. We can now define an operator that, as we will show, is the fixpoint operator we are looking for.

Definition 24 For every type α and

f ∈ K α define Fix α (f ) = n∈N (f n (fix α (f ) ↑ ))
We show that Fix α is monotone.

Lemma 25 Given f and g in K α→α , if f ≤ g then Fix α (f ) ≤ Fix α (g). Proof By Lemma 22, f ≤ g implies f ≤ g, as fix α is monotone, we have fix α (f ) ≤ fix α (g) and fix α (f ) ↑ ≤ fix α (g) ↑ by Proposition 3. As f ≤ g we have f k (fix α (f ) ↑ ) ≤ g k (fix α (g) ↑ ) for every k in N. Therefore n∈N f n (fix α (f ) ↑ ) ≤ n∈N g n (fix α (g) ↑ ).
The last step is to show that Fix α is actually in K (α→α)→α .

Proof

To prove that (h, g) is in L α→β , we resort to the remark we made in the proof of Lemma 28, so that it suffices to show that for every p 1 , . . . ,

p k respectively in K α 1 , . . . , K α k , (h(p 1 , . . . , p k ), g(p 1 , . . . , p k )) is in L β . We have that h(p 1 , . . . , p k ) = fix α (f (p 1 , . . . , p k ))
↑ that is in K α , and we have that

h(p 1 , . . . , p k ) = fix α (f (p 1 , . . . , p k )) ↑ = fix α (f (p 1 , . . . , p k )) = fix α (f (p 1 , . . . , p k )) by successive use of Lemma 21 = g(p 1 , . . . , p k ) This shows that (h, g) is in L α→β and thus h is in K α→β .
Given r in D γ→δ , from the fourth item of Proposition 3, we have that whenever (q, e) is in L α , then r ↑ (q) = (r(e)) ↑ , so that in particular r ↑ (q) = (r(q)) ↑ . A simple induction shows then that, for r in D γ 1 →•••→γn→δ , r ↑ (q 1 , . . . , q n ) = (r(q 1 , . . . , q n )) ↑ Therefore if δ = 0 and r(q 1 , . . . , q n ) = ⊥, we have (r(q 1 , . . . , q n )) ↑ = (⊥, Q Ω ). Moreover, in case r(q 1 , . . . , q n ) = , we have (r(q 1 , . . . , q n )) ↑ = ( , Q). The lemma follows from choosing r = g(p 1 , . . . , p k ) and remarking that (g(p 1 , . . . , p k )) ↑ = h(p 1 , . . . , p k ).

As in the case of GFP-models the semantics of a Böhm tree is defined in terms of its truncations:

[[BT (M )]] K = {[[BT (M ) ↓ n ]] K : n ∈ N}.
The subtle difference is that now Ω 0 and ω 0 do not have the same meaning. Nevertheless the analog of Proposition 1 still holds in K.

Theorem 33 For very closed term M of type 0:

[[M ]] K = [[BT (M )]] K . Proof First we show that [[M ]] K ≤ [[BT (M )]] K .
For this we define a finite approximation of the Böhm tree. Abstract Böhm tree up to depth l of a term M , denoted ABT l (M ), will be a term obtained by reducing M till it resembles BT (M ) up to depth l as much as possible. We define it by induction:

• ABT 0 (M ) = M ; • ABT l+1 (M ) is M if M does not have head normal form otherwise it
is a term λx.N 0 ABT l (N 1 ) . . . ABT l (N k ), where λx.N 0 N 1 . . . N k is the head normal form of M .

Since ABT l (M ) is obtained from M by a sequence of βδ-reductions,

[[M ]] K = [[ABT l (M )
]] K for every l. We now show that for every term M and every l:

[[ABT l (M )]] K ≤ [[BT (M ) ↓ l ]] K .
Up to depth l, the two terms have the same structure as trees. We will see that the meaning of every leaf in ABT l (M ) is not bigger than the meaning of the corresponding leaf of BT (M ) ↓ l . For leaves of depth l this is trivial since on the one hand we have a term and on the other the constant ω. For other leaves, the terms are either identical or on one side we have a term without head normal form and on the other Ω 0 . By 4 the two have the same meaning in S.

The desired inequality [[M ]]

K ≤ [[BT (M )]] K follows now directly from the definition of the semantics of BT (M ) since [[M ]] K = [[ABT l (M )]] K ≤ [[BT (M ) ↓ l ]] K for every l ∈ N.
For the inequality in the other direction we will also introduce a new notion. Observe that if a term M does not have Y combinators, then it is strongly normalizing and the theorem is trivial. So we need be able to deal with Y combinators in M . For this we introduce new constants c N for every subterm Y N of M . The type of c N is α → β if β is the type of Y N and α = α 1 . . . α k is the sequence of types of the sequence of free variables x = x 1 . . . x k occurring in Y N . We let the semantics of a constant c N be

[[c N ]] K = λ p. fix β ([[N ]] [ p/ x] ) ↑ .
First we need to check that indeed [[c N ]] is in K. For this we have pre-

pared Lemma 32. Indeed [[c N ]] K = λp 1 . . . p k . fix β (f (p 1 , . . . , p k )) ↑ , for f = λ p. [[N ]] [ p/ x] . So [[c N ]] K is h from Lemma 32 and [[c N ]] D = [[c N ]
] K is g from that lemma. The lemma additionally gives us that for every p 1 , . . . , p k ,q 1 , . . . , q l :

[[c N ]] K (p 1 , . . . , p k )(q 1 , . . . , q l ) = (⊥, Q Ω ) if [[c N ]] D (p 1 , . . . , p k )(q 1 , . . . , q l ) = ⊥ ( , Q) if [[c N ]] D (p 1 , . . . , p k )(q 1 , . . . , q l ) = (1) such that q 1 is in the second component of [[M l 1 ]] and q 2 is in the second component of [[M l
2 ]] for infinitely many l. We put r(1) = q 1 and r(2) = q 2 and repeat the argument starting from the nodes 1 and 2 respectively. It is easy to see that this inductive procedure gives a, potentially infinite, run of A. Hence BT (M ) ∈ L(A) as every run of A is accepting.

Reflection

The idea behind the notion of a reflecting term is that at every moment of its evaluation every subterm should know its meaning. Knowing the meaning amounts to extra labelling of constants. Formally, we express this by the notion of a reflective Böhm tree defined below. The definition can be made more general but we will be interested only in the case of terms of type 0. In this section we will show that reflective Böhm trees can be generated by λY -terms.

As usual we suppose that we are working with a tree signature Σ. We will need also a signature where constants are annotated with elements of the model. If S = {S α } α∈T , ρ is a finitary model then the extended signature Σ S contains constants a s where a is a constant in S and s ∈ S 0 ; so superscripts are possible interpretations of terms of type 0 in S.

Definition 35 Let S be a finitary model and M a closed term of type 0. A reflective Böhm tree with respect to S is obtained in the following way:

• If M → *
βδ bN 1 N 2 for some constant b : 0 → 0 → 0 then rBT S (M ) is a tree having the root labelled by b [[bN 1 N 2 ]] S and having rBT S (N 1 ) and rBT S (N 2 ) as subtrees.

• If M → * βδ c for some constant c : 0 then rBT S (M ) = c [[c]] S .
• Otherwise, M is unsolvable and BT (M ) = Ω 0 .

Observe that when S satisfies [[N ]] S = [[BT (N )]]

S for every term N then the superscripts in rBT (M ) are the meanings of respective subtrees in the Böhm tree. When, moreover, S recognizes a given property then these superscripts determine if the tree satisfies the property. These two conditions are fulfilled by the models we have considered in this paper. We will use terms to construct reflective Böhm trees.

Definition 36 Let Σ be a tree signature, and S a finitary model. Let M be a closed term of type 0 over the signature Σ. We say that a term M over the signature Σ S is a reflection of M in S if BT (M ) = rBT (M ).

The objective of this section is to construct reflections of terms. Since λYterms can be translated to schemes and vice versa, the construction would work for schemes too. (Translations between schemes and λY -terms that do not increase the type order are presented in [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF]).

Let us fix a tree signature Σ and a finitary model S. For the construction of reflective terms we enrich λY -calculus with some syntactic sugar. Consider a type α. The set S α is finite for every type α; say S α = {d 1 , . . . , d k }. We will introduce a new atomic type [α] and constants d 1 . . . , d k of this type; there will be no harm in using the same names for constants and elements of the model. We do this for every type α and consider terms over this extended type discipline. Notice that in the result there are no other closed normal terms than d 1 , . . . , d k of type [α].

Given a term M of type [α] and M 1 , . . . M n which are all terms of type β, we introduce the construct case

M {d i → M i } d i ∈Sα
which is a term of type β and which reduces to M i when M = d i . This construct is a simple syntactic sugar since we may represent the term d i of type [α] with the i th projection λx 1 . . . x n .x i by letting [α] = β k → β. When M represents d i , i.e. is equal to λx 1 . . . x n .x i , the term M M 1 . . . M k reduces to M i and thus represents well the semantic of the case construct.

We define a transformation on types α • by induction on their structure as follows:

α • = α when α is atomic (α → β) • = α • → [α] → β •
The translation we are looking for will be an instance of a more general translation [M, υ] of a term M of type α into a term of type α • where υ is a valuation over S.

[λx α .M, υ] =λx α • λy [α] . case y [α] {d → [M, v[d/x α ]]} d∈Sα [M N, υ] = [M, υ] [N, υ] [[N ]] υ [a, υ] =λx 0 1 λy [0] 1 λx 0 2 λy [0] 2 . case y [0] 1 {d 1 → case y [0] 2 {d 2 → a ρ(a)d 1 d 2 x 1 x 2 } d 2 ∈S 0 } d 1 ∈S 0 [x α , υ] =x α • Y (α→α)→α M, υ =Y (α • →α • )→α • (λx α • . [M, υ] x α • [[Y M ]] υ ) Lemma 38 If M → βδh M , then [M, υ] → + βδh [M , υ]. Proof
We proceed by induction on the structure of M . We only treat the cases where M is a redex, the other cases being trivial by induction. We are left with two cases: M = (λx α .P )Q and M = Y (α→α)→α P .

In case M = (λx α .P )Q, we have that M = P [Q/x α ], and using the Lemma 37 we have that

[M , υ] = [P, υ[[[Q]] υ /x α ]] [[Q, υ] /x α ]. But then we have [M, υ] = [λx α .P, υ] [Q, υ] [[Q]] υ = (λx α • y [α] .case y [α] {f → [P, υ[f /x α ]]} f ∈Sα ) [Q, υ] [[Q]] υ → + βδh [P, υ[[[Q]] υ /x α ]] [[Q, υ] /x α ] = M , υ
In case M = Y (α→α)→α P , we have M = P M and:

[M, υ] = Y (α • →α • )→α • (λx α • . [P, υ] x α • [[M ]] υ ) → βδh (λx α • . [P, υ] x α • [[M ]] υ ) [M, υ] → βδh [P, υ] [M, υ] [[M ]] υ = [P M, υ] = M , υ
Corollary 39 Given a term M of type 0 and a valuation υ , M →

* βδh aM 1 M 2 iff [M, υ] → * βδh a [[M ]] υ [M 1 , υ] [M 2 , υ].

Proof

The direction from left to right is a simple consequence of Lemma 38. For the direction from right to left, we use the well-known fact that a λ-term has a head normal form iff it can be head-reduced to a head normal form. Let us suppose that [M, υ] reduces to a [[M ]] υ P 1 P 2 in k steps of head-reduction. In case M has no head normal form, then, for l = k + 1 there is P such that M → l βδh P (where → l βδh denotes the relation of l steps of head reduction), but, then, by an iterative use of Lemma

Proof

This is a simple consequence of Corollary 39

Remark: If in the model S the divergence can be observed (as it is the case for GFP models and for the model K, cf. Proposition 4) then in the translation above we could add the rule [M, υ] = Ω whenever [[M ]] υ denotes a diverging term. We would obtain a term which would always converge. A different construction for achieving the same goal is proposed in [START_REF] Haddad | IO vs OI in higher-order recursion schemes[END_REF].

Remark: Even though the presented translation preserves the structure of a term, it makes the term much bigger due to case construction in the clause for λ-abstraction. The blow-up is unavoidable due to complexity lowerbounds on the model-checking problem. Nevertheless, one can try to limit the use of case construct. We present a slightly more efficient translation that takes the value of the known arguments into account and thus avoids the unnecessary use of case construction. For this, the translation is now parametrized also with a stack of values from S so as to recall the values taken by the arguments. For the sake of simplicity, we also assume that the constants always have all their arguments (this can be achieved by putting the λ-term in η-long form).

[λx α .M, υ, d :: S] = λx α • y [α] . [M, υ[d/x α ], S] [λx α .M, υ, ε] = λx α • y [α] .case y [α]

Conclusions

We have shown that a model-based approach to model-checking works for quite a big class of properties. While a priori it is more difficult to construct a finitary model than to come up with a decision procedure, in our opinion this additional effort is justified. It allows, as we show here, to use the techniques of the theory of the λ-calculus. It opens new ways of looking at the algorithmics of the model-checking problem. Since typing in intersection type systems [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF] and step functions in models are in direct correspondence [START_REF] Salvati | Loader and Urzyczyn are logically related[END_REF], model-based approach can also benefit from all the developments in algorithms based on typing. Finally, this approach allows to get new constructions as demonstrated by our transformation of a scheme to a scheme reflecting a given property. Observe that this transformation is general and does not depend on our particular model.

Let us note that the model-based approach is particularly straightforward for Ω-blind TAC automata. It uses standard observations on models of the λY -calculus and Proposition 2 with a simple inductive proof. The model we propose for insightful automata may seem involved; nevertheless, the construction is based on simple and standard techniques. Moreover, this model implements an interesting interaction between components. It succeeds to mix a GFP model for Ω-blind automaton with the model D for detecting solvability.

The approach through models opens several new perspectives. One can try to characterize what kinds of fixpoints correspond to what class of automata conditions. More generally, models hint a possibility to have a Eilenberg like variety theory for lambda-terms [START_REF] Eilenberg | Automata, Languages and Machines[END_REF]. This theory would cover infinite regular words and trees too as they can be represented by λY -terms. Finally, considering model-checking algorithms, the model-based approach puts a focus on computing fixpoints in finite partial orders. This means that a number of techniques, ranging from under/over-approximations, to program optimization can be applied.

Definition 5

 5 For a GFP model S over the base set S 0 . The language recognized by a subset F ⊆ S 0 is the set of closed λY -terms {M | [[M ]] S ∈ F }.

  not empty, and the conclusion follows directly from Lemma 10. Lemma 15 If α is a D-complete type, and d, e ∈ D α then: e ≤ d iff L e ≤ L d . Proof As α is D-complete both L e and L d are not empty and therefore, L e and L d are well-defined. Lemma 14 also gives that ( L e , e) is in L α . Now from D-completeness of α, we have that L e ≤ L d iff e ≤ d.

  ↑ (p) = L d(e) . By definition h ↑ (p) = e ∈Dα f h,e (p). Moreover f h,e (p) = L h(e ) if p ≤ L e , and f h,e (p) = β otherwise. By D-completeness of α: p ≤ L e iff e ≤ e . So h ↑ (p) = e ∈Dα f h,e (p) = { L h(e ) : e ≤ e }. By Lemma 15, if e ≤ e then L h(e) ≤ L h(e ) . Hence h ↑ (p) = L h(e) .

Proof

  This is proved by induction on the structure of the type. The case of the base type follows by direct examination. For the induction step consider a type α → β and suppose that α and β are D-complete. Given d in D α→β , Lemma 17 gives that (d ↑ , d) is in L α→β proving that L d = ∅, it also gives that ⊥ ⊥ α→β ≤ d ↑ and d ↑ = L d so that we obtain ⊥ ⊥ α→β ≤ L d . It just remains to prove that given (f, e) in L α→β , f ≤ L d iff e ≤ d. Let's first suppose that e ≤ d. Take a p ∈ K α . By definition of the model there is e , such that (p, e ) ∈ L α . Lemma 15 gives us L e(e ) ≤ L d(e ) . By definition of L α→β we have that (f (p), e(e )) ∈ L β , so f (p) ≤ L e(e ) by definition of L e(e ) . This gives f (p) ≤ L e(e ) ≤ L d(e ) . On the other hand Lemma 17 gives that L d(e ) = d ↑ (p) = ( L d ) (p). This shows the desired f (p) ≤ ( L d ) (p) for every p ∈ K α .

  The last equality follows from the fact that d ↑ = d since (d ↑ , d) is in L α by Proposition 3. Of course the same equalities hold for g too. So f (d) ≤ g(d) for arbitrary d, and we are done.

  38, we must have [M, υ] → m βδh [P, υ] with k < l ≤ m and we obtain a contradiction. In case M can be reduced in l reduction steps to bN 1 N 2 , then a simple use of Lemma 38 gives that b = a, P 1 = [N 1 , υ] and P 2 = [N 2 , υ]. Theorem 40 For every finitary model S and a closed term M of type 0: BT ([M, ∅]) = rBT S (M ).

  {d → [M, υ[d/x α ], ε]} d∈Sα [M N, υ, S] = [M, υ, [[N ]] υ :: S] [N, υ, ε] [[N ]] υ [a, υ, d 1 :: d 2 :: ε] = λx 0 1 λy [[a]]d 1 d 2 x 1 x 2 [x α , υ, S] = x α • [Y M, υ, S] = Y [M, υ, [[Y M ]] χ :: S]

This work has been supported by ANR 2010 BLAN 0202 01 FREC

Proposition 3 Given a type α, and d in D α , there is d ↑ in K α such that:

Proof

These properties follow directly from Lemma 17, except for the second property for which a small calculation is needed. Since (d ↑ , d) is in L α and d ≤ e then by Lemma 17: d ↑ ≤ L e . The later is precisely e ↑ by Lemma 17.

The next lemma shows that the relation L α is functional.

Lemma 19 For every type α and f in K α : if (f, d 1 ) and (f, d 2 ) are in L α , then d 1 = d 2 .

Proof

We proceed by induction on the structure of the type. The case of the base type follows from a direct inspection. For the induction step suppose that both (f, d 1 ) and (f, d 2 ) are in L α→β . Take arbitrary e ∈ D α . By Lemma 17 we have (e ↑ , e) ∈ L α . Therefore (f (e ↑ ), d 1 (e)) and (f (e ↑ ), d 2 (e)) in L β . The induction hypothesis implies that d 1 (e) = d 2 (e). Since e was arbitrary we get d 1 = d 2 .

Since, by definition, for every f ∈ K α we have (f, d) ∈ L α for some d ∈ D α , the above lemma gives us a projection of K α to D α .

Definition 20 For every type α and f ∈ K α we let f to be the unique element of D α such that (f, f ) ∈ L α .

We immediately state some properties of the projection.

We are ready to define the model we were looking for.

Definition 27 For a finite set Q and

where {K α } α∈T is as in Definition 9 and ρ is a valuation such that for every type α: ω α is interpreted as the greatest element of K α , Y (α→α)→α is interpreted as Fix α , and Ω 0 is interpreted as (⊥, Q Ω ).

We will show K(Q, Q Ω , ρ) is indeed a model of λY -calculus. Since K α→β does not contain all the functions from K α to K β we must show that there are enough of them to form a model of λY , the main problem being to show that [[λx.M ]] υ K defines an element of K. For this it will be more appropriate to consider the semantics of a term as a function of values of its free variables. Given a finite sequence of variables x = x 1 , . . . , x n of types α 1 , . . . , α n respectively and a term M of type β with free variables in x, the meaning of M in the model K with respect to x will be a function

represents the function λ p.[[M ]]

[p 1 /x 1 ,...,pn/xn] K . Formally it is defined as follows:

Note that λ symbol on the right hand side of the equality is the semantic symbol used to denote a relevant function, and not a part of the syntax while the sequence p denote a sequence of elements p 1 , . . . , p n respectively in K α 1 , . . . , K αn .

20

Lemma 26 ensures the existence of the meaning of Y in K. With this at hand, the next lemma provides all the other facts necessary to show that the meaning of a term with respect to x is always an element of the model.

Lemma 28 For every sequence of types α = α 1 . . . α n and every types β, γ we have the following:

Proof

The first item of the Lemma is given by Lemma 12, the second does not present more difficulty. Finally the third proceeds by a direct examination once we observe the following property of

This observation follows directly from Proposition 3 and the definition of the model.

Theorem 29 For every finite set Q and every set

Let us mention the following useful fact that showing a correspondence between the meanings of a term in K and in D. The proof is immediate since {L α } α∈T is a logical relation (cf [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]).

Lemma 30 For every type α and closed term M of type α:

Correctness and completeness of the model

It remains to show that the model we have constructed is indeed sufficient to recognize languages of TAC automata. For the rest of the section fix a tree signature Σ and a TAC automaton

Consider a model K based on K(Q, Q Ω , ρ) as in Definition 27, where Q Ω is the set of states q such that δ(q, Ω) = tt. It remains to specify the meaning of constants like c : 0 or a : 0 2 → 0 in Σ:

where

Proof

It is easy to see that ρ(a) is monotone. For the membership in K the witnessing function from D o 2 →o is 0 2 →0 .

Once we know that K is a model we can state some of its useful properties. The first one tells what the meaning of unsolvable terms is. The second indicates how unsolvability is taken into account in the computation of a fixpoint.

Proposition 4 Given a closed term M of type 0:

Lemma 32 Given a type β = β 1 → • • • → β l → 0, a sequence of types α = α 1 , . . . , α k , and a function f ∈ K α→β→β , consider functions:

We now define term iterate n (N ) for very n ∈ N.

From the definition of the fixpoint operator in K and the fact that

] for some n. Now we can apply this identity to all fixpoint subterms in M starting from the innermost subterms. So the term expand i (M ) is obtained by repeatedly replacing occurrences of subterms of the form Y N in M by iterate i (N ) x starting from the innermost occurrences. We get that for n chosen as above

We come back to the proof. The missing inequality will be obtained from

The first equality we have discussed above. The second is trivial since expand n (M ) does not have fixpoints. To finish the proof it remains to show

Let us denote BT (expand n (M )) by P . So P is a term of type 0 in a normal form without occurences of Y . For a term K let K stand for a term obtained from K by simultaneously replacing c N by λ x.Y N . Because of Lemma 23, we have

Moreover, as P = βδ M , we have that BT ( P ) = BT (M ). We need to show that [

Let us compare the trees BT (P ) and BT ( P ) by looking on every path starting from the root. The first difference appears when a node v of BT (P ) is labelled with c N for some N . Say that the subterm of P rooted in v is c N K 1 . . . K i . Then at the same position in BT (P ) we have the Böhm tree of the term (λ x.Y N ) K1 . . . Ki . Observe that both terms are closed and of type 0. We will be done if we show that [

Theorem 34 Let A be an insightful TAC automaton and K a model as constructed at the beginning of the subsection. For every closed term M of type 0:

Proof

Recall that K is constructed over the sets Q and Q Ω where Q is the set of states of A and Q Ω is the set of states that from which A accepts Ω:

For the left to right implication suppose that A accepts BT (M ). Since, by Theorem 33,

The tree BT (M ) is a ranked tree labeled with constants form the signature. The run of A is function r assigning to every node a state of A. The tree BT (M ) ↓ l is a prefix of this tree containing nodes up to depth l. Let us call it t l . Every node v in the domain of t l corresponds to a subterm of BT (M ) ↓ l that we denote M l v . By induction on the height of v we show that r(v) appears in the second component of [[M l v ]]. If v is a leaf at depth l then M v is ω 0 . We are done since [[ω 0 ]] = ( , Q). If v is a leaf of depth smaller than l then M l v is Ω 0 or a constant c of type 0. In the later case by definition of a run, we have r(v) ∈ {q | δ(q, c) = tt}. We are done by the semantics of c in the model.

and r(v) belongs to Q Ω by definition of the run. The last case is when v is an internal node of the tree t l . In this case M l w = aM l v1 M l v2 where a is the constant labeling v in t l . By induction assumption we have that r(vi) appears in the second component of [[M l vi ]], and we are done by using the semantics of a.

For the direction from right to left we suppose that q 0 in the second component of

[[M ]]. By Theorem 33, [[M ]] = [[BT (M )]

]. We will construct a run of A on BT (M ).

If M does not have head normal form then [[M ]] = (⊥, Q Ω ) by Proposition 4. In this case BT (M ) is the tree consisting only of the root labeled Ω 0 . Hence q 0 ∈ Q Ω and we are done.

Otherwise BT (M ) has some letter a in the root. In case it is a leaf, the conclusion is immediate. In case it is a binary symbol, since q 0 is in the second component of [[BT (M )]], it is also in the second component of [[BT (M ) ↓ l ]] for all l. We know that BT (M ) ↓ l is of the form aN l 1 N l 2 for some N l 1 , N l 2 . As δ A (q 0 , a) is a finite set of pairs, there is a pair (q 1 , q 2 ) ∈ δ A (q 0 , a)

To prove correctness of this translation, we need two lemmas.

Lemma 37 Given a term M and a valuation υ, and the terms N 1 , . . . , N n we have the following identity:

We proceed by induction on the structure of M .

In case M is a variable different from the variables x α 1 1 , . . . , x αn n or is a constant, then the result is obvious. In case M = x α i i , the conclusion also follows with no difficulty.

In case

In case M = λx α .N (we assume that x α is different from the x α i i ), then [λx α .M.σ, υ] = λx α • y [α] .case y [α] {f → M.σ, υ[f /x α ]} f ∈Sα . By induction we have that, for every f in M α [M.σ, υ[f /x α ]] = [M, υ [f /x α ]] .σ . But, λx α .M, υ .σ = (λx α • y [α] .case y [α] {f → M, υ [f /x α ] } f ∈Sα ).σ = λx α • y [α] .case y [α] {f → M, υ [f /x α ] .σ } f ∈Sα = λx α • y [α] .case y [α]


Jean-Antoine Désidéri

Multiple-Gradient Descent Algorithm (MGDA)

Keywords: Optimum-shape design, concurrent engineering, multi-criterion optimization, split of territory, Nash and Stackelberg game strategies, Pareto optimality, descent direction, steepestdescent direction

, a methodology for the numerical treatment of a two-objective optimization problem, possibly subject to equality constraints, was proposed. The method was devised to be adapted to cases where an initial design-point is known and such that one of the two disciplines, considered to be preponderant, or fragile, and said to be the primary discipline, achieves a local or global optimum at this point. Then, a particular split of the design variables was proposed to accomplish a competitive-optimization phase by a Nash game, whose equilibrium point realizes an improvement of a secondary discipline, while causing the least possible degradation of the primary discipline from the initial optimum. In this new report, the initial design point and the number of disciplines are arbitrary. Certain theoretical results are established and they lead us to define a preliminary cooperative-optimization phase throughout which all the criteria improve, by a so-called Multiple-Gradient Descent Algorithm (MGDA), which generalizes to n disciplines (n ≥ 2) the classical steepest-descent method. This phase is conducted until a design-point on the Pareto set is reached; then, the optimization is interrupted or continued in a subsequent competitive phase by a generalization of the former approach by territory splitting and Nash game.

Algorithme de descente à gradients multiples (MGDA)

Résumé :

Dans un précédent rapport [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF], on a proposé une méthodologie pour le traitement numérique d'un problème d'optimisation bicritère, éventuellement soumis à des contraintes d'égalité. La méthode a été conçue pour s'adapter aux cas où l'on connait un point de conception initial où l'une des disciplines, dite discipline principale car prépondérante, ou fragile, atteint un optimum local ou global. Alors, on a proposé une méthode de partage des variables afin de réaliser une phase d'optimisation compétitive par un jeu de Nash, dont le point d'équilibre produit une amélioration de la discipline secondaire, tout en causant la moindre dégradation possible de la discipline principale par rapport à l'optimum initial. Dans ce nouveau rapport, le point de conception initial et le nombre de disciplines sont arbitraires. On établit certains résultats théoriques qui nous conduisent à définir une phase préliminaire d'optimisation coopérative au cours de laquelle tous les critères s'améliorent, par un Algorithme de Descente à Gradients Multiples (MGDA) qui généralise à n disciplines l'algorithme classique du gradient. Cette phase est prolongée jusqu'à atteindre un point de conception du front de Pareto; alors, on peut éventuellement continuer l'optimisation par une phase suivante, compétitive, en généralisant l'approche précédente par partage de territoire et jeu de Nash.

Mots-clés : Conception optimale de forme, ingénierie concourante, optimisation multi-critère, partage de territoire, stratégies de jeux de Nash ou de Stackelberg, Pareto-optimalité, direction de descente, direction de plus grande pente

Introduction, problem setting and notations

In a previous report [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF], a methodology for the numerical treatment of a two-objective minimization problem, possibly subject to equality constraints was proposed. Such a problem is a basic step in multidisciplinary optimization, sometimes referred to as concurrent engineering. There, we considered the case where one criterion to be minimized, J A , is preponderant over the second, J B , that is, either more critical or more fragile. The problem was formulated as a parametric optimization in which the two criteria are smooth functions of a common design vector Y ∈ R N . The numerical procedure was defined in two steps.

In the first step, the criterion associated with the preponderant criterion J A (Y ), or primary discipline, is minimized first, alone, to full convergence by hypothesis, yielding the design vector Y A . As a result, the gradient vector, ∇J A , the Hessian matrix, H A , and the K constraint gradients, ∇g k are assumed to be known at Y = Y A . In practice, such information may be difficult to calculate exactly when the finite-dimensional parametric formulation is the result of discretizing functionals of the distributed solution of a complex set of partial differential equations, as it is the case in the prototype example of aerodynamic optimum-shape design; then, possibly, but not necessarily, the exact derivatives can be replaced by approximations through meta-modeling of the functionals.

In preparation of the second step, the entire parametric space is then split into two supplementary subspaces on the basis of the analysis of the second variation of the primary functional, subject to the K active constraints. The construction is such that infinitesimal perturbations in the design vector Y about Y A lying in the second subspace, whose dimension p is adjustable (p ≤ N -K), cause potentially the least degradation to the primary functional value. In other words, the second subspace is the subspace of dimension p of least sensitivity of the preponderant criterion J A .

In the second step of the optimization, a Nash equilibrium [START_REF] Nash | Non-Cooperative Games[END_REF] is sought between the two disciplines by introducing two virtual players, each one in charge of minimizing its own criterion, J A or J AB (a convex combination of J A /J A and θJ B /J B ), w.r.t. either subset of parameters that generates one of the two supplementary subspaces. In this way, the secondary criterion is potentially reduced, while not increasing unduly the primary criterion from its initial minimum. The Nash game is given a particular form in which a continuation parameter ε (0 ≤ ε ≤ 1) is introduced. The optimum solution Y A achieved at completion of the first step of the optimization is proved to be a Nash equilibrium solution of our formulation for ε = 0. Thus, as ε increases from 0 to 1, the formulation provides a continuum of Nash equilibrium solutions, corresponding to a smooth introduction of the trade-off between the two disciplines. Along the continuum, the initial derivative of the primary functional w.r.t. ε is also proved to be equal to zero, which can be viewed as a type of robust-design result. In practice this offers the designer the possibility to elect a design point along the continuum, not necessarily at the endpoint ε = 1.

Lastly we observed that the hierarchy introduced above between the criteria was applied to the split of territory in preparation of a Nash game, which is by essence symmetrical. The bias is therefore different in nature from the unsymmetrical treatment of the variables introduced in a Stackelberg-type game [START_REF] Basar | Dynamic noncooperative game theory[END_REF].

In [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF], our formulation was first demonstrated in the simple case of the minimization of two quadratic forms in R 4 subject to a linear, or a nonlinear equality constraint. The methodology was further illustrated by the treatment a difficult exercise of a generic aircraft wing shape optimization w.r.t. two criteria, one representative of the aerodynamic performance (drag subject to a lift constraint) and the other of the structural design (average stress subject to geometrical constraints) taken from B. Abou El Majd's doctoral thesis [START_REF] Désidéri | Algorithmes hiérarchiques et stratégies de jeux pour l'optimisation multidisciplinaire -Application à l'optimisation de la voilure d'un avion d'affaires[END_REF].

In this new report, we demonstrate how the general problem of the unconstrained simultaneous minimization of n smooth criteria (or disciplines) J i (Y ) (Y : design vector; Y ∈ H; H : working space, a Hilbert space usually equal to R N , but possibly a subspace of L 2 also) can formally be accomplished in two phases :

1. A cooperative phase, beneficial to all criteria, in the sense that all criteria are reduced at each step of this phase.

2. A competitive phase realized through a Nash game with an appropriate definition of the split of territory.

In the usual case of a finite-dimensional working space H = R N , no assumption is made on how the integers n and N compare.

The cooperative phase is conducted by an algorithm that generalizes the classical steepestdescent method to n concurrent disciplines. At completion of this phase, the design vector provides a point on the Pareto set that is not necessarily Pareto-optimal [START_REF] Miettinen | Nonlinear multiobjective optimization[END_REF], if not all the criteria are locally convex. In that case only, it makes sense to define a subsequent minimization phase, competitive in nature. For this, we propose to generalize the split of territory defined in the former report [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF] in preparation of a dynamic Nash game, implemented numerically, preferably on a parallel architecture.

Pareto concepts

We refer to the excellent textbook by K. Miettinen [START_REF] Miettinen | Nonlinear multiobjective optimization[END_REF] for a detailed review of fundamentals in nonlinear multiobjective optimization. and much more. Here, we simply formulate a number of theoretical results that are essential to our subsequent algorithmic construction.

Thus consider n smooth criteria J i (Y ) (Y : design vector; Y ∈ H; H : working space, a Hilbert space usually equal to R N , but possibly a subspace of L 2 also). In practice, these functions or functionals are assumed to be of class C 1 and convex in some working open ball B of the design space H. Throughout this report, unless specified otherwise, the symbol N denotes the dimension of the design-space H when it is finite and the symbol ∞ otherwise.

In this revised version of the report, the following two lemmas are introduced in the alternate order (and renumbered). Lemma 2 (formerly Lemma 1) is now given a more rigorous and general proof based on Lemma 1. In particular, the case n > N is now encompassed.

Lemma 1

Let H be a Hilbert space of finite or infinite dimension N , and {u i } (1 ≤ i ≤ n) a family of n vectors in H. Let U be the set of strict convex combinations of these vectors :

U = w ∈ H / w = n i=1 α i u i ; α i > 0 (∀i) ; n i=1 α i = 1 (1)
and U its closure (the convex hull of the family). Then, there exists a unique element ω ∈ U of minimum norm, and :

∀ū ∈ U : (ū, ω) ≥ (ω, ω) = ω 2 := C ω (2)
Proof : the convex hull U is a closed and convex set, and this implies existence and uniqueness of the element ω of minimum norm in U.

Let ū be an arbitrary element of U; set r = ū -ω so that ū = ω + r. Since the convex hull

U is convex, ∀ε ∈ [0, 1] , ω + εr ∈ U (3)
Since ω is the element of U of minimum norm, ω + εr ≥ ω , which writes :

ω + εr 2 -ω 2 = (ω + εr, ω + εr) -(ω, ω) = 2ε (r, ω) + ε 2 (r, r) ≥ 0 (4)
and since ε can be arbitrarily small, this requires that :

(r, ω) = (ū -ω, ω) ≥ 0 (5)
from which the result follows directly.

Let us introduce and use throughout the following very natural definition, although the terminology does not seem to be standard :

Definition 1 (Pareto-stationarity) Let J i (Y ) (1 ≤ i ≤ n, Y ∈ B ⊆ R N
) be smooth and convex objective-functions over the open ball B centered at the design-point Y 0 . These objective-functions are said to be Pareto-stationary at Y 0 iff there exists a convex combination of the gradient-vectors, u 0 i = ∇J i (Y 0 ), that is equal to zero:

∃α = {α i } such that α i ≥ 0 (∀i) , n i=1 α i = 1 , and n i=1 α i u 0 i = 0 . (6)
Lemma 2 Let Y 0 be a Pareto-optimal point, center of an open ball B in which the objective-functions J i (Y ) (1 ≤ i ≤ n) are smooth and convex, and define the gradient-vectors u 0 i = ∇J i Y 0 in which ∇ is the symbol for the gradient; then, the objective-functions are Pareto-stationary at Y 0 .

Proof : Without loss of generality, assume J i (Y 0 ) = 0 (∀i). Then:

Y 0 = Arg min Y J n (Y ) subject to: J i (Y ) ≤ 0 (∀i ≤ n -1) . (7)
Let U n-1 be the convex hull of the gradients {u 0 1 , u 0 2 , . . . , u 0 n-1 } and ω n-1 = Arg min u∈U n-1 u . By virtue of Lemma 1, the vector ω n-1 exists, is unique, and such that:

u 0 i , ω n-1 ≥ ω n-1 2 (∀i ≤ n -1) . (8)
Two situations are then possible:

1. ω n-1 = 0, and the objective-functions {J 1 , J 2 , . . . , J n-1 } satisfy the Pareto stationarity condition at Y = Y 0 . A fortiori, the condition is also satisfied by the whole set of objectivefunctions.

2. Otherwise ω n-1 = 0. Then let

j i ( ) = J i (Y 0 -ω n-1 ) (i = 1, . . . , n -1) (9)
so that j i (0) = 0 and

j i (0) = -u i , ω n-1 ≤ -ω n-1 2 < 0 , (10)
and for sufficiently small strictly-positive :

j i ( ) = J i (Y 0 -ω n-1 ) < 0 (∀i ≤ n -1) (11)
which establishes that Slater's qualification condition [START_REF] Boyd | Convex optimization[END_REF] is satisfied for the optimization problem (7) subject to inequality constraints. Thus, the Lagrangian

L = J n (Y ) + n-1 i=1 λ i J i (Y ) (12)
is stationary w.r.t. Y at Y = Y 0 , and this gives:

u 0 n + n-1 i=1 λ i u 0 i = 0 (13)
in which λ i > 0 (∀i ≤ n -1) since equality constraints hold J i (Y 0 ) = 0 (KKT condition). Normalizing this equation by dividing by the number 1 + n-1 i=1 λ i which is greater then 1 (thus, strictly-positive), results in the Pareto-stationarity condition. Thus, in general, for smooth and convex unconstrained criteria, Pareto-stationarity is a necessary condition for Pareto-optimality. Inversely, if the smooth criteria J i (Y ) (1 ≤ i ≤ n) are not Pareto-stationary at a given design-point Y 0 , descent directions common to all criteria exist. We now examine how such a direction can be identified. We have the following :

Combining Lemma 1 and Lemma 2 with Definition 1 yields the following :

Theorem 1 Let H be a Hilbert space of finite or infinite dimension N . Let J i (Y ) (1 ≤ i ≤ n) be n smooth and convex objective-functions of the vector Y ∈ B ⊆ H, and Y 0 a particular admissible design-point, at which the gradient-vectors are denoted u 0 i = ∇J i (Y 0 ), and

U = w ∈ H / w = n i=1 α i u 0 i ; α i > 0 (∀i) ; n i=1 α i = 1 (14)
Let ω be the minimal-norm element of the convex hull U, closure of U. Then :

1. either ω = 0, and the criteria

J i (Y ) (1 ≤ i ≤ n) are Pareto-stationary at Y = Y 0 ;
2. or ω = 0 and -ω is a descent direction common to all the criteria; additionally, if ω ∈ U, the scalar product (ū, ω) is equal to ω 2 for all ū ∈ U.

Proof : all the elements of this theorem are reformulations of previous results, except for the statement concerning the scalar product (ū, ω) in the second case when additionally ω ∈ U (and not simply U). To establish this last point, observe that under these assumptions, the element ω is the solution to the following minimization problem :

ω = u = n i=1 α i u 0 i , α = Argmin j(u) , j(u) = (u, u) , n i=1 α i = 1 (15)
since by hypothesis, none of the inequality constraints, α i > 0, is saturated. Consequently, using the vector α ∈ R n as the finite-dimensional variable, the Lagrangian writes :

L(α, λ) = j + λ n i=1 α i -1 (16)
and the optimality conditions satisfied by the vector α are the following :

∂L ∂α i = 0 (∀i) , ∂L ∂λ = 0 (17)
These equations imply that for all indices i :

∂j ∂α i + λ = 0 (18)
But, j(u) = (u, u) and for u = ω = n i=1 α i u i , one has :

∂j ∂α i = 2( ∂u ∂α i , u) = 2(u 0 i , ω) = -λ =⇒ (u 0 i , ω) = -λ/2 (19)
independently of i. Now consider an arbitrary element ū ∈ U :

ū = n i=1 µ i u 0 i (20)
Inria where µ i ≥ 0 (∀i) and n i=1 µ i = 1. Then :

(ū, ω) = n i=1 µ i (u 0 i , ω) = -λ/2 (a constant) = ω 2 (21)
where the constant has been evaluated by letting ū = ω.

In summary, one is led to identify the vector

ω = n i=1 α i u 0 i (22)
by solving the following quadratic-form constrained minimization problem in R n :

min α∈R n n i=1 α i u 0 i 2 (23)
subject to :

α i ≥ 0 (∀i) , n i=1 α i = 1 (24)
Note that in a finite-dimensional setting, and in a functional-space setting as well, the above problem can be solved in R n , so long as the gradients {u 0 i } (1 ≤ i ≤ n) and their scalar products {u 0 ij := (u 0 i , u 0 j )} are known. Then, a call to a library procedure should be sufficient. Let us now examine the instructive particular case of two criteria (n = 2). Let u = u 0 1 , v = u 0 2 , α = α 1 and α 2 = 1 -α, to simplify the notation, and consider the following quadratic form :

j(α) = αu + (1 -α)v 2 = αu + (1 -α)v, αu + (1 -α)v (25)
so that :

j (α) = 2 u -v, α(u -v) + v (26)
Hence, putting aside the trivial case where u = v, the minimum is achieved for

α = v.(v -u) u -v 2 = v 2 -v.u u 2 + v 2 -2u.v (27)
In fact, the orthogonal projection of the null vector 0 onto the the convex hull given by αu+(1-α)v (without limitation on α), is given by the condition :

αu + (1 -α)v .(u -v) = 0 (28)
which gives the same expression for α.

This expression shows that if the vectors u and v are first normalized so that u = v = 1, one gets α = 1 2 . Inversely, if the vectors u and v are not normalized first, it is not certain that the above α be in [0,1]; indeed, utilizing here the usual dot-product notation for the scalar product, one has :

0 < α < 1 ⇐⇒ 0 < v 2 -v.u < u 2 + v 2 -2u.v ⇐⇒ u.v < min u 2 , v 2 = min u , v 2 ⇐⇒ cos (u, v) < min u , v max u , v ⇐⇒ (u, v) > cos -1 min u , v max u , v (29)

Optional preliminary reformulation of criteria

In numerical experiments, it is preferable that the various criteria all be positive, and scaled in a somewhat unified way. To achieve this, we propose to modify the definitions of the criteria without altering the sense of the associated minimization problems.

For this purpose, let :

B R = B Y 0 , R (35)
be a working ball in the design space about the initial design-point Y 0 .

In a first step, we propose to replace each criterion J i (Y ) by the following :

Ji (Y ) = exp α i H 0 i ∇J 0 i 2 J i (Y ) -J 0 i ( 36
)
where :

-the superscript 0 indicates an evaluation at Y = Y 0 ; -∇J 0 i and H 0 i denote the gradient-vector and the Hessian matrix, and H 0 i can be computed economically as : trace (H 0 i ) 2 ;

α i is a dimensionless constant.

In this way, the new criteria are dimensionless, they vary in the same sense as the original ones, and :

∀i , Ji (Y 0 ) = 1 , ∇J i (Y 0 ) = γ R (37)
provided the constants α i 's are chosen to satisfy :

α i H 0 i ∇J 0 i = γ R ∼ 1 (38)
In the above, the dimensionless constant γ is given a value equal or close to the possiblydimensional measure of R in the utilized system of units.

For a reason that will appear later, without altering the regularity of the criteria, we would like them to be infinite when Y is infinite. For this, define the following function :

φ(x) =      0 if x ≤ 0 x exp - 1 x 2 if x > 0 ( 39
)
This function is C ∞ including at 0, and φ(x) ∼ x as x → +∞. The new criterion

Ji (Y ) = Ji (Y ) + ε 0 φ Y -Y 0 2 R 2 -1 (40)
in which ε 0 is some strictly-positive constant, is identical to the former one, J, inside the working ball B R , and grows at least like Y 2 outside. The match of Ji (Y ) with Ji (Y ) and J i (Y ) at the boundary of the working ball is infinitely smooth. Additionally :

lim Y →∞ Ji (Y ) = ∞ (41)
In what follows, it is implicit that the original criteria have been replaced by { Ji (Y )} (1 ≤ i ≤ n) and the double superscript ˜is omitted.

Conclusion

In this report, we have considered the problem of simultaneous unconstrained minimization of n smooth criteria. We have defined the notion of Pareto-stationarity, a weak form of the classical Pareto optimality. We have shown that when the current design point is not one of Pareto stationarity, the unique element ω of minimum norm in the convex hull of the gradient-vectors is nonzero, and -ω is a descent direction for all criteria simultaneously. This has led us to define the Multiple-Gradient Descent Algorithm (MGDA) which generalizes the classical steepest-descent algorithm to n disciplines, permitting to carry out a cooperative-optimization phase throughout which all criteria diminish at each iteration. This phase is possible until a Pareto-stationary designpoint is reached associated with a representation point on the Pareto set. Then a competitiveoptimization phase can be defined if the process of optimization should be continued. This new phase can be realized by a Nash game based on a split of variables guided by the analysis of the eigensystems of the Hessian matrices, in a way that generalizes the results of [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF].

RR n°6953

Inria

Acknowledgement

The author wishes to express his appreciation to his colleague Abderrahmane Habbal for extremely fruitful scientific discussions with him.

Thus the condition is that the angle (u, v) between the two gradient-vectors u and v be at least equal to a certain limit-angle which is a function of their norms whose values are in [0, π/2]. A sufficient condition is therefore that this angle be obtuse (u.v < 0). Whenever the norms of the gradient-vectors u and v are very different, the limit-angle is close to π/2. Inversely, if the norms are close to one another, the limit-angle is small, and the condition is satisfied except if the directions of the two gradient-vectors are too close (see Figure 1).

Figure 1: Various possible configurations of the two gradient-vectors u and v and the minimalnorm element ω depending on whether the angle (u, v) is obtuse (left), acute but superior to the limit-angle (center), or acute and inferior to the limit-angle (right). Also note that in the first two cases on the left of Figure 1, the vector ω points strictly in between the vectors representing u and v, and this corresponds to situations in which ω ∈ U, and not simply U. Then, ω is orthogonal to the dashed line that connects the extremities of these representatives, and evidently, as a result, the scalar product (ū, ω) is constant and equal to ω 2 for all ū ∈ U, as stated in the theorem.

Thus, the solution is the following :

otherwise, depending on whether min u , v = v or u .

(30)

Lastly, when α ∈ [0, 1], let :

One has :

Then :

which is symmetric w.r.t. u and v; hence :

which, in part, constitutes a direct verification of Theorem 1.

Numerical strategy for multiobjective optimization

Given an initial admissible design-point Y 0 at which the smooth criteria J i (Y ) (1 ≤ i ≤ n) are not Pareto-stationary, we propose to develop the optimization process in several stages described in the following subsections.

Cooperative-optimization phase : the Multiple-Gradient Descent Algorithm (MGDA)

The MGDA relies on the results of Theorem 1. The MGDA consists in iterating the following sequence :

1. Compute the gradient-vectors u 0 i = ∇J i (Y 0 ), and determine the minimum-norm element ω in the convex hull U. If ω = 0, stop.

2. Otherwise, determine the step-size h which is, presumably optimally, the largest strictlypositive real number for which all the functions j i (t

In practice, the test ω = 0 will be made with a tolerance ( ω < tol). In addition, note that the determination of the step-size h can be realized by the adaptation of nearly all standard one-dimensional search methods. This algorithm can be repeated a finite number of iterations if these iterations yield a design-point at which the Pareto-stationarity condition is satisfied, or indefinitely, if this never occurs.

Since at each iteration of the MGDA, all the criteria diminish, we refer to this process as a cooperative-optimization phase.

Convergence of the MGDA

The above MGDA can stop after a finite number of iterations if a Pareto-stationary design-point is reached. Otherwise, we have the following :

Theorem 2 If the sequence of iterates {Y r } of the MGDA is infinite, it admits a weakly convergent subsequence. (Here, the working Hilbert space H is assumed to be reflexive.)

Proof : the following elements hold, in part by virtue of the reformulation of the criteria :

• Since the sequence of values of any considered criterion, say {J 1 (Y r )}, is positive and monotone-decreasing, it is bounded.

• Since J 1 (Y ) is infinite whenever Y is infinite, the sequence of design-vectors {Y r } is bounded, and this implies the statement.

Let Y be the limit. We conjecture that the design-point Y is Pareto-stationary. In what follows, Y 0 is then reset to Y .

Competitive-optimization phase

From a Pareto-stationary design-point Y 0 , we propose either to interrupt the whole optimization process if the performance of the design-point is already satisfactory, or to continue this process by a competitive optimization phase. The competitive-optimization phase can be accomplished by a Nash game based on an appropriate split of variables (see next section for the case of two disciplines). In this section, we propose recommendations to construct a Nash game to carry out the competitiveoptimization phase, after completion of the cooperative-optimization phase, in the case of two disciplines (n = 2).

In the report [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF], a split of territory was defined from the knowledge of a stationary point of one discipline, the preponderant discipline. Since critical points of one discipline are particular Pareto-stationary points, this subsection is meant to generalize the results of the former report.

For simplicity, we consider the case of two disciplines only (n = 2). An initial Pareto-stationary design-point Y 0 is known, and should be used to define a split of variables based on local eigensystems, and a Nash equilibrium-point determined subsequently.

Here, the two criteria are denoted J A and J B , and at Y = Y 0 , the following holds :

for some α A ∈ [0, 1]. Therefore, three cases are possible :

1. Pareto-stationarity of type I : ∇J 0 A = ∇J 0 B = 0; 2. Pareto-stationarity of type II : ∇J 0 A = 0 and ∇J 0 B = 0 (or vice versa); 3. Pareto-stationarity of type III :

The question is what to do next to reaching a design-point Y 0 of Pareto-stationarity of the criteria (J A , J B )? To better understand the question, let us examine first the above three cases assuming both criteria are locally convex.

Convex case :

1. Pareto-stationarity of type I : then, both criteria have simultaneously achieved at Y = Y 0 local minimums of their own. In general the optimization process is terminated.

2. Pareto-stationarity of type II : e.g. ∇J 0 A = 0 and ∇J 0 B = 0. Then, J A has achieved a local minimum, whereas J B is still reducible. The decision can be to interrupt the process if the achieved design is acceptable, or to continue it using the formulation of the former theory [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF] : a Nash equilibrium is sought based on a hierarchical split of variables in the orthogonal basis made of the eigenvectors of matrix H 0 A .

Pareto-stationarity of type III : ∇J

Here, Pareto-optimality has been achieved and in the absence of an additional criterion, the optimization process is terminated.

We now turn to the general case in which the criteria are not assumed to be locally convex at Y = Y 0 .

Non convex case :

In what follows, we discuss the different cases according to various assumptions that can be made on the eigenvalues of the Hessian matrices H 0 A and H 0 B of the two criteria at Y = Y 0 .

Pareto-stationarity of type I :

Since both gradients are equal to zero, the principal term in the expansion of the variations of the two criteria caused by a perturbation δY of the design vector Y about Y 0 are the quadratic terms associated with the respective Hessian matrices, one of which, at least, is not positive-definite by assumption, and perhaps both.

If H 0

A is positive-definite and H 0 B alone has some negative eigenvalues, J A has achieved a minimum whereas J B is still reducible. Then we propose to terminate the optimization process, or to continue it using the formulation of the former theory [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF] : a Nash equilibrium is sought with a hierarchical split of variables based on the eigensystem of matrix H 0 A .

If both Hessian matrices H 0

A and H 0 B have some negative eigenvalues, define the following families of linearly independent eigenvectors associated with these eigenvalues :

Then :

in which {α i } i=1,...,p ∪ {β j } j=1,...,q = {0}, the vector

is not equal to zero (by linear independence of the families F A and F B separately), and it is a descent direction for both criteria. We then propose to make a step in that direction. • Otherwise, SpF A ∩ SpF B = {0}: then we propose to stop, or to determine the Nash equilibrium point using F A (resp. F B ) as the strategy of A (resp. B).

2. Pareto-stationarity of type II : say ∇J 0 A = 0 and ∇J 0 B = 0.

If the Hessian matrix H 0

A is positive-definite, the criterion J A has achieved a local minimum and this setting has been analyzed in [START_REF] Désidéri | Split of Territories in Concurrent Optimization[END_REF] : a Nash equilibrium is sought with a hierarchical split based on the structure of the eigenvectors of H 0 A .

If instead the matrix H 0

A has some negative eigenvalues, let

be a family of associated eigenvectors. Then :

• if ∇J 0 B is not orthogonal to SpF A : a descent direction common to J A and J B exists in SpF A : use it to reduce both criteria.

• otherwise, ∇J 0 B ⊥ SpF A : we propose to identify the Nash equilibrium using F A as the strategy of player A and the remaining eigenvectors of H 0 A as the strategy of player B.

Pareto-stationarity of type III : ∇J 0

A + λ∇J 0 B = 0 (λ > 0). Consider the direction defined by the vector :

Along this direction, the two criteria vary in opposite ways and no rational decision can be made in the absence of other criteria. Thus consider instead possible move in the hyperplane orthogonal to u AB . For this, consider reduced Hessian matrices :

where :

In this hyperplane, by orthogonality to the gradient-vectors, the analysis is that of Paretostationary point of type I in a subspace of dimension N -1.