Domains for HigherOrder GamesMatthew Hague and Roland Meyer and Sebastian MuskallaRoyal Holloway University of London and TU Braunschweig and TU Braunschweig 
Abstract: We study twoplayer inclusion games played over wordgenerating higherorder recursion schemes. While inclusion checks are known to capture verification problems, twoplayer games generalize this relationship to program synthesis. In such games, nonterminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words.We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixedpoint techniques, a direct algorithm for the analysis of twoplayer inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for orderk recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixedpoint computations can be applied.
Inclusion checking has recently received considerable attention [55, 23, 1, 2, 37]. One of the reasons is a new verification loop, which invokes inclusion as a subroutine in an iterative fashion. The loop has been proposed by Podelski et al. for the safety verification of recursive programs [33], and then been generalized to parallel and parameterized programs [43, 21, 19] and to liveness [20]. The idea of Podelski’s loop is to iteratively approximate unsound data flow in the program of interest, and add the approximations to the specification. Consider a program with controlflow language CF that is supposed to satisfy a safety specification given by a regular language R. If the check CF⊆ R succeeds, then the program is correct as the data flow only restricts the set of computations. If a computation w∈ CF is found that lies outside R, then it depends on the data flow whether the program is correct. If data is handled correctly, w is a counterexample to R. Otherwise, w is generalized to a regular language S of infeasible computations. We set R = R ∪ S and repeat the procedure.
Podelski’s loop has also been generalized to synthesis [36, 45]. In that setting, the program is assumed to have two kinds of nondeterminism. Some of the nondeterministic transitions are understood to be controlled by the environment. They provide inputs that the system has to react to, and are also referred to as demonic nondeterminism. In contrast, the socalled angelic nondeterminism are the alternatives of the system to react to an input. The synthesis problem is to devise a controller that resolves the angelic nondeterminism in a way that a given safety specification is met. Technically, the synthesis problem corresponds to a twoplayer perfect information game, and the controller implements a winning strategy for the system player. When generalizing Podelski’s loop to the synthesis problem, the inclusion check thus amounts to solving a strategysynthesis problem.
Our motivation is to synthesize functional programs with Podelski’s loop. We assume the program to be given as a nondeterministic higherorder recursion scheme where the nonterminals are assigned to two players. One player is the system player who tries to enforce the derivation of words that belong to a given regular language. The other player is the environment, trying to derive a word outside the language. The use of the corresponding strategysynthesis algorithm in Podelski’s loop comes with three characteristics: (1) The algorithm is invoked iteratively, (2) the program is large and the specification is small, and (3) the specification is nondeterministic. The first point means that the strategy synthesis should not rely on costly precomputation. Moreover, it should have the chance to terminate early. The second says that the cost of the computation should depend on the size of the specification, not on the size of the program. Computations on the program, in particular iterative ones, should be avoided. Together with the third characteristic, these two consequences rule out reductions to reachability games. The required determinization would mean a costly precomputation, and the reduction to reachability would mean a product with the program. This discussion in particular forbids a reduction of the strategysynthesis problem to higherorder model checking [47], which indeed can be achieved (see the full version [29] for a comparison to intersection types [42]). Instead, we need a strategy synthesis that can directly deal with nondeterministic specifications.
We show that the winning region of a higherorder inclusion game w.r.t. a nondeterministic righthand side can be computed with a standard fixedpoint iteration. Our contribution is a domain suitable for this computation. The key idea is to use Boolean formulas whose atomic propositions are the states of the targeted finite automaton. While a formulabased domain has recently been proposed for contextfree inclusion games [36] (and generalized to infinite words [45]), the generalization to higherorder is new. Consider a nonterminal that is ground and for which we have computed a formula. The Boolean structure reflects the alternation among the players in the plays that start from this nonterminal. The words generated along the plays are abstracted to sets of states from which these words can be accepted. Determining the winner of the game is done by evaluating the formula when sets of states containing the initial state are assigned the value true. To our surprise, the above domain did not give the optimal complexity. Instead, it was possible to further optimize it by resolving the determinization information. Intuitively, the existential player can also resolve the nondeterminism captured by a set. Crucially, our approach handles the nondeterminism of the specification inside the analysis, without preprocessing.
Besides offering the characteristics that are needed for Podelski’s loop, our development also contributes to the research program of effective denotational semantics, as recently proposed by Salvati and Walukiewicz [53] as well as Grellois and Melliès [25, 25], with [5, 50] being early works in this field. The idea is to solve verification problems by computing the semantics of a program in a suitable domain. Salvati and Walukiewicz studied the expressiveness of greatest fixedpoint semantics and their correspondence to automata [53], and constructions of enriched Scott models for parity conditions [52, 51]. A similar line of investigation has been followed in recent work by Grellois and Melliès [26, 27]. Hofmann and Chen considered the verification of more restricted ωpath properties with a focus on the domain [34]. They show that explicit automata constructions can be avoided and give a domain that directly captures subsets (socalled patches) of the ωlanguage. The work has been generalized to higher order [35]. Our contribution is related in that we focus on the domain (suitable for capturing plays).
Besides the domain, the correctness proof may be of interest. We employ an exact fixedpoint transfer result as known from abstract interpretation. First, we give a semantic characterization showing that the winning region can be captured by an infinite model (a greatest fixed point). This domain has as elements (potentially infinite) sets of (finite) Boolean formulas. The formulas capture plays (up to a certain depth) and the atomic propositions are terminal words. The infinite set structure is to avoid infinite syntax. Then we employ the exact fixedpoint transfer result to replace the terminals by states and get rid of the sets. The final step is another exact fixedpoint transfer that justifies the optimization. We give a matching lower bound. The problem is (k+1)EXPcomplete for orderk schemes.
The relationship between recursion schemes and extensions of pushdown automata has been well studied [16, 17, 38, 30]. This means algorithms for recursion schemes can be transferred to extensions of pushdown automata and vice versa. In the sequel, we will use pushdown automata to refer to pushdown automata and their family of extensions.
The decidability of Monadic Second Order Logic (MSO) over trees generated by recursion schemes was first settled in the restricted case of safe schemes by Knapik et al. [38] and independently by Caucal [14]. This result was generalized to all schemes by Ong [47]. Both of these results consider deterministic schemes only.
Related results have also been obtained in the consideration of games played over the configuration graphs of pushdown automata [54, 13, 39, 30]. Of particular interest are saturation methods for pushdown games [7, 22, 12, 8, 31, 32, 9]. In these works, automata representing sets of winning configurations are constructed using fixedpoint computations.
A related approach pioneered by Kobayashi et al. operating directly on schemes is that of intersection types [41, 42], where types embedding a property automaton are assigned to terms of a scheme. Recently, saturation techniques were transferred to intersection types by Broadbent and Kobayashi [10]. The typing algorithm is then a least fixedpoint computation analogous to an optimized version of our Kleene iteration, restricted to deterministic schemes. This has led to one of the most competitive modelchecking tools for schemes [40].
One may reduce our language inclusion problems to many of the above works. E.g. from an inclusion game for schemes, we may build a game over an equivalent kind of pushdown automaton and take the product with a determinization of the NFA. This obtains a reachability game over a pushdown automaton that can be solved by any of the above methods. However, such constructions are undesirable for iterative invocations as in Podelski’s loop.
We already discussed the relationship to modeltheoretic verification algorithms. Abstract interpretation has also been used by Ramsay [49], Salvati and Walukiewicz [52, 51], and Grellois and Melliès [25, 24] for verification. The former used a Galois connection between safety properties (concrete) and equivalence classes of intersection types (abstract) to recreate decidability results known in the literature. The latter two strands gives a semantics capable of computing properties expressed in MSO. Indeed, abstract interpretation has long been used for static analysis of higherorder programs [4].
Let (D, ≤) be a partial order with set D and (partial) ordering ≤ on D. We call (D, ≤) pointed if there is a greatest element, called the top element and denoted by ⊤ ∈ D. A descending chain in D is a sequence (d_{i})_{i ∈ N} of elements in D with d_{i} ≥ d_{i+1}. We call (D, ≤) ωcomplete if every descending chain has a greatest lower bound, called the meet or the infimum, and denoted by ⊓_{i ∈ N} d_{i}. If (D, ≤) is pointed and ωcomplete, we call it a pointed ωcomplete partial order (cppo). In the following, we will only consider partial orders that are cppos. Note, cppo is usually used to refer to the dual concept, i.e. partial orders with a least element and least upper bounds for ascending chains.
A function f : D → D is ⊓continuous if for all descending chains (d_{i})_{i ∈ N} we have f(⊓_{i ∈ N} d_{i}) = ⊓_{i ∈ N} f(d_{i}). We call a function f : D → D monotonic if for all d, d′ ∈ D, d ≤ d′ implies f(d) ≤ f(d′). Any function that is ⊓continuous is also monotonic. For a monotonic function, ⊤ ≥ f(⊤) ≥ f^{2} (⊤) = f(f(⊤)) ≥ f^{3} (⊤) ≥ … is a descending chain. If the function is ⊓continuous, then ⊓_{i ∈ N} f^{i} (⊤) is by Kleene’s theorem the greatest fixed point of f, i.e. f(⊓_{i ∈ N} f^{i} (⊤)) = ⊓_{i ∈ N} f^{i} (⊤) and ⊓_{i ∈ N} f^{i} (⊤) is larger than any other element d with f(d) = d. We also say ⊓_{i ∈ N} f^{i} (⊤) is the greatest solution to the equation x = f(x).
A lattice satisfies the descending chain condition (DCC) if every descending chain has to be stationary at some point. In this case ⊓_{i ∈ N} f^{i} (⊤) = ⊓_{i = 0}^{i0} f^{i} (⊤) for some index i_{0} in N. With this, we can compute the greatest fixed point: Starting with ⊤, we iteratively apply f until the result does not change. This process is called Kleene iteration. Note that finite cppos, i.e. with finitely many elements in D, trivially satisfy the descending chain condition.
A nondeterministic finite automaton (NFA) is a tuple A = (Q_{NFA}, Γ, δ, q_{0}, Q_{f}) where Q_{NFA} is a finite set of states, Γ is a finite alphabet, δ ⊆ Q_{NFA} × Γ × Q_{NFA} is a (nondeterministic) transition relation, q_{0} ∈ Q_{NFA} is the initial state, and Q_{f} ⊆ Q_{NFA} is a set of final states. We write q –[a]→ q′ to denote (q, a, q′) ∈ δ. Moreover, given a word w = a_{1}⋯ a_{ℓ}, we write q –[w]→ q′ whenever there is a sequence of transitions, also called run, q_{1} –[a_{1}]→ q_{2} –[a_{2}]→ ⋯ –[a_{ℓ}]→ q_{ℓ+1} with q_{1} = q and q_{ℓ+1} = q′. The run is accepting if q = q_{0} and q′ ∈ Q_{f}. The language of A is L(A) = {w  q_{0} –[w]→ q ∈ Q_{f}} .
We introduce higherorder recursion schemes, schemes for short, following the presentation in [28]. Schemes can be understood as grammars generating the computation trees of programs in a functional language. As is common in functional languages, we need a typing discipline. To avoid confusion with typebased approaches to higherorder model checking [41, 48, 42], we refer to types as kinds. Kinds define the functionality of terms, without specifying the data domain. Technically, the only data domain is the ground kind o, from which (potentially higherorder) function kinds are derived by composition:
κ ::= o ∣ ( κ_{1} → κ_{2} ) . 
We usually omit the brackets and assume that the arrow associates to the right. The number of arguments to a kind is called the arity. The order defines the functionality of the arguments: A firstorder kind defines functions that act on values, a secondorder kind functions that expect functions as parameters. Formally, we have
 = 0, 
 = 0,  




Let Κ be the set of all kinds. Higherorder recursion schemes assign kinds to symbols from different alphabets, namely nonterminals, terminals, and variables. Let Γ be a set of such kinded symbols. For each kind κ, we denote by Γ^{κ} the restriction of Γ to the symbols with kind κ. The terms T^{κ}(Γ) of kind κ over Γ are defined by simultaneous induction over all kinds. They form the smallest set satisfying
If term t is of kind κ, we also write t ∶ κ. We use T(Γ) for the set of all terms over Γ. We say a term is λfree if it contains no subterm of the form λ x . t. A term is variableclosed if all occurring variables are bound by a preceding λexpression.
The semantics of G is defined by rewriting subterms according to the rules in R. A context is a term C[•] ∈ T (Γ ⨃ { • ∶ o }) in which • occurs exactly once. Given a context C[•] and a term t:o, we obtain C[t] by replacing the unique occurrence of • in C[•] by t. With this, t ⇒_{G} t′ if there is a context C[•], a rule F = λ x_{1} … λ x_{n}.e, and a term F t_{1} … t_{n}:o such that t = C[F t_{1} … t_{n}] and t′ = C[e[x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}]]. In other words, we replace one occurrence of F in t by a righthand side of a rewriting rule, while properly instantiating the variables. We call such a replaceable F t_{1} … t_{n} a reducible expression (redex). The rewriting step is outermost to innermost (OI) if there is no redex that contains the rewritten one as a proper subterm. The OIlanguage L(G) of G is the set of all (finite, ranked, labeled) trees T over the terminal symbols that can be created from the initial symbol S via OIrewriting steps. We will restrict the rewriting relation to OIrewritings in the rest of this paper. Note, all words derivable by IOrewriting are also derivable with OIrewriting.
We consider wordgenerating schemes, i.e. schemes with terminals T⨃ {$:o} where exactly one terminal symbol $ has kind o and all others are of kind o→ o. The generated trees have the shape a_{1} (a_{2} (⋯ (a_{k} $))), which we understand as the finite word a_{1} a_{2} … a_{k} ∈ T^{*}. We also see L(G) as a language of finite words.
The above schemes are nondeterministic in that several rules may rewrite a nonterminal. We associate with a nondeterministic scheme G=(V, N, T, R, S) a deterministic scheme G^{det} with exactly one rule per nonterminal. Intuitively, G^{det} makes the nondeterminism explicit with new terminal symbols.
Formally, let F:κ be a nonterminal with rules F= t_{1} to F= t_{ℓ}. We may assume each t_{i} = λ x_{1} … λ x_{k}. e_{i}, where e_{i} is λfree. We introduce a new terminal symbol op_{F}: o → o → … → o of arity ℓ. Let the set of all these terminals be T^{det}={op_{F}  F∈ N}. The set of rules R^{det} now consists of a single rule for each nonterminal, namely F= λ x_{1} … λ x_{k}. op_{F} e_{1} ⋯ e_{ℓ}. The original rules in R are removed. This yields G^{det}=(V, N, T⨃ T^{det}, R^{det}, S). The advantage of resolving the nondeterminism explicitly is that we can give a semantics to nondeterministic choices that depends on the nonterminal instead of having to treat nondeterminism uniformly.
Let G=(V, N, T, R, S) be a deterministic scheme. A model of G is a pair M=(D, I), where D is a family of domains (D(κ))_{κ∈Κ} that satisfies the following: D(o) is a cppo and D(κ_{1}→ κ_{2})=Cont(D(κ_{1}), D(κ_{2})). Here, Cont(A, B) is the set of all ⊓continuous functions from domain A to B. We comment on this cppo in a moment. The interpretation I: T→ D assigns to each terminal s:κ an element I(s)∈D(κ).
The ordering on functions is defined componentwise, f ≤_{κ1 → κ2} g if (f x) ≤_{κ2} (g x) for all x∈D(κ_{1}). For each κ, we denote the top element of D(κ) by ⊤_{κ}. For the ground kind, ⊤_{o} exists since D(κ) is a cppo, and ⊤_{κ1 → κ2} is the function that maps every argument to ⊤_{κ2}. The meet of a descending chain of functions (f_{i})_{i ∈ N} is the function defined by (⊓_{κ1 → κ2} (f_{i})_{i ∈ N}) x = ⊓_{κ2} (f_{i} x)_{i ∈ N}. Note that the sequence on the righthand side is a descending chain. The semantics of terms defined by a model is a function
M〚−〛:T→ (N⨃ V↛ D)→D . 
that assigns to each term built over the nonterminals and terminals again a function. This function expects a valuation ν:N⨃ V↛ D and returns an element from the domain. A valuation is a partial function that is defined on all nonterminals and the free variables. We lift ⊓ to descending chains of valuations with (⊓_{i ∈ N} ν_{i})(y) = ⊓_{i ∈ N} (ν_{i}(y)) for y ∈ N ⨃ V. We obtain that the set of such valuations is a cppo where the greatest elements are those valuations which assign the greatest elements of the appropriate domain to all arguments.
Since the righthand sides of the rules in the scheme are variableclosed, we do not need a variable valuation for them. We need the variable valuation, however, whenever we proceed by induction on the structure of terms. The semantics is defined by such an induction:

We show that M〚t〛 is ⊓continuous for all terms t. This follows from continuity of the functions in the domain, but requires some care when handling application.
Given M, the rules F_{1}=t_{1},…, F_{k}=t_{k} of the (deterministic) scheme give a function
rhs_{M} : (N → D) → (N → D) , where rhs_{M}(ν)(F_{j}) = M〚t_{j}〛 ν . 
Since the righthand sides are variableclosed, the M〚t_{j}〛 are functions in the nonterminals. Provided M〚t_{1}〛 to M〚t_{k}〛 are ⊓continuous (in the valuation of the nonterminals), the function rhs_{M} will be ⊓continuous. This allows us to apply Kleene iteration as follows. The initial value is the greatest element σ_{M}^{0} where σ_{M}^{0}(F_{j}) = ⊤_{j} with ⊤_{j} the top element of D(κ_{j}). The (i+1)^{th} approximant is computed by evaluating the righthand side at the i^{th} solution, σ_{M}^{i+1} = rhs_{M}(σ_{M}^{i}). The greatest fixed point is the tuple σ_{M} defined below. It can be understood as the greatest solution to the equation ν = rhs_{M}(ν). We call this greatest solution σ_{M} the semantics of the scheme in the model.
σ_{M} = ⊓_{i ∈ N} σ_{M}^{i} = ⊓_{i ∈ N} rhs_{M}^{i} (σ_{M}^{0}) 
Our goal is to solve higherorder games, whose arena is defined by a scheme. We assume that the derivation process is controlled by two players. To this end, we divide the nonterminals of a wordgenerating scheme into those owned by the existential player ◇ and those owned by the universal player □. Whenever a nonterminal is to be replaced during the derivation, it is the owner who chooses which rule to apply. The winning condition is given by an automaton A, Player ◇ attempts to produce a word that is in L(A), while Player □ attempts to produce a word outside of L(A).
A play of the game is a sequence of OIrewriting steps. Since terms generate words, it is unambiguous which term forms the next redex to be rewritten. In particular, all terms are of the form a_{1} ( a_{2} ( ⋯ (a_{k} (t) ) ) ), where t is either $ or a redex F t_{1} ⋯ t_{m}. If O(F) = ◇ then Player ◇ chooses a rule F = λ x_{1} … λ x_{m} . e to apply, else Player □ chooses the rule. This moves the play to a_{1} (a_{2} (⋯ (a_{k} e[x_{1} ↦ t_{1}, …, x_{m} ↦ t_{m}]))).
Each play begins at the initial nonterminal S, and continues either ad infinitum or until a term a_{1} (a_{2} (⋯ (a_{k} $))), understood as the word w=a_{1}… a_{k}, is produced. Infinite plays do not produce a word and are won by Player ◇. Finite maximal plays produce such a word w. Player ◇ wins whenever w ∈ L(A), Player □ wins if w ∈ L(A). Since the winning condition is Borel, either Player ◇ or Player □ has a winning strategy [44].
Our contribution is a fixedpoint algorithm to decide HOG. We derive it in three steps. First, we develop a concrete model for higherorder games whose semantics captures the above winning condition. Second, we introduce a framework that for two models and a mapping between them guarantees that the mapping of the greatest fixed point with respect to the one model is the greatest fixed point with respect to the other model. Finally, we introduce an abstract model that uses a finite ground domain. The solution of HOG can be read off from the semantics in the abstract model, which in turn can be computed via Kleene iteration. Moreover, this semantics can be used to define Player ◇’s winning strategy. We instantiate the framework for the concrete and abstract model to prove the soundness of the algorithm.
Consider a HOG instance G = (G, A, O). Let G^{det} be the determinized version of G. Our goal is to define a model M^{C} = (D^{C}, I^{C}) such that the semantics of G^{det} in this model allows us to decide HOG. Recall that we only have to define the ground domain. For composed kinds, we use the functional lifting discussed in Section 3.
Our idea is to associate to kind o the set of positive Boolean formulas where the atomic propositions are words in T^{∗}. To be able to reuse the definition, we define formula domains in more generality as follows.
Given a (potentially infinite) set P of atomic propositions, the positive Boolean formulas PBool(P) over P are defined to contain true, every p from P, and compositions of formulas via conjunction and disjunction. We work up to logical equivalence, which means we treat φ_{1} and φ_{2} as equal as long as they are logically equivalent.
Unfortunately, if the set P is infinite, PBool(P) is not a cppo, because the meet of a descending chain of formulas might not be a finite formula. The idea of our domain is to have conjunctions of infinitely many formulas. As is common in logic, we represent them as infinite sets. Therefore, we consider the set of all sets of (finite) positive Boolean formulas P(PBool(T^{*}))∖{∅} factorized modulo logical equivalence, denoted (P(PBool(T^{*}))∖{∅}) /_{⇔}. To be precise, the sets may be finite or infinite, but they must be nonempty.
To define the factorization, let an assignment to the atomic propositions be given by a subset of P′ ⊆ P. The atomic proposition p is true if p ∈ P′. An assignment satisfies a Boolean formula, if the formula evaluates to true in that assignment. It satisfies a set of Boolean formulas, if it satisfies all elements. Given two sets of formulas Φ_{1} and Φ_{2}, we write Φ_{1}⇒ Φ_{2}, if every assignment that satisfies Φ_{1} also satisfies Φ_{2}. Two sets of formulas are equivalent, denoted Φ_{1}⇔ Φ_{2}, if Φ_{1}⇒ Φ_{2} and Φ_{2}⇒ Φ_{1} holds. The ordering on these factorized sets is implication (which by transitivity is independent of the representative). The top element is the set {true}, which is implied by every set. The conjunction of two sets is union. Note that it forms the meet in the partial order, and moreover note that meets over arbitrary sets exist, in particular the domain is a cppo. We will also need an operation of disjunction, which is defined by Φ_{1}∨ Φ_{2} = {φ_{1}∨ φ_{2}  φ_{1}∈ Φ_{1}, φ_{2}∈ Φ_{2}}. We will also use disjunctions of higher (but finite) arity where convenient. Note that the disjunction on finite formulas is guaranteed to result in a finite formula. Therefore, the above is welldefined.
In our case, the assignment P′ ⊆ T^{*} of interest is the language of the automaton A. Player ◇ will win the game iff the concrete semantics assigns a set of formulas to S that is satisfied by L(A).
From a ground domain, higherorder domains are defined as continuous functions as in Section 3. Thus we only need
D^{C}(o) =  ⎛ ⎜ ⎝  P(PBool  ⎛ ⎝  T^{*}  ⎞ ⎠  )∖  ⎧ ⎨ ⎩  ∅  ⎫ ⎬ ⎭  ⎞ ⎟ ⎠  /_{⇔} . 
The endmarker $ yields the set of formulas {ε}, i.e. I^{C}($)={ε}. A terminal a:o→ o prepends a to a given word w. That is I^{C}(a) = prepend_{a}, where prepend_{a} distributes over conjunction and disjunction:
prepend_{a}(φ) =  ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ 

We apply prepend_{a} to sets of formulas by applying it to every element. Finally, I^{C}(op_{F}) where op_{F} has arity ℓ is an ℓary conjunction (resp. disjunction) if Player □ (resp. ◇) owns F.
For M^{C} = (D^{C}, I^{C}) to be a model, we need our interpretation of terminals to be ⊓continuous. This follows largely by the distributivity of our definitions.

We need to show that the concrete semantics matches the original semantics of the game.
When σ_{MC}(S) is satisfied by L(A) the concrete semantics gives a winning strategy for ◇: From a term t such that M^{C}〚t〛 σ_{MC} is satisfied by L(A), Player ◇, when able to choose, picks a rewrite rule that transforms t to t′, where M^{C}〚t′〛 σ_{MC} remains satisfied. The proof of Theorem 1 shows this is always possible, and, moreover, Player □ is unable to reach a term for which satisfaction does not hold. This does not yet give an effective strategy since we cannot compute M^{C}〚t〛 σ_{MC}. However, the abstract semantics will be computable, and can be used in place of the concrete semantics by Player ◇ to implement the winning strategy.
The proof that σ_{MC}(S) being unsatisfied implies a winning strategy for Player □ is more involved and requires the definition of a correctness relation between semantics and terms that is lifted to the level of functions, and shown to hold inductively.
The concrete model M^{C} does not lead to an algorithm for solving HOG since its domains are infinite. Here, we consider an abstract model M^{A} with finite domains. The soundness of the resulting Kleene iteration relies on the two semantics being related by a precise abstraction α. Since both semantics are defined by fixed points, this requires us to prove α (σ_{MC}) = σ_{MA}. In this section, we provide a general framework to this end.
Consider the deterministic scheme G together with two models (left and right) M_{l} = (D_{l}, I_{l}) and M_{r} = (D_{r}, I_{r}). Our goal is to relate the semantics in these models in the sense that σ_{Mr}=α(σ_{Ml}). Such exact fixedpoint transfer results are wellknown in abstract interpretation. To generalize them to higherorder we give easy to instantiate conditions on α, M_{l}, and M_{r} that yield the above equality. Interestingly, exact fixedpoint transfer results seem to be rare for higherorder (e.g. [48]). Our development is inspired by Abramsky’s lifting of abstraction functions to logical relations [3], which generalizes [11, 4]. These works focus on approximation and the compatibility we need for exactness is missing. Our framework is easier to apply than [15, 6], which are again concerned with approximation and do not offer (but may lead to) exact fixedpoint transfer results.
For the terminology, an abstraction is a function α:D_{l}(o)→ D_{r}(o). To lift the abstraction to function domains, we define the notion of being compatible with α. Compatibility intuitively states that the function on the concrete domain is not more precise than what the abstraction function distinguishes. This allows us to define the abstraction of a function by applying the function and abstracting the result, α(f) α(v_{l})=α(f v_{l}). Compatibility ensures the independence of the choice of v_{l}.
By definition, all ground elements v_{l}∈D_{l}(o) are compatible with α. For function domains, compatibility and the abstraction are defined as follows.
We lift α to valuations ν : N ⨃ V ↛ D_{l} by α(ν)(F) = α(ν(F)) and similar for x. We also lift compatibility to valuations ν:N⨃ V↛ D_{l} by requiring ν(F) to be compatible for all F∈ N and similar for x∈ V.
The conditions needed for the exact fixedpoint transfer are the following.
(P1) is surjectivity of α. (P2) states that α is wellbehaved wrt. ⊓. (P3) says that the greatest element is mapped as expected. Note that (P1)(P3) are only posed for the ground domain. One can prove that they generalize to function domains by the definition of function abstraction. (P4) is that the interpretations of terminals in M^{C} and M^{A} are suitably related. Finally (P5) is compatibility. (P4) and (P5) are generalized to terms in Lemma 2.
To prove α(σ_{Ml})=σ_{Mr}, we need that rhs_{Mr} is an exact abstract transformer of rhs_{Ml}. The following lemma states this for all terms t, in particular those that occur in the equations. The generalization to product domains is immediate. Note that the result is limited to compatible valuations, but this will be sufficient for our purposes. The proof proceeds by induction on the structure of terms, while simultaneously proving M_{l}〚t〛 compatible with α. With this result, we obtain the required exact fixedpoint transfer for precise abstractions.
We propose two domains, abstract and optimized, that allow us to solve HOG. The computation is a standard fixedpoint iteration, and, in the optimized domain, this iteration has optimal complexity. Correctness follows by instantiating the previous framework.
Our goal is to define an abstract model for games that (1) suitably relates to the concrete model from Section 4 and (2) is computable. By a suitable relation, we mean the two models should relate via an abstraction function. Provided the conditions on precision hold, correctness of the abstraction then follows from Theorem 2. Combined with Theorem 1, this will allow us to solve HOG. Computable in particular means the domain should be finite and the operations should be efficiently computable.
We define the M^{A} = (D^{A}, I^{A}) as follows. Again, we resolve the nondeterminism into Boolean formulas. But rather than tracking the precise words generated by the scheme, we only track the current set of states of the automaton. To achieve the surjectivity required by precision, we restrict the powerset to those sets of states from which a word is accepted. Let acc(w) = { q  q –[w]→ q_{f} ∈ Q_{f} }. For a language L we have acc(L) = { acc(w)  w ∈ L }. The abstract domain for terms of ground kind is D^{A}(o) = PBool(acc(T^{*})). The lifting to functions is as explained in Section 3. Satisfaction is now defined relative to a set Ω of elements of P(Q_{NFA}) (cf. Section 4). With finitely many atomic propositions, there are only finitely many formulas (up to logical equivalence). This means we no longer need sets of formulas to represent infinite conjunctions, but can work with plain formulas. The ordering is thus the ordinary implication with the meet being conjunction and top being true.
The interpretation of ground terms is I^{A}($) = Q_{f} and I^{A}(a)= pre_{a}. Here pre_{a} is the predecessor computation under label a, pre_{a}(Q)={q′∈ Q_{NFA}  q′–[a]→ q ∈ Q}. It is lifted to formulas by distributing it over conjunction and disjunction. The composition operators are again interpreted as conjunctions and disjunctions, depending on the owner of the nonterminal. Since we restrict the atomic propositions to acc(T^{*}), we have to show that the interpretations use only this restricted set. Proving I^{A}(s) is ⊓continuous is standard.
Recall our concrete model is M^{C}=(D^{C}, I^{C}), where D^{C}=P(PBool(T^{*})). To relate this model to M^{A}, we define the abstraction function α:D^{C}(o)→D^{A}(o). It leaves the Boolean structure of a formula unchanged but maps every word (which is an atomic proposition) to the set of states from which this word is accepted. For a set of formulas, we take the conjunction of the abstraction of the elements. This conjunction is finite as we work over a finite domain, so there is no need to worry about infinite syntax. Technically, we define α on PBool(T^{*}) by α(Φ)=∧_{φ∈Φ}α(φ) for a set of formulas Φ∈P(PBool(T^{*})), and
α(φ) =  ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ 

This definition is suitable in that α(σ_{MC})=σ_{MA} entails the following.
To see that the theorem is a consequence of the exact fixedpoint transfer, observe that {Q ∈ acc(T^{*})  q_{0} ∈ Q} = acc(L(A)). Then, by σ_{MA}=α(σ_{MC}) we have acc(L(A)) satisfies σ_{MA}(S) iff it also satisfies α(σ_{MC}(S)). This holds iff L(A) satisfies σ_{MC}(S) (a simple induction over formulas). By Theorem 1, this occurs iff Player ◇ wins the game.
It remains to establish α(σ_{MC})=σ_{MA}. With the framework, the exact fixedpoint transfer follows from precision, Theorem 2. The proof of the following is routine.
The above model yields a decision procedure for HOG via Kleene iteration. Unfortunately, the complexity is one exponential too high: The height of the domain for a symbol of order k in the abstract model is (k+2)times exponential, where the height is the length of the longest strictly descending chain in the domain. This gives the maximum number of steps of Kleene iteration needed to reach the fixed point.
We present an optimized version of our model that is able to close the gap: In this model, the domain for an orderk symbol is only (k+1)times exponentially high. The idea is to resolve the atomic propositions in M^{A}, which are sets of states, into disjunctions among the states. The reader familiar with inclusion algorithms will find this decomposition surprising.
We first define α:PBool(acc(T^{*}))→ PBool(Q_{NFA}). The optimized domain will then be based on the image of α. This guarantees surjectivity. For a set of states Q, we define α(Q)=∨Q= ∨_{q∈ Q} q. For a formula, the abstraction function is defined to distribute over conjunction and disjunction. The optimized model is M^{O} = (D^{O}, I^{O}) with ground domain α(PBool(acc(T^{*}))). The interpretation is I^{O}($)=∨Q_{f}. For a, we resolve the set of predecessors into a disjunction, I^{O}(a) q = ∨pre_{a}({q}). The function distributes over conjunction and disjunction. Finally, I^{O}(op_{F}) is conjunction or disjunction of formulas, depending on the owner of the nonterminal. Since we use a restricted domain, we have to argue that the operations do not leave the domain. It is also straightforward to prove our interpretation is ⊓continuous as required.
We again show precision, enabling the required exact fixedpoint transfer.
It is sufficient to show σ_{MA}(S) is satisfied by {Q ∈ acc(T^{*})  q_{0} ∈ Q} iff σ_{MO}(S) is satisfied by {q_{0}}. Theorem 3 then yields the statement. Propositions Q in σ_{MA}(S) are resolved into disjunctions ∨Q in σ_{MO}(S). For such a proposition, we have Q∈ {Q ∈ acc(T^{*})  q_{0} ∈ Q} iff ∨Q is satisfied by {q_{0}}. This equivalence propagates to the formulas σ_{MA}(S) and σ_{MO}(S) as the Boolean structure coincides. The latter follows from α(σ_{MA}(S))=σ_{MO}(S).
To solve HOG, we compute the semantics σ_{MO} and then evaluate σ_{MO}(S) at the assignment {q_{0}}. For the complexity, assume that the highest order of any nonterminal in G is k. We show the number of iterations needed to compute the greatest fixed point is at most (k+1)times exponential. We do this via a suitable upper bound on the length of strictly descending chains in the domains assigned by D^{O}.
The lower bound is via a reduction from the word membership problem for alternating kiterated pushdown automata with polynomiallybounded auxiliary worktape. This problem was shown by Engelfriet to be (k+1)EXPhard. We can reduce this problem to HOG via wellknown translations between iterated stack automata and recursion schemes, using the regular language specifying the winning condition to help simulate the worktape.
Together, these results show the following corollary and final result.
Acknowledgments. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1]. The work instigated while some of the authors were visiting the Institute for Mathematical Sciences, National University of Singapore in 2016. The visit was partially supported by the Institute.
We elaborate on the relation of our work to the influential line of research on intersection types as pioneered by [42]. With intersection types, it is usually proven that there is a word or tree derivable by a HORS that is accepted by an automaton, i.e. a welltyped type environment can be certificate for the nonemptiness of the intersection L(scheme) ∩ L(Automaton) ≠ ∅. If the HORS is deterministic, L(scheme) consists of a single tree, so this is also decides the inclusion L(scheme) ⊆ L(Automaton). If we naively extend intersection types to nondeterministic schemes, this is not true anymore. To prove the inclusion in this case, we will need to complement the automaton and prove the emptiness of the intersection, i.e. L(scheme) ∩ L(Automaton) = ∅. Note that a welltyping (a welltyped type environment) cannot prove the emptiness by itself: If the type for the initial symbol does not contain a transition from a final to an initial state, that can either stem from the nonexistence of a such a transition sequence, or from the typing not being strong enough. For example, the empty typing that does not assign any type to any symbol (or the empty intersection, if you want), is a welltyping and does not prove anything. Therefore, an algorithm that decides the nonemptiness of the intersection by using intersectiontypes has to guarantee that it constructs a welltyping strong enough to prove the existence of an accepting transition sequence if such a sequence exists. Note that algorithms that compute intersection types usually allow alternating automata as the specification. It is conceptually easier to complement an alternating automaton than it is to complement a nondeterministic automaton: The transition for each origin and label is given as a Boolean formula, and we can get the complement automaton by considering the dual formula (i.e. the formula in which conjunctions and disjunctions are swapped). Note that usually, the transition formulas are normalized to disjunctive normal form (DNF), so computing the dual formula (which will then be in CNF) and renormalizing it to DNF can lead to an exponential blowup.
Work by Neatherway et al. [46] and Ramsay [48] considers schemes with nondeterminism in the form of case statements. To handle this nondeterminism they introduce union types as a ground type. Neatherway et al. give an optimised algorithm for checking such schemes against deterministic trivial automata (where all infinite runs are accepting – i.e. a Büchi condition where all states are accepting). In his thesis, Ramsay extends this to checking nondeterministic schemes against nondeterministic trivial automata using abstract interpretation from schemes to types. In our work, we generalise nondeterminism to games (played over wordgenerating schemes), with a nondeterministic target language.
Let (ν_{i})_{i ∈ N} be a descending chain of evaluations, i.e. ν_{i} ≥ ν_{i+1} for all i ∈ N. It is to show that for all t, M〚t〛 is ⊓continuous (in the argument ν) over the respective lattice, i.e.
M〚t〛  ⎛ ⎝  ⊓_{i ∈ N} ν_{i}  ⎞ ⎠  = ⊓_{i ∈ N} (M〚F〛 ν_{i}) . 
We proceed by induction over t.
M〚F〛 (⊓_{i ∈ N} ν_{i}) = (⊓_{i ∈ N} ν_{i})(F) = ⊓_{i ∈ N} (ν_{i}(F)) = ⊓_{i ∈ N} (M〚F〛 ν_{i}) 
M〚s〛 (⊓_{i ∈ N} ν_{i}) = I(s) = ⊓_{i ∈ N} (M〚s〛 ν_{i}) 
M〚t_{1} t_{2}〛 (⊓_{i ∈ N} ν_{i})  
(Definition of semantics) =  (M〚t_{1}〛 (⊓_{i ∈ N} ν_{i})) (M〚t_{2}〛 (⊓_{i ∈ N} ν_{i})) 
(Induction hypothesis) =  (⊓_{i ∈ N} (M〚t_{1}〛 ν_{i})) (⊓_{i ∈ N} (M〚t_{2}〛 ν_{i})) 
(Definition of ⊓ for functions) =  ⊓_{i ∈ N} ( (M〚t_{1}〛 ν_{i}) (⊓_{i ∈ N} (M〚t_{2}〛 ν_{i})) ) 
(Continuity of M〚t_{1}〛 ν_{i} ∈ D) =  ⊓_{i ∈ N} ⊓_{j ∈ N} ( (M〚t_{1}〛 ν_{i}) (M〚t_{2}〛 ν_{j})) ) 
(Argued below) =  ⊓_{i ∈ N} ( (M〚t_{1}〛 ν_{i}) (M〚t_{2}〛 ν_{i})) ) 
(Definition of semantics) =  ⊓_{i ∈ N} (M〚t_{1} t_{2}〛 ν_{i}) . 
⊓_{i ∈ N} ⊓_{j ∈ N} ( (M〚t_{1}〛 ν_{i}) (M〚t_{2}〛 ν_{j})) ) = ⊓_{i ∈ N} ( (M〚t_{1}〛 ν_{i}) (M〚t_{2}〛 ν_{i})) ) . 
((M〚t_{1}〛 ν_{m}) (M〚t_{2}〛 ν_{m})) ≤ ((M〚t_{1}〛 ν_{i}) (M〚t_{2}〛 ν_{j})) . 
M〚λ x . t′〛 (⊓_{i ∈ N} ν_{i})  
(Definition of semantics) =  v ↦ (M〚t′〛 (⊓_{i ∈ N} ν_{i})[x ↦ v]) 
(Induction hypothesis) =  v ↦ (⊓_{i ∈ N} (M〚t′〛 ν_{i}[x ↦ v])) 
(Definition of ⊓ for functions) =  ⊓_{i ∈ N} ( (v ↦ M〚t_{1}〛 ν_{i}[x ↦ v]) ) 
(Definition of semantics) =  ⊓_{i ∈ N} (M〚λ x . t′〛 ν_{i}) . 
▫
Since we have not syntactically defined the evaluation of a λterm, our development will need a simple substitution lemma.
We show that for all ν : N⨃ V↛ D and all suitable terms t, t′, we have
M〚(λ x . t) t′〛 ν = M〚t[x ↦ t′]〛 ν . 
We have by definition
M〚(λ x . t) t′〛 ν = (M〚(λ x . t)〛 ν) (M〚t′〛 ν) = M〚t〛 (ν[x ↦ M〚t′〛 ν]) 
and show by induction over t that
M〚t〛 ν[x ↦ M〚t′〛 ν] = M〚t[x ↦ t′]〛 ν . 
In the base cases we have
Then, for the induction step, we first consider application. That is
M〚t_{1} t_{2}〛 ν[x ↦ M〚t′〛 ν] =  ⎛ ⎝  M〚t_{1}〛 ν[x ↦ M〚t′〛 ν]  ⎞ ⎠  ⎛ ⎝  M〚t_{2}〛 ν[x ↦ M〚t′〛 ν]  ⎞ ⎠ 
which is equal to, by induction,
⎛ ⎝  M〚t_{1}[x ↦ t′]〛 ν  ⎞ ⎠  ⎛ ⎝  M〚t_{2}[x ↦ t′]〛 ν  ⎞ ⎠  = M〚t_{1}[x ↦ t′] t_{2}[x ↦ t′]〛 ν = M〚(t_{1} t_{2})[x ↦ t′]〛 ν . 
Finally, for abstraction, we can assume by αconversion that y ≠ x, and we have
M〚λ y . t_{1}〛 ν[x ↦ M〚t′〛 ν] = v ↦ M〚t_{1}〛 ν[x ↦ M〚t′〛 ν, y ↦ v] 
which is by induction equal to the function
v ↦ M〚t_{1}[x ↦ t′]〛 ν[y ↦ v] = M〚λ y . t_{1}[x ↦ t′]〛 ν = M〚(λ y . t_{1})[x ↦ t′]〛 ν . 
Thus, by induction, we have the lemma as required. ▫
We show that for all nonground terminals s, I^{C}(s) is ⊓continuous. We need to treat the terminals a ∶ o → o of the original scheme and the terminals op_{F} that were introduced for the determinisation separately. In each case, assume a descending chain of arguments (x_{i})_{i ∈ N}.
prepend_{a} (⊓_{i ∈ N} x_{i}) = ⊓_{i ∈ N}(prepend_{a} x_{i}) 
Now assume op_{F} has arity ℓ+1, and I^{C}(op_{F}) = ∨_{ℓ+1} is an ℓ+1fold disjunction. We have
∨_{ℓ+1} (⊓_{i ∈ N} x_{i})  
(Definition of ∨_{ℓ+1}) =  y_{1}, …, y_{ℓ} ↦ (⊓_{i ∈ N} x_{i}) ∨ ∨_{ℓ} y_{1} ⋯ y_{ℓ} 
(Distributivity (see below)) =  y_{1}, …, y_{ℓ} ↦ ⊓_{i ∈ N} (x_{i} ∨ ∨_{ℓ} y_{1} ⋯ y_{ℓ}) 
(Definition of ⊓ for functions) =  ⊓_{i ∈ N} (y_{1}, …, y_{ℓ} ↦ x_{i} ∨ ∨_{ℓ} y_{1} ⋯ y_{ℓ}) 
(Definition of ∨_{ℓ+1}) =  ⊓_{i ∈ N} ∨_{ℓ+1} x_{i} 
In the above we required ∨ to distribute over ⊓, which can be seen by induction over types. In the base case, that ∨ distributes over ⊓ = ∧ is standard. For the step case, we have for all f_{i}, g, and v
 
(Definition of ∨ and ⊓) = 
 
(Induction) = 
 
(Definition of ∨ and ⊓) = 

▫
We are required to show σ_{MC}(S) is satisfied by L(A) iff there is a winning strategy foryer Player ◇. The theorem is shown in the following two lemmas.
First, we introduce some notation. We write prepend_{w} for w=a_{1}… a_{n} to abbreviate prepend_{a1} ∘ ⋯ ∘ prepend_{an}.
In what follows, whenever we refer to a term t, we mean a term built over N⨃ T, but not over T^{det}. The terminals op_{F} are excluded because they do not occur in the game, they are only introduced in the determinized scheme.
We will demonstrate a strategy for ◇ that maintains the invariant that the current (variablefree) term t reached is such that M^{C}〚t〛 σ_{MC} is satisfied by L(A). All plays are infinite or generate a word w. Since we maintain M^{C}〚t〛 σ_{MC} is satisfied by L(A), if t represents a word w, we know w is accepted by A and Player ◇ wins the game.
Initially, we have M^{C}〚S〛 σ_{MC} = σ_{MC}(S) which is satisfied by L(A) by assumption. Thus, suppose play reaches a term t such that M^{C}〚t〛 σ_{MC} is satisfied by L(A). There are two cases.
In the first case t = a_{1} (⋯ (a_{n} $)) and let w = a_{1} … a_{n}. Since
M^{C}〚a_{1}(⋯(a_{n}($)))〛 σ_{MC} = prepend_{a1… an}(ε) = w 
and w is satisfied by L(A), we know w ∈ L(A) and Player ◇ has won the game.
In the second case, we have t = a_{1}(⋯(a_{n}(F t_{1} ⋯ t_{m}))). By assumption, we know
M^{C}〚a_{1}(⋯(a_{n}(F t_{1} ⋯ t_{m})))〛 σ_{MC} = 
prepend_{a1 … an}( (M^{C}〚F〛 σ_{MC}) (M^{C}〚t_{1}〛 σ_{MC}) ⋯ (M^{C}〚t_{m}〛 σ_{MC}) ) 
is satisfied by L(A). Let F = e_{1}, …, F = e_{ℓ} be the rewrite rules for F. There are two subcases.
prepend_{a1 … an}( (M^{C}〚e_{i}〛 σ_{MC}) (M^{C}〚t_{1}〛 σ_{MC}) ⋯ (M^{C}〚t_{m}〛 σ_{MC}) ) 
We need to show the invariant is maintained. Let e_{i} = λ x_{1}, …, x_{m} . e. We have (using the substitution lemma, Lemma 7),
prepend_{a1 … an}( (M^{C}〚λ x_{1}, …, x_{m} . e〛 σ_{MC}) (M^{C}〚t_{1}〛 σ_{MC}) ⋯ (M^{C}〚t_{m}〛 σ_{MC}) )  
=  prepend_{a1 … an}( M^{C}〚(λ x_{1}, …, x_{m} . e) t_{1} … t_{m}〛 σ_{MC} ) 
=  prepend_{a1 … an}( M^{C}〚e[x_{1} ↦ t_{1}, …, x_{m} ↦ t_{m}]〛 σ_{MC} ) 
=  M^{C}〚a_{1}(⋯(a_{n}(e[x_{1} ↦ t_{1}, …, x_{m} ↦ t_{m}])))〛 σ_{MC} . 
Note that the term a_{1}(⋯(a_{n}(e[x_{1} ↦ t_{1}, …, x_{m} ↦ t_{m}]))) is the result of Player ◇ rewriting F via F = e_{i}. Since the satisfaction by L(A) passes through the equalities, Player ◇’s move maintains the invariant as required.
prepend_{a1 … an}( (M^{C}〚e_{i}〛 σ_{MC}) (M^{C}〚t_{1}〛 σ_{MC}) ⋯ (M^{C}〚t_{m}〛 σ_{MC}) ) 
▫
In what follows, whenever we refer to a term t, we mean a term built over N⨃ T, but not over T^{det}. The terminals op_{F} are excluded because they do not occur in the game, they are only introduced in the determinized scheme.
For φ ∈ D^{C}(o) and a variableclosed term t of kind o, we define φ to be sound for t, denoted φ ⊢ t, if for all w∈ T^{*} such that prepend_{w}(φ) is not satisfied by L(A), Player □ has a winning strategy from term w(t). For w=ε, we set prepend_{ε}(φ)=φ and let ε(t)=t. We can now restate the lemma as
σ_{MC}(S) ⊢ S . 
In particular, since σ_{MC}(S) is not satisfied by L(A) it is the case that prepend_{ε}(σ_{MC}(S)) is not satisfied. This means Player □ has a winning strategy from ε(S) = S.
In general, for Ξ ∈ D^{C}(κ_{1} → κ_{2}), we will also define Ξ ⊢ t for terms of kind κ_{1} → κ_{2}. That is, for a variableclosed term t of kind κ_{1} → κ_{2} and a function Ξ ∈ D^{C}(κ_{1} → κ_{2}), we define Ξ ⊢ t to hold whenever for all variableclosed terms t′ of kind κ_{1} and Ξ′ ∈ D^{C}(κ_{1}) such that Ξ′ ⊢ t′ we have Ξ Ξ′ ⊢ t t′:
Ξ ⊢ t, if ∀ Ξ′, t′ such that Ξ′ ⊢ t′, we have Ξ Ξ′ ⊢ t t′ . 
Similarly, we need to extend ⊢ to terms t with free variables x=x_{1} … x_{m}. Here, we make the free variables explicit and write t (x). We define for Ξ : (V↛ D^{C}) → D^{C} that Ξ ⊢ t(x) by requiring that for any variableclosed terms t_{1}, …, t_{m} and any Ξ_{1}, …, Ξ_{m} ∈ D^{C} with Ξ_{j} ⊢ t_{j} for all 1≤ j≤ m, we have Ξ ν ⊢ t [∀ j ∶ x_{j} ↦ t_{j}], where ν maps x_{j} to Ξ_{j}.
We now show the following. For every number of iterations i in the fixedpoint calculation, we have M^{C}〚t〛 σ_{MC}^{i} ⊢ t, for all terms t built over the terminals and nonterminals in the scheme of interest. After the induction, we will show that the result holds for the greatest fixed point. Note that we have a nested induction: the outer induction is along i, the inner is along the structure of terms.
Since we are inducting over nonclosed terms, we will have to extend σ_{MC}^{i} to assign valuations to freevariables. Thus we will write ν^{i} to denote a valuation such that ν^{i}(F) = σ_{MC}^{i}(F) for any nonterminal F.
Base case i.
In the base case, we have i=0 and ν^{i}=⊤ for all nonterminals.
We proceed by induction on the structure of terms.
We will emphasize if an argumentation is independent of the iteration count.
This is the case for all terms except nonterminals.
Base case t.
The base cases of the inner induction that are independent of the iteration count are the following.
M^{C}〚a〛 ν^{i} Ξ = prepend_{a}(Ξ) ⊢ a(t) 
M^{C}〚x〛 ν^{i} = ν^{i}(x). 
The only base case of the inner induction that depends on the iteration count is t=F. Let F take m arguments and consider variableclosed terms t_{1}, …, t_{m} with corresponding Ξ_{j} such that Ξ_{j} ⊢ t_{j}. We have
M^{C}〚F〛 ν^{0} Ξ_{1} … Ξ_{m} = σ_{MC}(F)^{0} Ξ_{1} … Ξ_{m} = true. 
Thus, trivially M^{C}〚F〛 ν^{0} ⊢ F since true is never unsatisfied.
Step case t.
In both cases, the argumentation is independent of the actual iteration count.
Therefore, we give it for a general i rather than for 0.
M^{C}〚t′〛 ν^{i} ⊢ t′ and M^{C}〚t″〛 ν^{i} ⊢ t″ . 
M^{C}〚t′ t″〛 ν^{i} = (M^{C}〚t′〛 ν^{i}) (M^{C}〚t″〛 ν^{i}) ⊢ t′ t″ . 
M^{C}〚t′ t″〛 ν^{i} =  (M^{C}〚t′〛 ν^{i}) (M^{C}〚t″〛 ν^{i}) 
⊢  (t′[∀ j: x_{j} ↦ t_{j}]) (t″[∀ j: x_{j} ↦ t_{j}]) = (t′ t″)[∀ j: x_{j} ↦ t_{j}] . 
M^{C}〚λ x.e〛 ν^{i} ⊢ (λ x.e)[∀ j: x_{j}↦ t_{j}] . 
(M^{C}〚λ x.e〛 ν^{i}) Ξ⊢ ((λ x.e)[∀ j: x_{j}↦ t_{j}]) t . 
(M^{C}〚λ x.e〛 ν^{i}) Ξ = M^{C}〚e〛 ν^{i}[x↦ Ξ] . 
((λ x.e)[∀ j: x_{j}↦ t_{j}]) t = (λ x.(e[∀ j: x_{j}↦ t_{j}])) t. 
M^{C}〚e〛 ν^{i}[x↦ Ξ] ⊢ e[x↦ t, ∀ j: x_{j}↦ t_{j}] . 
Step case i.
We again do an induction along the structure of terms.
The only case that has not been treated in full generality is F.
We now show that M^{C}〚F〛 ν^{i+1}⊢ F.
Let F take m arguments and consider Ξ_{1}⊢ t_{1} to Ξ_{m}⊢ t_{m}.
The task is to prove M^{C}〚F〛 ν^{i+1} Ξ_{1} … Ξ_{m}⊢ F t_{1} … t_{m}.
To ease the notation, assume there are two right hand sides e_{1}′, e_{2} for F, i.e. we have the rules
F = λ x_{1} … λ x_{m}.e_{1} and F = λ x_{1} … λ x_{m}.e_{2}.
This means the righthand side in the determinised scheme is
F = λ x_{1} … λ x_{m} . (op_{F} e_{1} e_{2}).
Then,
M^{C}〚F〛 ν^{i+1}  = ν^{i+1}(F)  
= M^{C}〚 λ x_{1} … λ x_{m} . (op_{F} e_{1} e_{2}) 〛 ν^{i}  
= v_{1}, …, v_{m} ↦ M^{C}〚(op_{F} e_{1} e_{2})[x_{1} ↦ v_{1}, …, x_{m} ↦ v_{m}]〛 ν^{i}  
 

Here, I^{C}(op_{F}) is a conjunction or disjunction, depending on the owner of F. Recall that the conjunction and disjunction of functions are defined by evaluating the argument functions separately and combining the results. This means
M^{C}〚F〛 ν^{i+1} 
 
 
 
 

With the same reasoning, we obtain
M^{C}〚F〛 ν^{i+1} Ξ_{1} … Ξ_{m}  
= (M^{C}〚e_{1}′〛 ν^{i} Ξ_{1} … Ξ_{m}) (∨/∧) (M^{C}〚e_{2}′〛 ν^{i} Ξ_{1} … Ξ_{m}). 
We have to prove that for any w∈ T^{*}, if L(A) does not satisfy the formula
prepend_{w}((M^{C}〚e_{1}′〛 ν^{i} Ξ_{1} … Ξ_{m}) (∨/∧) (M^{C}〚e_{2}′〛 ν^{i} Ξ_{1} … Ξ_{m}))  
=  prepend_{w}(M^{C}〚e_{1}′〛 ν^{i} Ξ_{1} … Ξ_{m}) (∨/∧) prepend_{w}(M^{C}〚e_{2}′〛 ν^{i} Ξ_{1} … Ξ_{m}), 
then Player □ has a winning strategy from w(F t_{1} … t_{m}).
Assume Player ◇ owns F and the formula is not satisfied.
If Player □ owns F, the reasoning is similar.
Since we have a disjunction for Player ◇, prepend_{w}(M^{C}〚e_{1}′〛 ν^{i} Ξ_{1} … Ξ_{m}) is not satisfied.
By the hypothesis of the outer induction, we obtain M^{C}〚e_{1}′〛 ν^{i} ⊢ e_{1} and thus M^{C}〚e_{1}′〛 ν^{i} Ξ_{1} … Ξ_{m} ⊢ e_{1}′ t_{1} … t_{m}.
As in the case of λabstraction above, we use that the game identifies e_{1}′ t_{1} … t_{m} and e_{1} [x_{1} ↦ t_{1}, … e_{m} ↦ t_{m}].
Hence, Player □ has a winning strategy from w(e_{1} [x_{1} ↦ t_{1}, … e_{m} ↦ t_{m}]).
The same argumentation applies to prepend_{w}(M^{C}〚e_{2}〛 ν^{i} Ξ_{1} … Ξ_{m}).
Consequently, whichever move Player ◇ makes at
w(F t_{1} … t_{m}),
Player □ has a winning strategy.
This finishes the outer induction, proving that M^{C}〚t〛 σ_{MC}^{i} ⊢ t for all terms t and all i ∈ N.
We would like to conclude M^{C}〚t〛 σ_{MC} ⊢ t.
Since the cppo under consideration is not finite, this needs to be proven separately.
Limit case.
We have shown
M^{C}〚t〛 σ_{MC}^{i} ⊢ t
for all i ∈ N; we now show
M^{C}〚t〛 σ_{MC} ⊢ t
noting by Kleene that
σ_{MC} = ⊓_{i ∈ N} σ_{MC}^{i}.
Once we have this we have
σ_{MC}(S) ⊢ S
which proves the lemma.
We formulate a slightly more general induction hypothesis for induction over kinds: Given a descending sequence of Ξ_{i} for all i ∈ N such that each Ξ_{i} ⊢ t, we have ⊓_{i ∈ N} Ξ_{i} ⊢ t. In the base case we have t is of kind o and we assume Ξ_{i} ⊢ t. We now argue ⊓_{i ∈ N} Ξ_{i} ⊢ t.
Take any w and suppose prepend_{w}(⊓_{i ∈ N} Ξ_{i}) is not satisfied, then we need to show by the definition of ⊢ that Player □ has a winning strategy. Since ⊓ is conjunction, if
prepend_{w}(⊓_{i ∈ N} Ξ_{i}) = ⊓_{i ∈ N} prepend_{w}(Ξ_{i}) 
is not satisfied, it must be the case that for some i we have prepend_{w}(Ξ_{i}) is not satisfied. In this case, we have Ξ_{i} ⊢ t by assumption and thus by the definition of ⊢ that Player □ has a winning strategy from w(t). This proves ⊓_{i ∈ N} Ξ_{i} ⊢ t.
If t is of kind κ_{1} → κ_{2} we need to show for all Ξ ⊢ t′ that (⊓_{i ∈ N} Ξ_{i}) Ξ ⊢ t t′. We have by the definition of ⊓ over functions
(⊓_{i ∈ N} Ξ_{i}) Ξ = ⊓_{i ∈ N} (Ξ_{i} Ξ) 
Since by assumption on Ξ_{i} and definition of ⊢ for function kinds, we have Ξ_{i} Ξ ⊢ t t′ for each i. By the induction on the kind, we obtain ⊓_{i ∈ N}(Ξ_{i} Ξ) ⊢ t t′ . Since (⊓_{i ∈ N} Ξ_{i}) σ = ⊓_{i ∈ N} (Ξ_{i} σ) we establish the desired statement that finishes the induction.
Finally, since M^{C}〚t〛 σ_{MC}^{i} satisfies the conditions of the above induction hypothesis and because we have already shown M^{C}〚t〛 σ_{MC}^{i} ⊢ t for all t, we obtain
⊓_{i ∈ N} (M^{C}〚t〛 σ_{MC}^{i}) ⊢ t . 
Then, since using continuity of M^{C}〚t〛 we have
M^{C}〚t〛 σ_{MC} = M^{C}〚t〛 (⊓_{i ∈ N} σ_{MC}^{i}) = ⊓_{i ∈ N} (M^{C}〚t〛 σ_{MC}^{i}) 
we obtain the lemma as required. ▫
We show that several properties needed for precision can be lifted from the ground domain to function domains.
We show that, if (P1) holds, then for every κ∈ Κ and every v_{r}∈D_{r}(κ) there is a compatible v_{l}∈D_{l}(κ) with α(v_{l})=v_{r}. We proceed by induction on kinds. The base case is given by the assumption (P1) and the fact that every ground element is compatible. Assume we have the required surjectivity of α for κ_{1} and κ_{2} and consider f_{r}∈D_{r}(κ_{1}→ κ_{2}). The task is to find a compatible function f_{l} so that α(f_{l})=f_{r}. Assume f_{r} v_{r} = v_{r}′. By surjectivity for κ_{1}, there are compatible elements in α^{−1}(v_{r}), and similar for v_{r}′. Let v_{l}′ be a compatible element that is mapped to v_{r}′ by α. We define f_{l} v_{l} = v_{l}′ for all compatible v_{l} ∈ α^{−1}(v_{r}). Since α is total on D(κ_{1}), this assigns a value to all compatible v_{l}. We do not impose any requirements on how to map elements that are not compatible.
We argue that f_{l} is compatible. To this end, consider compatible v_{l}^{1} and v_{l}^{2} with α(v_{l}^{1})=α(v_{l}^{2}). By definition, both are mapped identically by f_{l}, f_{l} v_{l}^{1}=f_{l} v_{l}^{2}. Hence, in particular the abstractions coincide. Moreover, given a compatible v_{l}, we defined f_{l} v_{l} = v_{l}′ to be a compatible element.
Concerning the equality of the functions, we have α(f_{l}) v_{r} = α(f_{l} v_{l}) = α(v_{l}′) = v_{r}′. The first equality is the definition of abstraction for functions and the fact that α^{−1}(v_{r}) contains compatible elements, one of them being v_{l}, the second is the fact that v_{l} is mapped to v_{l}′, and the last is by v_{l}′ ∈ α^{−1}(v_{r}′). ▫
We proceed by induction on kinds to show that, if (P1) and (P2) hold, then for all kinds κ∈ Κ and for all descending chains of compatible values f_{1}, f_{2}, … ∈D(κ), we have ⊓_{i∈ N}f_{i} again compatible and α(⊓_{i∈ N}f_{i})=⊓_{i∈ N}α(f_{i}). The base case is the assumption.
In the induction step, let κ=κ_{1}→ κ_{2} and f_{1}, f_{2},…∈D_{l}(κ) be a descending chain of compatible elements. Let v_{l}∈ D_{l}(κ_{1}) be compatible. The following equalities will be helpful:
α((⊓_{i∈ N} f_{i}) v_{l})=α(⊓_{i∈ N} (f_{i} v_{l}))=⊓_{i∈ N} α(f_{i} v_{l}) = ⊓_{i∈ N} (α(f_{i}) α(v_{l}))=(⊓_{i∈ N} α(f_{i})) α(v_{l}). 
The first equality is the definition of ⊓ on functions, the second is the induction hypothesis for κ_{2}, the third is compatibility of the f_{i} and v_{l}, the last is again ⊓ on functions.
To show compatibility, note that the above implies α((⊓_{i∈ N} f_{i}) v_{l})=α((⊓_{i∈ N} f_{i}) v_{l}′) as long as α(v_{l})=α(v_{l}′), for all compatible v_{l}, v_{l}′∈D_{l}(κ_{1}). For compatibility of (⊓_{i∈ N} f_{i}) v_{l} with v_{l}∈D_{l}(κ_{1}) compatible, note that (⊓_{i∈ N} f_{i}) v_{l}=⊓_{i∈ N} (f_{i} v_{l}). The latter is the meet over a descending chain of compatible elements in κ_{2}. By the induction hypothesis on κ_{2}, it is again compatible.
For ⊓continuity, consider a value v_{r}∈D_{r}(κ_{1}). By Lemma 10, there is a compatible v_{l}∈D_{l}(κ_{1}) with α(v_{l})=v_{r}. We have
α(⊓_{i∈ N}f_{i}) v_{r} =α((⊓_{i∈ N}f_{i}) v_{l})= (⊓_{i∈ N} α(f_{i})) α(v_{l})=(⊓_{i∈ N} α(f_{i})) v_{r}. 
The first equality is the definition of abstraction on functions. Note that we need here the fact that ⊓_{i∈ N}f_{i} is compatible by the induction hypothesis. The second equality is the auxiliary one from above. The last equality is by α(v_{l})=v_{r}. ▫
We show that, if (P3) holds, then α(⊤_{κ}^{l})=⊤_{κ}^{r} for all κ∈ Κ. We proceed by induction on kinds. The base case is given by the assumption (P3). Assume for κ_{2}, we have α(⊤_{κ2}^{l})=⊤_{κ2}^{r}. Consider function ⊤_{κ1→ κ2}^{l}∈D_{l}(κ_{1}→κ_{2}). We have to show α(⊤_{κ1→ κ2}^{l})=⊤_{κ1→ κ2}^{r}. If the given top element is not compatible, this holds. Assume it is. For v_{r} ∈ D_{r}(κ_{1}), there are two cases. If there is no compatible v_{l}∈ D_{l}(κ_{1}) with α(v_{l})=v_{r}, we have
α(⊤_{κ1→ κ2}^{l}) v_{r} = ⊤_{κ2}^{r} = ⊤_{κ1→ κ2}^{r} v_{r}. 
If there is such a v_{l}, we obtain
α(⊤_{κ1→ κ2}^{l}) v_{r} =α(⊤_{κ1→ κ2}^{l} v_{l}) = α(⊤_{κ2}^{l})=⊤_{κ2}^{r} = ⊤_{κ1→ κ2}^{r} v_{r}. 
The first equality is the definition of abstraction for functions, the next is the fact that ⊤_{κ1→ κ2}^{l} maps every element v_{l} ∈ D_{l}(κ_{1}) to ⊤_{κ2}^{l}. The image of ⊤_{κ2}^{l} is ⊤_{κ2}^{r} by the induction hypothesis. The last equality is the definition of ⊤_{κ1→ κ2}^{r}. ▫
Assume (P1), (P4), and (P5) hold. We show, for all terms t and all compatible ν, M_{l}〚t〛 ν is compatible and α(M_{l}〚t〛 ν)=M_{r}〚t〛 α(ν). We proceed by structural induction on t.
α(M_{l}〚F〛 ν)=α(ν(F))=α(ν)(F)=M_{r}〚F〛 α(ν) 
α(I_{l}(s) v_{l})=I_{r}(s) α(v_{l}) = I_{r}(s) α(v_{l}′) = α(I_{l}(s) v_{l}′). 
α(I_{l}(s)) v_{r} = α(I_{l}(s) v_{l})= I_{r}(s) α(v_{l}) =I_{r}(s) v_{r}. 
For the induction step, assume the claim holds for t_{1} and t_{2}.
M_{r}〚t_{1} t_{2}〛 α(ν) = (M_{r}〚t_{1}〛 α(ν)) (M_{r}〚t_{2}〛 α(ν)) = α(M_{l}〚t_{1}〛 ν) α(M_{l}〚t_{2}〛 ν). 
α(M_{l}〚t_{1}〛 ν) α(M_{l}〚t_{2}〛 ν) = α((M_{l}〚t_{1}〛 ν) (M_{l}〚t_{2}〛 ν)) = α(M_{l}〚t_{1} t_{2}〛 ν). 
α((M_{l}〚λ x.t_{1}〛 ν) v_{l}) = α(M_{l}〚t_{1}〛 ν[x↦ v_{l}]) = M_{r}〚t_{1}〛 α(ν[x↦ v_{l}]) . 
For the second requirement in compatibility, let v_{l} be compatible.
By definition of the semantics, (M_{l}〚λ x.t_{1}〛 ν) v_{l} = M_{l}〚t_{1}〛 ν[x↦ v_{l}].
Since ν and v_{l} are compatible, ν[x↦ v_{l}] is compatible.
Hence, M_{l}〚t_{1}〛 ν[x↦ v_{l}] is compatible by the induction hypothesis.
To prove
M_{r}〚λ x.t_{1}〛 α(ν) = α(M_{l}〚λ x.t_{1}〛 ν), consider an arbitrary value v_{r} ∈ D_{r}(κ).
Let v_{l}∈D_{l}(κ_{1}) be compatible with α(v_{l})=v_{r}, which exists by Lemma 10.
We have:
(M_{r}〚λ x.t_{1}〛 α(ν)) v_{r} = M_{r}〚t_{1}〛 α(ν)[x ↦ v_{r}] = M_{r}〚t_{1}〛 α(ν[x↦ v_{l}]) . 
We showed above that M_{l}〚λ x.t_{1}〛 ν is compatible. Using the definition of abstraction for functions and the definition of the semantics, the other function yields
α(M_{l}〚λ x.t_{1}〛 ν) v_{r} = α((M_{l}〚λ x.t_{1}〛 ν) v_{l})= α(M_{l}〚t_{1}〛 ν[x↦ v_{l}]) . 
With the induction hypothesis, α(M_{l}〚t_{1}〛 ν[x↦ v_{l}])=M_{r}〚t_{1}〛 α(ν[x↦ v_{l}]).
▫
Recall σ_{l}^{0} and σ_{r}^{0} are the greatest elements of the respective domains. We have
α(σ_{l})=α(⊓_{i∈ N} rhs_{Ml}^{i}(σ_{l}^{0}))= ⊓_{i∈N} α(rhs_{Ml}^{i}(σ_{l}^{0})) = ⊓_{i∈N} rhs_{Mr}^{i}(σ_{r}^{0}) = σ_{r}. 
The first equality is Kleene’s theorem. The second equality uses the fact that each rhs_{Ml}^{i}(σ_{l}^{0}) is compatible and that they form a descending chain (both by induction on i), and then applies Lemma 11. The third equality also relies on compatibility of the rhs_{Ml}^{i}(σ_{l}^{0}) and invokes Lemma 2. Moreover, it needs α(σ_{l}^{0})=σ_{r}^{0} by Lemma 12. The last equality is again Kleene’s theorem. ▫
Observe I^{A}($) = Q_{f} = acc(ε). Given a formula φ∈ PBool(acc(T^{*})), we have to show that pre_{a}(φ)∈ PBool(acc(T^{*})). Since pre_{a} distributes over conjunction and disjunction, it is sufficient to show the requirement for atomic propositions. Consider Q=acc(w). We have I^{A}(a) acc(w) = pre_{a}(acc(w)) = acc(a.w). Finally, I^{A}(op_{F}) with F∈ N is conjunction or disjunction, and there is nothing to do as the formula structure is not modified. ▫
We require, for all terminals s, I^{A}(s) is ⊓continuous over the respective lattices. We remark that the case s = op_{F} is identical to Lemma 1. Hence, we show the case s = a ∈ Γ. Given a descending chain (x_{i})_{i∈N}, we have to show I(a) (⊓_{i∈N} x_{i}) = ⊓_{i∈N} (I(a) x_{i}). Recall that the meet of formulas is conjunction, and that we are in a finite domain. The latter means that the infinite conjunction is really the conjunction of finitely many formulas. Now pre_{a} is defined to distribute over finite conjunctions. We have
I(a) (⊓_{i∈N} x_{i}) = pre_{a}  ⎛ ⎜ ⎜ ⎝ 
 x_{i}  ⎞ ⎟ ⎟ ⎠  = 
 pre_{a}  ⎛ ⎝  x_{i}  ⎞ ⎠  = ⊓_{i∈N} (I(a) x_{i}) 
as required. ▫
To show α is precise, we have to show (P1) to (P5).
For (P1), it is sufficient to argue that for every set of states Q∈ acc(T^{*}) there is a word that is mapped to it — which holds by definition.
For formulas, note that α=acc distributes over conjunction and disjunction, which means we can take the same connectives in the concrete as in the abstract and replace the leaves appropriately. Note that we only need a set consisting of one formula.
(P2) is satisfied by the concrete meet being the union of sets of formulas and α being defined by an elementwise application.
For (P3), note that the greatest elements are {true} for D^{C}(o) and true for D^{A}(o). By definition, α({true})=α(true)=true.
For (P4), consider $.
We have
α(I^{C}($)) = α({ε})=acc(ε)=Q_{f}=I^{A}($).
The first equality is by definition of the concrete interpretation, the second is the definition of α, the third uses the fact that ε is accepted precisely from the final states, and the last equality is the interpretation of the $ in the abstract domain.
For a letter a and a word w⊆ T^{*}, we have

The first equality is the interpretation of a in the concrete, the second is the definition of prepending a letter, the third is the definition of the abstraction, the next is how taking predecessors changes the set of states from which a word is accepted, and the last equality is the interpretation of a in the abstract domain and the definition of the abstraction function. The relation generalizes to formulas by noting that both the concrete interpretation and the abstract interpretation of a distribute over conjunction and disjunction. It also generalizes to sets of formulas by noting that prepend_{a} is applied to all elements in the set and, in the abstract domain, pre_{a} distributes over conjunction.
Let F be a nonterminal owned by □. To simplify the notation, let the associated operation be binary, op_{F}:o→ o → o. Let Φ_{1},Φ_{2}∈D^{C}(o) be sets of formulas. We have
α(I^{C}(op_{F}) Φ_{1} Φ_{2}) = α(Φ_{1}⋃ Φ_{2}) 
 

The first equality is the concrete interpretation of op_{F}. The second is the definition of the abstraction function. The third equality holds as we work up to logical equivalence. The last is the abstract interpretation of op_{F} and again the definition of the abstraction.
Assume F is owned by ◇ and op_{F} is again binary. Consider Φ_{1},Φ_{2}∈D^{C}(o). It will be convenient to denote {φ_{1}∨φ_{2}  φ_{1}∈ Φ_{1},φ_{2}∈ Φ_{2}} by Φ. We have
α(I^{C}(op_{F}) Φ_{1} Φ_{2}) = α(Φ) 
 
 

The first equality is the concrete interpretation of op_{F}, the second is the definition of α on sets of formulas.
The third equality is the fact that α distributes over disjunctions and rewrites the iteration over the elements of Φ.
The following equality is distributivity of conjunction over disjunction, and the fact that we work up to logical equivalence.
The last is the abstract interpretation of op_{F} and the definition of the abstraction function.
It remains to show (P5).
For I^{C}($) and I^{C}(a), there is nothing to do as all ground values are compatible.
Assume F is owned by □ and op_{F} is binary.
The proof for ◇ is similar.
We show that, given a set of formulas Φ, the function
Φ∪ − is compatible.
An inspection of the proof of (P4) shows that for any set of formulas φ_{1}, we have
α(Φ⋃ Φ_{1}) = α(Φ)∧ α(Φ_{1}). 
Hence, if α(Φ_{1})=α(Φ_{2}), then α(Φ∪ Φ_{1})= α(Φ∪ Φ_{2}). That Φ∪ Φ_{1} is compatible holds as the element is ground. ▫
v We have I^{O}($)=∨Q_{f}= α(Q_{f})=α(acc(ε)). For I^{O}(a), we note that both the abstract and the optimized interpretation distribute over conjunctions and disjunctions. Hence, it remains to consider whether the application to leaves results in a disjunction that is the image of an abstract set. Let Q=acc(w). We have

 
 
=∨pre_{a}(Q)  

The first equality is the definition of the abstraction function. Then we apply distributivity of the optimized interpretation of a over disjunctions. The following equality is the actual interpretation of a in the optimized model. The next equality uses pre_{a}(Q)=∪_{q∈ Q}pre_{a}(q). The following is again the definition of the abstraction function. Then we replace Q by its definition. Finally, we note the interplay between pre_{a} and acc(−).
For conjunction and disjunction, which are used as the interpretation of op_{F} depending on the player, we note that α distributes to the arguments. Hence, if the arguments are α(φ_{1}) and φ_{2}, we have α(φ_{1})∧ α(φ_{2})=α(φ_{1}∧ φ_{2}). ▫
We need, for all terminals s, I^{O}(s) is ⊓continuous over the respective lattices. We remark that the case s = op_{F} is identical to Lemma 1. The case s = a ∈ Γ follows from distributivity of I^{O}(a) as in the proof of Lemma 4. ▫
We show the optimized abstraction is precise.
Surjectivity in (P1) holds by definition as does (P3).
Also ⊓continuity in (P2) is by the fact that the meets over the concrete domain are finite, and hence the definition of α already yields continuity.
We argue for (P4).
For $, Lemma 5 yields I^{O}($)=α(Q_{f}), which is α(I^{A}($)) as required.
For a, the same lemma shows I^{O}(a) α(acc(w))=α(pre_{a}(acc(w))), which is α(I^{A}(a) acc(w)).
The equality generalizes to formulas as both, the abstraction function and the interpretations distribute over conjunctions and disjunctions.
For op_{F}, assume it is a binary conjunction.
We have
I^{O}(op_{F}) α(φ_{1}) α(φ_{2})= α(φ_{1})∧ α(φ_{2})=α(φ_{1}∧ φ_{2})=α(I^{A}(op_{F}) φ_{1} φ_{2}). 
The first equality is the definition of the interpretation in the optimized model, the next is distributivity of α over conjunction.
Finally, we have the interpretation of op_{F} in the abstract model.
For (P5), there is nothing to do for
I^{C}($) and I^{C}(a), as all ground values are compatible.
We consider the conjunctions and disjunctions used to resolve the nondeterminism.
Consider a formula φ.
The task is to show that the function φ∧ − is compatible.
Consider φ_{1} and φ_{2} with α(φ_{1})=α(φ_{2}).
Then
α(φ∧ φ_{1})=α(φ)∧α(φ_{1})=α(φ)∧α(φ_{2})=α(φ∧φ_{2}). 
The first equality is distributivity of the abstraction function over conjunctions. The next is the assumed equality. The third is again distributivity. Compatibility of φ∧φ_{1} holds as ground values are always compatible. ▫
To show the complexity, we argue the upper and lower bounds separately.
[Proof of Proposition 4] We need to argue that σ_{MO} can be computed in (k+1)times exponential time. We have that σ_{MO} = ⊓_{i ∈ N} rhs_{MO}^{i}(σ_{l}^{0}). Since the domains D^{O}(κ) are finite for all kinds κ, there is an index i_{0} ∈ N such that σ_{MO} = ⊓_{i = 0}^{i0} rhs_{MO}^{i}(σ_{l}^{0}) = rhs_{MO}^{i0}(σ_{l}^{0}). In the following, we will see that the number of iterations, i.e. the index i_{0} is at most (k+1)times exponential, and that one iteration can be executed in (k+1)times exponentially many steps.
First, we reason about the number of iterations. For a partial order D, we define its height h(D) as the length of the longest strictly descending chain, i.e. the height is m if the longest such chain is of the shape
x_{0} > x_{1} > … > x_{k} . 
The height of the domain is an upper bound for i_{0} by its definition: If for some index i_{1} we have rhs_{MO}^{i1}(σ_{l}^{0}) = rhs_{MO}^{i1 + 1}(σ_{l}^{0}), we know ⊓_{i = 0}^{i0} rhs_{MO}^{i}(σ_{l}^{0}) = rhs_{MO}^{i01}(σ_{l}^{0}) and thus i_{1} = i_{0}. Such an index i_{1} has to exist and has to be smaller than the height of the domain, otherwise the sequence of the rhs_{MO}^{i}(σ_{l}^{0}) would form a chain that is strictly longer than the height, a contradiction to the definition.
It remains to see what the height of our optimized domain is. Recall that rhs_{MO} has the type signature (N → D^{O}) → (N → D^{O}). Our goal in the following is to determine h(N → D^{O} ). We can identify N → D^{O} with D^{O}(F_{1}) × … × D^{O}(F_{ℓ}), where F_{1}, …, F_{ℓ} are the nonterminals of the scheme. The height of this product domain is the sum of its height. We are done if we show that even the domain D^{O}(F) with the maximal height is (k+1)times exponentially high, since the number of nonterminals is polynomial in the input scheme.
In the following we prove: If kind κ is of order k′, then D^{O}(κ) has (k′+1)times exponential height. For the induction step, we also need to consider the cardinality of D^{O}(κ), therefore, we strengthen the statement and also prove that the cardinality D^{O}(κ) is (k′+2)times exponential.
We proceed by induction on k′.
In the base case k′ = 0, we necessarily have κ = o, and indeed the domain α(PBool(acc(T^{*}))) ⊆ PBool(Q_{NFA}) is singly exponentially high. To see that this is the case, consider a strictly decreasing chain (φ_{j})_{j ∈ N} of positive boolean formulas over Q_{NFA}, i.e. a chain where each formula is strictly implied by the next. To each formula, φ_{j}, we assign the set Q_{j} = {Q ⊆ Q_{NFA}  Q satisfies φ_{j}} of assignments under which φ_{j} evaluates to true. That φ_{j} is strictly implied by φ_{j+1} translates to the fact that Q_{j} is a strict subset of Q_{j+1}. This gives us that the sets Q_{j} themselves form a strictly ascending chain in P(P(Q_{NFA})), and it is easy to see that such a chain has length at most  P(Q_{NFA})  = 2^{QNFA}.
Furthermore, we can represent each equivalence class of formulas in PBool(Q_{NFA}) by a representative in conjunctive normal form, i.e. by an element of P(P(Q_{NFA})). This shows that the cardinality of the domain is indeed bounded by  P(P(Q_{NFA}))  = 2^{ P(QNFA) } = 2^{2QNFA}.
Now assume the statement holds for k′, and consider κ of order k′+1. We need an inner induction on the arity m of κ.
Since o is the only kind of arity 0, and does not have order k′+1 for any k′, there is nothing to do in the base case.
Now assume that κ = κ_{1} → κ_{2}. By the definitions of arity and order, we know that κ_{1} is of order at most k′, therefore we now by the outer induction that the height of D^{O}(κ_{1}) is at most (k′+1)times exponential. The order of κ_{2} is at most (k′+1), but the arity of κ_{2} is strictly less than the arity of κ, thus we get by the inner induction that the height of D^{O}(κ_{2}) is at most (k′+2)times exponential.
The domain D^{O}(κ_{1} → κ_{2}) = Cont(D^{O}(κ_{1}), D^{O}(κ_{2})) is a subset of all functions from D^{O}(κ_{1}) to D^{O}(κ_{2}). Let us reason about the height of this more general function domain. We know that its height is the height of the target times the size of the source, i.e. h(D^{O}(κ_{2})) ·  D^{O}(κ_{1}) . The induction completes the proof, as both h(D^{O}(κ_{2})) and  D^{O}(κ_{1})  are at most (k′+2)times exponential.
It remains to argue that each iteration can be implemented in at most (k+1)times exponentially many steps. To this end, we argue that each element of D^{O}(κ) can be represented by an object of size (k′+1)times exponential, where k′ is the order of κ. It is easy to see that all operations that need to be executed on these objects, namely evaluation, conjunction, disjunction, and predecessor computation can be implemented in polynomial time in the size of the objects.
Let k′ = 0, i.e. κ = o. We again represent each element of D^{O}(o) by a formula over Q_{NFA} in conjunctive normal form, i.e. as an element of P( P( Q_{NFA})). In the worst case, one single formula φ contains everyone of the 2^{QNFA} many clauses, each clause having size at most Q_{NFA}. This means that one formula needs at most singly exponential space.
For the induction step, consider κ of order k+1. As above, we need an inner induction on the arity of κ, for which the base case is trivial.
Let κ = κ_{1} → κ_{2}. An element of D^{O}(κ) is a function that assigns to each of the D^{O}(κ_{1})many elements of D^{O}(κ_{1}) an element of D^{O}(κ_{2}). In the previous part of the proof, we have argued, that D^{O}(κ_{1}) is at most (k+1) times exponential. By the induction on the arity, we know that each object in D^{O}(κ_{2}) can be represented in at most (k+2)times exponential space. This shows that objects of D^{O}(κ) can be represented using (k+2)times exponential space, and finishes the proof. ▫
We show that determining the winner in a higherorder word game is (k+1)EXPhard for an orderk recursion scheme.
[Proof of Proposition 5] We begin with a result due to Engelfriet [18] that shows alternating kiterated pushdown automata with a polynomially bounded auxiliary worktape (kPDA^{+}) characterize the (k+1)EXP word languages. We fix any (k+1)EXPhard language and its corresponding alternating kPDA B. Let L(B) be the set of words accepted by B. Deciding if a given word w is in the language defined by B is (k+1)EXPhard in the size of w (recall B is fixed). We show that this problem can be reduced in polynomial time to an inclusion problem L(B′) ⊆ L(A) for some kiterated pushdown automaton (without worktape) (kPDA) B′ and NFA A of size polynomial in the length of w. From B′, we can construct in polynomial time an equivalent game over a scheme G. This will show the game language inclusion problem for orderk schemes is (k+1)EXPhard.
In an alternating kPDA^{+}, there are two Players ◇ and □. When decided whether a word w is in the language of a kPDA^{+}, ◇ will attempt to prove the word is in the language, while □ will try to refute it.
We first describe how to obtain B′ from B. Since the word w is fixed, we can force B to output the word w by forming a product of w with the states of B. Call this automaton B × w. This reduces the word membership problem to the problem of determining whether B × w can reach an accepting state. Next, to remove the worktape from B × w (and form B′) we replace the output of B × w (which will always be w or empty) with a series of guesses of the worktape. That is, a transition of B × w will be simulated by B′ by first making a transition as expected, and then outputting a guess (consistent with the transition) of what the worktape of B × w should be. The automaton A will accept a guessed sequence of worktapes iff it is able to find an error in the sequence. The word w will be in the language of B if B′ is able to reach a final state and produce a word w′ that is correct; that is, w′ is not in the language of A.
Note, here, the reversal of the roles of the Players. In B, control states are owned by ◇ or □. When determining if w ∈ L(B) for some w, the first Player ◇ tries to show the word is accepted, while the second Player □ tries to force a nonaccepting run. In B′, however, w is accepted iff the output of B′ is not included in the language of A. Thus, □ will effectively be aiming to prove that w ∈ L(B).
In more detail, we take any (k+1)EXPhard language and its equivalent (fixed) alternating kPDA^{+}. Given a word w, deciding w ∈ L(B) is (k+1)EXPhard. We define B′ directly from B rather than going through the intermediate B × w.
A transition (p, a, o, σ, p′) of B means the following. From control state p, upon reading a character a from w, apply operation o to the worktape (which may become stuck if not applicable) and operation σ to the stack (which may also become stuck if not applicable). Next, move to control state p′, from which the remainder of w is to be read.
Let m be the polynomial bound on the size of the worktape of A given the input word w. Let Σ be the alphabet of the worktape. Let the set of worktape operations O = {o_{1}, …, o_{n}} and worktape positions P = [1..m] be disjoint from Σ. Also, let ∘ ∈ Σ be the initial symbol appearing in each cell of the initial worktape. We will construct A′ such that
L  ⎛ ⎝  A′  ⎞ ⎠  ⊆ ∘^{m}  ⎛ ⎝  P O Σ^{m}  ⎞ ⎠  ^{∗} . 
That is, A′ outputs a sequence of worktape configurations separated by positions in P and operations in O. That is, A′ will simulate a run of A over w.
For every control state p of A, we will have control states (p, w′) of A′, where w′ is a suffix of w. We will also have (p, w′, o) where o is a worktape operation to be applied. Then for each transition (p, a, o, σ, p′) of B we have a transition ((p, aw′), ε, σ, (p′, w′, o)) of B × w. From (p′, w′, o) the automaton B′ will output some character from P (a guess at the worktape head position), followed by o (to indicate the operation applied). It will then be able to output any word from Σ^{m} (a guess of the worktape contents) before moving to (p′, w′) and continuing the simulation. Initially, B′ will simply output ∘^{m} and move to control state (p, w) where p is the initial control state of B.
The final step in defining B′ is to assign ownership of the control states. Recall, we needed to switch the roles of the Players. Thus, we define O((p, w)) = ◇ whenever p belongs to □ in B. All other control states of B′ are owned by □. We define the accepting control states to be those of the form (p, ε) where p is accepting in B. Observe these have no outgoing transitions.
Next we define the regular automaton A which detects mistakes in the worktape. Such an error is either due to a poorly updated cell, or due to a poorly updated head position. The set of worktape operations O is such that there is a mapping
π : (P × O → P) ⋃ (P × Σ × P × O → Σ ⋃ {⊥}) 
where ⊥ ∉ Σ and
Thus, we require the following regular language, for which a polynomiallysized regular automaton is straightforward to construct. Let Γ = Σ ∪ P ∪ O.
L  ⎛ ⎝  A  ⎞ ⎠  =  ⎛ ⎜ ⎜ ⎝  Γ^{∗}  ⎛ ⎜ ⎜ ⎝ 
 i o Σ^{m} j  ⎞ ⎟ ⎟ ⎠  Γ^{∗}  ⎞ ⎟ ⎟ ⎠  ⋃  ⎛ ⎜ ⎜ ⎝  Γ^{∗}  ⎛ ⎜ ⎜ ⎝ 
 i o Σ^{j} α Γ^{m+2} β  ⎞ ⎟ ⎟ ⎠  Γ^{∗}  ⎞ ⎟ ⎟ ⎠  . 
We have thus defined a kPDA B′ that produces some word w′ not accepted by A iff w is accepted by B.
The final step is to produce a game over a scheme G that is equivalent to the game problem for kiterated pushdown automata. This is in fact a straightforward adaptation of the techniques introduced by Knapik et al. [38]. However, we choose to complete the sketch using definitions from Hague et al. [30] as we believe these provide a clearer reference. In particular, we adapt their Definition 4.3.
The key to the reduction is a tight correspondence (given in op. cit.) between configurations (q, s) of a kiterated pushdown automaton, and terms of the form^{1} F_{q}^{a} Ψ_{k−1} ⋯ Ψ_{0}. That is, every configuration is represented (in a precise sense) by such a term and every term of such a form represents a configuration. Moreover, for every transition (q, a, o, σ, q′) of the pushdown automaton, when o ≠ ε we can associate a rewrite rule of the scheme
F_{q}^{a} = λ 
 . o(e_{(q′, σ)}) 
such that the term obtained by applying the rewrite rule to F_{q}^{a} Ψ_{k−1} ⋯ Ψ_{0} is a term o(F_{q′}^{b} Ψ′_{k−1} ⋯ Ψ′_{0}) where F_{q′}^{b} Ψ′_{k−1} ⋯ Ψ′_{0} represents the configuration reached by the transition. That is, (q′, σ(s)). When o = ε we simply omit o, that is
F_{q}^{a} = λ 
 . e_{(q′, σ)} . 
To each nonterminal, we assign O(F_{q}^{a}) = ◇ whenever q is a ◇ control state. Otherwise, O(F_{q}^{a}) = □. For every accepting control state q we introduce the additional rule
F_{q}^{a} = λ 
 . $ . 
Finally, we have an initial rule
S = t 
where t is the term representing the initial configuration.
Given the tight correspondence between configurations and transitions of the kPDA and terms and rewrite steps of G, alongside the direct correspondence between the owner of a control state q and the owner of a nonterminal of G, it is straightforward to see, via induction over the length of an accepting run in one direction, or derivation sequence in the other, that B′ is able to produce a word not in A iff a word not in A is derivable from S. Thus, we have reduced the word acceptance problem for some alternating kPDA^{+} to the game problem for language inclusion of a scheme. This shows the problem is (k+1)EXPhard. ▫
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.