Andrzej S Murawski

Igor Walukiewicz

Third-Order Idealized Algol with Iteration is Decidable

The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (IA *

3 ). They are approached via a combination of game semantics and language theory. It is shown that for each IA * 3 -term one can construct a pushdown automaton recognizing a representation of the strategy induced by the term. The automata have some additional properties ensuring that the associated equivalence and inclusion problems are solvable in Ptime. This gives an Exptime decision procedure for contextual equivalence and approximation for β-normal terms. Exptime-hardness is also shown in this case, even in the absence of iteration.

Introduction

In recent years game semantics has provided a new methodology for constructing fully abstract models of programming languages. By definition, such models capture the notions of contextual equivalence and approximation and so offer a semantic framework in which to study these two properties. In this paper we focus on the game semantics of Idealized Algol, a language proposed by Reynolds as a synthesis of functional and imperative programming [START_REF] Reynolds | The essence of Algol[END_REF]. It is essentially the simply-typed λ-calculus extended with constants for modelling arithmetic, assignable variables and recursion. This view naturally determines fragments of the language when the typing framework is constrained not to exceed a particular order. Many versions of Algol have been considered in the literature. Typically, for decidability results, general recursion has to be left out completely or restricted to iteration, e.g. in the form of while-loops as will be the case in this paper. For similar reasons, base types are required to be finite.

In game models, terms of a programming language are modelled by strategies. These in turn can sometimes be represented by formal languages, i.e. sets of finite words, such that equivalence and approximation are established by verifying respectively equality and inclusion of the induced languages. This approach to modelling semantics is interesting not only because it gives new insights into the semantics but also because it opens up the possibility of applying existing algorithms and techniques developed for dealing with various families of formal languages [START_REF] Abramsky | Applying game semantics to compositional software modelling and verification[END_REF]. Therefore, it is essential that the class of languages one uses is as simple as possible -ideally its containment problem should be decidable and of relatively low complexity.

In this paper we show how to model terms of third-order Idealized Algol with iteration (IA *

3 ) using variants of visibly pushdown automata [START_REF] Alur | Visibly pushdown languages[END_REF]. One of the advantages of taking such specialized automata is that the instances of the containment problem relevant to us will be decidable in Ptime. Another is the relative simplicity of the inductive constructions of automata for the constructs of the language. We give the constructions only for terms in β-normal form taking advantage of the fact that each term can be effectively normalized. The automata constructed by our procedure have exponential size with respect to the size of the term, which leads to an exponential-time procedure for checking approximation and equivalence of such terms. We also provide the matching lower bound by showing that equivalence of third-order terms, even without iteration, is Exptime-hard.

Ghica and McCusker [START_REF] Ghica | Reasoning about Idealized Algol using regular expressions[END_REF] were the first to show how certain strategies can be modelled by languages. They have defined a procedure which constructs a regular language for every term of second-order Idealized Algol with iteration. Subsequently, Ong [START_REF] Ong | Observational equivalence of 3rd-order Idealized Algol is decidable[END_REF] has shown how to model third-order Idealized Algol without iteration using deterministic pushdown automata. Our work can be seen as an extension of his in two directions: a richer language is considered and a more specialized class of automata is used (the latter is particularly important for complexity issues). In contrast to the approach of [START_REF] Ong | Observational equivalence of 3rd-order Idealized Algol is decidable[END_REF], we work exclusively with the standard game semantics and translate terms directly into automata, while the translation in [START_REF] Ong | Observational equivalence of 3rd-order Idealized Algol is decidable[END_REF] relies on an auxiliary form of game semantics (with explicit state) in which strategies are determined by view-functions. In the presence of iteration these functions are no longer finite and the approach does not work any more (in yet unpublished work Ong proposes to fix this deficiency by considering view-functions whose domains are regular sets and which act uniformly with respect to the regular expressions representing these sets). It should also be noted that our construction yields automata without pushdowns for terms of order two, hence it also subsumes the construction by Ghica and McCusker. Our results bring us closer to a complete classification of decidable instances of Idealized Algol and their complexity. Since the fourth-order fragment without iteration was shown undecidable in [START_REF] Murawski | On program equivalence in languages with ground-type references[END_REF], the only unresolved cases seem to be those of second-and third-order fragments with recursively defined terms of base types (of which iteration is a special case). Recursive functions lead to undecidability at order two as shown in [START_REF] Ong | Observational equivalence of 3rd-order Idealized Algol is decidable[END_REF].

The outline of the paper is as follows. We present Idealized Algol and its thirdorder fragment IA * 3 in Section 2. Then we recapitulate the game model of the language. Next the class of simple terms is defined. These are terms that induce plays in which pointers can be safely omitted which makes it possible to represent their game semantics via languages. In Section 4 we introduce our particular class of automata and give an inductive construction of such an automaton for every simple term in β-normal form. In Section 5 we show how to deal with terms that are not simple. The last section concerns the Exptime lower bound for the complexity of equivalence in IA * 3 .

Idealized Algol

We consider a finitary version IA f of Idealized Algol with active expressions [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF]. It can be viewed as a simply typed λ-calculus over the base types com, exp, var (of commands, expressions and variables respectively) augmented with the constants

skip : com i : exp (0 ≤ i ≤ max ) Ω B : B succ : exp → exp pred : exp → exp ifzero B : exp → B → B → B seq B : com → B → B deref : var → exp assign : var → exp → com cell B : (var → B) → B mkvar : (exp → com) → exp → var
where B ranges over base types and exp = { 0,

Γ M : T → T ∆ N : T Γ, ∆ M N : T Γ, x 1 : T, x 2 : T M : T Γ, x : T M [x/x 1 , x/x 2 ] : T .
The linear application simply corresponds to composition: in any cartesian-closed category Γ, ∆ M N : T is equal (up to currying) to

∆ N : T ; λx T .λΓ.M x : T → (Γ → T ) ∆ ⇒ T T ⇒ ( Γ ⇒ T ).
Thanks to the applicative syntax and the above decomposition the process of interpreting the language can be divided into simple stages: the modelling of base constructs (free identifiers and constants), composition, contraction and currying.

The operational semantics of IA f can be found in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF]; we will write M ⇓ if M reduces to skip. We study the induced equivalence and approximation relations.

Definition 1. Two terms Γ M 1 , M 2 : T are equivalent (Γ M 1 ∼ = M 2 ) if for any context C[-] such that C[M 1 ], C[M 2 ] are closed terms of type com, we have C[M 1 ] ⇓ if and only if C[M 2 ] ⇓. Similarly, M 1 approximates M 2 (Γ M 1 ∼ M 2 ) iff
for all contexts satisfying the properties above whenever

C[M 1 ] ⇓ then C[M 2 ] ⇓.
In general, equivalence of IA f terms is not decidable [START_REF] Murawski | On program equivalence in languages with ground-type references[END_REF]. To obtain decidability one has to restrict the order of types, which is defined by: ord(B) = 0 and ord(T → T ) = max(ord(T ) + 1, ord(T )). Definition 2. An IA f term Γ M : T is an ith-order term provided its typing derivation uses sequents in which the types of free identifiers are of order less than i and the type of the term has order at most i. The collection of ith-order IA f terms will be denoted by IA i .

To establish decidability of program approximation or equivalence of ith-order terms it suffices to consider ith-order terms in β-normal form. To type such terms, one only needs a restricted version of the application rule in which the function term M is either a constant or a term of the form f M 1 • • • M k , where f : T is a free identifier (and so ord(T ) < i).

In this paper we will be concerned with IA 3 enriched with while, which we denote by IA * 3 for brevity.

Game semantics

Here we recall the basic notions of game semantics and discuss how to code strategies in terms of languages. To that end we investigate when it is not necessary to represent pointers in plays and obtain the class of simple terms for which pointers can be disregarded. We use the game semantics of Idealized Algol as described in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF]. The games are defined over arenas which specify the available moves and the relationship between them.

Definition 3. An arena A is a triple M A , λ A , A , where M A is the set of moves, λ A : M A → { O, P } × { q, a
} indicates whether a move is an O-move or a P-move and whether it is a question or an answer, and A ⊆ (M A +{ })×M A is the enabling relation which must satisfy the following two conditions.

-For all m, n ∈ M A if m A n then m and n belong to different players and m is a question.

-If

A m then m is an O-question which is not enabled by any other move. Such moves are called initial; the set containing them will be denoted by I A .

The permitted scenarios in a given arena are required to be legal justified sequences of moves. A justified sequence s over an arena A is a sequence of moves from M A equipped with pointers so that every non-initial move n (in the sense of Definition 3) in s has a pointer to an earlier move m in s with m A n (m is then called the justifier of n). Given a justified sequence s, its O-view s and P-view s are defined as follows, where o and p stand for an O-move and a P-move respectively:

= so = s o so t p = s o p = so = o (if o is initial) sp = s p sp t o = s p o.
Definition 4. A justified sequence s is legal if it satisfies the following:

-players alternate (O begins), -the visibility condition holds: in any prefix tm of s if m is a non-initial Omove then its justifier occurs in t and if m is a P-move then its justifier is in t ,

-the bracketing condition holds: for any prefix tm of s if m is an answer then its justifier must be the last unanswered question in t.

The set of legal sequences over arena A is denoted by L A .

Formally, a game will be an arena together with a subset of L A . This makes it possible to define different games over the same arenas.

Definition 5. A game is a tuple M A , λ A , A , P A such that M A , λ A , A is an arena and P A is a non-empty, prefix-closed subset of L A (called the set of positions or plays in the game) 3 .

Games can be combined by a number of constructions, notably ×, ⊗, !, , ⇒.

We describe them briefly below. In the first three cases the enabling relation is simply inherited from the component games. As for plays, we have P A×B = P A + P B in the first case. In contrast, each play in P A⊗B is an interleaving of a play from A with a play from B (and only O can switch between them). Similarly, positions in P !A are interleavings of a finite number of plays from P A (again only O can jump between them). The construction is more complicated: we have

M A B = M A + M B but the ownership of A moves in M A B is reversed. The enabling relation is defined by A B = A + B +{ (b, a) | b ∈ I B ∧ a ∈ I A } and plays of A
B are interleavings of single plays from A and B. This time, however, each such play has to begin in B and only P can switch between the interleaved plays. The game A ⇒ B is defined as !A B.

Example 1. The underlying arena of (( com ⇒ com ) ⇒ com ) ⇒ com has the following shape:

d 3 r 3 d 2 r 2 d 1 r 1 d 0 r 0 Definition 6.
In arenas corresponding to IA f types we can define the order of a move inductively (we denote it by ord A (m)). The initial O-questions have order 0. For all other questions q we define ord A (q) to be ord A (q ) + 1 where q q (this definition is never ambiguous for the arenas in question). Answers inherit their order from the questions that enable them. The order of an arena is the maximal order of a question in it.

For instance, in the example above r 3 is a third-order move. We will continue to use subscripts to indicate the order of a move.

The next important definition is that of a strategy. Strategies determine unique responses for P (if any) and do not restrict O-moves. Definition 7. A strategy in a game A (written as σ : A) is a prefix-closed subsets of plays in A such that: (i) whenever sp 1 , sp 2 ∈ σ and p 1 , p 2 are Pmoves then p 1 = p 2 ; (ii) whenever s ∈ σ and so ∈ P A for some O-move o then so ∈ σ. We write comp(σ) for the set of non-empty complete plays in σ, i.e. plays in which all questions have been answered.

An IA f term Γ M : T , where Γ = x 1 : T 1 , • • • , x n :
T n , is interpreted by a strategy (denoted by Γ M : T ) for the game

Γ T = T 1 × • • • × T n ⇒ T =!( T 1 ) ⊗ • • • ⊗!( T n ) T .
Remark 1. From the definitions of the ⊗ and constructions we can deduce the following switching properties. A play in Γ T always starts with an initial O-question in T . Subsequently, whenever P makes a move in T i or T , O must also follow with a move in T i or T respectively. We also note that the arenas used to interpret ith-order terms are of order i.

The interpretation of terms presented in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] gives a fully abstract model in the sense made precise below.

Theorem 1. Γ M 1 ∼ M 2 iff comp( Γ M 1 ) ⊆ comp( Γ M 2 ). Conse- quently, Γ M 1 ∼ = M 2 iff comp( Γ M 1 ) = comp( Γ M 2 ).
In the sections to follow we will show how to represent strategies defined by β-normal IA * 3 -terms via languages. The simplest, but not always faithful, representation consists in taking the underlying set of moves. Definition 8. Given P ⊆ P G we write L(P ) for the language over the alphabet M G consisting of the sequences of moves of the game G underlying positions in P .

While in L(P ) we lose information about pointers, the structure of the alphabet M G remains unchanged; in particular each letter has an order as it is a move from M G . Some β-normal IA * 3 terms define strategies σ for which L(σ) constitutes a faithful representation. This will be the case if pointers are uniquely reconstructible. To identify such terms it is important to understand when pointers can be ignored in positions over third-order arenas and when they have to be represented explicitly in some way. Due to the well-bracketing condition, pointers from answer-moves always lead to the last unanswered question, hence they are uniquely determined by the underlying sequence of moves. The case of questions is more complicated. Initial questions do not have pointers at all, however all non-initial ones do, which is where ambiguities might arise. Nevertheless it turns out that in the positions of interest pointers leading from first-order and second-order questions are determined uniquely, because only one unanswered enabler will occur in the respective view. Third-order questions do need pointers though, the standard example [START_REF] Hyland | On full abstraction for PCF[END_REF] being λf.f (λx.f (λy.x)) and λf.f (λx.f (λy.y)). The terms define the following positions respectively: q 0 q 1 q 2 q 1 q 2 q 3 q 0 q 1 q 2 q 1 q 2 q 3 .

Here pointers from third-order questions cannot be omitted, because several potential justifiers occur in the P-view. To get around the difficulties we will first focus on terms where the ambiguities for third-order questions cannot arise.

Definition 9. A β-normal IA * 3 -term will be called simple iff it can be typed without applying the contraction rule to identifiers of second-order types.

Clearly, the two terms above are not simple.

Lemma 1. Suppose Γ M : T is simple and sq 3 ∈ Γ M : T . Then s contains exactly one unanswered occurrence of an enabler of q 3 . Consequently, the justifiers of all third-order moves in positions generated by simple terms are uniquely determined so, if σ denotes a simple term, L(σ) uniquely determines σ. In the next section we focus on defining automata accepting L(comp(σ)).

Automata for simple terms

This section presents the construction of automata recognizing the languages defined by simple terms. The construction proceeds by induction on the term structure. The only difficult case is application. We have chosen to pass through the intermediate step of linear composition to make the technical details more transparent.

Automata model

The pushdown automata we are going to use to capture simple terms are specialized deterministic visibly pushdown automata [START_REF] Alur | Visibly pushdown languages[END_REF]. Their most important feature is the dependence of stack actions on input letters. Another important point in the following definitions is that the automata will use the stack only when reading third-order moves.

Definition 10. A strategy automaton is a tuple

A = Q, M push , M pop , M noop , Γ, i, δ push , δ pop , δ noop , F
where Q is a finite set of states; (M push , M pop , M noop ) is the partition of the input alphabet into push, pop and noop (no stack change) letters; Γ is the stack alphabet; i is the initial state and F ⊆ Q is the set of final states. The transitions are given by the partial functions:

δ push : Q × M push • → Q × Γ δ pop : Q × M pop × Γ • → Q δ noop : Q × M noop • → Q.
Observe that while doing a push or a noop move the automaton does not look at the top symbol of the stack. We will sometimes use an arrow notation for transitions:

s a/x --→ s for δ push (s, a) = (s , x), s a,x --→ s for δ pop (s, a, x) = s , and s a -→ s for δ noop (s, a) = s .
The definitions of a configuration and a run of a strategy automaton are standard. A configuration is a word from QΓ * . The initial configuration is i (the initial state and the empty stack). The transition functions define transitions between configurations, e.g. the transition s a/x --→ s of the automaton gives transitions sv a -→ s xv for all v ∈ Γ * . A run on a word w = w 1 . . . w n is a sequence of configurations: c 0 w1 --→ c 1 w2 --→ . . . wn --→ c n where c 0 = i is the initial configuration. A run is accepting if the state in c n is from F . We write L(A) for the set of words accepted by A.

Since we want to represent sequences that are not necessarily positions, notably interaction sequences, we make the next definition general enough to account for both cases.

Definition 11. Let ρ be a prefix-closed subset of sequences over a set of moves M , and let comp(ρ) be the subset of ρ consisting of non-empty sequences with an equal number of question-and answer-moves 4 . We say that a strategy automaton A is proper for ρ if the following conditions hold.

(A1) L(A) = comp(ρ). (A2) Every run of A corresponds to a sequence from ρ (as A is deterministic each run uniquely specifies the input sequence). (A3) The alphabets M push and M pop consist of third-order questions and answers from M respectively.

A is almost proper for ρ if L(A) = { } ∪ comp(ρ) and (A2) is satisfied.

Remark 2. If A is proper or almost proper for ρ = L(σ) then thanks to (A2) we can then make a number of useful assumptions about its structure.

1. If there is a transition on a P-move from a state, then it is either the unique transition from this state or it is a pop transition and the other transitions are pop transitions on different stack letters. This is because strategies are deterministic and the push and noop moves do not look at the contents of the stack. 2. If the game in question is well-opened, i.e. none of its plays contains two initial moves, then A will never return to the initial state. Otherwise σ would contain just such a play. Hence, we can assume that the initial state does not have any incoming transitions and that it does not have any outgoing pop transitions.

Our first goal will be to model simple terms. The following remark summarizes what needs to be done.

Remark 3. Recall the linear application rule from Section 2. Whenever it is applied when typing β-normal IA * 3 terms we have ord(T ) ≤ 1 and if ord(T ) = 1 then M is cell B , mkvar or a term of the shape f M 1 • • • M k where the order of f 's type is at most 2. Consequently, the corresponding instances of composition are restricted accordingly. To sum up, the following semantic elements are needed to model β-normal simple IA * 3 -terms.

-A strategy for each of the constants.

-Identity strategies id T (ord(T ) ≤ 2).

-Composition of σ : T ⇒ T and τ : T ⇒ T where ord(T ) ≤ 2, ord(T ) ≤ 1 and ord(T ) ≤ 3; moreover, if ord(T ) = 1 then either τ = cell B , or τ = mkvar , or

τ = λx.λΓ.f M 1 • • • M k x .
-A way of modelling contraction up to order 1.

We have not included (un)currying in the list because in the games setting they amount to identities (up to the associativity of the disjoint sum).

The strategies for the constants and identities up to order 1 do not contain thirdorder moves and it is easy to construct finite automata (without stack) which are proper for each of them. The strategy automata for identity strategies at order 2 can be constructed using the † construction (to be introduced shortly) and the equality id A⇒B = id † A id B . Contraction up to order 1 can be interpreted simply by relabelling, so in the remainder of this section we concentrate on composition.

Composition

Let σ : A ⇒ B and τ :

B ⇒ C. Recall that A ⇒ B =!A B and B ⇒ C = !B
C. In order to compose the strategies, one first defines σ † :!A !B by

σ † = { s ∈ L !A !B | for all initial m, s m ∈ σ },
where s m stands for the subsequence of s (pointers included) whose moves are hereditarily justified by m. Then σ; τ : A ⇒ C is taken to be σ † ; lin τ , where ; lin is discussed below. The linear composition σ; lin τ : A C of two strategies σ : A B and τ : B C is defined in the following way. Let u be a sequence of moves from arenas A, B and C with justification pointers from all moves except those initial in C. The set of all such sequences will be denoted by int(A, B, C). Define u B, C to be the subsequence of u consisting of all moves from B and C (pointers between A-moves and B-moves are ignored). u A, B is defined analogously (pointers between B and C are then ignored). Finally, define u A, C to be the subsequence of u consisting of all moves from A and C, but where there was a pointer from a move m A ∈ M A to an initial move m B ∈ M B extend the pointer to the initial move in C which was pointed to from m B . Then given two strategies σ : A B and τ : B C the composite strategy σ; lin τ : A C is defined in two steps:

σ||τ ={ u ∈ int(A, B, C) | u A, B ∈ σ, u B, C ∈ τ }, σ; lin τ ={ u A, C | u ∈ σ||τ }.
Thus in order to carry out the composition of two strategies we will study separately: the dagger construction σ † , interaction sequences σ||τ , and finally the hiding operation leading to σ; lin τ .

Dagger

Recall from Remark 3 that to model β-normal IA * 3 -terms we only need to apply † for B = T where ord(T ) ≤ 1. It is possible to describe precisely what this construction does in this case; we will write q i , a i to refer to any ith-order question and answer from B (i = 0, 1). The definition of σ † describes it as an interleaving of plays in σ but much more can be said about the way the copies of σ are intertwined thanks to the switching conditions, cf. Remark 1, controlling the play on !A !B. For instance, only O will be able to switch between different copies of σ and this can only happen after P plays in B. Consequently, if ord(T ) = 0 (no q 1 , a 1 is available then) a new copy of σ can be started only after P plays a 0 , i.e. when the previous one is completed. Thus σ † in this case consists of iterated copies of σ. If ord(T ) = 1 then a new copy of σ can be started by O each time P plays q 1 or a 0 . An old copy of σ can be revisited with a 1 , which will then answer some unanswered occurrence of q 1 . However, due to the bracketing condition, this will be possible only after all questions played after that q 1 have been answered, i.e. when all copies of σ opened after q 1 are completed. Thus, σ † contains "stacked" copies of σ. Thanks to this we can then characterize K = { } ∪ comp(σ † ) by the (infinite) recursive equation

K = {ε} ∪ {q 0 q 1 Ka 1 . . . q 1 Ka 1 a 0 K : q 0 q 1 a 1 . . . q 1 a 1 a 0 ∈ comp(σ)},
where 's stand for (possibly empty and possibly different) segments of moves from A. Note that q 1 is always followed by a 1 in a position of σ due to switching conditions and the fact that B represents a first-order type.

Lemma 2. Let T = B k → • • • → B 1 → B 0
be a type of order at most 1. If there exists a proper automaton A for σ :! T T then there exists an almost proper automaton A † for σ † . In this automaton the questions and answers from M B k , • • • , M B1 become push and pop letters respectively.

Proof. We will refer to the questions and answers of B 0 by q 0 , a 0 respectively and to those from B i (i > 0) by q 1 and a 1 . Let L = comp(σ) and K = { } ∪ comp(σ † ). Recall that K satisfies the equation given above.

Let i and f be the initial and final states of A respectively. As A is proper for σ, we can assume that there are no transitions to i (Remark 2(2.)). Because A accepts only well-opened plays we can assume that all the transitions to f are of the form s a0 -→ f and there are no transitions from f . In order to define A † we first "merge" f with i or, more precisely, change each transition as above to s a0 -→ i and make i the final state. This produces an automaton accepting L * (observe that L * ⊆ K). Then we make the following additional modifications:

replace s q1 -→ s by s q1/s ---→ i and replace s a1 -→ s by i a1,s ---→ s .
The intuition behind the construction of A † is quite simple. When A † reads q 1 it goes to the initial state and stores the return state s on the stack (the return state is the state A would go to after reading q 1 ). After this A † is ready to process a new copy of K. When finished with this copy it will end up in the state i. From this state it can read a 1 and at the same time the return state from the stack which will let it continue the simulation of A. Consequently, it is not difficult to see that A † satisfies (A2).

Next we argue that A † is deterministic. Because A was, the modifications involving a 0 could not introduce nondeterminism. Those using q 1 and a 1 might, if A happened to have an outgoing noop transition from i on a 1 . However, since ! T T is well-opened, by Remark 2 (2.) we can assume that this is not the case.

Finally, observe that A † currently accepts a superset of K. To be precise, it accepts a word from K iff both a final state is entered and the stack is empty. Thus, in order to accept by final state only, we have to make the automaton aware of whether the stack is empty. The solution is quite simple. The automaton starts with the empty stack. When it wants to put the first symbol onto the stack it actually puts this symbol with a special marker. Now, when popping, the automaton can realize that there is a special marker on the symbol being popped and learn this way that the stack becomes empty. This information will then be recorded in the state. The solution thus requires doubling the number of stack symbols (one normal copy and one marked copy) and doubling the number of states (information whether stack is empty or not is kept in the state).

Note that by (A3) A does not change the stack when reading q 1 and a 1 (which are first-order moves). In A † these letters become push and pop letters respectively.

Interaction sequences: σ † ||τ

The next challenge in modelling composition is to handle the interaction of two strategies. Recall from Remark 3 that in all instances of composition that we need to cover we have B = T , where either ord(T ) = 0 or ord(T ) = 1 and

τ = cell B , mkvar , λx.λΓ.f M 1 • • • M k x .
Lemma 3. Suppose τ :!B C is as above. Let q 1 , a 1 denote any first-order question and answer from B respectively (note that in !B C they are secondorder moves). If τ = cell B , mkvar then, in positions from τ , q 1 is always followed by a 1 and a 1 is always preceded by q 1 . In the remaining case, q 1 will be followed by a third-order question from C and each third-order answer to that question will be followed immediately by a 1 . Lemma 4. Suppose there exist proper automata for σ :!A B and τ :!B C. If τ is as before then there exists a proper automaton A || for σ † ||τ . Moreover, if there is a transition on a B move from a state of A || then it is a noop transition and there is no other transition from that state.

Proof. Let A 1 be the almost proper automaton for σ † :!A !B constructed in Lemma 2 and let A 2 be proper for τ :!B C. We use indices 1 and 2 to distinguish between the components of A 1 and A 2 . The set of states and the stack alphabet of A || will be given by

Q = (Q 1 × Q 2 ) ∪ ({i 1 } × Q 1 × Q 2 ) and Γ = Γ 1 ∪ Γ 2 ∪ (Γ 2 × Q 1 ). i = (i 1 , i 2
) and F = F 1 × F 2 will be respectively the initial state and the set of final states. The alphabet of A || will be partitioned in the following way.

M push = (M 1 push -M B ) ∪ M 2 push M pop = (M 1 pop -M B ) ∪ M 2 pop M noop = M 1 noop ∪ M 2 noop
The definitions are not symmetric because first-order moves from B are push or pop letters for A 1 and noop letters for A 2 . Note that moves from B are in M noop . Finally, we define the transitions of A || in several stages starting from those on A-and C-moves:

(s 1 , s 2 ) m --→ (s 1 , s 2 ) if m ∈ M A and s 1 m --→ s 1 , (s 1 , s 2 ) m --→ (s 1 , s 2 ) if m ∈ M C and s 2 m --→ s 2 .
denotes an arbitrary stack action (push, pop or noop). Intuitively, for the letters considered above A || just simulates the move of the appropriate component.

Next we deal with moves from B. Moves of order 0 are noop letters both for A 1 and A 2 . So, we can simulate the transitions componentwise:

(s 1 , s 2 ) m -→ (s 1 , s 2 ) if s 1 m -→ s 1 , s 2 m -→ s 2 , m ∈ M B and ord B (m) = 0.
First-order moves from B are noop letters in A 2 but push or pop letters in A 1 .

We want them to be noop letters in A || , so we memorize the push operation in the state:

(s 1 , s 2 ) q1 -→ (i 1 , s, s 2 ) if q 1 ∈ M B , ord B (q 1 ) = 1, s 1 q1/s ---→ i 1 and s 2 q1 -→ s 2 , (i 1 , s, s 2 ) a1 -→ (s 1 , s 2 ) if a 1 ∈ M B , ord B (a 1 ) = 1, i 1 a1,s --→ s 1 and s 2 a1 -→ s 2 .
Observe that we know that the transition on q 1 in A 1 is a push transition leading to the initial state i 1 , because A 1 comes from Lemma 2. In order for the construction to work the information recorded in the state has to be exploited by the automaton in future steps. By Lemma 3, q 1 is always followed either by a 1 or by a third-order question from C. The above transitions take care of the first case. In the second case we will arrange for the symbol to be preserved on the stack together with the symbol pushed by the third-order question. Dually, when processing third-order answers we should be ready to process the combined symbols and decompress the information back into the state to be used by the following a 1 . Thus we add the following transitions

(i 1 , s, s 2 ) q3/(X,s) -----→ (i 1 , s 2 ) if q 3 ∈ M C and s 2 q3/X ---→ s 2 , (i 1 , s 2 ) a3,(X,s) -----→ (i 1 , s, s 2 ) if a 3 ∈ M C and s 2 a3,X ---→ s 2 ,
which complete the definition of A || . It is not difficult to verify that A || is proper for σ † ||τ . Note that for each state (s 1 , s 2 ) with an outgoing transition on a Bmove m there is no other transition, because m is always a P -move either for A 1 or for A 2 and we can then appeal to Remark 2 for that automaton.

Rounding up

We are now ready to interpret the linear application rule introduced in Section 2.

Assuming we have proper automata for σ = ∆ N : T : ∆ ⇒ T and τ = λx T .λΓ.M x : T ⇒ ( Γ ⇒ T ) respectively, we would like to find an automaton A lin which is proper for σ † ; lin τ = Γ, ∆ λΓ.M N : Γ → T . To that end it suffices to consider the automaton A || from Lemma 4 and hide the moves from T . Recall that by Lemma 4 if there exists a transition on a move from T from a state of A || then it is a noop transition and no other transitions leave that state. Hence, the automaton for σ † ; lin τ can be obtained by "collapsing" the sequences of T transitions in A || . This can be done by first replacing each transition s 0 m --→ s 1 by s 0 m --→ s k+1 when there is a sequence of transitions in A || of the form:

s 0 m --→ s 1 m1 --→ s 2 m2 --→ . . . m k --→ s k+1
where m is not from T , m 1 , . . . , m k are from T , and s k+1 does not have an outgoing transition on a move from T (note that k is bounded by the number of states in A || ). After this it is enough to remove all the transitions on letters from T . It is easy to see that the resulting automaton A lin is proper for σ † ; lin τ . This completes the description of the construction of automata for simple terms. It remains to calculate the size of the resulting automata. For us the size of an automaton, denoted |A|, will be the sum of the number of states and the number of stack symbols. We ignore the size of the alphabet because it is determined by types present in a sequent and hence is always linear in the size of the sequent. The number of transitions is always bounded by a polynomial in the size of the automaton.

The strategy automata for simple terms have been constructed from automata for base strategies using composition and contraction (λ-abstraction being the identity operation). Contraction does not increase the size of the automaton so it remains to calculate the increase due to composition. Suppose we have two automata A σ and A τ . Let Q σ , Γ σ (Q τ , Γ τ ) stand for the sets of states and stack symbols of A σ (A τ ). Examining the dagger construction we have that

Lemma 5 .

 5 |Q † σ | = 2|Q σ | and |Γ † σ | = 2(|Γ σ | + |Q σ |). For A || we have |Q || | = 2|Q † σ × Q τ | and |Γ || | = |Γ † σ | + |Γ τ | + |Γ τ × Q σ |.Putting the two together and approximating both the number of states and stack symbols with |A σ | and |A τ | we obtain:|Q lin | ≤ 4|A σ ||A τ | and |Γ lin | ≤ 5|A σ ||A τ |. Thus |A lin | ≤ 9|A σ ||A τ |which gives us: For every simple term Γ M : T there exists an automaton which is proper for Γ M : T and whose size is exponential in the size of Γ M : T .

  • • • , max }. Each of the constants corresponds to a different programming feature. For instance, sequential composition of M and N is expressed as seq B M N , assignment of N to M is represented by assignM N and cell B (λx.M ) amounts to creating a local variable x visible in M . Other features can be added in a similar way, e.g. while-loops will be introduced via the constant while : exp → com → com. In order to gain control over multiple occurrences of free identifiers during typing (cf. Definition 9) we shall use a linear form of the application rule and the contraction rule:

PA also has to satisfy a closure condition[START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] which we omit here.

Note that this coincides with the concept of a complete play when ρ = L(σ) for some strategy σ.

Supported by British EPSRC (GR/R88861) and St John's College, Oxford. Supported by the European Community Research Training Network Games.

In this section we address the gap between simple terms and other β-normal IA * 3 -terms. Lemma 6. Any IA * 3 -term Γ M : T in β-normal form can be obtained from a simple term Γ M : T by applications of the contraction rule for second-order identifiers followed by λ-abstractions.

Hence, in order to account for all β-normal terms we only need to show how to interpret contraction at second order, because λ-abstraction is easy to interpret by renaming. As already noted at the end of Section 3, interpreting contraction will require an explicit representation scheme for pointers from third-order moves. Given a position sq 3 ending in a third-order move q 3 let us write α(s) (resp. α(s, q 3 )) for the number of open second-and third-order questions in s (resp. between q 3 and its justifier in s; if the justifier occurs immediately before q 3 then α(s, q 3 ) = 0). Definition 12. Suppose σ = Γ M : T , where Γ M : T is an IA * 3 -term. The languages P(σ) and P (σ) over M Γ T +{ check, hit } are defined as follows:

Note that q 3 is always a P-move, so s uniquely determines q 3 . Clearly, L(σ)∪P(σ) represents σ faithfully in the sense that equality of representations coincides with equality of strategies. The subtlety is that we should compare only complete positions in strategies. This is why we introduce P (σ). Using the results from the previous section, we first show how to construct automata recognizing L(comp(σ)) ∪ P(σ) and L(comp(σ)) ∪ P (σ), where σ denotes a simple term. For this we will need to consider the nondeterministic version of strategy automata defined in the obvious way by allowing transition relations in place of functions.

By Lemma 1, in any position from σ the pointer from a third-order move q 3 points to the unique unanswered enabler visible in the P-view and hence is uniquely determined. Below we give a different characterization of the justifier relative to the whole position rather than to its P-view.

Lemma 7. If sq 3 ∈ Γ M : T , where Γ M : T is simple, and q 3 is a third-order question then q 3 's justifier in sq 3 is the last open enabler of q 3 in s.

Lemma 8. For any simple term Γ M : T let σ = Γ M : T . Then there exist a strategy automaton recognizing L(comp(σ))∪P(σ) and a nondeterministic strategy automaton accepting L(comp(σ)) ∪ P (σ) such that the push and pop letters are respectively questions and answers of order at least 2 and check , hit are pop letters. Their sizes are exponential in the size of Γ M : T . Proof. By Lemma 5 there exists a proper automaton A for L(σ). First we modify A so that second-order questions are pushed on the stack when read and taken off the stack when the corresponding second-order answers are processed. Note that the resulting automaton, let us call it A , still accepts L(comp(σ)), because σ satisfies the bracketing condition. Due to the modification above, the symbols present on the stack during a run of A will correspond exactly to the unanswered second-and third-order questions in the sequence of moves read by the automaton (of course in the case of second-order questions these symbols are the questions themselves).

Next we modify A to recognize L(comp(σ)) ∪ P(σ). We add new transitions so that when the new automaton sees a check letter while being in state s it enters into a special mode. If A could not read a third-order question q 3 from s, the new automaton rejects immediately. Otherwise there is precisely one question q 3 that can be read from s (Remark 2 (1.)). By Lemma 7 it suffices to make the new automaton read check letters and pop the stack as long as the stack symbol is not an enabler of q 3 . When the first one comes, the automaton should read hit and subsequently continue accepting check as long as the stack is not empty.

The construction of a nondeterministic automaton accepting L(comp(σ)) ∪ P (σ) is similar except that while reading check and hit the automaton will need to guess how to extend sq 3 to a complete position accepted by A. For this the automaton uses a pre-calculated table of triples (s 1 , x, s 2 ) such that there is a computation of A from the state s 1 with only x on the stack to the state s 2 with the empty stack. The nondeterministic automaton uses this table during the last phase to guess a possible extension of the computation of A.

As all these modifications increase the size of the automaton only by a linear factor we obtain the complexity bound required by the lemma. Lemma 8 can be extended to all IA * 3 -terms in β-normal form. By Lemma 6, it suffices to be able to interpret λ-abstraction and contraction. Both can now be done by a suitable relabelling. Note that by identifying moves originating from the two distinguished copies of T in the contraction rule we do not lose information about pointers any more, because these are now represented explicitly.

Theorem 2. For any IA * 3 -term Γ M : T in β-normal form there exist a strategy automaton accepting L(comp(σ)) ∪ P(σ) and a nondeterministic strategy automaton accepting L(comp(σ)) ∪ P (σ), where σ = Γ M : T . Their sizes are exponential in the size of the term.

Suppose the strategies σ 1 , σ 2 denote two β-normal IA * 3 -terms. Observe that comp(σ 1 ) ⊆ comp(σ 2 ) is equivalent to L(comp(σ 1 )) ∪ P (σ 1 ) ⊆ L(comp(σ 2 )) ∪ P(σ 2 ). We can verify the containment in the same way as for deterministic finite automata using complementation and intersection. Because the strategy automaton representing the rhs is deterministic, complementation does not incur an exponential increase in size. For intersection we can construct a product automaton in the obvious way because stack operations are determined by the input and, for a given input letter, will be of the same kind in both automata. From this observation and the above theorem we obtain our main result.

Lower bound

We show Exptime-hardness of the equivalence problem for IA * 3 terms in βnormal form. This implies Exptime-hardness of the approximation problem. We use a reduction of the equivalence problem of nondeterministic automata on binary trees [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF].

Labelled binary trees will be represented by positions of the game exp → ((com → com) → com) → com . The sequence of moves S(t) corresponding to a given binary tree t is defined as follows

where x, y range over nullary and binary labels respectively. Observe that S(t) corresponds to a left-to-right depth-first traversal of t. Note that the term λf.f (λx.x; x) defines complete positions of the shape r 0 r 1 U d 1 d 0 where U ::= | r 2 r 3 U d 3 r 3 U d 3 d 2 , i.e. λf.f (λx.x; x) generates all possible sequences of r i , d i (0 ≤ i ≤ 3) corresponding to trees. In order to represent a given tree automaton we can decorate the term with code that asks for node labels and prevents the positions incompatible with trees from developing into complete ones.