Strain Rate Dependent Hardening of DP600 Sheet Metal for Large Strains Under In-plane Biaxial Loadings

In this work, an in-plane biaxial tensile test of cruciform specimen is performed to identify the visco-plastic hardening behaviour of metallic sheets for both large strains and intermediate strain rates at room temperature. Firstly, an optimal shape of the specimen is suggested. Then, dynamic biaxial tensile tests are carried out for a dual phase DP600 steel sheet. Experimental forces on the two axes of the specimen are measured during the test and strains in the central area of the specimen are post-treated by means of Digital Image Correlation (DIC) technique. Finally, considering a Hill48 anisotropic yield criterion, two strain rate dependent hardening laws are identified thanks to an inverse procedure based on a Finite Element (FE) modelling of the biaxial tensile test and on the experimental data mentioned above. The identified biaxial flow curves are then compared with the ones from a classical uniaxial tensile test.

INTRODUCTION

In sheet metal forming processes, the material is deformed under multi-axial states and is subjected to large strains. Hence, the identification of material constants, corresponding to the different behaviour models (yield criterion, hardening, …), under biaxial tensile state has become a basic issue for the characterization of phenomenological models.

In the last decades, the in-plane biaxial tensile test has been used to capture anisotropic elastic constants or 2D yield surfaces of metallic sheets by different authors [START_REF] Muller | New experiments for determining yield loci of sheet metal[END_REF][START_REF] Merklein | Characterization of yielding behavior of sheet metal under biaxial stress condition at elevated temperatures[END_REF]. Recently, based on works of Kuwabara [START_REF] Kuwabara | Measurement and analysis of differential work hardening in cold-rolled steel sheet under biaxial tension[END_REF], a standardized flat cruciform specimen shape has been proposed (international standard ISO16842 [START_REF]International Standard ISO16842, Metallic materials -Sheet and strip -Biaxial tensile testing method using a cruciform test piece[END_REF]). Biaxial stressstrain curves and initial or subsequent contours of plastic work of sheet metals subject to biaxial tension at arbitrary stress ratios can be determined. Stress and strain fields are assumed to be homogeneous in the specimen central zone. Stresses are evaluated analytically from measured forces by considering an equivalent cross section and strains in the central zone are obtained from gauge sensor.

More recently, the development of optical full-field measurement techniques for analysing heterogeneous strain fields, such as DIC technique, coupled with an inverse strategy of parameter identification, including the FE model of the specimen, have led to new characterization methodologies of material plastic behaviours. Based on this new methodology, several works have been proposed in the last years (Teaca [5], Prates [START_REF] Prates | A new strategy for the simultaneous identification of constitutive laws parameters of metal sheets using a single test[END_REF], Zhang [START_REF] Zhang | Potential of the cross biaxial test for anisotropy characterization based on heterogeneous strain field[END_REF]).

Several attempts of cruciform shape design to reach large strains have also been presented. Green [START_REF] Green | Experimental investigation of the biaxial behaviour of an aluminum sheet[END_REF] has proposed specimen geometry with a central section thinner than the rest of the specimen and seven parallel slots in each arm. Tasan [START_REF] Tasan | In-Plane Biaxial Loading of Sheet Metal until Fracture[END_REF] has demonstrated that a significant thickness reduction in the centre is necessary to reach fracture under a biaxial strain path. Souto et al. [START_REF] Souto | A numerical methodology to design heterogeneous mechanical tests[END_REF] have proposed an innovative numerical optimization process for the design of heterogeneous tests. Results show that the best specimen shape is the cruciform shape for promoting a rich mechanical information when biaxial loading path is applied. However, in all works presented above, only relatively low values of equivalent plastic strain (close to those obtained in uniaxial tension) are reached before plastic instabilities occur.

For characterizations at large strains, Zidane [11] have proposed a specific cruciform shape to determine the whole forming limit curves (FLC) of metallic sheet. In this specimen, a central thickness reduction is defined by a curved profile to obtain the onset of necking at the central point. Strain path is then completely defined by the displacement ratio imposed on the two axes of the cross specimen. Recently, an optimized cruciform specimen with a flat thickness reduced central section, four slots in each arm and radius fillet between two arms, as shown in Fig. 1, has been proposed from a parametric study by Liu [12]. This shape has been validated by experiments, performed on the same experimental device than the one used by Zidane's, for large strains and static applications for the determination of hardening law parameters up to 30% of equivalent plastic strain on an AA5086 aluminium alloy.

Concerning material behaviour investigations under biaxial tensile strain path at intermediate strain rates, Grolleau [START_REF] Grolleau | Biaxial testing of sheet materials at high strain rates using viscoelastic bars[END_REF] have proposed a dynamic bulge testing device to identify the hardening law of aluminium alloy A1611-T4 sheet at high strain rate up to 500s -1 . A movable bulge cell is designed and installed in a split Hopkinson pressure bar (SHPB) system. Ramezani [START_REF] Ramezani | Combined experimental and numerical analysis of bulge test at high strain rates using split Hopkinson pressure bar apparatus[END_REF] have also introduced a similar high strain rate bulge test technique on the basis of SHPB system. In order to investigate the material behaviour under dynamic and different biaxial stress state, Shimamoto et al. [START_REF] Shimamoto | The development of servo dynamic biaxial loading device[END_REF] have developed a servo-hydraulic dynamic biaxial loading device. The in-plane dynamic biaxial test on cruciform specimen is carried out at 2m/s to reveal the crack extension behaviour of aluminium alloy AA7075-T6.

In the present work, the specific biaxial tensile device with four independent servo-hydraulic actuators already used in [START_REF] Zhang | Potential of the cross biaxial test for anisotropy characterization based on heterogeneous strain field[END_REF]11,[START_REF] Liu | Identification of sheet metal hardening for large strains with an in-plane biaxial tensile test and a dedicated cross specimen[END_REF] to perform in-plane biaxial tensile tests on cruciform specimens at quasi-static strain rate is adopted to performed quasi-static and dynamic biaxial tensile tests on Dual Phase DP600 steel specimens. Strainrate dependent hardening of this material is characterized at room temperature. Moderate strain rates (up to 10s -1 ) and large strains (up to 40% of equivalent plastic strain) are tested. The deformation-induced thermal effects are not considered in this study even if this phenomenon can be significant at tested strain rates which are closer to the adiabatic limit. Experiments being performed at room temperature, temperature sensitivity of flow stress can be considered as a secondary material factor. The identified biaxial flow stress curves are then compared with uniaxial ones for the quasi-static and intermediate strain rates to show the benefits of the proposed methodology.

BIAXIAL TENSILE TESTS

Testing specimen

Dual Phase DP600 steel provided in sheets of thickness 2 mm is used in this study. Main dimensions of the specimen shape are given in Fig. 1.

FIGURE 1. Geometry of the cruciform shape

The ends of each arm of the specimen used to connect the specimen to the actuator rod are not presented in this figure but a general view of the whole specimen is shown in Fig. 2. This geometry has been validated in [START_REF] Liu | Identification of sheet metal hardening for large strains with an in-plane biaxial tensile test and a dedicated cross specimen[END_REF] for the characterization of the hardening behaviour for large strains (up to 30%) in quasi-static conditions. The thickness reduction of the central zone is manufactured by milling and slits are obtained by a wire cut electric discharge machine.

Experimental device

The biaxial machine is equipped of four independent servo-hydraulic actuators. Each end of the cruciform specimen is connected to an actuator rod through a mechanical part assembly as shown in Fig. 2. For dynamic tests, the impactor is accelerated along the sliding bar to obtain the specific velocity before the specimen is loaded. Due to the initial impact, oscillations appear on force signal. To reduce these oscillations a damping layer of elastomer is setting up at the interface between the sliding bar and impactor. The thickness of damping layer is 3mm. After the impact, the displacement of the sliding bar is transmitted to each specimen end through the load sensor and the biarticulated link. During the test, the velocity is maintained almost constant due to the inertia effect of impactor. Tensile tests on cruciform specimens are carried out at three loading velocities: 0.02mm/s, 1mm/s and 250mm/s. The experimental forces along the two perpendicular directions are measured by deformation gauge load sensors. A high speed camera is adopted to record the surface deformation of the central zone of specimen. Digital image correlation (DIC) technique is used to determine the true strain field on the specimen surface. Details about posttreatment by DIC technique can be found in [START_REF] Liu | Identification of sheet metal hardening for large strains with an in-plane biaxial tensile test and a dedicated cross specimen[END_REF]. The evolutions of the major and minor principal strains at the central point of the specimen are shown in Figs. 3a,3c, 3e for respectively the three velocities 0.02mm/s, 1mm/s and 250mm/s corresponding to an approximate strain rate of 0.005s -1 , 0.2s -1 and 20s -1 . An equivalent plastic strain of more than 30% is observed whatever the tested velocity. Due to little asynchronization between the two tensile directions at the beginning of tests, major principal strain curves does not exactly coincide with the minor principal strain.

PARAMETER IDENTIFICATION OF HARDENING BEHAVIOR

Procedure of identification

The calibration of material constants of DP600 strain rate dependent hardening behavior is obtained by an inverse procedure based on a finite element (FE) modelling of the biaxial test coupling with an optimization platform. The global experimental forces along the two arms are applied to the FE model. The experimental database is made up of the time evolutions of the major and minor strains for the three tested velocities. The experimental and simulated principal strains at the central point of specimen are compared to identify the parameters of strain rate dependent hardening laws. The cost function to be minimized is defined as follows:

( ) ( ) ( ) ( ) ( ) 2 2 2 exp exp 1 1 1 2 n n sim i j i j i j i j j Q t t t n ε ε ε = =   = -    

∑ ∑ ∑

Where n is the total number of time points,

Material models

Considering isotropic elasticity for the DP600 steel, elastic constants are defined by the Young's modulus, 200

E GPa =
, and the Poisson's ratio, 0

. The associated normal flow rule and an isotropic hardening model are assumed. Two different formulations of the general strain rate dependent hardening behaviour, given in equations 1) and 2), are considered. The first one, the Ludwick's law, presents a stiffening behaviour whereas the second one, the Voce's law, shows a saturating behaviour. From experimental observations, strain rate dependence is associated to the initial yield stress 0 σ for the two hardening laws.

2 1 0 m n p m K ε ε ε σ ɺ ɺ + = 1) 1 2 0 exp (1 ( )) m m n p K n σ σ ε ε ε = + - - ɺ ɺ 2)
Based on previous works [START_REF] Liu | Identification of sheet metal hardening for large strains with an in-plane biaxial tensile test and a dedicated cross specimen[END_REF], a Hill48 yield criterion is chosen to describe the DP600 plastic anisotropy. Hill's parameters are calculated by the three anisotropic coefficients defined for the three orientations (0°, 45° and 90°) from the rolling direction: r 0 =0.89 ; r 45 =0.85 ; r 90 =1.12.

RESULTS

The material constants identified for the two hardening laws are presented in Table 1. As it can be seen, relatively close cost functions are found, about 9% whatever the law. For the two hardening laws, a small strain rate dependency of the initial yield function is observed (low values of m 1 ) while a more important one is observed on the hardening behaviour. The simulated principal strains have been compared with the experimental ones, as shown in Fig. 3. Although the simulated principal strains are lower than the experimental ones at the beginning of tests, the observed trends of simulated principal strains are in relatively good agreement with the experimental ones for principal strains above 3% whatever the strain rate considered. The biaxial flow stress curves identified on the basis of Ludwick and Voce models are compared in Fig. 4a. It can be observed that the two hardening laws identified for an equivalent plastic range from 0 to 30% are very close. This result demonstrated that the hardening is well described, whatever the law, until 30%. The Fig. 4b shows a comparison of Ludwick and Voce hardening laws identified from uniaxial tests, i.e. up to 20% equivalent plastic strain, on same DP600 steel sheets (not presented in this paper). As it can be seen, compared to Fig. 4a, very different results are observed for large strains both for Voce and Ludwick formulations. Therefore, as already shown, the dynamic biaxial tensile test is validated to identify the hardening behaviour for large strains and also strain rate hardening dependency under biaxial tensile state.

CONCLUSION

In this work, the potential of the in-plane biaxial tensile test on cross specimen to characterize the strain rate dependent hardening behaviour of metallic sheets under large strains (up to 30% of the equivalent strain level) has been investigated. Due to the complex specimen shape, exhibiting non-homogeneous strain and stress fields, a numerical FE model of the dynamic biaxial tensile test used in an inverse calibration procedure is needed. Strain rate sensitivity of DP600 metallic sheets in an intermediate strain rate range has been identified considering two different hardening models (Ludwick and Voce) and Hill48 anisotropic plastic criterion.

Like the bulge test, in-plane biaxial tensile test permits the identification of hardening behaviour up to large strains. Nevertheless, contrary to the bulge test, strain path is controlled by actuator displacements in the two main directions of the cross specimen and effects of strain path changes can be investigated without any restriction about the type of non-linear path. This feature provides interesting perspectives for the identification of advanced hardening behaviours like isotropic-kinematical combined models.

FIGURE 2 .

 2 FIGURE 2. Dynamic biaxial device with damping layer

sim 1 ε and sim 2 ε 1 ε and exp 2 ε

 212 are the simulated major and minor principal strains at the central element of the FE model and exp are the experimental principal strains at the central point of specimen. The optimization algorithm of Simplex has been chosen to optimize the material parameters. In order to make sure that the global minimum is found, different initial values are compared and more feasible initial sets are chosen for inverse analysis.

FIGURE 3 .

 3 FIGURE 3. Comparison of experimental and simulated strain curves

  (a). From biaxial tensile tests (b). From uniaxial tensile tests

FIGURE 4 .

 4 FIGURE 4. Identified Ludwick and Voce strain rate dependent hardening laws

TABLE 1 .

 1 Identified hardening parameters

	Hardening Law	σ σ σ σ 0 (MPa)	K (MPa)	n	m 1	m 2	Error Q (%) (%) (%) (%)
	Ludwick	339.2	839.7	0.3864	0.0052	0.0158	8.69
	Voce	437.9	446.2	8.2412	0.0032	0.0245	9.63


Sylvain Salvati

Igor Walukiewicz

Typing weak MSOL properties

We consider λY -calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSO) is well suited to express properties of such trees. We give a type system for ensuring that the result of the execution of a λY -program satisfies a given wMSO property. In order to prove soundness and completeness of the system we construct a denotational semantics of λY -calculus that is capable of computing properties expressed in wMSO.

Introduction

Higher-order functional programs are more and more often used to write interactive applications. In this context it is important to reason about behavioral properties of programs. We present a kind of type and effect discipline [START_REF] Nielson | Type and effect systems[END_REF] where a well-typed program will satisfy behavioral properties expressed in weak monadic second-order logic (wMSO).

We consider the class of programs written in the simply-typed calculus with recursion and finite base types: the λY -calculus. This calculus offers an abstraction of higher-order programs that faithfully represents higher-order control. The dynamics of an interaction of a program with its environment is represented by the Böhm tree of a λY -term that is a tree reflecting the control flow of the program. For example, the Böhm tree of the term Y x.ax is the infinite sequence of a's, representing that the program does an infinite sequence of a actions without ever terminating. Another example is presented in Figure 1. A functional program for the factorial function is written as a λY -term Fct and the value of Fct applied to a constant c is calculated. Observe that all constants in Fct are non-interpreted. The Böhm tree semantics means call-by-name evaluation strategy. Nevertheless, call-by-value evaluation can be encoded, so can be finite data domains, and conditionals over them [START_REF] Kobayashi | Model checking higher-order programs[END_REF][START_REF] Haddad | Model checking and functional program transformations[END_REF]. The approach is then to translate a functional program to a λY -term and to examine the Böhm tree it generates.

Since the dynamics of the program is represented by a potentially infinite tree, monadic second-order logic (MSOL) is a natural candidate for the language to formulate properties in. This logic is an extension of first-order logic with quantification over sets. MSOL captures precisely regular properties of trees [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF], and it is decidable if the Böhm tree generated by a given λY -term satisfies a given property [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF]. In this paper we will restrict to weak monadic second-order logic (wMSO). The difference is that in wMSO quantification is restricted to range Fig. 1. Böhm tree of the factorial function over finite sets. While wMSO is a proper fragment of MSO, it is sufficiently strong to express safety, reachability, and many liveness properties. Over sequences, that is degenerated trees where every node has one successor, wMSO is equivalent to full MSO.

The basic judgments we are interested in are of the form BT (M ) α meaning that the result of the evaluation of M , i.e. the Böhm tree of M , has the property α formulated in wMSO. Going back to the example of the factorial function from Figure 1, we can consider a property: all computations that eventually take the "if" branch of the conditional are finite. This property holds in BT (Fct c). Observe by the way that BT (Fct c) is not regular -it has infinitely many non-isomorphic subtrees as the number of subtractions is growing. In general the interest of judgments of the form BT (M ) α is to be able to express liveness and fairness properties of executions, like: "every open action is eventually followed by a close action", or that "there are infinitely many read actions". Various other verification problems for functional programs can be reduced to this problem [START_REF] Kobayashi | Model checking higher-order programs[END_REF][START_REF] Kobayashi | Higher-order multi-parameter tree transducers and recursion schemes for program verification[END_REF][START_REF] Ong | Verifying higher-order programs with patternmatching algebraic data types[END_REF][START_REF] Tobita | Exact flow analysis by higher-order model checking[END_REF][START_REF] Grabowski | Type-based enforcement of secure programming guidelines -code injection prevention at SAP[END_REF].

Technically, the judgment BT (M ) α is equivalent to determining whether a Böhm tree of a given λY -term is accepted by a given weak alternating automaton. This problem is known to be decidable thanks to the result of Ong [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], but here we present a denotational approach. Our two main contributions are:

-A construction of a finitary model for a given weak alternating automaton.

The value of a term in this model determines if the Böhm tree of the term is accepted by the automaton. So verification is reduced to evaluation. -Two type systems. A typing system deriving statements of the form "the value of a term M is bigger than an element d of the model"; and a typing system for dual properties. These typing systems use standard fixpoint rules and follow the methodology coined as Domains in Logical Form [START_REF] Abramsky | Domain theory in logical form[END_REF]. Thanks to the first item, these typing systems can directly talk about acceptance/rejection of the Böhm tree of a term by an automaton. These type systems are decidable, and every term has a "best" type that simply represents its value in the model.

Having a model and a type system has several advantages over having just a decision procedure. First, it makes verification compositional: the result for a term is calculated from the results for its subterms. In particular, it opens possibilities for a modular approach to the verification of large programs. Next, it enables semantic based program transformations as for example reflection of a given property in a given term [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF][START_REF] Salvati | Using models to model-check recursive schemes[END_REF][START_REF] Haddad | Model checking and functional program transformations[END_REF]. It also implies the transfer theorem for wMSO [START_REF] Salvati | Evaluation is MSOL-compatible[END_REF] with a number of consequences offered by this theorem. Finally, models open a way to novel verification algorithms be it through evaluation, type system, or through hybrid algorithms using typing and evaluation at the same time [START_REF] Terui | Semantic evaluation, intersection types and complexity of simply typed lambda calculus[END_REF]. We come back to these points in the conclusions.

Historically, Ong [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] has shown the decidability of the MSO theory of Böhm trees for all λY -terms. This result has been revisited in several different ways. Some approaches take a term of the base type, and unroll it to some infinite object: tree with pointers [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], computation of a higher-order pushdown automaton with collapse [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF], a collection of typing judgments that are used to define a game [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF], a computation of a Krivine machine [START_REF] Salvati | Krivine machines and higher-order schemes[END_REF]. Very recently Tsukada and Ong [START_REF] Tsukada | Compositional higher-order model checking via ω-regular games over Böhm trees[END_REF] have presented a compositional approach: a typing system is used to reduce the verification problem to a series of game solving problems. Another recent advance is given by Hofmann and Chen who provide a type system for verifying path properties of trees generated by first-order λY -terms [START_REF] Chen | Buchi abstraction[END_REF]. In other words, this last result gives a typing system for verifying path properties of trees generated by deterministic pushdown automata. Compared to this last work, we consider the whole λY -calculus and an incomparable set of properties.

Already some time ago, Aehligh [START_REF] Aehlig | A finite semantics of simply-typed lambda terms for infinite runs of automata[END_REF] has discovered an easy way to prove Ong's theorem restricted to properties expressed by tree automata with trivial acceptance conditions (TAC automata). The core of his approach can be formulated by saying that the verification problem for such properties can be reduced to evaluation in a specially constructed and simple model. Later, Kobayashi proposed a type system for such properties and constructed a tool based on it [START_REF] Kobayashi | Model checking higher-order programs[END_REF]. This in turn opened a way to an active ongoing research resulting in the steady improvement of the capacities of the verification tools [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higherorder programs[END_REF][START_REF] Broadbent | C-shore: a collapsible approach to higher-order verification[END_REF][START_REF] Broadbent | Saturation-based model checking of higherorder recursion schemes[END_REF][START_REF] Ramsay | A type-directed abstraction refinement approach to higher-order model checking[END_REF]. TAC automata can express only safety properties. Our model and typing systems set the stage for practical verification of wMSO properties.

The model approach to verification of λY -calculus is quite recent. In [START_REF] Salvati | Using models to model-check recursive schemes[END_REF] it is shown that simple models with greatest fixpoints capture exactly properties expressed with TAC automata. An extension is then proposed to allow one to detect divergence. The simplicity offered by models is exemplified by Haddad's recent work [START_REF] Haddad | Model checking and functional program transformations[END_REF] giving simple semantic based transformations of λY -terms.

We would also like to mention two other quite different approaches to integrate properties of infinite behaviors into typing. Naik and Palsberg [START_REF] Naik | A type system equivalent to a model checker[END_REF] make a connection between model-checking and typing. They consider only safety properties, and since their setting is much more general than ours, their type system is more complex too. Jeffrey [START_REF] Jeffrey | LTL types FRP: Linear-time Temporal Logic propositions as types, proofs as functional reactive programs[END_REF][START_REF] Jeffrey | Functional reactive types[END_REF] has shown how to incorporate Linear Temporal Logic into types using a much richer dependent types paradigm. The calculus is intended to talk about control and data in functional reactive programming framework, and aims at using SMT solvers.

In the next section we introduce the main objects of our study: λY -calculus, and weak alternating automata. Section 3 presents the type system. Its soundness and completeness can be straightforwardly formulated for closed terms of atomic type. For the proof though we need a statement about all terms. This is where the model based approach helps. Section 4 describes how to construct models for wMSO properties. In Section 5 we come back to our type systems. The general soundness and completeness property we prove says that types can denote every element of the model, and the type systems can derive precisely the judgments that hold in the model (Theorem 3). In the conclusion section we mention other applications of our model. All proofs can be found in a long version of the paper [START_REF] Salvati | Typing weak MSOL properties[END_REF].

Preliminaries

We quickly fix notations related to the simply typed λY -calculus and to Böhm trees. We then recall the definition of weak alternating automata on ranked trees. These will be used to specify properties of Böhm trees. λY -calculus The set of types T is constructed from a unique basic type o using a binary operation → that associates to the right. Thus o is a type and if A, B are types, so is (A → B). The order of a type is defined by: order (o) = 0, and order (A → B) = max(1 + order (A), order (B)). We work with tree signatures that are finite sets of typed constants of order at most 1. Types of order 1 are of the form o → • Simply typed λY -terms are built from the constants in the signature, and constants Y A , Ω A for every type A. These stand for the fixpoint combinator and undefined term, respectively. Apart from constants, for each type A there is a countable set of variables x A , y A , . . . . Terms are built from these constants and variables using typed application and λ-abstraction. We shall write sequences of λ-abstractions λx 1 . . . . λx n . M with only one λ: either λx 1 . . . x n . M , or even shorter λx. M . We will often write Y x.M instead of Y (λx.M ). Every λY -term can be written in this notation since Y N has the same Böhm tree as Y (λx.N x), and the latter term is Y x.(N x). We take for granted the operational semantics of the calculus given by β and δ reductions. The Böhm tree of a term M is obtained by reducing it until one reaches a term of the form λx.N 0 N 1 . . . N k with N 0 a variable or a constant. Then BT (M ) is a tree having its root labeled by λx.N 0 and having BT (N 1 ), . . . , BT (N k ) as subtrees. Otherwise BT (M ) = Ω A , where A is the type of M . Böhm trees are infinite normal forms of λY -terms. A Böhm tree of a closed term of type o over a tree signature is a potentially infinite ranked tree: a node labeled by a constant a of type o i → o has i successors (c.f. Figure 1). wMSO and weak alternating automata We will be interested in properties of trees expressed in weak monadic second-order logic. This is an extension of first-order logic with quantification over finite sets of elements. The interplay of negation and quantification allows the logic to express many infinitary properties. The logic is closed for example under constructs: "for infinitely many vertices a given property holds", "every path consisting of vertices having a given property is finite". From the automata point of view, the expressive power of the logic is captured by weak alternating automata. A weak alternating automaton accepts trees over a fixed tree signature Σ.

Example

A weak alternating tree automaton over the signature Σ is:

A = Q, Σ, q 0 ∈ Q, {δ i } i∈N , ρ : Q → N
where Q is a finite set of states, q 0 ∈ Q is the initial state, ρ is the rank function, and

δ i : Q × Σ (i) → P(P(Q) i
) is the transition function. For q in Q, we call ρ(q) its rank. The automaton is weak in the sense that when (S 1 , . . . , S i ) is in δ i (q, a), then the rank of every q in 1≤j≤i S j is not bigger than the rank of q, ρ(q ) ≤ ρ(q). Observe that since Σ is finite, only finitely many δ i are nontrivial. From the definition it follows that δ 2 : Q × Σ (2) → P(P(Q) × P(Q)) and δ 0 : Q × Σ (0) → {0, 1}. We will simply write δ without a subscript when this causes no ambiguity.

Automata will work on Σ-labeled binary trees that are partial functions t : N * • → Σ ∪ {Ω} such that the number successors of a node is determined by the label of the node. In particular, if t(u) ∈ Σ (0) ∪ {Ω} then u is a leaf.

The acceptance of a tree is defined in terms of games between two players that we call Eve and Adam. A play between Eve and Adam from some node v of a tree t and some state q ∈ Q proceeds as follows. If v is a leaf and is labeled by some c ∈ Σ (0) then Eve wins iff δ 0 (q, c) holds. If the node is labeled by Ω then Eve wins iff the rank of q is even. Otherwise, v is an internal node; Eve chooses a tuple of sets of states (S 1 , . . . , S i ) ∈ δ(q, t(v)). Then Adam chooses S j (for j = 1, . . . , i) and a state q ∈ S j . The play continues from the j-th son of v and state q . When a player is not able to play any move, he/she looses. If the play is infinite then the winner is decided by looking at ranks of states appearing on the play. Due to the weakness of A the rank of states in a play can never increase, so it eventually stabilizes at some value. Eve wins if this value is even. A tree t is accepted by A from a state q ∈ Q if Eve has a winning strategy in the game started from the root of t and from q.

Automata with trivial acceptance conditions, as considered by Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higherorder programs[END_REF], are obtained by requiring that all states have rank 0. Automata with co-trivial are just those whose all states have rank 1.

Observe that without a loss of generality we can assume that δ is monotone, i.e. if (S 1 , . . . , S i ) ∈ δ(q, a) then for every (S 1 , . . . , S i ) such that S j ⊆ S j ⊆ {q : ρ(q ) ≤ ρ(q)} we have (S 1 , . . . , S i ) ∈ δ(q, a). Indeed, adding the transitions needed to satisfy the monotonicity condition does not give Eve more winning possibilities.

An automaton defines a language of closed terms of type o whose Böhm trees it accepts from its initial state q 0 :

L(A) = {M : M is closed term of type o, BT (M ) is accepted by A from q 0 }

Type systems for wMSOL

In this section we describe the main result of the paper. We present a type system to reason about wMSO properties of Böhm trees of terms (a dual type system is presented in the appendix). We will rely on the equivalence of wMSO and weak alternating automata, and construct a type system for an automaton. For a fixed weak alternating automaton A we want to characterize the terms whose Böhm trees are accepted by A, i.e. the set L(A). The characterization will be purely type theoretic (cf. Theorem 1).

Fix an automaton A = Q, Σ, q 0 , {δ i } i∈N , ρ . Let m be the maximal rank, i.e., the maximal value ρ takes on Q. For every 0 ≤ k ≤ m we write Q k = {q ∈ Q : ρ(q) = k} and Q ≤k = {q ∈ Q : ρ(q) ≤ k}.

The type system we propose is obtained by allowing the use of intersections inside simple types. This idea has been used by Kobayashi [18] to give a typing characterization for languages of automata with trivial acceptance conditions. We work with, more general, weak acceptance conditions, and this will be reflected in the stratification of types, and two fixpoint rules: greatest fixpoint rule for even strata, and the least fixpoint rule for odd strata.

First, we define the sets of intersection types. They are indexed by a rank of the automaton and by a simple type. Note that every intersection type will have a corresponding simple type; this is a crucial difference with intersection types characterizing strongly normalizing terms [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF]. Letting Types k A = 0≤l≤k types l A we define:

types k o = {q ∈ Q : ρ(q) = k}, types k A→B = {T → s : T ⊆ Types k A and s ∈ types k B } .
The difference with simple types is that now we have a set constructor that will be interpreted as the intersection of its elements. When we write types A or Types A we mean types m A and Types m A respectively; where m is the maximal rank used by the automaton A.

For S ⊆ Types k A and T ⊆ types k B we write S → T for {S → t : t ∈ T }. Notice that S → T is included in types k A→B .

We now give subsumption rules that express the intuitive dependence between types. So as to make the connection with the model construction later, we have adopted an ordering of intersection types that is dual to the usual one.

S ⊆ T ⊆ Q S 0 T ∀s ∈ S, ∃t ∈ T, s A t S A T s = t s 0 t T A S s B t S → s A→B T → t
Given S ⊆ Types A→B and T ⊆ Types A we write S(T ) for the set {t : (U → t) ∈ S ∧ U T }.

The typing system presented in Figure 2 derives judgments of the form Γ M ≥ S where Γ is an environment containing all the free variables of the term M , and S ⊆ Types A with A the type of M . As usual, an environment Γ is a finite list x 1 ≥ S 1 , . . . , x n ≥ S n where x 1 , . . . , x n are pairwise distinct variables of type A i , and S i ⊆ Types Ai . We will use a functional notation and write Γ (x i ) for S i . We shall also write Γ, x ≥ S with its usual meaning.

The rules in the first row of Figure 2 express standard intersection types dependencies: the axiom, the intersection rule and the subsumption rule. The rules in the second line are specific to our fixed automaton. The third line contains the usual rules for application and abstraction. The least fixpoint rule in the next

Γ (λx.M ) ≥ S Γ (Y x.M ) ≥ T Y odd Γ Y x.M ≥ S(T ) S ⊆ types 2k A , T ⊆ Types 2k-1 A , Γ λx.M ≥ (S ∪ T ) → S Γ Y x.M ≥ T Y even Γ Y x.M ≥ S ∪ T Fig. 2. Type system
The main result of the paper says that the typing in this system is equivalent to accepting with our fixed weak alternating automaton.

Theorem 1. For every closed term M of type o and every state q of A: the judgment M ≥ q is derivable iff A accepts BT (M ) from q.

Since there are finitely many types, this typing system is decidable. As we will see in the following example, this type system allows us to prove in a rather simple manner properties of Böhm trees that are beyond the reach of trivial automata. Compared to Kobayashi and Ong type system [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF], the fixpoint typing rules we propose avoid the use of an external solver for a parity game. Our type system makes it also evident what is the meaning of higher-order terms with free variables. In the example below we use fixpoint rules on terms of order 2.

Example 2 Consider the term M = (Y F.N )a where N = λg.g(b(F (λx.g(g x)))).

As we have seen on page 5, BT (M ) = aba 2 ba 4 b . . . a 2 n b . . . . We show with typing that there are infinitely many occurrences of b in BT (M ). To this end we take an automaton has states Q = {q 1 , q 2 }, and works over the signature that contains a and b. The transitions of the automaton are:

δ(q1, a) = {q1} δ(q2, a) = {q1, q2} δ(q1, b) = ∅ δ(q2, b) = q2
The ranks of states are indicated by their subscripts. Starting with state q 2 , the automaton only accepts sequences that contain infinitely many b's. So our goal is to derive (Y F.N )a ≥ q 2 . First observe that from the definition of the transitions of the automaton we get axioms:

a ≥ q1 → q1 a ≥ {q1, q2} → q2 b ≥ ∅ → q1 b ≥ q2 → q2
Looking at the typings of a, we can see that we will get our desired judgment from the application rule if we prove:

Y F.N ≥ S
where S is {q1 → q1, {q1, q2} → q2} → q2.

To this end, we apply subsumption rule and the greatest fixpoint rule:

λF.N ≥ (S ∪ T ) → S Y F.N ≥ T Y even Y F.N ≥ S ∪ T Y F.N ≥ S where T = {(q1 → q1) → q1}
The derivation of the top right judgment uses the least fixpoint rule:

g ≥ q1 → q1 g ≥ q1 → q1 g ≥ q1 → q1 b(F (λx.g(g x))) ≥ q1 g ≥ q1 → q1 g(b(F (λx.g(g x)))) ≥ q1 λF λg.g(b(F (λx.g(g x)))) ≥ ∅ → (q1 → q1) → q1 Y odd Y F.N ≥ (q1 → q1) → q1 Γ g ≥ {q1, q2} → q2 Γ b(F (λx.g(g x))) ≥ q1, q2 Γ g(b(F (λx.g(g x)))) ≥ q2 λF λg.g(b(F (λx.g(g x)))) ≥ (S ∪ T ) → S
where Γ is F ≥ S ∪T, g ≥ {q 1 → q 1 , {q 1 , q 2 } → q 2 }. So the upper left judgment is an axiom. The other judgment on the top is an abbreviation of two judgments: one to show ≥ q 1 and the other one to show ≥ q 2 . These two judgments are proven directly using application and intersection rules.

Models for weak automata

This section presents the model that captures wMSO properties. We assume basic knowledge about domain theory. More specifically, we shall work with (finite) complete lattices and with monotone functions between complete lattices. Given two complete lattices L 1 and L 2 we write mon[L 1 → L 2 ] for the complete lattice of monotone functions between L 1 and L 2 . We construct a model that captures the language defined by a weak automaton: this model depends only on the states of the automaton and their ranks. The transitions of the automaton will be encoded in the interpretation of constants. The challenge in this construction comes from the fact that simply using the least or greatest fixpoints is not sufficient. Indeed, we have shown in [START_REF] Salvati | Using models to model-check recursive schemes[END_REF] that extremal fixpoints in finitary models of λY -calculus capture precisely boolean combinations of properties expressed by automata with trivial acceptance conditions. The structure of a weak automaton will help us here. For the sake of the discussion let us fix an automaton A, and let A ≤k stand for A restricted to states of rank at most k. Ranks stratify the automaton: transitions for states of rank k depend only on states of rank at most k. We will find this stratification in our model too. The interpretation of a term at stratum k will give us the complete information about the behaviour of the term with respect to A ≤k . Stratum k + 1 will refine this information. Since in a run the ranks cannot increase, the information calculated at stratum k +1 does not change what we already know about A ≤k . Abstract interpretation tells us that refinements of models are obtained via Galois connections which are instrumental in our construction. In our model, every element in the stratum k is refined into a complete lattice in the stratum k + 1 (cf. Figure 3). Therefore we will be able to define the interpretations of fixpoints by taking at stratum k the least or the greatest fixpoint depending on the parity of k. In the whole model, the fixpoint computation will perform a sort of zig-zag as represented in Figure 4.

We fix a finite set of states Q and a ranking function ρ : Q → N. Let m be the maximal rank, i.e., the maximal value ρ takes on Q. Recall that for every 0

≤ k ≤ m we let Q k = {q ∈ Q : ρ(q) = k} and Q ≤k = {q ∈ Q : ρ(q) ≤ k}.
We define by induction on k ≤ m an applicative structure D k = (D k A ) A∈types and a logical relation L k (for 0 < k) between D k-1 and D k . For k = 0, the model D 0 is just the model of monotone functions over the powerset of Q 0 with

D 0 o = P(Q 0 ) and D 0 A→B = mon[D 0 A → D 0 B ].
For k > 0, we define D k by means of D k-1 and a logical relation L k :

D k o =P(Q ≤k ) L k o = {(R, P ) ∈ D k-1 o × D k o : R = P ∩ Q ≤(k-1) }, L k A→B ={(f 1 , f 2 ) ∈ D k-1 A→B × mon[D k A → D k B ] : ∀(g 1 , g 2 ) ∈ L k A . (f 1 (g 1 ), f 2 (g 2 )) ∈ L k B } D k A→B ={f 2 : ∃f 1 ∈ D k-1 A→B . (f 1 , f 2 ) ∈ L k A→B }
Observe that D k A is defined by a double induction: the outermost on k and the auxiliary induction on the size of the type. Since L k is a logical relation between

D k-1 and D k , each D k is an applicative structure. As D k-1 o = P(Q ≤(k-1) ), the refinements of elements R in D k-1 o are simply the sets P in P(Q ≤k ) so that R = P ∩ Q ≤(k-1)
. This explains the definition of L k o . For higher types, L k is defined as it is usual for logical relations. Notice that D k A→B is the subset of the monotone functions e from D k A to D k B for which there exist an element d in D k-1 A→B so that (d, e) is in L k A→B ; that is we only keep those monotone functions that correspond to refinements of elements in D k-1 A→B . Remarkably this construction puts a lot of structure on D k A . The first thing to notice is that for each type A,

D k A is a complete lattice. Given d in D k-1 A , we write L k A (d) for the set {e ∈ D k A : (d, e) ∈ L k A }.
For each d, we have that L k A (d) is a complete lattice and that moreover, for

d 1 and d 2 in D k-1 A , L k A (d 1 ) and L k A (d 2
) are isomorphic complete lattices. We write d ↑∨ and d ↑∧ respectively for the greatest and the least elements of L k A (d). Finally, for each element e in D k A , there is a unique d so that (d, e) is in L k A , we write e ↓ for that element. Figure 3 We can now define fixpoint operators in every applicative structure

D k . Definition 1. For f ∈ D 0 A→A we define fix 0 A (f ) = {f n ( 0 ) : n ≥ 0}. For 0 < 2k ≤ m and f ∈ D 2k
A→A we define

fix 2k A (f ) = {f n (e) : n ≥ 0} where e = (fix 2k-1 A (f ↓ )) ↑∨ For 0 < 2k + 1 ≤ m and f ∈ D 2k+1 A→A we define fix 2k+1 A (f ) = {f n (d) : n ≥ 0} where d = (fix 2k A (f ↓ )) ↑∧
Observe that, for even k, e is obtained with (•) ↑∨ ; while for odd k, (•) ↑∧ is used.

The intuitive idea behind the definition of the fixpoint is presented in Figure 4. On stratum 0 it is just the greatest fixpoint. Then this greatest fixpoint is lifted to stratum 1, and the least fixpoint computation is started from it. The result is then lifted to stratum 2, and once again the greatest fixpoint computation is started, and so on. The Galois connections between strata guarantee that this process makes sense. Fig. 4. A computation of a fixpoint: it starts in D 0 , and then the least and the greatest fixpoints alternate.

Equipped with the interpretation of fixpoints given by Definition 1 the applicative structure D k is a model of the λY -calculus. In particular, two terms that are βδ-convertible have the same interpretation in that model. A constant c in Σ (i) , is then interpreted as the function f k,c of D k o i →o so that for every

S 1 , . . . , S i ⊆ D k o , f k,c (S 1 , . . . , S i ) = {q ∈ D k o : (S 1 , . . . , S i ) ∈ δ(c, q)}. Observe that the identity (f k+1,c ) ↓ = f k,c holds. Moreover if we let A(M ) = {q ∈ Q : A accepts BT (M )
from q} be the set of states from which A accepts the tree BT (M ), then we have that: Theorem 2. For every closed term M of type 0, and for every 0 ≤ k ≤ m we have:

[[M ]] k = A(M ) ∩ Q ≤k .
The two directions of Theorem 2 are proved using different techniques. The left to right inclusion uses a rather simple unrolling. The other inclusion is proved using a standard technique based on logical relations.

From models to type systems

We are now in a position to show that our type system from Figure 2 can reason about the values of λY -terms in a stratified model (Theorem 3). Thanks to Theorem 2 this means that the type system can talk about the acceptance of the Böhm tree of a term by the automaton. This implies soundness and completeness of our type system, Theorem 1.

Throughout this section we work with a fixed signature Σ and a fixed weak alternating automaton A = Q, Σ, q 0 , δ o , δ o 2 →o , ρ . As in the previous section, for simplicity of notations we will assume that the constants in the signature are of type o or o → o → o. We will also prefer the notation Y x.M to Y (λx.M ).

The arrow constructor in types will be interpreted as a step function in the model. Step functions are particular monotone functions from a lattice L 1 to a lattice L 2 . For d in L 1 and e in L 2 , the step function d e is defined by:

(d e)(h) = e when d ≤ h ⊥ otherwise
Types can be meaningfully interpreted at every level of the model. So [[t]] l will denote the interpretation of t in D l defined as follows.

[

[q]] l = {q} if ρ(q) ≤ l, ∅ otherwise [[S]] l = {[[t]] l : t ∈ S} for S ⊆ Types A [[T → s]] l = [[T ]] l [[s]]
k : [[M ]] k [[Γ ]] k ≥ [[S]] k iff Γ M ≥ S is derivable.
The above theorem implies Theorem 1 stating soundness and completeness of the type system. Indeed, let us take a closed term M of type o, and a state q of our fixed automaton A. Theorem 2 tells us that [[M ]] = A(M ); where A(M ) is the set of states from which A accepts BT (M ). So M ≥ q is derivable iff

[[M ]] ⊇ {q} iff q ∈ A(M ).
One may ask if it is also possible to reason about over-approximations of the value of a term, i.e. about statements of the form

[[M ]] k [[Γ ]] k ≤ d.
This is indeed possible thanks to the dualities of the model. It is enough to dualize the type system: restricting the rule for greatest fixpoint on odd ranks instead of even ones, taking the dual subsumption order for the types, and typing constant with the transitions of the dual weak alternating automaton. This dual system is presented in the appendix. It derives judgments of the form: Γ M S since the interpretation of S is also dualized. Without going into details of this dualization we can state the following theorem. Theorem 4. For every closed term M of type o and every state q of A: the judgment M q is derivable iff A does not accept BT (M ) from q. Together the type system and its dual give a precise characterization of [[M ]] = L(A) that is the set of states from which our fixed automaton A accepts BT (M ).

Conclusions

We have shown how to construct a model for a given weak alternating tree automaton so that the value of a term in the model determines if the Böhm tree of the term is accepted by the automaton. Our construction builds on ideas from [START_REF] Salvati | Using models to model-check recursive schemes[END_REF] but requires to bring out the modular structure of the model. This structure is very rich, as testified by Galois connections. This structure allows us to derive type systems for wMSO properties following the "domains in logical form" approach.

The type systems are relatively streamlined: the novelty is the stratification of types used to restrict applicability of the greatest fixpoint rule. In comparison, Kobayashi and Ong [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF] use a type system only as an intermediate formalism to obtain a game whose solution answers the model-checking problem. Their type system handles only closed terms of type o. It does not have a rule for lambdaabstraction, nor for fixpoints (that are handled via games). Tsukada and Ong have recently proposed a higher-order analogue of this system [START_REF] Tsukada | Compositional higher-order model checking via ω-regular games over Böhm trees[END_REF]. Even in this new approach the fixpoint is still handled by games, and the algorithmic properties of the model behind their system are not investigated. While our approach applies only to wMSO, our model is simply based on functions over finite sets with standard application operation. Typing in our system is decidable, actually the height of the derivation is bounded by the size of the term. Yet the width can be large, that is unavoidable given that the typability is n-Exptime hard for terms of order n [START_REF] Terui | Semantic evaluation, intersection types and complexity of simply typed lambda calculus[END_REF]. Due to the correspondence of the typing with semantics, every term has a "best" type.

While the paper focuses on typing, our model construction can be also used in other contexts. It allows us to immediately deduce reflection [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF] and transfer [START_REF] Salvati | Evaluation is MSOL-compatible[END_REF] theorems for wMSO. Our techniques used to construct models and prove their correctness rely on usual techniques of domain theory [START_REF] Amadio | Domains and Lambda-Calculi[END_REF], offering an alternative, and arguably simpler, point of view to techniques based on unrolling.

The idea behind the reflection construction is to transform a given term so that at every moment of its evaluation every subterm "knows" its meaning in the model. In [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF] this property is formulated slightly differently and is proved using a detour to higher-order pushdown automata. Recently Haddad [START_REF] Haddad | Model checking and functional program transformations[END_REF] has given a direct proof for all MSO properties. The proof is based on some notion of applicative structure that is less constrained than a model of the λY -calculus. One could apply his construction, or take the one from [START_REF] Salvati | Using models to model-check recursive schemes[END_REF].

The transfer theorem says that for a fixed finite vocabulary of terms, an MSOL formula ϕ can be effectively transformed into an MSOL formula ϕ such that for every term M of type 0 over the fixed vocabulary: M satisfies ϕ iff the Böhm tree of M satisfies ϕ. Since the MSO theory of a term, that is a finite graph, is decidable, the transfer theorem implies decidability of MSO theory of Böhm trees of λY -terms. As shown in [START_REF] Salvati | Evaluation is MSOL-compatible[END_REF] it gives also a number of other results.

A transfer theorem for wMSO can be deduced from our model construction. For every wMSO formula ϕ we need to find a formula ϕ as above. For this we transform ϕ into a weak alternating automaton A, and construct a model D ϕ based on A. Thanks to the restriction on the vocabulary, it is quite easy to write for every element d of the model D ϕ a wMSO formula α d such that for every term M of type 0 in the restricted vocabulary:

M α d iff [[M ]] Dϕ = d.
The formula ϕ is then just a disjunction d∈F α d , where F is the set elements of D ϕ characterizing terms whose Böhm tree satisfies ϕ.

The fixpoints in our models are non-extremal: they are neither the least nor the greatest fixpoints. From [START_REF] Salvati | Using models to model-check recursive schemes[END_REF] we know that this is unavoidable. We are aware of very few works considering such cases. Our models are an instance of cartesian closed categories with internal fixpoint operation as studied by Bloom and Esik [START_REF] Stephen | Bloom and Zoltàn Ésik. Fixed-point operations on CCC's. part I[END_REF]. Our model satisfies not only Conway identities but also a generalization of the commutative axioms of iteration theories [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF]. Thus it is possible to give semantics to the infinitary λ-calculus in our models. It is an essential step towards obtaining an algebraic framework for weak regular languages [START_REF] Blumensath | An algebraic proof of Rabin's tree theorem[END_REF].

A Example of a weak alternating automaton

Consider a weak alternating automaton A defining the property "action b appears infinitely often". The automaton has states Q = {q 1 , q 2 }, and the signature Σ = {a, b} consisting of two constants of type o → o. Over this signature, the Böhm trees are just sequences. The transitions of A are: δ(q 1 , a) = {q 1 } δ(q 2 , a) = {q 1 , q 2 }δ(q 1 , b) = ∅ δ(q 2 , b) = q 2

The ranks of states are indicated by their subscripts. When started in q 2 the automaton spawns a run from q 1 each time it sees letter a. The spawned runs must stop in order to accept, and they stop when they see letter b. So every a must be eventually followed by b.

B Dual type system

The dual type system is presented on figure 6. This system is obtained from the one presented in Section 3 and Figure 2 in several way:

the subsumption order on types is dual to the one used in the type system of Figure 2, the greatest fixpoint rule is restricted to apply only for the odd ranks instead of the even ranks as in the type system of Figure 2, the types of the constants are induced by the behavior of the automaton that is dual to the one used in the type system of Figure 2.

A last difference is that the notation S(T ) now refers to the set {s : U → s ∈ S ∧ U T }.

We are now going to explain how the dual type system is related to the model D k . As we have seen, the applicative structure D k A is a lattice, therefore each construction can be dualized: in Abramsky's methodology, this consists in considering ∧-prime elements of the models, meets and co-step functions instead of ∨-primes, joins and step functions. It is worth noticing that dualizing at the level of the model amounts to dualizing the automaton. So, in particular, we can define a system so that BT (M ) is not accepted by A from state q iff Γ M q is derivable. While the first typing system establishes positive facts about the semantics, the second one refutes them. For this, we use the same syntax to denote types, but we give types a different semantics that is dual to the first semantics we have used.

For the dual system we will need co-step functions. For comparison we recall also step functions.

Step and co-step functions are particular monotone functions from a lattice L 1 to a lattice To emphasize that we work in D l we will write d l e and d l e. Co-step functions help us to give an alternate dual interpretation of types in the models.

q k = Q ≤k -{q}, S → f k = { g k : g ∈ S} k f k .

Similarly to the definition of [[•]]

k , we write S k for { s k : s ∈ S} and we also have that T → S k = T k k S k .

We then obtain a theorem that is dual to Theorem 3.

  As an example take (Y F. N )a where N = λg.g(b(F (λx.g(g x)))). Both a and b have the type o → o; while F has type (o → o) → o, and so does N . Observe that we are using a more convenient notation Y F here. The Böhm tree of (Y F.N )a is BT ((Y F.N )a) = aba 2 ba 4 b . . . a 2 n b . . . after every consecutive occurrence of b the number of occurrences of a doubles because of the double application of g inside N .

1 A 1 AFig. 3 .

 113 Fig. 3. Relation between models D k-1 and D k . Every element in D k-1 is related to a sub-lattice of elements in D k .

lTheorem 3 .

 3 for (T → s) ∈ Types A Actually every element of D l is the image of some type via [[•]] l : types are syntactic representations of the model. The next theorem is the main technical result of the paper. It says that the type system can derive all lower-approximations of the meanings of terms in the model. For an environment Γ , we write [[Γ ]] k for the valuation such that [[Γ ]] k (x) = [[Γ (x)]] k . For k = 0, . . . , m and S ⊆ Types

Corollary 1 .

 1 For a closed term M of type o, [[M ]] = [[S]] iff both M ≥ S and M (Q -S).

Fig. 5 .

 5 Fig. 5. A run of an alternating automaton on a . . . ab . . .

L 2 .

 2 For d in L 1 and e in L 2 , the step function d e and the co-step function d g are defined by: (d e)(h) = e when d ≤ h ⊥ otherwise (d e)(h) = e when h ≤ d otherwise .

Theorem 5 .ΓFig. 6 .

 56 Fig. 6. Dual type system

  • • → o → o that we abbreviate o i → o when they contain i + 1 occurrences of o. For convenience we assume that o 0 → o is just o. If Σ is a signature, we write Σ (i) for the set of constants of type o i → o. In examples we will often use constants of type o → o as this makes the examples more succinct. At certain times, we will restrict to the types o and o 2 → o that are representative for all the cases.

line is standard. The greatest fixpoint rule in the last line is more intricate. It is allowed only on even strata. If taken for k = 0 the rule becomes the standard rule for the greatest fixpoint as the set T must be the empty set. For k > 0 the rule permits to incorporate T that is the result of the fixpoint computation on the lower stratum.Γ, x ≥ S x ≥ S Γ M ≥ S Γ M ≥ T Γ M ≥ S ∪ T Γ M ≥ S T S Γ M ≥ T Γ c ≥ {q : δo(q, c) holds} (S1, . . . , Si) ∈ δ(a, q) Γ a ≥ {S1 → • • • → Si → q} Γ M ≥ S Γ N ≥ T Γ M N ≥ S(T ) S ⊆ Types k , T ⊆ types k Γ, x ≥ S M ≥ T Γ λx.M ≥ S → T

We have displayed only one of the two premises of the Y odd rule since the other is of the form ≥ ∅ so it is vacuously true. The top right judgment is derivable directly from the axiom on b. The derivation of the remaining judgment λF.N ≥ (S ∪ T ) → S is as follows.