A S Murawski

C.-H L Ong

I Walukiewicz

Idealized Algol with Ground Recursion, and DPDA Equivalence

We prove that observational equivalence of IA3 + Y0 (3rdorder Idealized Algol with 0th-order recursion) is equivalent to the DPDA Equivalence Problem, and hence decidable. This completes the classification of decidable fragments of Idealized Algol. We also prove that observational approximation of IA1 + Y0 is undecidable by reducing the DPDA Containment Problem to it.

Introduction

Observational equivalence is an extensional notion of program equivalence. Two program phrases are observationally equivalent if one can be replaced by the other in any program without causing any observable difference to the computational outcome. Reynolds's Idealized Algol (IA) is an elegant and compact programming language that combines imperative programming with high-order features, mediated by a simple type theory. Observational equivalence in IA is in general undecidable even when ground types are finite sets. This paper is concerned with the question of decidability of observational equivalence for appropriate fragments of IA.

We begin with a quick review of IA. Ground types of IA, which are ranged over by β, are exp (expressions), com (commands) and var (assignable variables). Types of IA, ranged over by θ, θ etc., are generated from ground types by the function space constructor θ → θ . The order of a type is defined by ord(β) = 0 and ord(θ → θ ) = max(ord(θ) + 1, ord(θ )). Finitary Idealized Algol, IA f , is just recursion-free Idealized Algol over finite ground types. An IA f -term, Γ M : θ, reference to Figure 2 removed is an ith-order term provided the types of the free identifiers in Γ are of order less than i and ord(θ) ≤ i. The collection of ith-order IA f terms will be denoted by IA i . We can extend IA f with iteration by adding the rule Γ M : exp Γ N : com Γ while M do N : com and with general recursion by adding the rule Γ, x : θ M : θ Γ µx θ .M : θ .

We write IA i + Y j to mean IA i augmented by the collection of ith-order terms j < i removed of the shape Γ µx θ .M : θ where ord(θ) ≤ j. We tabulate all known results on the complexity of observational equivalence of β-normal terms in IA [START_REF] Ong | Observational equivalence of 3rd-order Idealized Algol is decidable[END_REF][START_REF] Murawski | On program equivalence in languages with ground-type references[END_REF][START_REF] Murawski | Games for complexity of second-order call-by-name programs[END_REF][START_REF] Murawski | Third-order Idealized Algol with iteration is decidable[END_REF] The same results as above also hold for observational approximation.

This paper addresses the cases marked with question marks. In IA i + Y 0 only programs of ground type can call themselves recursively. For example, whileloops while b do c can then be defined by b : exp, c : com, z µz com . ifzero b skip (c; z).

We show that observational equivalence in IA i + Y 0 is decidable for i = 1, 2, 3 by giving a reduction to the DPDA Equivalence Problem (recently proved decidable by Sénizergues [START_REF] Sénizergues | L(A)=L(B)? decidability results from complete formal systems[END_REF]). This does not tell much about the complexity, though. At the moment it is only known that the complexity of DPDA Equivalence is bounded by a primitive recursive function [START_REF] Stirling | Deciding DPDA equivalence is primitive recursive[END_REF]. We also show that already for i = 1 observational equivalence is at least as hard as DPDA Equivalence. In consequence, no advance on the complexity of the former problem can be made without an advance on the latter. Another result is that observational approximation in IA i + Y 0 is undecidable for i = 1, 2, 3, because the undecidable DPDA Containment Problem [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF] can be reduced to it.

Let us comment on the relationship of our results to a recent paper [START_REF] Murawski | Third-order Idealized Algol with iteration is decidable[END_REF] showing decidability of IA 3 + while. In that paper a simpler language was considered but it was translated to a weaker form of pushdown automata. This was essential to get a precise complexity bound. In this paper we model a richer language but do not concentrate on complexity, hence our constructions are not designed to optimize the size of the resulting automata. In [START_REF] Murawski | Third-order Idealized Algol with iteration is decidable[END_REF] most constructions relied on parallel composition of automata. This is not possible here as DPDAs are not closed under that operation.

Game semantics: complete plays

We assume familiarity with the treatment of game semantics of IA as presented, for example, in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF]. Recall that the multiplicative composition σ; m τ : A C of two strategies σ : A B and τ : B C is defined by parallel composition with hiding by letting the strategies interact in the shared subgame B and subsequently hiding the B-moves.

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 σ † ; m τ . Given a set σ of positions on G we write L(σ) for the set of the underlying sequences of moves from M G . For a given strategy σ, we write comp σ for the set of its non-empty plays in which the number of questions matches the number of answers; such plays are called complete. Remark 1. We will be interested in the † construction when B = θ and ord(θ) ≤ 1. Then σ † can be characterized explicitly as follows.

-B = β : Then σ † = (comp σ) * σ, i.e. σ † simply iterates σ.

-B = β 1 → β 0 : Then the switching conditions in the game !A !B imply that a new copy of σ can be started each time σ is finished (as above) and, additionally, after each question q 1 from β 1 . We can thus capture K = { } ∪ comp (σ † ) by the equation below.

K = {ε}∪ {q 0 U q 1 Ka 1 U • • • q 1 Ka 1 U a 0 K | q 0 U q 1 a 1 U • • • q 1 a 1 U a 0 ∈ comp σ},
where U 's stand for (possibly empty and possibly different) segments of moves from A.

The operational semantics of IA 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 write M ⇓ if the closed term M reduces to skip. Recall that two terms Γ M 1 , M 2 : θ are observationally equivalent, written

Γ M 1 ∼ = M 2 , if for any context C[-] such that C[M 1 ] and C[M 2 ] are closed terms of type com, we have C[M 1 ]⇓ iff C[M 2 ]⇓. Similarly, M 1 observationally approximates M 2 , written Γ M 1 ∼ M 2 , just if for all contexts satisfying the properties above, C[M 1 ]⇓ implies C[M 2 ]⇓. Theorem 1 ([7]). Γ M 1 ∼ M 2 iff comp Γ M 1 ⊆ comp Γ M 2 . Conse- quently, Γ M 1 ∼ = M 2 iff comp Γ M 1 = comp Γ M 2 .
3 Simple terms and pointer-free representation

Suppose θ = θ 1 → • • • → θ n → β.
Then we write tail (θ) = β. Given Γ M : θ, depending on whether tail (β) is com, exp or var respectively, we define the sets of sequences of moves Γ M : θ by the following decompositions:

L(comp Γ M : θ ) = run • Γ M • done L(comp Γ M : θ ) = q • max j=0 ( Γ M j • j) L(comp Γ M : θ ) = max j=0 write(j) • Γ M w j • ok + read • max j=0 ( Γ M r j • j).
It will turn out convenient to define automata accepting • • • instead of L(comp • • • ), because then it will be not necessary to interpret hiding in many cases (an operation under which DCFLs are not closed in general). Since • • • are sets of sequences of moves, they do not always represent comp • • • faithfully because they ignore pointers. Nevertheless, we are going to identify a sufficiently rich class of terms for which comp • • • can be recovered from • • • .

First, we note that to establish decidability it suffices to consider β-normal terms only. This does not solve the pointer problem though. To address it we replace the application rule with its multiplicative version (left) and contraction (right):

Γ M : θ → θ ∆ N : θ Γ, ∆ M N : θ Γ, x 1 : θ, x 2 : θ M : θ Γ, x : θ M [x/x 1 , x/x 2 ] : θ .
All β-normal terms in IA 3 +Y 0 are typable if we allow the above rules for ord(θ) ≤ 2. We will call a β-normal IA 3 + Y 0 term simple if it can be typed by using the contraction rule only for θ such that ord(θ) < 2. For instance, λf.f (λx.f (λy.x)) is not simple. Note that pointer reconstruction is uniquely defined for all moves except third-order questions (pointers for answers can be reconstructed uniquely thanks to the bracketing condition; first-order moves must point to the unique initial move; finally, because of Visibility, second-order questions must point to the necessarily unique first-order question in the appropriate O-view). As made precise in the lemma below, for simple terms, we can still recover comp

• • • from • • • . Lemma 1. Suppose Γ M : θ is simple. If sq 3 ∈ Γ M : θ ,
and q 3 is a third-order question then q 3 's justifier in sq 3 is the last unanswered enabler of q 3 in s.

Proof. By induction on the structure of simple terms. The crucial point is that if σ : A B satisfies the Lemma for B = θ such that ord(θ) ≤ 1, so does σ † . This follows from the description in Remark 1.

On the other hand, simple terms are good representatives of β-normal terms. Any β-normal term of IA 3 + Y 0 can be typed by extending a typing derivation of a simple term with a number of applications of the contraction rule for θ of order 2 followed by a number of applications of the λ-abstraction rule.

G-automata

We are going to use a variant of deterministic pushdown automata. Their states will be divided into O-states and P-states and the stack will be modified and inspected only during -moves.

-In O-states the automaton will only be able to read an O-move from the input without inspecting or changing the stack; after the transition the state will always change to a P-state. -In P-states the automaton will either: read a single P-move without modifying the stack and move to an O-state, or perform an -move and go to a P-state having a possibility to modify a stack.

qO m 1 O Ô Ô Ù Ù Ù Ù Ù Ù m k O & & S S S S S S qP m P or qP or qP /γ or qP ,γ 1 Ô Ô Ù Ù Ù Ù Ù Ù ,γ k & & S S S S S S q 1 P • • • q k P qO q P q P q 1 P • • • q k P Fig. 1. Transitions in G-automata
The constraints are summarized in Figure 1 and captured formally below.

Definition 1. Let G be a game. A G-automaton A is a tuple Q, Ω, i, F, δ such that -Q = Q O + Q P is the set of states partitioned into Q O and Q P ,
called the sets of O-states and P-states respectively; -Ω is the stack alphabet; -i ∈ Q P is the initial state, i does not have any incoming transitions; -F ⊆ Q P is the set of final states, final states do not have any outgoing transitions;

-δ : [Q O (M O G Q P )]+[Q P (M P G ×Q O )+Q P +(Ω×Q P )+(Ω Q P ) ] is the transition function. The interpretation of a transition δ(q O ) ∈ M O G → Q P is that the automaton reads a letter a ∈ M O
G from the input and changes the state to δ(q O )(a). Similarly for δ(q P ) = (b, q O ) ∈ M P G × Q O , the automaton expects to see b as the input and then changes its state to q O . On a transition δ(q P ) = q P the automaton changes its state but does not consume the input or change the stack. On a transition δ(q P ) = (γ, q P ) the automaton changes the state and pushes γ to the stack. On a transition δ(q P ) ∈ Ω Q P the automaton makes a pop move and changes its state depending on the letter that was popped. We will use arrow notation for transitions as in Figure 1. Note that slash and comma denote push and pop operations, respectively.

We write L(A) for the language that A accepts by final state and the empty stack. It is easy to see that G-automata are DPDAs. They have a particularity that they look at the stack only when doing a pop move. We make this restriction to simplify the definitions that follow. It is not difficult to see that for every deterministic pushdown automaton there is an equivalent one with this property.

By a G-automaton configuration, we mean a pair qw, where q is a state and w ∈ Ω * is the content of the stack. Definition 2. We say that a G-automaton is productive if every non-initial reachable configuration is productive, i.e. the configuration occurs in some accepting run of the automaton. Lemma 2. For every G-automaton there is an equivalent productive automaton. G-added Proof. Let A = Q, Ω, i, F, δ be a G-automaton. Consider the function β : Ω * → P(Q) which for all contents of the stack w ∈ Ω * returns the set of states q such that the configuration qw is productive. We will first modify A so that it keeps the current value of β in its state. Note that it is easy to update β after push-transitions, because β(wa) depends only on β(w) and a: q ∈ β(wa) iff there exists q such that q ∈ β(w) and when A starts with a on the stack in state q it can end up in q with empty stack (states q with this property can be precomputed at the very beginning of the construction). In order to handle poptransitions, we simply force the automaton to push the old value of β in addition to the pushed stack symbol. Finally, it now suffices to suppress all transitions that are not consistent with β to obtain a productive automaton.

Remark 2. (i) The productiveness of the automaton will play an important role in our constructions for several reasons. One is that when A is productive we can be sure that when running as a subautomaton of some automaton construction (as in the proof of Theorem 2), it will only use the symbols it pushed (it cannot try to make a pop operation on the empty stack as that would be an unproductive configuration). Another consequence of productiveness is that the automaton cannot enter an accepting state while the stack is not empty. Indeed, since there are no outgoing transitions from an accepting state, the resulting configuration would not be productive. Further, as the automaton stack is necessarily empty whenever it reaches a final state, we also know that when it finishes the stack will be exactly as before it has started. (ii) From an O-state there are in principle several input letters from M O G that can make the automaton advance. However, because of productiveness, in general, not every playable O-move can label an outgoing transition from the O-state. From a P-state there is only one input letter from M P G that the automaton is prepared to read. We have this asymmetry because Gautomata are designed to accept strategies. Thus, an automaton works in cycles: it reads a letter from M P G , then a letter from M O G and then does some internal manipulations on the stack. Definition 3. We say that an automaton is careful if whenever it reaches a configuration qw after reading the sequence of moves s then the sequence of open second-order questions in s appears in the stack w. More formally, there is a

Γ replaced by Ω function π A : Ω → M G ∪ { } such that π * A (w) is the sequence of open second- π by π * order questions in s.
The final definition of this section makes it precise what kind of automata we want to construct. Below, by A(F ) we will denote the automaton A with F as the set of accepting states.

Definition 4. We say that a tuple of G-automata A 1 , • • • , A n , where each A j = Q j , Ω j , i j , F j , δ j , is fully productive for Γ M : θ just if each A j is productive and careful; further suppose tail (θ) = com: we have n = 1 and L(A 1 ) = Γ M : θ suppose tail (θ) = exp: we have n = 1, F 1 = ⊕ max j=0 F j and L(A 1 (F j )) = Γ M : θ j for any 0 ≤ j ≤ max ; in case tail (θ) = var : we have n = max + 2, F 1 = ⊕ max j=0 F j and L(A 1 (F j )) = Γ M : θ r j for any 0 ≤ j ≤ max ; for each 0 ≤ k ≤ max , we have L(A k+2 ) = Γ M : θ w k .

Modelling simple terms

Here we focus on simple terms. The extension to other β-normal terms is discussed in Section 6.

Theorem 2. For any simple IA 3 + Y 0 term Γ M : θ there exists a fully productive tuple of Γ θ -automata for Γ M : θ.

Proof. We use structural induction. Whenever our constructions fail to preserve productiveness, we simply appeal to Lemma 2 to obtain an equivalent productive automaton.

Thanks to the equalities below and the fact that productive G-automata compose well (see Remark 2 (i))

Γ λx.M = Γ, x M Γ !M j = Γ M r j Γ M ; N = Γ M • Γ N Γ M := N = max j=0 ( Γ N j • Γ M w j ) Γ if M then N 1 else N 2 = Γ M 0 • Γ N 2 + ( max j=1 Γ M j ) • Γ N 1
the corresponding cases are easy. We can simply appeal to the inductive hypothesis and construct the new automata by connecting suitable final states with suitable initial states with -transitions. Note that this does not violate determinism as final states do not have outgoing transitions. Equivalently, one could "glue" final states with initial ones suitably. If one performs the constructions for reachable final states only, productiveness will be preserved. The remaining cases are treated as follows:

The case of Γ new X in M : β. Suppose β = com and A is fully productive for Γ, X : var M : β. Let us construct max + 1 copies of A denoted by A 0 , • • • , A max . We will use superscripts to refer to their states. The unique automaton B in the fully productive tuple for Γ new X in M will consist of all these copies, the idea being that the index of the copy corresponds to the interim value stored in the variable X. The new initial state will be i 0 , i.e. the initial state of A 0 . The set of final states will be H = max h=0 F h , i.e. the set of final states from all the copies A h of A. We make the following changes to the copies of A. Because A is productive, we can assume that each A-transition using the P-moves read X or write(k) X (0 ≤ k ≤ max ) originating from the distinguished copy of var is followed by transitions on i 1 X , • • • , i d X and ok X respectively, where

{ i 1 , • • • , i d } ⊆ { 0, • • • , max }.
To construct B we redirect transitions in the various copies of A as shown below

p h read X p h o h i 1 X i d X 1 1 c c c c → p h i 1 • • • p h i d p h h p h write(k)X p h o h ok X → p h 0 p k 0
where 0 ≤ h ≤ max . These transformations redirect only the transition form p h , while the transitions from o h remain as they were. In the first case the transformation is performed only if h = i c for some 1 ≤ c ≤ d. Otherwise, the transition from p h is just erased. Note that in the second case the new transition connects A h to A k . After all the transitions on P-moves are dealt with, we delete the transitions from o h . It is clear that the B is careful if A is. Using Lemma 2 we can make it productive. If β = exp the same construction can be line break removed performed to give us a fully productive tuple for Γ new X in M . To define the required partition of states H = ⊕ max j=0 H j we simply take H j = max h=0 F h j , where F = ⊕ max j=0 F j is the partition given by the inductive hypothesis. The case of β = var combines the previous two cases.

ditto

The case of Γ µx β .M : β. Suppose β = com and A is a fully productive tuple for Γ, x : β M : β, where A = Q, Ω, i, F, δ . The unique automaton B in the fully productive tuple for Γ µx.M will be constructed from two copies A 0 , A 1 of A. Intuitively, A 1 will be used to process recursive calls from M , whereas A 0 will correspond to the base copy of M . Accordingly, the initial state will be i 0 and the final states will be those from F 0 . The stack alphabet of B will, in addition to the stack alphabet of A, contain two copies of the set of O-states of A. By productiveness of A, we can assume that each transition on run x is followed by a transition on done x . In order to define B, for each h = 0, 1 and for each block of the shape p h run x ---→ o h donex ----→ p h done we erase the transition from p h and add the transitions:

p h /o h ---→ i 1 and f 1 ,o h --→ p h done for any f ∈ F . inlined
The case of β = exp is similar but, additionally, we have to pass on the result of ditto the recursive call. The notion of a productive tuple will make that easy. Suppose F = ⊕ max j=0 F j . Then we first create two copies A 0 , A 1 of A and for h = 0, 1 and for each block

p h qx o h i 1 x i d x 1 1 c c c c p h i 1 • • • p h i d
we erase the transition from p h and add the transitions:

p h /o h ---→ i 1 and f 1 i c ,o h --→ inlined p h i c for any 1 ≤ c ≤ d and f i c ∈ F i c .
The initial state of the new automaton is i 0 , the final states are those in F 0 = ⊕ max j=0 F 0 j . The remaining case of β = var is more no line break tedious but completely analogous to the previous two. Given a fully productive tuple A 1 , • • • , A max +2 for Γ, x M , blocks write(j) x ok x are replaced with calls to A j+2 as for com, while blocks read x j x are replaced by calls to A 1 . It is easy to see that the obtained automaton is careful. After the above constructions we can apply Lemma 2 to make the resulting automaton productive.

The case of f M 1 • • • M k .
For demonstration we assume that k = 1, M 1 = M and f M : com and f does not occur in M , i.e. f : θ → com, Γ f M : com. Let us write r f , d f and r, d for the com -moves on the left and right respectively. Observe that because f M is interpreted by interaction of the identity strategy (cor-

responding to f ) with ( Γ M ) † we have comp f : θ → com, Γ f M : com = inlined r r f ({ } ∪ L) d f d, where L = φ(comp Γ M : θ † )
and φ is the (injective) renaming map which acts like identity on moves from Γ and maps θ -moves to their copies in θ → com . Below we examine two representative examples in detail and give the precise shape of φ. We use subscripts to refer to (moves from) various copies of com.

-Suppose Γ M : com 0 and f :

com f,1 → com f , Γ f M : com. Then L = comp Γ M † [r 0 → r f,1 , d 0 → d f,1 ]. -Suppose Γ M : com 1 → com 0 and f : (com f,2 → com f,1 ) → com f , Γ f M : com. Then L = comp Γ M † [r 0 → r f,1 , d 0 → d f,1 , r 1 → r f,2 , d 1 → d f,2 ].
Consequently, the main difficulty is the construction of an automaton accepting comp (σ † ) ∪ { }, where σ = Γ M : θ and ord(θ) ≤ 1. What is constructed in the following is not a Γ θ -automaton (the initial state, which is an O-state, will coincide with the final one and it will have both incoming and outgoing transitions), but the crucial fact is that it becomes one when the transitions on r f and d f (which will become the new initial and final moves respectively) are added. We consider the case of θ = com 1 → com 0 for illustration.

Suppose A is fully productive for Γ M : θ, A = Q, Ω, i, F, δ and ord(θ) ≤ 1. Recall from Remark 1 that in this case † iterates as well as stacks copies of the original strategy and a new copy can start either if the previous one finished or after r 1 . To model that, we create two copies A 0 , A 1 of A with the aim of delegating the copies started after r 1 to A 1 . The outermost iterated copies will be processed by A 0 .

First we define a few new states: i 0 new (which will be the initial and final state of the automaton) and (•, q), (•, q), where q ∈ Q 0 + Q 1 + { i 0 new }. We make the following additions to A 0 , A 1 :

-i 0 new r0 -→ (•, i 0 new ) /(i 0 new ,r0) -------→ i 0 and f 0 ,(i 0 new ,r0) -------→ (•, i 0 new ) d0 -→ i 0 new for any f ∈ F .
-Observe that r 1 is always followed by d 1 in σ. By productiveness of A, we can assume that each transition p h r1 -→ o h (h = 0, 1) is followed by

o h d1 -→ p h 0 . Then we add o h r0 -→ (•, o h ) /(o h ,r0)
------→ i 1 . This makes it possible for the automaton to start processing a new copy of σ, the return state is saved on the stack. To process call returns, we add

f 1 ,(o h ,r0) -----→ (•, o h ) d0 -→ o h for any f ∈ F .
Note that in addition to return addresses in the form of O-states we have also arranged for the questions r 0 to be pushed on the stack. They will remain there as long as they are not answered in the corresponding position. These questions are redundant for accepting comp (σ † ) ∪ { }, but are necessary for the resulting automaton to be careful. Since r 0 will be substituted by r f,1 , the questions r 0 are exactly the second-order questions contributed by f . The case of f M 1 • • • M k is analogous, except that we need to apply † to k i=1 Γ M i .

The contraction rule. The contraction rule for free identifiers of type θ, where ord(θ) = 0, 1, is interpreted simply by identifying moves from the two copies of θ . In general this might lead to nondeterminism, but thanks to the structure of our automata this can never happen in our case. There is no problem with P-moves as from each P-state the automaton can read at most one letter. Suppose that a nondeterminism arises from some O-state reachable from the initial configuration. This means that there exists a position s such that the automaton can read both s o 1 and s o 2 , where o 1 and o 2 are the O-moves from two different copies of θ. However, this contradicts that fact that at most one of s o 1 and s o 2 can satisfy Visibility (because only one first-order question is O-visible in s).

Consequently, contraction can be interpreted without loss of determinacy.

Representing pointers

We are going to introduce a representation of pointers for simple terms by following Lemma 1. Consider a position sq 3 , where q 3 is a third-order question.

We define π(s, q 3 ) = k -j + 2 where q j 2 is the last enabler of q 3 in the sequence q 1 2 , • • • , q k 2 of all second-order unanswered questions in s (written in the order they appear in s). Definition 5. Suppose σ = Γ M : θ , where Γ M : θ is an IA 3 + Y 0 term. The language P(σ) over the alphabet M Γ θ + { check } is defined by P(σ) = { s check π(s,q3) | sq 3 s ∈ comp σ for some s }. Lemma 3. For any simple term Γ M : θ there exists a DPDA accepting L(comp σ) ∪ P(σ), where σ = Γ M : θ . Proof. By Theorem 2 there is a fully productive tuple for Γ M : θ. By adding transitions on the missing initial and final moves, we can construct an automaton A accepting L(comp σ). Though A is not, strictly speaking, a G-automaton, it is nonetheless a DPDA that is productive and careful. (The definitions of productive and careful do carry over in this case.) Next, we will construct a DPDA accepting L(comp σ) ∪ P(σ). Suppose that the automaton A reads the sequence sq 3 where q 3 is a third-order question. Note that q 3 is always a P-move, so it is uniquely determined by s and σ. As A is productive, we know that sq 3 can be extended to a complete position. It remains to take care of check letters. As A is careful, all second-order questions that are open in sq 3 will be stored on the stack. Hence, in order to accept the right number of check 's after reading s, the automaton can move to a fresh state (reading the letter check ) and enter a new mode in which it will repeatedly pop the stack reading check whenever the topmost stack symbol contains a second-order question and otherwise. It accepts exactly after it encounters the first enabler of q 3 . Now that we can represent the semantics of simple terms with pointers, the semantics of other β-normal terms can be obtained by renaming, because in order to type such terms we only need to perform contraction at order 2 and λ-abstraction. The former is done by relabelling (in the same manner as at order 0 or 1; the previous argument that determinism is preserved remains valid), the latter amounts to identity in the games setting. Consequently, we get: Theorem 3. For any IA 3 + Y 0 term Γ M : θ in β-normal form there exists a DPDA accepting L(comp σ) ∪ P(σ), where σ = Γ M : θ . Hence, the theorem also holds for any IA 3 + Y 0 term.

By Lemma 1, L(comp σ) ∪ P(σ) is a faithful representation of comp σ. Thus, by Theorem 3 and the decidability of DPDA equivalence [START_REF] Sénizergues | L(A)=L(B)? decidability results from complete formal systems[END_REF], we get Theorem 4. Observational equivalence is decidable for terms in IA 3 + Y 0 .

Hardness

A DPDA [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF] is a tuple B = Q, Σ, Γ, δ, q 0 , Z 0 , where δ : Q × (Σ ∪ { }) × Γ Q × Γ * . Additionally, whenever δ(q, a, X) is defined for some a ∈ Σ, δ(q, , X) must be undefined. We consider acceptance by empty stack (initially the stack contains Z 0 ) and write N (B) for the language accepted by B. For simplicity, we further assume that B can either pop the stack or push one symbol onto it, i.e. if δ(q, a, X) = (q , α) then α = or α = α 0 α 1 (α 0 , α 1 ∈ Γ ) and α 0 = X. Any DPDA can be easily converted into this form.

We identify values of type exp with Σ. Consider the game G = exp ⇒ com so that we have Proof. Push transitions are simulated by recursive calls, pop moves by call returns. Before each call, the symbol to be pushed is stored in the variable TOP which is used to initialize the local copy of X after the call. Take M B to be x : exp new Q := q 0 , TOP := Z 0 , CH in µz com . new POP := 0, X := !TOP in while (not !POP) do (if δ(!Q, , !X) = (q , α) then (Q := q ; if α = then POP := 1 else ((TOP := α 1 ); z)) else (CH := x; if δ(!Q, !CH , !X) = (q , α) then (Q := q ; if α = then POP := 1 else ((TOP := α 1 ); z)) else Ω com )) : com Observe that the term used in Lemma 4 is from IA 1 +Y 0 . Since the Containment Problem for DPDAs is undecidable [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF] we have: Corollary 1. Observational approximation is undecidable for IA 1 + Y 0 terms; observational equivalence is at least as hard as DPDA Equivalence.

M G = { q } ∪ Σ ∪ { r, d }. Given L ⊆ Σ * define L ⊆ M * G by L = { rqx 1 • • • qx n d | x 1 • • • x n ∈ L }. Note that L 1 = L 2 iff L 1 = L 2 .
Our results complete the classification of decidable and undecidable fragments section header removed of IA. The exact complexity of observational equivalence for β-normal terms is known in most cases, as shown in the table in Section 1. The complexity of IA i + Y 0 depends on the complexity of DPDA Equivalence, which is not known at present. Our construction, when suitably optimized, yields DPDAs that are doubly exponentially larger than the given term in β-normal form. It is also not yet understood how the presence of β-redexes affects the complexity.

Lemma 4 .

 4 For any DPDA B there exists a term x : exp M B : com such that L(comp x : exp M B : com ) = N (B).

Proposition 1 .

 1 For any DPDAsB 1 , B 2 we have N (B 1 ) ⊆ N (B 2 ) iff M B1 ∼ M B2 .

Figure 2 .

 2 Figure 2. erased

Work supported by the UK EPSRC (GR/R88861/01), the European Research Training Network GAMES and St John's College, Oxford.


Teodor Knapik
email: knapik@univ--nc.nc

Damian Niwiński
email: niwinski@mimuw.edu.pl

⋆ Pawe L Urzyczyn

⋆⋆ Igor Walukiewicz

Unsafe Grammars and Panic Automata

We show that the problem of checking if an infinite tree generated by a higher-order grammar of level 2 (hyperalgebraic) satisfies a given µ-calculus formula (or, equivalently, if it is accepted by an alternating parity automaton) is decidable, actually 2-Exptime-complete. Consequently, the monadic second-order theory of any hyperalgebraic tree is decidable, so that the safety restriction can be removed from our previous decidability result. The last result has been independently obtained by Aehlig, de Miranda and Ong. Our proof goes via a characterization of possibly unsafe second-order grammars by a new variant of higher-order pushdown automata, which we call panic automata. In addition to the standard pop 1 and pop 2 operations, these automata have an option of a destructive move called panic. The model-checking problem is then reduced to the problem of deciding the winner in a parity game over a suitable 2nd order pushdown system.

Introduction

Context-free tree grammars constitute the basic level in an infinite hierarchy of higher-order grammars introduced by W. Damm [START_REF] Damm | The IO-and OI-hierarchies[END_REF] (built on the earlier ideas of [START_REF] Engelfriet | [END_REF]). Courcelle [START_REF] Courcelle | The monadic second-order theory of graphs IX: Machines and their behaviours[END_REF] proved decidability of the monadic second-order (MSO) theory of any tree generated by an algebraic (context-free) tree grammar. Later Knapik et al [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF][START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] attempted to extend this decidability result to all levels of the Damm hierarchy. This has been achieved partially, namely with an additional syntactic restriction imposed on the grammars, called safety: the MSO theory of any tree generated by a safe grammar of level n is decidable.

Higher-order grammars can be seen as program schemes, where functions can take higher-order arguments. The tree generated by such a grammar describes completely the semantics of the program scheme. Thus decidability of the MSO theory of such a tree implies decidability for a large class of properties of behaviours of higher-order program schemes.

The safety requirement, roughly speaking, prevents the use of individual parameters in the functional arguments of higher-order functions. The concept of safe (tree) grammars has been further justified by a characterization in terms of higher-order pushdown automata originally introduced by Maslov [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF]: the trees generated by safe higher-order grammars of level n coincide with the trees recognized (in suitable sense) by pushdown automata of level n [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF]. See [START_REF] Caucal | On infinite terms having a decidable monadic second-order theory[END_REF][START_REF] Courcelle | The evaluation of if first-order substitution is monadic second-order compatible Theoretical[END_REF] for another characterization of this hierarchy.

Monadic second-order logic is extremely succinct, which yields the nonelementary complexity of the MSO theories, even for regular trees. However, over trees, the MSO logic has the same expressive power as the µ-calculus, which is much better tractable algorithmically. Cachat [START_REF] Cachat | Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games[END_REF] showed that the modelchecking problem for the µ-calculus and the trees recognized by the pushdown automata of level n is in n-Exptime, actually n-Exptime-complete [?, 5].

In this paper we show that for the level 2 (hyperalgebraic), the model checking problem remains decidable, actually 2-Exptime-complete, also for grammars without safety restriction.

To this end, we first find an automata-theoretic counterpart of unsafe hyperalgebraic grammars, which is an extension of second-order pushdown automata by a new destructive operation that we call panic. This operation allows us to simulate the change of environment needed to evaluate parameters of unsafe productions. We further introduce 2nd order pushdown systems with panic (equipped with alternation and ranks), which can be viewed as a generalization of pushdown systems studied in [START_REF] Walukiewicz | Pushdown processes: Games and model checking[END_REF][START_REF] Cachat | Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games[END_REF]. The model-checking problem then reduces to the problem of deciding the winner in a parity game over such a system. The key step is a reduction of this game to a game over a 2nd order pushdown system without panic, for which a 2-Exptime procedure is already known [START_REF] Cachat | Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games[END_REF].

An immediate consequence of our result is that the model checking problem for the hyperalgebraic grammars is decidable also for the monadic second-order logic, consequently the MSO theory of any hyperalgebraic tree is decidable. This result has been recently independently obtained by Aehlig, de Miranda and Ong [START_REF] Aehlig | The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable[END_REF] 4 , by a different proof, based on transformations of infinite lambda terms. Compared to [START_REF] Aehlig | The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable[END_REF], the present paper has two new elements: (1) it gives a characterization of unsafe grammars by panic automata, (2) the actual proof yields an optimal decision procedure for the µ-calculus model checking.

At present we do not know if the safety requirement really restricts the generating power of the tree grammars. Recently, Aehlig, de Miranda and Ong have studied the safety restriction [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF]. They have shown that it is inessential for the word grammars of level 2, where a grammar, as usual, can generate a set of words. To simulate a non-safe grammar by a safe one, they use nondeterminism in an essential way, hence their result is not directly applicable here.

Due to space limitations, many arguments are omitted or sketchy; they will appear in the full paper (see [START_REF] Knapik | Unsafe grammars and panic automata[END_REF] for a preliminary version).

Trees

Types, terms, and trees. We fix the set of simple types τ constructed from a unique basic type 0, by the rules τ ::= 0 | (τ 1 → τ 2 ). The level of a type is defined by ℓ(0) = 0, and ℓ(τ 1 → τ 2 ) = max(1 + ℓ(τ 1 ), ℓ(τ 2 )). Thus 0 is the only type of level 0 and each type of level 1 is of the form 0 n → 0 for some n > 0 (which abbreviates (0 → (0 → (• • • (0 → 0) . . .))), with n + 1 occurrences of 0).

A typed alphabet is a set Γ of symbols, each γ in Γ given with its type, γ : τ . We inductively extend Γ to the set T (Γ ) of (applicative) terms over Γ ; if t : τ 1 → τ 2 and s : τ 1 then (ts) : τ 2 . As usual we abbreviate ( The set of natural numbers is denoted by ω. A tree (over a set X) is any nonempty prefix-closed subset T of the free monoid X * , with ε as the root. If u ∈ T , x ∈ X, and ux ∈ T then ux is a successor of u in T . Now let Σ be a signature, i.e., a typed alphabet of symbols of level ≤ 1. A Σ-tree is a mapping t : dom t → Σ, where dom t ⊆ ω * is a tree, and if t(w) is a symbol of type 0 k → 0 then w has exactly k successors, w1, . . . , wk (hence w is a leaf if t(w) : 0). The set of Σ-trees is written T ∞ (Σ). A limit of a sequence t 0 , t 1 , . . . of Σ-trees is defined, provided that for any k, there is m = m(k), such that t n ↾k and t n ′ ↾k coincide, for all n, n ′ ≥ m(k) (where, in general, t↾k is restriction of t to the set {w ∈ dom t : |w| ≤ k}). Then lim t n ∈ T ∞ (Σ) is just the set-theoretical union of the functions t n ↾m(n).

Grammars. We fix an infinite typed alphabet of variables (or parameters), X . A grammar is a tuple G = (Σ, N, S, E), where Σ is a signature, N is a finite typed alphabet set of nonterminals5 , S ∈ N is a start symbol of type 0, and E is a set of productions of the form

Fz 1 . . . z m ⇒ w where F : τ 1 → τ 2 • • • → τ m → 0 is a nonterminal, z i a
variable of type τ i , and w an applicative term in T (Σ ∪ N ∪ {z 1 . . . z m }) of type 0. The level of a grammar is the highest level of its nonterminals. Since we are interested in grammars as generators of (single) Σ-trees, we assume that for each F, there is exactly one production with F on the left hand side.

The single-step reduction relation → G between terms over Σ ∪ N is defined inductively by the following clauses.

1.

Ft 1 . . . t k → G t[z 1 :=t 1 , . . . , z k :=t k ] if there is a production Fz 1 . . . z k ⇒ t (with z i : ρ i , i = 1, . . . , k), and t i ∈ T (Σ ∪ N ) ρi , for i = 1, . . . , k. 2. If t → G t ′ then (st) → G (st ′ ) and (tq) → G (t ′ q)
, whenever the expressions in question are applicative terms.

That is, t → G t ′ whenever t ′ is obtained from t by replacing some occurrence of a nonterminal F by the right-hand side of the appropriate production in which all parameters are in turn replaced by the actual arguments of F .

In order to define the result of an infinite derivation, we extend Σ to Σ ⊥ = Σ ∪ {⊥}, with ⊥ : 0. With any term t over Σ ∪ N , we inductively associate a term t ⊥ over Σ ⊥ , by setting

f ⊥ = f (for f ∈ Σ), X ⊥ = ⊥ (for X ∈ N ), and (st) ⊥ = (s ⊥ r ⊥ ) whenever s ⊥ = ⊥, otherwise (st) ⊥ = ⊥. Then, we define relation t ։ ∞ G t ′ , where t is a term in T (Σ ∪ N ) and t ′ a tree in T ∞ (Σ ⊥ ), by
t ′ is finite, and there is reduction sequence

t = t 0 → G . . . → G t n = t ′ , or -t ′ is infinite, and there is an infinite reduction sequence t = t 0 → G t 1 → G . . . such that t ′ = lim t ⊥ n .
To define a unique tree produced by the grammar, we recall a standard approximation ordering on T ∞ (Σ ⊥ ): t ′ ⊑ t if dom t ′ ⊆ dom t and, for each w ∈ dom t ′ , t ′ (w) = t(w) or t ′ (w) = ⊥. Then the tree generated by G is defined by

[[G]] = sup{t ∈ T ∞ (Σ ⊥ ) : S ։ ∞ G t}
It is easy to see that, by the Church-Rosser property of our grammar, the above set is directed, and hence [[G]] is well defined since T ∞ (Σ ⊥ ) with the approximation ordering is a cpo.

In this paper we only study grammars of level 2, which we call hyperalgebraic, as they constitute the next level above the algebraic (context-free) grammars.

Parity games. A parity game is a perfect information game of possibly infinite duration played by two players, say Eve and Adam. We present it as a tuple (V ∃ , V ∀ , E, p 1 , Ω), where V ∃ and V ∀ are (disjoint) sets of positions of Eve and Adam, respectively, E ⊆ V × V is the relation of possible moves, with V = V ∃ ∪ V ∀ , p 1 ∈ V is a designated initial position, and Ω : V → ω is the ranking function.

The players start a play in the position p 1 and then move the token according to relation E (always to a successor of the current position), thus forming a path in the graph (V, E). The move is selected by Eve or Adam, depending on who is the owner of the current position. If a player cannot move, she/he looses. Otherwise, the result of the play is an infinite path in the graph, v 0 , v 1 , v 2 , . . .. Eve wins the play if lim sup n→∞ Ω(v n ), is even, otherwise Adam wins.

Parity games, introduced by Emerson and Jutla [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF][START_REF] Mostowski | Games with forbidden positions[END_REF], have been recognized as a combinatorial essence of many model checking problems. A crucial property is the positional determinacy: any position is winning for one of the players, and moreover a winning strategy of player θ can be made positional , i.e., represented by a (partial) function σ : V θ → V . 6 We say simply that Eve wins the game G if she has a winning strategy, the similar for Adam. We refer the reader to [START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games. A Guide to Current Research[END_REF] for an introduction to parity games.

Model checking. The model checking problem in our consideration is to verify if the tree generated by a given grammar G satisfies a property ϕ expressed in some logical language, in symbols [[G]] |= ϕ. The most expressive logics considered in literature are the monadic second-order logic (MSO) or the µ-calculus; both have the same expressive power over Σ-trees [START_REF] Niwiński | Fixed points characterization of infinite behaviour of finite state systems[END_REF]. In this paper we avoid a logical machinery by using an equivalent formalism of alternating parity automata (defined below). A polynomial-time translation from the µ-calculus to alternating automata, ϕ → A ϕ , is known [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF], such that, for any tree t, t |= ϕ iff t is recognized by A ϕ .

An alternating parity tree automaton over signature Σ can be presented as a tuple

B = Σ, Q ∃ , Q ∀ , q 1 , δ, Ω where Q ∃ ∪ Q ∀ = Q is a
finite set of states with the initial state q 1 , Ω : Q → ω is a ranking function, and δ is a set of transitions of the form q → f (q 1 , . . . , q k ), where q, q 1 , . . . , q k ∈ Q and f ∈ Σ with type f :

0 k → 0.
The acceptance of a tree t ∈ T ∞ (Σ) by the automaton B can be presented by a suitable parity game. We first define a the computation tree, r : dom r → Q with dom r ⊆ (ω × ω) * , such that, for any u ∈ dom r, the projection π 1 (u) on the first component is a node in dom t. We let r(ǫ) = q 1 , and whenever r(u) = q and t(π 1 (u)) = f , then, for any transition of the form q → f (q 1 , . . . , q k ), the node u has a successor u(i, j) with r(u(i, j)) = q i , for some j, and i = 1, . . . , k. Now consider a parity game Game(B, t) with V = dom r partitioned such that u ∈ V ∃ iff r(u) ∈ Q ∃ , the initial configuration ε, and Ω(u) = Ω(r(u)). We let B accept the tree t iff Eva wins this game.

The model checking problem addressed in this paper will be the following.

Panic automata

Classically the content of a pushdown store is just a word over the pushdown alphabet. For our purpose, it is convenient to consider pushdown symbols with "time stamps" (sort of). We let a level 1 pushdown store (or a 1-pds or 1-stack) over an alphabet Γ be a non-empty word a 1 . . . a l over Γ × ω. A level 2 pds (2-pds, 2-stack) is a non-empty sequence s 1 . . . s l of 1-pds's, which may also be written as

[s 1 ][s 2 ] . . . [s l ] or as s ′ [s l ], where s ′ stands for [s 1 ][s 2 ] . . . [s l-1 ]
. The 1-stack s i is called the i-th row of s. We assume that push-down stores grows to the right, so that, for instance, the item (a, m) is on top of the 2-pds s ′ [w(a, m)]. By top(s) we denote the topmost Γ -symbol of s, i.e., top(s ′ [w(a, m)]) = a.

The following operations are possible on level 2 push-down stores.

push 1 a ([s 1 ][s 2 ] . . . [s l ][w]) = [s 1 ][s 2 ] . . . [s l ][w(a, l)] pop 1 (α[wξ]) = α[w] push 2 (α[w]) = α[w][w] pop 2 (α[v][w]) = α[v] panic([s 1 ][s 2 ] . . . [s m ] . . . [s l ][w(a, m)]) = [s 1 ][s 2 ] . . . [s m ] skip(s) = s
The operation pop 2 (resp. pop 1 ) is undefined on a 2-stack s if it contains only one row (resp. the top row of s has only one element).

Let ⊥ be a symbol in Γ . It is easy to see that if a 2-pds [s 1 ] . . . [s m ] is generated from [(⊥, 0)] by the above operations, and s i = (a i,1 , m i,1 ) . . . (a i,ki , m i,ki ) then m i,j ≤ i -1, and j ≤ j ′ follows m i,j ≤ m i,j ′ . Intuitively, whenever a new symbol a ∈ Γ is placed on the top of the stack, the second component registers number of the stack row which is directly below the current top row. Later the symbol can be duplicated several times by subsequent executions of push 2 , but the second component keeps record of the level when it first appeared in the stack. The panic operation returns to the 2-stack previous to the first appearance of the actual top symbol. Now let Σ be a signature, and let Σ r ⊆ Σ be the set of symbols of type 0 r → 0. A panic automaton is defined as a tuple

A = Σ, Q, Γ, q 1 , δ, ⊥ ,
where Q is a finite set of states, with an initial state q 1 , Γ is a stack alphabet, with a distinguished bottom symbol ⊥, and δ : Q×Γ → I is a transition function, where I is the set of possible instructions,

I ⊆ Op Γ × Q ∪ r Σ r × Q r ,
where Op Γ = {push 1 a : a ∈ Γ } ∪ {pop 1 , push 2 , pop 2 , panic, skip}.

A configuration of an automaton A as above is a pair (q, s), where q ∈ Q, and s is a 2-stack (over Γ ). The initial configuration is (q 1 , [(⊥, 0)]). We define the relation → A on configurations as follows. Let s

= [s 1 ] . . . [s l ][w(a, m)].
1. If δ(q, a) = (α, q ′ ) with α ∈ Op Γ then q, s → A q ′ , α(s) . 2. If δ(q, a) = (f, p 1 , . . . , p r ) then q, s → A p i , s , for all i = 1, . . . , r.

In the first case we write •

A instead of → A . The symbol → → A stands for the reflexive and transitive closure of → A , and similarly for → → • A . Let t : dom t → Σ be a Σ-tree. A partial run of A on t is a partial function ̺ from an initial segment of dom t to the set of all configurations, such that if ̺(w) = q, s , for some w ∈ dom t, then δ(q, a) = (f, p 1 , . . . , p r ), where f = t(w) and a = top(s). In addition p i , s → → • A ̺(wi), for each i = 1, . . . , r when ̺(wi) is defined.

If a partial run is a total function over dom t, we call it a run. As our automaton is deterministic, there can be at most one tree over which A has a run. This is the tree accepted by A.

3 Automata vs grammars Theorem 3.1. For any panic automaton A, one can construct a hyperalgebraic grammar G A , such that if the automaton recognizes a tree t in T

∞ (Σ) then t = [[G A ]].
Conversely, for a hyperalgebraic grammar G, one can construct a panic automaton A G such that if the grammars generates a tree in T ∞ (Σ), this is the (unique) tree recognized by A G . Both constructions can be realized in polynomial time.

Here we only sketch the direction G → A G , which is essential for the upper bound result.

Let • 1 , • 2 , . . . be fresh identifiers of type 0, which we call holes. The pushdown alphabet Γ of A G consists of subterms of the right hand sides of the productions of G, possibly applied to some holes, so that the result is of type 0. More precisely, let u = F t 1 . . . t d be such a subterm, where F is an operator (variable or nonterminal) of type

τ 1 → • • • → τ d → 0 k → 0. Then u • 1 . . . • k ∈ Γ .
In particular, if u : 0 then simply u ∈ Γ .

The holes • 1 , . . . , • k represent "missing arguments" of the operator F . Since holes are new identifiers, one can safely identify

F t 1 . . . t d • 1 . . . • k with F t 1 . . . t d if this is convenient.
The idea of our simulation is that the top of pds (an expression u) represents a variable-free expression u ′ occurring in a derivation of G. Since the pds alphabet must be finite, the term u can only be an "approximation" of u ′ . This approximation is "evaluated" to yield an approximate representation of the next step of reduction. The contents of the pds represents an environment in which the evaluation takes place. The environment is searched if one needs to find the meaning of a variable, or to find a missing argument.

The bottom pds symbol is S, the initial nonterminal. This is our approximation in the first step of reduction. The automaton then works in phases, each phase beginning and ending in the distinguished state q 1 . We define automaton informally, by describing the possible behaviour in a phase, beginning with a configuration (q 1 , s).

T1 Let top(s) = Fu 1 . . . u n , where F is a nonterminal, and let the corresponding production be Fx 1 . . . x n ⇒ u. The automaton executes the instruction δ(q 1 , Fu 1 . . . u n ) = (push 1 u , q 1 ), so that our next approximation is u.

T2 If top(s) = f t 1 . . . t r
where f is a terminal, then the the automaton executes the instruction δ(q 1 , f t 1 . . . t r ) = (f, p 1 , . . . , p r ), followed (at the i-th branch of the run) by a pop 1 and push 1 t i . Thus the next approximation at the i-th branch is t i . (If f is a constant, there is no further step.) T3 Let top(s) = x, where x is an (ordinary) variable of type 0. To "evaluate"

x, the automaton restores the environment where x was defined. It executes pop 1 and inspects the new top symbol. It should be of the form Ft 1 . . . t e , where F is a nonterminal. In addition, the variable x should be one of the formal parameters of F, say, the j-th one. The next approximation is t j , and it should be evaluated in the present environment (that of the caller).

Another pop 1 is now executed, followed by a push 1 t j , and the machine returns to state q 1 . T4 Let top(s) = ϕu 1 . . . u h where ϕ is a variable of type 0 h → 0. If we now executed a pop 1 as above then the information about the actual parameters u 1 , . . . , u h would be lost. Instead, a push 2 is executed, followed by a pop 1 . As in the previous case the top of the stack should be of the form Ft 1 . . . t e and ϕ should be one of the formal parameters of F, say, the j-th one. However now the new approximant t j is an expression of a functional type and we place t j • 1 . . • h on the pds rather than t j . T5 The last case is when top(s) is a hole, say • i . The automaton gets now into panic. After the panic move the top of the pds should be ψv 1 . . . v l for some variable ψ. The new approximation is v i . We execute in order pop 1 and push 1 v i and return to state q 1 .

To explain the last case let us first observe that holes (missing arguments) are created when we attempt to evaluate a function variable (the fourth case). Holes correspond to the arguments (actual parameters) of this function variable that were "left behind" for a while. Later, a hole is found at top of the pds when we need to evaluate such a missing argument of an operator. In order to do so, we must restore the situation from the time of the call. The crucial thing is that the "time stamp" of the topmost item points out to exactly the moment in the past we need, namely to the stage when the hole was created.

Pushdown systems

By now, we have considered panic automata as tree acceptors, with the aim to characterize hyperalgebraic grammars. For the model-checking applications, it is convenient to use a related concept of pushdown systems which do not take inputs, but are equipped with ranks and alternation (c.f. [START_REF] Cachat | Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games[END_REF][START_REF] Walukiewicz | Pushdown processes: Games and model checking[END_REF]).

A 2nd order pushdown system with panic (or 2-PPDS, for short) is a tuple C = (P, P ∃ , P ∀ , Γ, p 1 , ∆, Ω) where P is a finite set of control locations partitioned into P ∃ and P ∀ , Γ is a finite store alphabet, p 1 ∈ P is the initial location, Ω : P → ω is the rank function, and ∆ ⊆ P × Γ × P × Op Γ is the finite set of (unlabeled) transition rules (where Op Γ is as in Sect. 2). A transition (p, a, p ′ , α) ∈ ∆ is often written by p, a → ∆ p ′ , α.

A configuration of a 2-PPDS C is a pair (p, s) where p ∈ P and s is a 2-stack over Γ . A 2-PPDS C gives rise to a parity game Game(C) = (V ∃ , V ∀ , E, (p 1 , [⊥, 0]), Ω), where -V ∃ the set of configurations of C with a location from P ∃ , similarly for V

∀ ; -(p, s)E(p ′ , s ′ ) iff ∃(p, a, p ′ , α) ∈ ∆, top(s) = a and s ′ = α(s); -Ω(p, s) = Ω(p). -If p, a → ∆ p ′ , pop 2 then p, (a, R) → ∆ ′ p ′ , pop 2 ; pop 1 , for all R ∈ Ret. -If p, a → ∆ p ′ , panic then p, (a, R) → ∆ ′ ⊤, skip if Rank (a)
R(p ′ ), and we have p, (a, R) → ∆ ′ ⊥, skip otherwise, i.e., when Rank (a) ≺ R(p ′ ) or R(p ′ ) is undefined.

-There are no transitions from states ⊤ and ⊥. This implies that Eve wins in ⊤ and loses in ⊥.

Proposition 5.6. Eve wins in Game(C ′ ) iff she wins in Game(C).

Proof: (Idea) Together with the mechanism of returns, this allows them to transfer the strategies from Game(C) to Game(C ′ ).

⊓ ⊔

We are now ready to state our main result.

Theorem 5.7. The problem of checking if Eva wins Game(C), for a given 2nd order pushdown system with panic C, is 2-Exptime-complete (Problem 2). Consequently, so is the problem of checking if an alternating parity tree automaton B accepts the tree [[G]] generated by an hyperalgebraic grammar G (Problem 1).

Proof: The 2-Exptime hardness result follows from Lemma 5.5, and Proposition 4.2. To show the upper bound, let C be a 2-PPDS. By Lemma 4.4 we can assume that C is rank-aware. To solve Game(C) we construct a 2-PDS C ′ (without panic), as in Proposition 5.6. The system C ′ has the number of stack letters which is exponential in the size of C, but the number of locations of C ′ is linear in the number of locations of C. By the first part of Lemma 5.5, the winner in the game Game(C ′ ) can be decided in time doubly exponential in the number of states and singly exponential in the number of stack symbols, which gives us the desired complexity.

⊓ ⊔

By the relation between automata, µ-calculus, and monadic logic (c.f. section 1), we obtain the following.

Corollary 5.8. It is 2-Exptime-complete to check if [[G]] |= ϕ, for a given 2nd order grammar G, and a given µ-calculus formula ϕ. Consequently, the analogous problem for the monadic second-order logic (MSO) is decidable, in particular the MSO theory of any hyperalgebraic tree is decidable.

Problem 1

 1 Given a 2nd order grammar G and an alternating parity tree automaton B. Does B accept [[G]] ?

  • • • ((t 0 t 1 )t 2 ) • • • )t n by t 0 t 1 . . . t n . For terms t, t 1 , . . . , t m , and symbols z 1 , . . . , z m , of appropriate types, term t[z 1 :=t 1 , . . . , z k :=t k ] results from simultaneous replacement in t of z i by t i .

  The construction guarantees that a 2-pds in a reachable configuration ofC ′ has a form v = [w 1 R 1 ] . . . [w k R k ][w k+1 ], where w i ∈ (Γ × Ret) * and R i ∈ Ret. We say that v represents a 2-pds s = [s 1 ] . . . [s k+1 ] of C if, for all i, s i ↓ 1 = w i ↓ 1 , and if s i ↓ 2 = ℓ then w i ↓ 2 = R ℓ .Note that a possibly infinite domain of "time stamps" (in C) is represented here by the finite set Ret. Both players can ensure that the 2-stacks reachable in Game(C ′ ) represent the 2-stacks of C.

C.f. the joint message of the authors to the TYPES Forum[START_REF] Aehlig | Paper announcements: MSO theory of hyperalgebraic trees is decidable[END_REF].

Without loss of generality, we assume that the types of nonterminals are homogeneous, i.e., 0 or τ1 → • • • → τn → 0, where if each τi is homogeneous and ℓ(τ1) ≥ ℓ(τ2) ≥ . . . ≥ ℓ(τn).

Positional strategy σ is winning for θ if every play p1 = q1, q2, . . . is won by θ, provided that q ℓ ∈ V ∃ follows q ℓ+1 = σ(q ℓ ).

The single exponential dependence on |Γ | is not made explicit in these references, but it follows from the analysis of level 1 pushdown systems in[START_REF] Walukiewicz | Pushdown processes: Games and model checking[END_REF].

Notation like p, a → ∆ ′ p ′ , α1; α2 clearly abbreviates two rules.

⋆ Partly supported by KBN Grant 4 T11C 042 25. ⋆⋆ Partly supported by KBN Grant 3 T11C 002 27. ⋆ ⋆ ⋆ The 2nd and the 4th author were also supported by the EC Research Training Network Games.

Problem 2. Given a 2-PPDS C, decide if Eva wins the game Game(C). Proof: (Sketch) By Theorem 3.1, we reduce Problem 1 to the question if a tree recognized by a panic automaton A is accepted by an alternating tree automaton B. Then a suitable 2-PPDS C is obtained by a standard product construction, such that Eve wins Game(C) if and only if she wins Game(B, t A )

The converse transformation of Problem 2 to Problem 1 is also easy, after introduction of a suitable functional signature Σ (depending on the 2-PPDS C).

⊓ ⊔

Before proceeding to proof of our main result, we show a useful transformation of 2-PPDS's, which will allow us to control the dynamics of ranks by the topmost symbols on the pushdown store.

Let Tr (C) be the tree obtained by unfolding the graph of Game(C). That is, the root of Tr (C) is by the initial configuration, and a node labeled by (p, s) has a successor labeled (p ′ , s ′ ), whenever (p, s)E(p ′ , s ′ ). Note that a node of the tree determines a computation up to this node. Definition 4.3 Let a node v of Tr (C) be labeled with q, s such that panic(s) is defined. Let v ′ be the closest to v ancestor of v labeled with q ′ , panic(s) , for some q ′ . We call v ′ the panic ancestor of v. The panic rank of v is the maximal rank of a state occurring between the panic ancestor of v and v, including the rank of v and excluding the rank of the panic ancestor of v.

A 2-PPDS C is rank-aware iff there exists a function Rank : Γ → Rg(Ω) such that the panic rank of every node v of Tr (C) labeled (q, s) is equal to Rank (top(s)). That is, the panic rank is determined by the top of the stack. Proof: (Idea) The stack alphabet of C ′ is defined as Γ ′ = Γ ×{0, . . . , d} 2 , where d is the highest rank in Rg(Ω). The construction ensures that if (a, m p , m l ) is currently on top of the stack, then m p is the panic rank of the node, and m l is the highest rank of a state seen since the creation of the current top row.

The construction of transitions of C ′ goes naturally case by case. The correctness proof is straightforward, but tedious.

⊓ ⊔

Deciding the winner in Game(C)

A 2nd order pushdown system (or 2-PDS, for short) is like a 2-PPDS defined in section 4, but without panic, that is, ∆ ⊆ P × Γ × P × (Op Γ -{panic}). Then a level 1 pushdown store can be viewed just as a word over Γ (not Γ × ω). The concepts of 2-pds, configuration, and Game(C) are simplified accordingly. Games over such pushdown systems have been considered by Engelfriet [START_REF] Engelfriet | Iterated push-down automata and complexity classes[END_REF], Cachat [START_REF] Cachat | Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games[END_REF], and others. Lemma 5.5 ([11, 4, 5]). It is decidable if Eve wins Game(C) for a given 2ndorder pushdown system C = (P, P ∃ , P ∀ , Γ, p 1 , ∆, Ω). There is an algorithm working in time 7 2 |Γ |2 O(|P |) , and the problem is 2-Exptime-complete.

We now transform a rank-aware 2nd order pushdown system with panic C = (P, P ∃ , P ∀ , Γ, p 1 , ∆, Ω) into a 2nd order pushdown system without panic C ′ = (P ′ , P ′ ∃ , P ′ ∀ , Γ ′ , p ′ 1 , ∆ ′ , Ω ′ ), such that Eve wins Game(C) iff she wins Game(C ′ ). For technical convenience, we assume that a transition p, a → ∆ p ′ , α with α = skip is possible only for p ∈ P ∃ . Clearly, we can always achieve this property by duplicating locations and using skip operation.

Let Rank : Γ → Rg(Ω) = {0, . . . , d} be the function of Definition 4.3. We introduce an ordering on ranks: n iff (-1) m • m ≤ (-1) n • n (e.g., for d = 6, this yields an ordering 5, 3, 1, 0, 2, 4, 6).

We define the set of returns as

The intention is that a partial function R ∈ Ret assigns to a location p the worst, in -order, panic rank still acceptable for the panic moves ending in position p. We let

The rank function Ω ′ is 0 for all the locations except for Ω ′ (p) = Ω(p), Ω ′ (p rank =i ) = i; for all p ∈ P .

The transition rules ∆ ′ are defined by the following clauses.

-If p, a → ∆ p ′ , skip then p, (a, R) → ∆ ′ p ′ , skip, for all R ∈ Ret.

-If p, a → ∆ p ′ , push 1 a then p, (a, R) → ∆ ′ p ′ ver , push 1 (a ′ , R ′ ) , for all R, R ′ ∈ Ret. Additionally we have p ′ ver , (a ′ , R ′ ) → ∆ ′ ver , skip, and p ′ ver , (a ′ , R ′ ) → ∆ ′ p ′ , skip.

-From the location ver the moves are defined in such a way that Eve wins iff R in the top letter of the top-most 1-stack is the same as R at the top of 1-stack just below the top-most 1-stack. -If p, a → ∆ p ′ , push 2 then p, (a, R) → ∆ ′ p ′ push , push 1 R ′ , for all R, R ′ ∈ Ret. Additionally we put in ∆ ′ the rules 8 p ′ push , R ′ → ∆ ′ p ′ , push 2 ; pop 1 , as well as p ′ push , R ′ → ∆ ′ p ′′ rank =R ′ (p ′′ ) , pop 1 , and p ′′ rank =R ′ (p ′′ ) , (a, R) → ∆ ′ p ′′ , skip, for all p ′′ such that R ′ (p ′′ ) is defined.

-If p, a → ∆ p ′ , pop 1 then p, (a, R) → ∆ ′ p ′ , pop 1 , for all R ∈ Ret.