Domains for Higher-Order Games

TL;DR

This paper introduces a novel finite domain for analyzing two-player inclusion games over higher-order recursion schemes, enabling an optimal algorithm for program synthesis verification.

Contribution

It develops a new domain based on Boolean formulas and automaton states, providing a direct fixed-point algorithm for two-player inclusion games with proven optimal complexity.

Findings

Finite domain representation of winning regions.

Algorithm with (k+1)EXP complexity for order-k schemes.

Matching lower bound proving optimality.

Abstract

We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals 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 fixed-point techniques, a direct algorithm for the analysis of two-player 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 order-k 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 fixed-point computations can be applied.

Equations

$$\kappa ::=o\mid ({\kappa }_1\to {\kappa }_2).$$

$$\displaystyle\mathsf{arity}\mathopen{}\mathclose{{}\left(o}\right)$$

$$\displaystyle\mathsf{arity}\mathopen{}\mathclose{{}\left(\kappa_{1}\to\kappa_{2}}\right)$$

$$\displaystyle\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket-}\right\rrbracket:\mathcal{T}\rightarrow(N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D})\rightarrow\mathcal{D}\ .$$

$$\displaystyle\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ \nu$$

$$\displaystyle\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket x}\right\rrbracket\ \nu$$

$$\mathit{rhs}_{\mathcal{M}}:(N\rightarrow\mathcal{D})\rightarrow(N\rightarrow\mathcal{D})\ ,\quad\text{ where}\quad\mathit{rhs}_{\mathcal{M}}(\nu)(F_{j})=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{j}}\right\rrbracket\ \nu\ .$$

$${\sigma }_{\mathcal{M}}={\text{bigsqcap}}_{i\in \mathbb{N}}{\sigma }_{\mathcal{M}}^i={\text{bigsqcap}}_{i\in \mathbb{N}}{rhs}_{\mathcal{M}}^i({\sigma }_{\mathcal{M}}^0)$$

$$\mathcal{D}^{\mathit{C}}(o)=\mathopen{}\mathclose{{}\left({\mathcal{P}}\mathopen{}\mathclose{{}\left(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)}}\right)\setminus\mathopen{}\mathclose{{}\left\{\emptyset}\right\}}\right)/_{\Leftrightarrow}\ .$$

$$\mathsf{prepend}_{a}(\phi)=\mathopen{}\mathclose{{}\left\{\begin{array}[]{ll}aw&\phi=w\ ,\\ \mathsf{prepend}_{a}(\phi_{1})\mathop{\mathit{op}}\mathsf{prepend}_{a}(\phi_{2})&\phi=\phi_{1}\mathop{\mathit{op}}\phi_{2}\text{ and }\mathop{\mathit{op}}\in\mathopen{}\mathclose{{}\left\{\land,\lor}\right\}\ ,\\ \phi&\phi=\mathsf{true}\ .\\ \end{array}}\right.$$

$$\displaystyle\sigma_{\mathcal{M}^{\mathit{C}}}(S)=\bigcup_{k>0}\mathsf{prepend}_{a}^{2k}(\mathopen{}\mathclose{{}\left\{\varepsilon}\right\})\vee\mathsf{prepend}_{b}(\mathopen{}\mathclose{{}\left\{\varepsilon}\right\})=\mathopen{}\mathclose{{}\left\{a^{2k}\vee b\ \middle|\ k>0}\right\}.$$

$$\alpha(\phi)=\mathopen{}\mathclose{{}\left\{\begin{array}[]{ll}\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)&\text{if }\phi=w,\\ \alpha(\phi_{1})\mathop{\mathit{op}}\alpha(\phi_{2})&\text{if }\phi=\phi_{1}\mathop{\mathit{op}}\phi_{2}\text{ and }\mathop{\mathit{op}}\in\mathopen{}\mathclose{{}\left\{\land,\lor}\right\},\\ \phi&\text{if }\phi=\mathsf{true}\ .\\ \end{array}}\right.$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\mathopen{}\mathclose{{}\left(\bigsqcap_{i\in{\mathbb{N}}}\nu_{i}}\right)=\bigsqcap\limits_{i\in{\mathbb{N}}}(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ \nu_{i})\ .$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ (\bigsqcap\limits_{i\in{\mathbb{N}}}\nu_{i})=(\bigsqcap\limits_{i\in{\mathbb{N}}}\nu_{i})(F)=\bigsqcap\limits_{i\in{\mathbb{N}}}(\nu_{i}(F))=\bigsqcap\limits_{i\in{\mathbb{N}}}(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ \nu_{i})$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ (\bigsqcap\limits_{i\in{\mathbb{N}}}\nu_{i})=\mathcal{I}(s)=\bigsqcap\limits_{i\in{\mathbb{N}}}(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ \nu_{i})$$

$$\displaystyle\ \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}\ t_{2}}\right\rrbracket\ (\bigsqcap\limits_{i\in{\mathbb{N}}}\nu_{i})$$

$$\text{(Definition of semantics)}=$$

$$\text{(Induction hypothesis)}=$$

$$\text{(Definition of ⊓ for functions)}=$$

$$\displaystyle\text{(Continuity of $\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i}\in\mathcal{D}$)}=$$

$$\text{(Argued below)}=$$

$$\text{(Definition of semantics)}=$$

$$\bigsqcap\limits_{i\in{\mathbb{N}}}\bigsqcap\limits_{j\in{\mathbb{N}}}((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{j})))=\bigsqcap\limits_{i\in{\mathbb{N}}}((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{i})))\ .$$

$$((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{m})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{m}))\leqslant((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{j}))\ .$$

$$\displaystyle\ \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket\lambda x.t^{\prime}}\right\rrbracket\ (\bigsqcap\limits_{i\in{\mathbb{N}}}\nu_{i})$$

$$\text{(Definition of semantics)}=$$

$$\text{(Induction hypothesis)}=$$

$$\text{(Definition of ⊓ for functions)}=$$

$$\text{(Definition of semantics)}=$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(\lambda x.t)\ t^{\prime}}\right\rrbracket\ \nu=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}\ .$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(\lambda x.t)\ t^{\prime}}\right\rrbracket\ {\nu}=(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(\lambda x.t)}\right\rrbracket\ {\nu})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu})=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ (\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}])$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t[x\mapsto t^{\prime}]}\right\rrbracket\ \nu\ .$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}\ t_{2}}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=\mathopen{}\mathclose{{}\left(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}}\right)\ \mathopen{}\mathclose{{}\left(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}}\right)$$

$$\mathopen{}\mathclose{{}\left(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}}\right)\ \mathopen{}\mathclose{{}\left(\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}}\right)=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}[x\mapsto t^{\prime}]\ t_{2}[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(t_{1}\ t_{2})[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}\ .$$

$$\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket\lambda y.t_{1}}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=v\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu},y\mapsto v]}$$

$$v\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu[y\mapsto v]}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket\lambda y.t_{1}[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(\lambda y.t_{1})[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}\ .$$

Full text

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 fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a $(k+1)\mathsf{EXP}$ algorithm for order-$k$ 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 fixed-point computations can be applied.

1. Introduction

Inclusion checking has recently received considerable attention [54, 23, 1, 2, 36]. 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 [32], and then been generalized to parallel and parameterized programs [42, 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 control-flow language $\mathit{CF}$ that is supposed to satisfy a safety specification given by a regular language $R$. If the check $\mathit{CF}\subseteq R$ succeeds, then the program is correct as the data flow only restricts the set of computations. If a computation $w\in\mathit{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\cup S$ and repeat the procedure.

Podelski’s loop has also been generalized to synthesis [35, 44]. In that setting, the program is assumed to have two kinds of non-determinism. Some of the non-deterministic 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 non-determinism. In contrast, the so-called angelic non-determinism are the alternatives of the system to react to an input. The synthesis problem is to devise a controller that resolves the angelic non-determinism in a way that a given safety specification is met. Technically, the synthesis problem corresponds to a two-player 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 strategy-synthesis problem.

Our motivation is to synthesize functional programs with Podelski’s loop. We assume the program to be given as a non-deterministic higher-order recursion scheme where the non-terminals 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 strategy-synthesis 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 non-deterministic. 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 strategy-synthesis problem to higher-order model checking [46], which indeed can be achieved (see Appendix A for a comparison to intersection types [41]). Instead, we need a strategy synthesis that can directly deal with non-deterministic specifications.

We show that the winning region of a higher-order inclusion game wrt. a non-deterministic right-hand side can be computed with a standard fixed-point 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 formula-based domain has recently been proposed for context-free inclusion games [35] (and generalized to infinite words [44]), the generalization to higher-order is new. Consider a non-terminal 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 non-terminal. 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 non-determinism captured by a set. Crucially, our approach handles the non-determinism 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 [52] as well as Grellois and Melliès [25, 25], with [5, 49] 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 fixed-point semantics and their correspondence to automata [52], and constructions of enriched Scott models for parity conditions [51, 50]. 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 $\omega$-path properties with a focus on the domain [33]. They show that explicit automata constructions can be avoided and give a domain that directly captures subsets (so-called patches) of the $\omega$-language. The work has been generalized to higher order [34]. 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 fixed-point 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 fixed-point transfer result to replace the terminals by states and get rid of the sets. The final step is another exact fixed-point transfer that justifies the optimization. We give a matching lower bound. The problem is $(k+1)\mathsf{EXP}$-complete for order-$k$ schemes.

Related Work.

The relationship between recursion schemes and extensions of pushdown automata has been well studied [16, 17, 37, 29]. 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. [37] and independently by Caucal [14]. This result was generalized to all schemes by Ong [46]. 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 [53, 13, 38, 29]. Of particular interest are saturation methods for pushdown games [7, 22, 12, 8, 30, 31, 9]. In these works, automata representing sets of winning configurations are constructed using fixed-point computations.

A related approach pioneered by Kobayashi et al. operating directly on schemes is that of intersection types [40, 41], 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 fixed-point computation analogous to an optimized version of our Kleene iteration, restricted to deterministic schemes. This has led to one of the most competitive model-checking tools for schemes [39].

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 model-theoretic verification algorithms. Abstract interpretation has also been used by Ramsay [48], Salvati and Walukiewicz [51, 50], 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 higher-order programs [4].

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.

2. Preliminaries

Complete Partial Orders.

Let $(D,\leqslant)$ be a partial order with set $D$ and (partial) ordering $\leqslant$ on $D$. We call $(D,\leqslant)$ pointed if there is a greatest element, called the top element and denoted by $\top\in D$. A descending chain in $D$ is a sequence $(d_{i})_{i\in{\mathbb{N}}}$ of elements in $D$ with $d_{i}\geqslant d_{i+1}$. We call $(D,\leqslant)$ $\omega$-complete if every descending chain has a greatest lower bound, called the meet or the infimum, and denoted by $\bigsqcap_{i\in{\mathbb{N}}}d_{i}$. If $(D,\leqslant)$ is pointed and $\omega$-complete, we call it a pointed $\omega$-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\to D$ is $\sqcap$-continuous if for all descending chains $(d_{i})_{i\in{\mathbb{N}}}$ we have $f(\bigsqcap_{i\in{\mathbb{N}}}d_{i})=\bigsqcap_{i\in{\mathbb{N}}}f(d_{i})$. We call a function $f:D\to D$ monotonic if for all $d,d^{\prime}\in D$, $d\leqslant d^{\prime}$ implies $f(d)\leqslant f(d^{\prime})$. Any function that is $\sqcap$-continuous is also monotonic. For a monotonic function, $\top\geqslant f(\top)\geqslant f^{2}(\top)=f(f(\top))\geqslant f^{3}(\top)\geqslant\ldots$ is a descending chain.

If the function is $\sqcap$-continuous, then $\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top)$ is by Kleene’s theorem the greatest fixed point of $f$, i.e. $f(\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top))=\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top)$ and $\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top)$ is larger than any other element $d$ with $f(d)=d$. We also say $\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top)$ 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 $\bigsqcap_{i\in{\mathbb{N}}}f^{i}(\top)=\bigsqcap_{i=0}^{i_{0}}f^{i}(\top)$ for some index $i_{0}$ in ${\mathbb{N}}$. With this, we can compute the greatest fixed point: Starting with $\top$, 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.

Finite Automata.

A non-deterministic finite automaton (NFA) is a tuple $A=(Q_{\mathit{NFA}},\Gamma,\delta,q_{0},Q_{f})$ where $Q_{\mathit{NFA}}$ is a finite set of states, $\Gamma$ is a finite alphabet, $\delta\subseteq Q_{\mathit{NFA}}\times\Gamma\times Q_{\mathit{NFA}}$ is a (non-deterministic) transition relation, $q_{0}\in Q_{\mathit{NFA}}$ is the initial state, and $Q_{f}\subseteq Q_{\mathit{NFA}}$ is a set of final states. We write $q\xrightarrow{a}{\to}q^{\prime}$ to denote $(q,a,q^{\prime})\in\delta$. Moreover, given a word $w=a_{1}\cdots a_{\ell}$, we write $q\xrightarrow{w}{\to}q^{\prime}$ whenever there is a sequence of transitions, also called run, $q_{1}\xrightarrow{a_{1}}{\to}q_{2}\xrightarrow{a_{2}}{\to}\cdots\xrightarrow{a_{\ell}}{\to}q_{\ell+1}$ with $q_{1}=q$ and $q_{\ell+1}=q^{\prime}$. The run is accepting if $q=q_{0}$ and $q^{\prime}\in Q_{f}$. The language of $A$ is \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)=\mathopen{}\mathclose{{}\left\{w\ \middle|\ q_{0}\xrightarrow{w}{\to}q\in Q_{f}}\right\}\ .

3. Higher-Order Recursion Schemes

We introduce higher-order 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 type-based approaches to higher-order model checking [40, 47, 41], 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 higher-order) function kinds are derived by composition:

[TABLE]

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 first-order kind defines functions that act on values, a second-order kind functions that expect functions as parameters. Formally, we have

[TABLE]

Let $K$ be the set of all kinds. Higher-order recursion schemes assign kinds to symbols from different alphabets, namely non-terminals, terminals, and variables. Let $\Gamma$ be a set of such kinded symbols. For each kind $\kappa$, we denote by $\Gamma^{\kappa}$ the restriction of $\Gamma$ to the symbols with kind $\kappa$. The terms $\mathcal{T}^{\kappa}(\Gamma)$ of kind $\kappa$ over $\Gamma$ are defined by simultaneous induction over all kinds. They form the smallest set satisfying

1. (1)

$\Gamma^{\kappa}\subseteq\mathcal{T}^{\kappa}(\Gamma)$, 2. (2)

\bigcup_{\kappa_{1}}\mathopen{}\mathclose{{}\left\{t\ v\ \middle|\ t\in\mathcal{T}^{\kappa_{1}\to\kappa_{2}}(\Gamma),v\in\mathcal{T}^{\kappa_{1}}(\Gamma)}\right\}\subseteq\mathcal{T}^{\kappa_{2}}(\Gamma), and 3. (3)

\mathopen{}\mathclose{{}\left\{\lambda x.t\ \middle|\ x\in\mathcal{T}^{\kappa_{1}}(\Gamma),t\in\mathcal{T}^{\kappa_{2}}(\Gamma)}\right\}\subseteq\mathcal{T}^{\kappa_{1}\to\kappa_{2}}(\Gamma).

If term $t$ is of kind $\kappa$, we also write $t\colon\kappa$. We use $\mathcal{T}(\Gamma)$ for the set of all terms over $\Gamma$. We say a term is $\lambda$-free if it contains no sub-term of the form $\lambda x.t$. A term is variable-closed if all occurring variables are bound by a preceding $\lambda$-expression.

Definition 3.1**.**

A higher-order recursion scheme, (scheme for short), is a tuple $G=(V,N,T,R,S)$, where $V$ is a finite set of kinded symbols called variables, $T$ is a finite set of kinded symbols called terminals, and $N$ is a finite set of kinded symbols called non-terminals with $S\in N$ the initial symbol. The sets $V$, $T$, and $N$ are pairwise disjoint. The finite set $R$ consists of rewriting rules of the form $F=\lambda x_{1}\ldots\lambda x_{n}.e$, where $F\in N$ is a non-terminal of kind $\kappa_{1}\to\ldots\kappa_{n}\to o$, $x_{1},\ldots,x_{n}\in V$ are variables of the required kinds, and $e$ is a $\lambda$-free, variable-closed term of ground kind from \mathcal{T}^{o}(T\mathop{\mathaccent 0{\cdot}\cup}N\mathop{\mathaccent 0{\cdot}\cup}\mathopen{}\mathclose{{}\left\{x_{1}\colon\kappa_{1},\ldots,x_{n}\colon\kappa_{n}}\right\}).

The semantics of $G$ is defined by rewriting subterms according to the rules in $R$. A context is a term C[\bullet]\in\mathcal{T}(\Gamma\mathop{\mathaccent 0{\cdot}\cup}\mathopen{}\mathclose{{}\left\{\bullet\colon o}\right\}) in which $\bullet$ occurs exactly once. Given a context $C[\bullet]$ and a term $t:o$, we obtain $C[t]$ by replacing the unique occurrence of $\bullet$ in $C[\bullet]$ by $t$. With this, $t\Rightarrow_{G}t^{\prime}$ if there is a context $C[\bullet]$, a rule $F=\lambda x_{1}\ldots\lambda x_{n}.e$, and a term $F\ t_{1}\ \ldots\ t_{n}:o$ such that $t=C[F\ t_{1}\ \ldots\ t_{n}]$ and t^{\prime}=C\mathopen{}\mathclose{{}\left[e[x_{1}\mapsto t_{1},\ldots,x_{n}\mapsto t_{n}]}\right]. In other words, we replace one occurrence of $F$ in $t$ by a right-hand side of a rewriting rule, while properly instantiating the variables. We call such a replaceable $F\ t_{1}\ \ldots\ 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 OI-language \mathcal{L}\mathopen{}\mathclose{{}\left(G}\right) 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 OI-rewriting steps. We will restrict the rewriting relation to OI-rewritings in the rest of this paper. Note, all words derivable by IO-rewriting are also derivable with OI-rewriting.

Word-Generating Schemes.

We consider word-generating schemes, i.e. schemes with terminals T\mathop{\mathaccent 0{\cdot}\cup}\mathopen{}\mathclose{{}\left\{\:o}\right}$where exactly one terminal symbol$$$has kind$o$and all others are of kind$o\to o$. The generated trees have the shape$a_{1}\ (a_{2}\ (\cdots\ (a_{k}\ $)))$, which we understand as the finite word$a_{1}a_{2}\ldots a_{k}\in T^{*}$. We also see$\mathcal{L}\mathopen{}\mathclose{{}\left(G}\right)$ as a language of finite words.

Determinism.

The above schemes are non-deterministic in that several rules may rewrite a non-terminal. We associate with a non-deterministic scheme $G=(V,N,T,R,S)$ a deterministic scheme $G^{\mathit{det}}$ with exactly one rule per non-terminal. Intuitively, $G^{\mathit{det}}$ makes the non-determinism explicit with new terminal symbols.

Formally, let $F:\kappa$ be a non-terminal with rules $F=t_{1}$ to $F=t_{\ell}$. We may assume each $t_{i}=\lambda x_{1}\ldots\lambda x_{k}.e_{i}$, where $e_{i}$ is $\lambda$-free. We introduce a new terminal symbol $\mathit{op}_{F}:o\to o\to\ldots\to o$ of arity $\ell$. Let the set of all these terminals be T^{\mathit{det}}=\mathopen{}\mathclose{{}\left\{\mathit{op}_{F}\ \middle|\ F\in N}\right\}. The set of rules $R^{\mathit{det}}$ now consists of a single rule for each non-terminal, namely $F=\lambda x_{1}\ldots\lambda x_{k}.\mathit{op}_{F}\ e_{1}\ \cdots\ e_{\ell}$. The original rules in $R$ are removed. This yields $G^{\mathit{det}}=(V,N,T\mathop{\mathaccent 0{\cdot}\cup}T^{\mathit{det}},R^{\mathit{det}},S)$. The advantage of resolving the non-determinism explicitly is that we can give a semantics to non-deterministic choices that depends on the non-terminal instead of having to treat non-determinism uniformly.

Semantics.

Let $G=(V,N,T,R,S)$ be a deterministic scheme. A model of $G$ is a pair $\mathcal{M}=(\mathcal{D},\mathcal{I})$, where $\mathcal{D}$ is a family of domains $(\mathcal{D}({\kappa}))_{\kappa\in K}$ that satisfies the following: $\mathcal{D}({o})$ is a cppo and $\mathcal{D}({\kappa_{1}\rightarrow\kappa_{2}})=\mathit{Cont}(\mathcal{D}({\kappa_{1}}),\mathcal{D}({\kappa_{2}}))$. Here, $\mathit{Cont}(A,B)$ is the set of all $\sqcap$-continuous functions from domain $A$ to $B$. We comment on this cppo in a moment. The interpretation $\mathcal{I}:T\rightarrow\mathcal{D}$ assigns to each terminal $s:\kappa$ an element $\mathcal{I}(s)\in\mathcal{D}({\kappa})$.

The ordering on functions is defined component-wise, $f\leqslant_{\kappa_{1}\to\kappa_{2}}g$ if $(f\ x)\leqslant_{\kappa_{2}}(g\ x)$ for all $x\in\mathcal{D}({\kappa_{1}})$. For each $\kappa$, we denote the top element of $\mathcal{D}({\kappa})$ by $\top_{\kappa}$. For the ground kind, $\top_{o}$ exists since $\mathcal{D}({\kappa})$ is a cppo, and $\top_{\kappa_{1}\to\kappa_{2}}$ is the function that maps every argument to $\top_{\kappa_{2}}$. The meet of a descending chain of functions $(f_{i})_{i\in{\mathbb{N}}}$ is the function defined by $(\bigsqcap_{\kappa_{1}\to\kappa_{2}}(f_{i})_{i\in{\mathbb{N}}})\ x=\bigsqcap_{\kappa_{2}}(f_{i}\ x)_{i\in{\mathbb{N}}}$. Note that the sequence on the right-hand side is a descending chain.

The semantics of terms defined by a model is a function

[TABLE]

that assigns to each term built over the non-terminals and terminals again a function. This function expects a valuation $\nu:N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D}$ and returns an element from the domain. A valuation is a partial function that is defined on all non-terminals and the free variables. We lift $\sqcap$ to descending chains of valuations with $(\bigsqcap_{i\in{\mathbb{N}}}\nu_{i})(y)=\bigsqcap_{i\in{\mathbb{N}}}(\nu_{i}(y))$ for $y\in N\mathop{\mathaccent 0{\cdot}\cup}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 right-hand sides of the rules in the scheme are variable-closed, 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:

[TABLE]

We show that \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket is $\sqcap$-continuous for all terms $t$. This follows from continuity of the functions in the domain, but requires some care when handling application.

Proposition 3.2**.**

For all $t$, \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket is $\sqcap$-continuous (in $\nu$) over the respective lattice.

Given $\mathcal{M}$, the rules $F_{1}=t_{1},\ldots,F_{k}=t_{k}$ of the (deterministic) scheme give a function

[TABLE]

Since the right-hand sides are variable-closed, the \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{j}}\right\rrbracket are functions in the non-terminals. Provided \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket to \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{k}}\right\rrbracket are $\sqcap$-continuous (in the valuation of the non-terminals), the function $\mathit{rhs}_{\mathcal{M}}$ will be $\sqcap$-continuous. This allows us to apply Kleene iteration as follows. The initial value is the greatest element $\sigma^{0}_{\mathcal{M}}$ where $\sigma^{0}_{\mathcal{M}}(F_{j})=\top_{j}$ with $\top_{j}$ the top element of $\mathcal{D}({\kappa_{j}})$. The $(i+1)\textsuperscript{th}$ approximant is computed by evaluating the right-hand side at the $i\textsuperscript{th}$ solution, $\sigma^{i+1}_{\mathcal{M}}=\mathit{rhs}_{\mathcal{M}}(\sigma_{\mathcal{M}}^{i})$. The greatest fixed point is the tuple $\sigma_{\mathcal{M}}$ defined below. It can be understood as the greatest solution to the equation $\nu=\mathit{rhs}_{\mathcal{M}}(\nu)$. We call this greatest solution $\sigma_{\mathcal{M}}$ the semantics of the scheme in the model.

[TABLE]

4. Higher-Order Inclusion Games

Our goal is to solve higher-order 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 non-terminals of a word-generating scheme into those owned by the existential player $\Diamond$ and those owned by the universal player $\Box$. Whenever a non-terminal 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 $\Diamond$ attempts to produce a word that is in \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right), while Player $\Box$ attempts to produce a word outside of \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right).

Definition 4.1**.**

A higher-order game is a triple $\mathcal{G}=(G,A,O)$ where $G$ is a word-generating scheme, $A$ is an NFA, $O:N\rightarrow\{\Diamond,\Box\}$ is a partitioning of the non-terminals of $G$.

A play of the game is a sequence of OI-rewriting 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}(\cdots(a_{k}(t))))$, where $t$ is either \$$ or a redex F\ t_{1}\ \cdots\ t_{m}$. If$O(F)=\Diamond$then Player$\Diamond$chooses a rule$F=\lambda x_{1}\ldots\lambda x_{m}.e$to apply, else Player$\Box$chooses the rule. This moves the play to$a_{1}\ (a_{2}\ (\cdots\ (a_{k}\ e[x_{1}\mapsto t_{1},\ldots,x_{m}\mapsto t_{m}])))$.

Each play begins at the initial non-terminal $S$, and continues either ad infinitum or until a term a_{1}\ (a_{2}\ (\cdots\ (a_{k}\ \)))$, understood as the word$w=a_{1}\ldots a_{k}$, is produced. Infinite plays do not produce a word and are won by Player$\Diamond$. Finite maximal plays produce such a word$w$. Player$\Diamond$wins whenever$w\in\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)$, Player$\Box$wins if$w\in\overline{\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)}$. Since the winning condition is Borel, either Player$\Diamond$or Player$\Box$ has a winning strategy [43].

Problem 4.2**.**

Our contribution is a fixed-point algorithm to decide $\mathsf{HOG}$. We derive it in three steps. First, we develop a concrete model for higher-order 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 $\mathsf{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 $\Diamond$’s winning strategy. We instantiate the framework for the concrete and abstract model to prove the soundness of the algorithm.

Concrete Semantics

Consider a $\mathsf{HOG}$ instance $\mathcal{G}=(G,A,O)$. Let $G^{\mathit{det}}$ be the determinized version of $G$. Our goal is to define a model $\mathcal{M}^{\mathit{C}}=(\mathcal{D}^{\mathit{C}},\mathcal{I}^{\mathit{C}})$ such that the semantics of $G^{\mathit{det}}$ in this model allows us to decide $\mathsf{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^{\ast}$. To be able to reuse the definition, we define formula domains in more generality as follows.

Domains of Boolean Formulas

Given a (potentially infinite) set $P$ of atomic propositions, the positive Boolean formulas \mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(P}\right)} over $P$ are defined to contain $\mathsf{true}$, every $p$ from $P$, and compositions of formulas via conjunction and disjunction. We work up to logical equivalence, which means we treat $\phi_{1}$ and $\phi_{2}$ as equal as long as they are logically equivalent.

Unfortunately, if the set $P$ is infinite, \mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(P}\right)} 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 {\mathcal{P}}\mathopen{}\mathclose{{}\left(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)}}\right)\setminus\mathopen{}\mathclose{{}\left\{\emptyset}\right\} factorized modulo logical equivalence, denoted ({\mathcal{P}}\mathopen{}\mathclose{{}\left(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)}}\right)\setminus\mathopen{}\mathclose{{}\left\{\emptyset}\right\})/_{\Leftrightarrow}. To be precise, the sets may be finite or infinite, but they must be non-empty.

To define the factorization, let an assignment to the atomic propositions be given by a subset of $P^{\prime}\subseteq P$. The atomic proposition $p$ is true if $p\in P^{\prime}$. 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 $\Phi_{1}$ and $\Phi_{2}$, we write $\Phi_{1}\Rightarrow\Phi_{2}$, if every assignment that satisfies $\Phi_{1}$ also satisfies $\Phi_{2}$. Two sets of formulas are equivalent, denoted $\Phi_{1}\Leftrightarrow\Phi_{2}$, if $\Phi_{1}\Rightarrow\Phi_{2}$ and $\Phi_{2}\Rightarrow\Phi_{1}$ holds.

The ordering on these factorized sets is implication (which by transitivity is independent of the representative). The top element is the set \mathopen{}\mathclose{{}\left\{\mathsf{true}}\right\}, 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 \Phi_{1}\vee\Phi_{2}=\mathopen{}\mathclose{{}\left\{\phi_{1}\vee\phi_{2}\ \middle|\ \phi_{1}\in\Phi_{1},\phi_{2}\in\Phi_{2}}\right\}. 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 well-defined.

In our case, the assignment $P^{\prime}\subseteq T^{*}$ of interest is the language of the automaton $A$. Player $\Diamond$ will win the game iff the concrete semantics assigns a set of formulas to $S$ that is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right).

The Concrete Domains and Interpretation of Terminals.

From a ground domain, higher-order domains are defined as continuous functions as in Section 3. Thus we only need

[TABLE]

The endmarker \$$ yields the set of formulas \mathopen{}\mathclose{{}\left{\varepsilon}\right}$, i.e.$\mathcal{I}^{\mathit{C}}($)=\mathopen{}\mathclose{{}\left{\varepsilon}\right}$. A terminal$a:o\to o$prepends$a$to a given word$w$. That is$\mathcal{I}^{\mathit{C}}(a)=\mathsf{prepend}{a}$, where$\mathsf{prepend}{a}$ distributes over conjunction and disjunction:

[TABLE]

We apply $\mathsf{prepend}_{a}$ to sets of formulas by applying it to every element. Finally, $\mathcal{I}^{\mathit{C}}(\mathit{op}_{F})$ where $\mathit{op}_{F}$ has arity $\ell$ is an $\ell$-ary conjunction (resp. disjunction) if Player $\Box$ (resp. $\Diamond$) owns $F$.

For $\mathcal{M}^{\mathit{C}}=(\mathcal{D}^{\mathit{C}},\mathcal{I}^{\mathit{C}})$ to be a model, we need our interpretation of terminals to be $\sqcap$-continuous. This follows largely by the distributivity of our definitions.

Lemma 4.3**.**

For all non-ground terminals $s$, $\mathcal{I}^{\mathit{C}}(s)$ is $\sqcap$-continuous.

Example 4.4**.**

Consider the higher-order game defined by the scheme S=H\ a\ \\ |\ b\ $$and$H=\lambda f.\lambda x.f\ (f\ x)\ |\ \lambda f.\lambda x.H\ (H\ f)\ x$. Assume$S$is owned by Player$\Diamond$and$H$is owned by Player$\Box$. Let the automaton accept the language$\mathopen{}\mathclose{{}\left{b}\right}$. Player$\Diamond$can choose to rewrite$S$to$b\ $$and therefore has a strategy to produce a word in the language. To derive this information from the concrete semantics, we compute$\sigma_{\mathcal{M}^{\mathit{C}}}(H)$. It is the function mapping$f\in\mathit{Cont}(\mathcal{D}^{\mathit{C}}(o),\mathcal{D}^{\mathit{C}}(o))$and$d\in\mathcal{D}^{\mathit{C}}(o)$to$\bigcup_{k>0}f^{2k}(d)$. Note that the union is the conjunction of sets of formulas, which is the interpretation of$\mathit{op}_{H}$for the universal player. Moreover, note that due to non-determinism we obtain all even numbers of applications of$f$, not only the powers of$2$. With this, the semantics of the initial symbol is

[TABLE]

The assignment \mathopen{}\mathclose{{}\left\{b}\right\} given by the language of the NFA satisfies \mathopen{}\mathclose{{}\left\{a^{2k}\vee b\ \middle|\ k>0}\right\}. Indeed, since $b$ evaluates to true, every formula in the set evaluates to true.

Correctness of Semantics and Winning Strategies.

We need to show that the concrete semantics matches the original semantics of the game.

Theorem 4.5**.**

$\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) iff there is a winning strategy for Player $\Diamond$.

When $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) the concrete semantics gives a winning strategy for $\Diamond$: From a term $t$ such that \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \sigma_{\mathcal{M}^{\mathit{C}}} is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right), Player $\Diamond$, when able to choose, picks a rewrite rule that transforms $t$ to $t^{\prime}$, where \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ \sigma_{\mathcal{M}^{\mathit{C}}} remains satisfied. The proof of Theorem 4.5 shows this is always possible, and, moreover, Player $\Box$ is unable to reach a term for which satisfaction does not hold. This does not yet give an effective strategy since we cannot compute \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \sigma_{\mathcal{M}^{\mathit{C}}}. However, the abstract semantics will be computable, and can be used in place of the concrete semantics by Player $\Diamond$ to implement the winning strategy.

The proof that $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ being unsatisfied implies a winning strategy for Player $\Box$ 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.

5. Framework for Exact Fixed-Point Transfer

The concrete model $\mathcal{M}^{\mathit{C}}$ does not lead to an algorithm for solving $\mathsf{HOG}$ since its domains are infinite. Here, we consider an abstract model $\mathcal{M}^{\mathit{A}}$ with finite domains. The soundness of the resulting Kleene iteration relies on the two semantics being related by a precise abstraction $\alpha$. Since both semantics are defined by fixed points, this requires us to prove $\alpha(\sigma_{\mathcal{M}^{\mathit{C}}})=\sigma_{\mathcal{M}^{\mathit{A}}}$. In this section, we provide a general framework to this end.

Consider the deterministic scheme $G$ together with two models (left and right) $\mathcal{M}_{l}\leavevmode\nobreak\ =\leavevmode\nobreak\ (\mathcal{D}_{l},\mathcal{I}_{l})$ and $\mathcal{M}_{r}=(\mathcal{D}_{r},\mathcal{I}_{r})$. Our goal is to relate the semantics in these models in the sense that $\sigma_{\mathcal{M}_{r}}=\alpha(\sigma_{\mathcal{M}_{l}})$. Such exact fixed-point transfer results are well-known in abstract interpretation. To generalize them to higher-order we give easy to instantiate conditions on $\alpha$, $\mathcal{M}_{l}$, and $\mathcal{M}_{r}$ that yield the above equality. Interestingly, exact fixed-point transfer results seem to be rare for higher-order (e.g. [47]). 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 fixed-point transfer results.

For the terminology, an abstraction is a function $\alpha:\mathcal{D}_{l}(o)\rightarrow\mathcal{D}_{r}(o)$. To lift the abstraction to function domains, we define the notion of being compatible with $\alpha$. 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, $\alpha(f)\ \alpha(v_{l})=\alpha(f\ v_{l})$. Compatibility ensures the independence of the choice of $v_{l}$.

By definition, all ground elements $v_{l}\in\mathcal{D}_{l}(o)$ are compatible with $\alpha$. For function domains, compatibility and the abstraction are defined as follows.

Definition 5.1**.**

Assume $\alpha$ and the notion of compatibility are defined on $\mathcal{D}_{l}(\kappa_{1})$ and $\mathcal{D}_{l}(\kappa_{2})$. Let $\top^{l}_{\kappa}$ (resp. $\top^{r}_{\kappa}$) be the greatest element of $\mathcal{D}_{l}(\kappa)$ (resp. $\mathcal{D}_{r}(\kappa)$) for each $\kappa$.

1. (1)

Function $f\in\mathcal{D}_{l}(\kappa_{1}\rightarrow\kappa_{2})$ is compatible with $\alpha$, if

1. (a)

for all compatible $v_{l},v_{l}^{\prime}\in\mathcal{D}_{l}(\kappa_{1})$ with $\alpha(v_{l})=\alpha(v_{l}^{\prime})$ we have $\alpha(f\ v_{l})=\alpha(f\ v_{l}^{\prime})$, and 2. (b)

for all compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ we have that $f\ v_{l}$ is compatible. 2. (2)

We define $\alpha(f)\in\mathcal{D}_{r}(\kappa_{1}\rightarrow\kappa_{2})$ as follows.

1. (a)

If $f$ is compatible, we set $\alpha(f)\ v_{r}=\alpha(f\ v_{l})$, provided there is a compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ with $v_{r}=\alpha(v_{l})$, and $\alpha(f)\ v_{r}=\top^{r}_{\kappa_{2}}$ otherwise. 2. (b)

If $f$ is not compatible, $\alpha(f)=\top^{r}_{\kappa_{1}\rightarrow\kappa_{2}}$.

We lift $\alpha$ to valuations $\nu:N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D}_{l}$ by $\alpha(\nu)(F)=\alpha(\nu(F))$ and similar for $x$. We also lift compatibility to valuations $\nu:N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D}_{l}$ by requiring $\nu(F)$ to be compatible for all $F\in N$ and similar for $x\in V$.

The conditions needed for the exact fixed-point transfer are the following.

Definition 5.2**.**

Function $\alpha$ is precise for $\mathcal{M}_{l}$ and $\mathcal{M}_{r}$, if

• $(\mathsf{P1})$

$\alpha(\mathcal{D}_{l}(o))=\mathcal{D}_{r}(o)$,

• $(\mathsf{P2})$

$\alpha:\mathcal{D}_{l}(o)\rightarrow\mathcal{D}_{r}(o)$ is $\sqcap$-continuous,

• $(\mathsf{P3})$

$\alpha(\top^{l}_{o})=\top^{r}_{o}$,

• $(\mathsf{P4})$

$\alpha(\mathcal{I}_{l}(s))=\mathcal{I}_{r}(s)$ for all terminals $s\colon o$, and similarly $\alpha(\mathcal{I}_{l}(s)\ v_{l})=\mathcal{I}_{r}(s)\ \alpha(v_{l})$ for all terminals $s:\kappa_{1}\rightarrow\kappa_{2}$ and all compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$,

• $(\mathsf{P5})$

$\mathcal{I}_{l}(s)\ v_{l}$ is compatible for all terminals $s:\kappa_{1}\rightarrow\kappa_{2}$, and all compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$.

$(\mathsf{P1})$ is surjectivity of $\alpha$. $(\mathsf{P2})$ states that $\alpha$ is well-behaved wrt. $\sqcap$. $(\mathsf{P3})$ says that the greatest element is mapped as expected. Note that $(\mathsf{P1})$-$(\mathsf{P3})$ are only posed for the ground domain. One can prove that they generalize to function domains by the definition of function abstraction. $(\mathsf{P4})$ is that the interpretations of terminals in $\mathcal{M}^{\mathit{C}}$ and $\mathcal{M}^{\mathit{A}}$ are suitably related. Finally $(\mathsf{P5})$ is compatibility. $(\mathsf{P4})$ and $(\mathsf{P5})$ are generalized to terms in Lemma 5.3.

To prove $\alpha(\sigma_{\mathcal{M}_{l}})=\sigma_{\mathcal{M}_{r}}$, we need that $\mathit{rhs}_{\mathcal{M}_{r}}$ is an exact abstract transformer of $\mathit{rhs}_{\mathcal{M}_{l}}$. 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 \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket compatible with $\alpha$. With this result, we obtain the required exact fixed-point transfer for precise abstractions.

Lemma 5.3**.**

Assume $(\mathsf{P1})$, $(\mathsf{P4})$, and $(\mathsf{P5})$ hold. For all terms $t$ and all compatible $\nu$, we have \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \nu compatible and \alpha(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \nu)=\mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \alpha(\nu).

Theorem 5.4** (Exact Fixed-Point Transfer).**

Let $G$ be a scheme with models $\mathcal{M}_{l}$ and $\mathcal{M}_{r}$. Let $\sigma_{l}$ and $\sigma_{r}$ be the corresponding semantics. If $\alpha:\mathcal{D}_{l}\rightarrow\mathcal{D}_{r}$ is precise, we have $\sigma_{r}=\alpha(\sigma_{l})$.

6. Domains for Higher-Order Games

We propose two domains, abstract and optimized, that allow us to solve $\mathsf{HOG}$. The computation is a standard fixed-point iteration, and, in the optimized domain, this iteration has optimal complexity. Correctness follows by instantiating the previous framework.

Abstract Semantics.

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 5.4. Combined with Theorem 4.5, this will allow us to solve $\mathsf{HOG}$. Computable in particular means the domain should be finite and the operations should be efficiently computable.

We define the $\mathcal{M}^{\mathit{A}}=(\mathcal{D}^{\mathit{A}},\mathcal{I}^{\mathit{A}})$ as follows. Again, we resolve the non-determinism 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 \mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)=\mathopen{}\mathclose{{}\left\{q\ \middle|\ q\xrightarrow{w}{\to}q_{f}\in Q_{f}}\right\}. For a language $L$ we have \mathsf{acc}\mathopen{}\mathclose{{}\left(L}\right)=\mathopen{}\mathclose{{}\left\{\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)\ \middle|\ w\in L}\right\}. The abstract domain for terms of ground kind is \mathcal{D}^{\mathit{A}}(o)=\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)}\right)}. The lifting to functions is as explained in Section 3. Satisfaction is now defined relative to a set $\Omega$ of elements of {\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right) (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 $\mathsf{true}$.

The interpretation of ground terms is \mathcal{I}^{\mathit{A}}(\)=Q_{f}$and$\mathcal{I}^{\mathit{A}}(a)=\mathsf{pre}{a}$. Here$\mathsf{pre}{a}$is the predecessor computation under label$a$,$\mathsf{pre}{a}(Q)=\mathopen{}\mathclose{{}\left{q^{\prime}\in Q{\mathit{NFA}}\ \middle|\ q^{\prime}\xrightarrow{a}{\to}q\in Q}\right}$. 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 non-terminal. Since we restrict the atomic propositions to$\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)$, we have to show that the interpretations use only this restricted set. Proving$\mathcal{I}^{\mathit{A}}(s)$is$\sqcap$-continuous is standard.

Lemma 6.1**.**

The interpretations are defined on the abstract domain.

Lemma 6.2**.**

For all terminals $s$, $\mathcal{I}^{\mathit{A}}(s)$ is $\sqcap$-continuous over the respective lattices.

Recall our concrete model is $\mathcal{M}^{\mathit{C}}=(\mathcal{D}^{\mathit{C}},\mathcal{I}^{\mathit{C}})$, where \mathcal{D}^{\mathit{C}}={\mathcal{P}}\mathopen{}\mathclose{{}\left(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)}}\right). To relate this model to $\mathcal{M}^{\mathit{A}}$, we define the abstraction function $\alpha:\mathcal{D}^{\mathit{C}}(o)\rightarrow\mathcal{D}^{\mathit{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 $\alpha$ on \mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)} by $\alpha(\Phi)=\bigwedge_{\phi\in\Phi}\alpha(\phi)$ for a set of formulas \Phi\in{\mathcal{P}}\mathopen{}\mathclose{{}\left(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(T^{*}}\right)}}\right), and

[TABLE]

This definition is suitable in that $\alpha(\sigma_{\mathcal{M}^{\mathit{C}}})=\sigma_{\mathcal{M}^{\mathit{A}}}$ entails the following.

Theorem 6.3**.**

$\sigma_{\mathcal{M}^{\mathit{A}}}(S)$ is satisfied by \mathopen{}\mathclose{{}\left\{Q\in\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)\ \middle|\ q_{0}\in Q}\right\} iff Player $\Diamond$ wins $\mathcal{G}$.

To see that the theorem is a consequence of the exact fixed-point transfer, observe that \mathopen{}\mathclose{{}\left\{Q\in\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)\ \middle|\ q_{0}\in Q}\right\}=\mathsf{acc}\mathopen{}\mathclose{{}\left(\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)}\right). Then, by $\sigma_{\mathcal{M}^{\mathit{A}}}=\alpha(\sigma_{\mathcal{M}^{\mathit{C}}})$ we have \mathsf{acc}\mathopen{}\mathclose{{}\left(\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)}\right) satisfies $\sigma_{\mathcal{M}^{\mathit{A}}}(S)$ iff it also satisfies $\alpha(\sigma_{\mathcal{M}^{\mathit{C}}}(S))$. This holds iff \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) satisfies $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ (a simple induction over formulas). By Theorem 4.5, this occurs iff Player $\Diamond$ wins the game.

It remains to establish $\alpha(\sigma_{\mathcal{M}^{\mathit{C}}})=\sigma_{\mathcal{M}^{\mathit{A}}}$. With the framework, the exact fixed-point transfer follows from precision, Theorem 5.4. The proof of the following is routine.

Proposition 6.4**.**

$\alpha$ is precise. Hence, $\alpha(\sigma_{\mathcal{M}^{\mathit{C}}})=\sigma_{\mathcal{M}^{\mathit{A}}}$.

Optimized Semantics.

The above model yields a decision procedure for $\mathsf{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 order-$k$ symbol is only $(k+1)$-times exponentially high. The idea is to resolve the atomic propositions in $\mathcal{M}^{\mathit{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 \alpha:\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)}\right)}\rightarrow\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}. The optimized domain will then be based on the image of $\alpha$. This guarantees surjectivity. For a set of states $Q$, we define $\alpha(Q)=\bigvee Q=\bigvee_{q\in Q}q$. For a formula, the abstraction function is defined to distribute over conjunction and disjunction. The optimized model is $\mathcal{M}^{\mathit{O}}=(\mathcal{D}^{\mathit{O}},\mathcal{I}^{\mathit{O}})$ with ground domain \alpha(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)}\right)}). The interpretation is \mathcal{I}^{\mathit{O}}(\)=\bigvee Q_{f}$. For$a$, we resolve the set of predecessors into a disjunction,$\mathcal{I}^{\mathit{O}}(a)\ q=\bigvee\mathsf{pre}{a}(\mathopen{}\mathclose{{}\left{q}\right})$. The function distributes over conjunction and disjunction. Finally,$\mathcal{I}^{\mathit{O}}(\mathit{op}{F})$is conjunction or disjunction of formulas, depending on the owner of the non-terminal. 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$\sqcap$-continuous as required.

Lemma 6.5**.**

The interpretations are defined on the optimized domain.

Lemma 6.6**.**

For all terminals $s$, $\mathcal{I}^{\mathit{O}}(s)$ is $\sqcap$-continuous over the respective lattices.

We again show precision, enabling the required exact fixed-point transfer.

Proposition 6.7**.**

$\alpha$ is precise. Hence, $\alpha(\sigma_{\mathcal{M}^{\mathit{A}}})=\sigma_{\mathcal{M}^{\mathit{O}}}$.

Theorem 6.8**.**

$\sigma_{\mathcal{M}^{\mathit{O}}}(S)$ is satisfied by \mathopen{}\mathclose{{}\left\{q_{0}}\right\} iff Player $\Diamond$ wins $\mathcal{G}$.

It is sufficient to show $\sigma_{\mathcal{M}^{\mathit{A}}}(S)$ is satisfied by \mathopen{}\mathclose{{}\left\{Q\in\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)\ \middle|\ q_{0}\in Q}\right\} iff $\sigma_{\mathcal{M}^{\mathit{O}}}(S)$ is satisfied by \mathopen{}\mathclose{{}\left\{q_{0}}\right\}. Theorem 6.3 then yields the statement. Propositions $Q$ in $\sigma_{\mathcal{M}^{\mathit{A}}}(S)$ are resolved into disjunctions $\bigvee Q$ in $\sigma_{\mathcal{M}^{\mathit{O}}}(S)$. For such a proposition, we have Q\in\mathopen{}\mathclose{{}\left\{Q\in\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)\ \middle|\ q_{0}\in Q}\right\} iff $\bigvee Q$ is satisfied by \mathopen{}\mathclose{{}\left\{q_{0}}\right\}. This equivalence propagates to the formulas $\sigma_{\mathcal{M}^{\mathit{A}}}(S)$ and $\sigma_{\mathcal{M}^{\mathit{O}}}(S)$ as the Boolean structure coincides. The latter follows from $\alpha(\sigma_{\mathcal{M}^{\mathit{A}}}(S))=\sigma_{\mathcal{M}^{\mathit{O}}}(S)$.

Complexity.

To solve $\mathsf{HOG}$, we compute the semantics $\sigma_{\mathcal{M}^{\mathit{O}}}$ and then evaluate $\sigma_{\mathcal{M}^{\mathit{O}}}(S)$ at the assignment \mathopen{}\mathclose{{}\left\{q_{0}}\right\}. For the complexity, assume that the highest order of any non-terminal in $\mathcal{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 $\mathcal{D}^{\mathit{O}}$.

Proposition 6.9**.**

The semantics $\sigma_{\mathcal{M}^{\mathit{O}}}$ can be computed in $(k+1)\mathsf{EXP}$, where $k$ is the highest order of any non-terminal in the input scheme.

The lower bound is via a reduction from the word membership problem for alternating $k$-iterated pushdown automata with polynomially-bounded auxiliary work-tape. This problem was shown by Engelfriet to be $(k+1)\mathsf{EXP}$-hard. We can reduce this problem to $\mathsf{HOG}$ via well-known translations between iterated stack automata and recursion schemes, using the regular language specifying the winning condition to help simulate the work-tape.

Proposition 6.10**.**

Determining whether Player $\Diamond$ wins $\mathcal{G}$ is $(k+1)\mathsf{EXP}$-hard for $k>0$.

Together, these results show the following corollary and final result.

Corollary 6.11**.**

$\mathsf{HOG}$ is $(k+1)\mathsf{EXP}$-complete for order-$k$ schemes and $k>0$.

Appendix A Relation to Higher-Order Model Checing

We elaborate on the relation of our work to the influential line of research on intersection types as pioneered by [41]. 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 well-typed type environment can be certificate for the non-emptiness of the intersection \mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{scheme}}\right)\cap\mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{Automaton}}\right)\neq\emptyset. If the HORS is deterministic, \mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{scheme}}\right) consists of a single tree, so this is also decides the inclusion \mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{scheme}}\right)\subseteq\mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{Automaton}}\right). If we naively extend intersection types to non-deterministic 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. \mathcal{L}\mathopen{}\mathclose{{}\left(\mathit{scheme}}\right)\cap\mathcal{L}\mathopen{}\mathclose{{}\left(\overline{\mathit{Automaton}}}\right)=\emptyset. Note that a well-typing (a well-typed 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 non-existence 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 well-typing and does not prove anything. Therefore, an algorithm that decides the non-emptiness of the intersection by using intersection-types has to guarantee that it constructs a well-typing 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 non-deterministic 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 re-normalizing it to DNF can lead to an exponential blowup.

Work by Neatherway et al. [45] and Ramsay [47] considers schemes with non-determinism in the form of case statements. To handle this non-determinism 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 non-deterministic schemes against non-deterministic trivial automata using abstract interpretation from schemes to types. In our work, we generalise non-determinism to games (played over word-generating schemes), with a non-deterministic target language.

Appendix B Proofs for Section 3

B.1. Proof of Proposition 3.2

Proof B.1**.**

Let \mathopen{}\mathclose{{}\left(\nu_{i}}\right)_{i\in{\mathbb{N}}} be a descending chain of evaluations, i.e. $\nu_{i}\geqslant\nu_{i+1}$ for all $i\in{\mathbb{N}}$. It is to show that for all $t$, \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket is $\sqcap$-continuous (in the argument $\nu$) over the respective lattice, i.e.

[TABLE]

We proceed by induction over $t$.

1. (1)

**Case $t=F$ or $t=x$.

**Both of these cases are identical, hence we only show the former. We have

[TABLE]

where the first and final equalities are by definition of the concrete semantics, and the second is by definition of $\sqcap$ over valuations $\nu_{i}$. 2. (2)

**Case $t=s$ for some terminal $s$.

**Similar to the previous case, we have

[TABLE]

by definition. 3. (3)

**Case $t=t_{1}\ t_{2}$.

**We have

[TABLE]

We have to argue the step indicated above. That is,

[TABLE]

The right-hand side is greater than the left-hand side, because terms of the form ((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{j})) where $\nu_{i}\neq\nu_{j}$ are missing in the RHS. To see that it is in fact equal, note that for two indices $i,j\in{\mathbb{N}}$, we have either $\nu_{i}\leqslant\nu_{j}$ or $\nu_{j}\leqslant\nu_{i}$, since the valuations form a descending chain. Let m=\min\mathopen{}\mathclose{{}\left\{i,j}\right\}. We now use that $\sqcap$-continuity implies monotonicity, and thus we have

[TABLE]

Hence, for any expression ((\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu_{i})\ (\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu_{j})) that is missing in the meet in the RHS, the meet in the RHS contains an expression that is smaller, hence, they are equal. 4. (4)

**Case $t=\lambda x.t^{\prime}$.

**We have

[TABLE]

B.2. Substitution Lemma

Since we have not syntactically defined the evaluation of a $\lambda$-term, our development will need a simple substitution lemma.

Lemma B.2**.**

For all $\nu:N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D}$, we have \mathcal{M}\mathopen{}\mathclose{{}\left\llbracket(\lambda x.t)\ t^{\prime}}\right\rrbracket\ \nu=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}.

Proof B.3**.**

We show that for all $\nu:N\mathop{\mathaccent 0{\cdot}\cup}V\nrightarrow\mathcal{D}$ and all suitable terms $t,t^{\prime}$, we have

[TABLE]

We have by definition

[TABLE]

and show by induction over $t$ that

[TABLE]

In the base cases we have

1. (1)

\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=\mathopen{}\mathclose{{}\left(\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}\right)(F)=\nu(F)=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket F[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}, 2. (2)

\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=\mathcal{I}(s)=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket s[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}, 3. (3)

\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket x}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket x[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}, and 4. (4)

\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket y}\right\rrbracket\ {\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}=\mathopen{}\mathclose{{}\left(\nu[x\mapsto\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu}]}\right)(y)=\nu(y)=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket y}\right\rrbracket\ {\nu}=\mathcal{M}\mathopen{}\mathclose{{}\left\llbracket y[x\mapsto t^{\prime}]}\right\rrbracket\ {\nu}, for variable $y\neq x$.

Then, for the induction step, we first consider application. That is

[TABLE]

which is equal to, by induction,

[TABLE]

Finally, for abstraction, we can assume by $\alpha$-conversion that $y\neq x$, and we have

[TABLE]

which is by induction equal to the function

[TABLE]

Thus, by induction, we have the lemma as required.

Appendix C Proofs for Section 4

C.1. Proof of Lemma 4.3

Proof C.1**.**

We show that for all non-ground terminals $s$, $\mathcal{I}^{\mathit{C}}(s)$ is $\sqcap$-continuous. We need to treat the terminals $a\colon o\to o$ of the original scheme and the terminals $\mathit{op}_{F}$ that were introduced for the determinisation separately. In each case, assume a descending chain of arguments $(x_{i})_{i\in{\mathbb{N}}}$.

1. (1)

**Case $s=a$.

**Since $\mathcal{I}^{\mathit{C}}(a)=\mathsf{prepend}_{a}$ and we have

[TABLE]

by definition of $\mathsf{prepend}_{a}$, we have the property as required. 2. (2)

**Case $s=\mathit{op}_{F}$.

**We show the property when $\mathit{op}_{F}$ is owned by $\Diamond$, and thus interpreted as $\ell$-fold disjunction, conjunction is similar. We proceed by induction on the arity $\ell$. In the base case $\ell=1$, $\mathcal{I}^{\mathit{C}}(\mathit{op}_{F})$ is the identity function that is $\sqcap$-continuous

Now assume $\mathit{op}_{F}$ has arity $\ell+1$, and $\mathcal{I}^{\mathit{C}}(\mathit{op}_{F})=\bigvee{}_{\!\ell+1}$ is an $\ell+1$-fold disjunction. We have

[TABLE]

In the above we required $\vee$ to distribute over $\sqcap$, which can be seen by induction over types. In the base case, that $\vee$ distributes over $\sqcap=\wedge$ is standard. For the step case, we have for all $f_{i}$, $g$, and $v$

[TABLE]

C.2. Proof of Theorem 4.5

We are required to show $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) iff there is a winning strategy foryer Player $\Diamond$. The theorem is shown in the following two lemmas.

First, we introduce some notation. We write $\mathsf{prepend}_{w}$ for $w=a_{1}\ldots a_{n}$ to abbreviate $\mathsf{prepend}_{a_{1}}\circ\cdots\circ\mathsf{prepend}_{a_{n}}$.

Lemma C.2** (Player $\Diamond$).**

If $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) there is a winning strategy for $\Diamond$.

Proof C.3**.**

In what follows, whenever we refer to a term $t$, we mean a term built over $N\mathop{\mathaccent 0{\cdot}\cup}T$, but not over $T^{\mathit{det}}$. The terminals $\mathit{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 $\Diamond$ that maintains the invariant that the current (variable-free) term $t$ reached is such that \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \sigma_{\mathcal{M}^{\mathit{C}}} is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). All plays are infinite or generate a word $w$. Since we maintain \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}} is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right), if $t$ represents a word $w$, we know $w$ is accepted by $A$ and Player $\Diamond$ wins the game.

Initially, we have \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket S}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}}=\sigma_{\mathcal{M}^{\mathit{C}}}(S) which is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) by assumption. Thus, suppose play reaches a term $t$ such that \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}} is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). There are two cases.

In the first case t=a_{1}\ (\cdots\ (a_{n}\ \))$and let$w=a_{1}\ldots a_{n}$. Since

[TABLE]

and $w$ is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right), we know w\in\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) and Player $\Diamond$ has won the game.

In the second case, we have $t=a_{1}(\cdots(a_{n}(F\ t_{1}\cdots t_{m})))$. By assumption, we know

[TABLE]

is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). Let $F=e_{1}$, …, $F=e_{\ell}$ be the rewrite rules for $F$. There are two subcases.

1. (1)

If $F$ is owned by $\Diamond$, then since \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket=\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{1}}\right\rrbracket\lor\cdots\lor\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{\ell}}\right\rrbracket there must exist some $i$ such that

[TABLE]

is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). The strategy of Player $\Diamond$ is to choose the $i\textsuperscript{th}$ rewrite rule.

We need to show the invariant is maintained. Let $e_{i}=\lambda x_{1},\ldots,x_{m}.e$. We have (using the substitution lemma, Lemma B.2),

[TABLE]

Note that the term $a_{1}(\cdots(a_{n}(e[x_{1}\mapsto t_{1},\ldots,x_{m}\mapsto t_{m}])))$ is the result of Player $\Diamond$ rewriting $F$ via $F=e_{i}$. Since the satisfaction by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) passes through the equalities, Player $\Diamond$’s move maintains the invariant as required. 2. (2)

If $F$ is owned by $\Box$ the argument proceeds as in the previous case. The key difference is that we have to show satisfaction is maintained no matter which move $\Box$ chooses. However, since in this case \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket=\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{1}}\right\rrbracket\land\cdots\land\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{\ell}}\right\rrbracket then for all $i$ we have

[TABLE]

is satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). The remainder of the argument is identical.

Lemma C.4** (Player $\Box$).**

If $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is not satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) there is a winning strategy for $\Box$.

Proof C.5**.**

In what follows, whenever we refer to a term $t$, we mean a term built over $N\mathop{\mathaccent 0{\cdot}\cup}T$, but not over $T^{\mathit{det}}$. The terminals $\mathit{op}_{F}$ are excluded because they do not occur in the game, they are only introduced in the determinized scheme.

For $\phi\in\mathcal{D}^{\mathit{C}}(o)$ and a variable-closed term $t$ of kind $o$, we define $\phi$ to be sound for $t$, denoted $\phi\vdash t$, if for all $w\in T^{*}$ such that $\mathsf{prepend}_{w}(\phi)$ is not satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right), Player $\Box$ has a winning strategy from term $w(t)$. For $w=\varepsilon$, we set $\mathsf{prepend}_{\varepsilon}(\phi)=\phi$ and let $\varepsilon(t)=t$. We can now restate the lemma as

[TABLE]

In particular, since $\sigma_{\mathcal{M}^{\mathit{C}}}(S)$ is not satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) it is the case that $\mathsf{prepend}_{\varepsilon}(\sigma_{\mathcal{M}^{\mathit{C}}}(S))$ is not satisfied. This means Player $\Box$ has a winning strategy from $\varepsilon(S)=S$.

In general, for $\Xi\in\mathcal{D}^{\mathit{C}}(\kappa_{1}\to\kappa_{2})$, we will also define $\Xi\vdash t$ for terms of kind $\kappa_{1}\to\kappa_{2}$. That is, for a variable-closed term $t$ of kind $\kappa_{1}\to\kappa_{2}$ and a function $\Xi\in\mathcal{D}^{\mathit{C}}(\kappa_{1}\to\kappa_{2})$, we define $\Xi\vdash t$ to hold whenever for all variable-closed terms $t^{\prime}$ of kind $\kappa_{1}$ and $\Xi^{\prime}\in\mathcal{D}^{\mathit{C}}(\kappa_{1})$ such that $\Xi^{\prime}\vdash t^{\prime}$ we have $\Xi\ \Xi^{\prime}\vdash t\ t^{\prime}$:

[TABLE]

Similarly, we need to extend $\vdash$ to terms $t$ with free variables $\vec{x}=x_{1}\ldots x_{m}$. Here, we make the free variables explicit and write $t(\vec{x})$. We define for $\Xi:(V\nrightarrow\mathcal{D}^{\mathit{C}})\rightarrow\mathcal{D}^{\mathit{C}}$ that $\Xi\vdash t(\vec{x})$ by requiring that for any variable-closed terms $t_{1},\ldots,t_{m}$ and any $\Xi_{1},\ldots,\Xi_{m}\in\mathcal{D}^{\mathit{C}}$ with $\Xi_{j}\vdash t_{j}$ for all $1\leqslant j\leqslant m$, we have $\Xi\ \nu\vdash t[\forall j\colon x_{j}\mapsto t_{j}]$, where $\nu$ maps $x_{j}$ to $\Xi_{j}$.

We now show the following. For every number of iterations $i$ in the fixed-point calculation, we have \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}^{i}}\vdash t, for all terms $t$ built over the terminals and non-terminals 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 non-closed terms, we will have to extend $\sigma_{\mathcal{M}^{\mathit{C}}}^{i}$ to assign valuations to free-variables. Thus we will write $\nu^{i}$ to denote a valuation such that $\nu^{i}(F)=\sigma_{\mathcal{M}^{\mathit{C}}}^{i}(F)$ for any non-terminal $F$.

Base case $i$.

In the base case, we have $i=0$ and $\nu^{i}=\top$ for all non-terminals. 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 non-terminals.

Base case $t$.

The base cases of the inner induction that are independent of the iteration count are the following.

1. (1)

**Case $t=$$.

**For all $i$, we have \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket\}\right\rrbracket\ {\nu^{i}}=\varepsilon$. Take any word$w$such that$\mathsf{prepend}_{w}(\varepsilon)$is not satisfied by$\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right)$. No moves can be made from$w(\varepsilon)$and Player$\Box$ has won the game. 2. (2)

Case $t=a$.

We again reason over all $i$ and show that

[TABLE]

for any variable-closed term $t:o$ and any $\Xi{}$ so that $\Xi{}\vdash t$. Take any word $w$ such that $\mathsf{prepend}_{w}(\mathsf{prepend}_{a}(\Xi{}))$ is not satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). It follows that $\mathsf{prepend}_{wa}(\Xi{})$ is also not satisfied by \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right). From $\Xi{}\vdash t$, Player $\Box$ has a winning strategy from $wa(t)$. Since $wa(t)=w(a(t))$ we are done. 3. (3)

Case $t=x$.

For all $i$ and all extensions $\nu^{i}$ of $\sigma_{\mathcal{M}^{\mathit{C}}}^{i}$, we have

[TABLE]

Take any $\nu^{i}(x)=\Xi$ and any variable-closed term $t^{\prime}$ with $\Xi\vdash t^{\prime}$. Then $\nu^{i}(x)\vdash x[x\mapsto t^{\prime}]$ is immediate.

The only base case of the inner induction that depends on the iteration count is $t=F$. Let $F$ take $m$ arguments and consider variable-closed terms $t_{1},\ldots,t_{m}$ with corresponding $\Xi_{j}$ such that $\Xi_{j}\vdash t_{j}$. We have

[TABLE]

Thus, trivially \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ {\nu^{0}}\vdash 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 [math].

1. (1)

Case $t=t^{\prime}\ t^{\prime\prime}$.

Assume we already know that

[TABLE]

Our task is to show that

[TABLE]

Let the free variables be $x_{1},\ldots,x_{n}$ and consider $\Xi_{1}\vdash t_{1}$ to $\Xi_{n}\vdash t_{n}$. Let $\nu^{i}$ map $x_{j}$ to $\Xi_{j}$ for all $1\leqslant j\leqslant n$. By the definition of $\vdash$ for terms with free variables, we have \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}}\right\rrbracket\ {\nu^{i}}\vdash t^{\prime}[\forall j:x_{j}\mapsto t_{j}] and \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t^{\prime\prime}}\right\rrbracket\ {\nu^{i}}\vdash t^{\prime\prime}[\forall j:x_{j}\mapsto t_{j}]. Then, by the definition of $\vdash$ for functions, we obtain

[TABLE]

This means \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t^{\prime}\ t^{\prime\prime}}\right\rrbracket\ {\nu^{i}}\vdash t^{\prime}\ t^{\prime\prime} as required. 2. (2)

Case $t=\lambda x.e$.

Let the free variables of $e$ be $x,x_{1},\ldots,x_{n}$. For \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket\lambda x.e}\right\rrbracket\ {\nu^{i}}\vdash\lambda x.e, we have to argue that for any $\Xi_{1}\vdash t_{1}$ to $\Xi_{n}\vdash t_{n}$ with $\nu^{i}$ mapping $x_{i}$ to $\Xi_{i}$ for all $1\leqslant i\leqslant n$, we get

[TABLE]

This in turn means that for any $\Xi\vdash t$, we have to show

[TABLE]

By the definition of the semantics, we have

[TABLE]

Moreover, since the $t_{j}$ are variable-closed, they in particular are not affected by replacing $x$ and we get

[TABLE]

In the game, $\lambda$-redexes of the form $(\lambda x.e)\ t$ do not occur at all: When a non-terminal $F$ is rewritten to its right-hand side $\lambda x.e$, this yields $e[x\mapsto t]$ within a single step. This means the game equates $(\lambda x.(e[\forall j:x_{j}\mapsto t_{j}]))\ t$ with $e[x\mapsto t,\forall j:x_{j}\mapsto t_{j}]$. Hence, all that remains to be shown is

[TABLE]

This holds by the hypothesis of the inner induction, showing \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e}\right\rrbracket\ {\nu^{i}}\vdash e.

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 \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ {\nu^{i+1}}\vdash F. Let $F$ take $m$ arguments and consider $\Xi_{1}\vdash t_{1}$ to $\Xi_{m}\vdash t_{m}$. The task is to prove \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ {\nu^{i+1}}\ \Xi_{1}\ \ldots\ \Xi_{m}\vdash F\ t_{1}\ \ldots\ t_{m}. To ease the notation, assume there are two right hand sides $e_{1}^{\prime},e_{2}$ for $F$, i.e. we have the rules $F=\lambda x_{1}\ldots\lambda x_{m}.e_{1}$ and $F=\lambda x_{1}\ldots\lambda x_{m}.e_{2}$. This means the right-hand side in the determinised scheme is $F=\lambda x_{1}\ldots\lambda x_{m}.(\mathit{op}_{F}\ e_{1}\ e_{2})$. Then,

[TABLE]

Here, $\mathcal{I}^{\mathit{C}}(\mathit{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

[TABLE]

With the same reasoning, we obtain

[TABLE]

We have to prove that for any $w\in T^{*}$, if \mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) does not satisfy the formula

[TABLE]

then Player $\Box$ has a winning strategy from $w(F\ t_{1}\ldots\ t_{m})$.

Assume Player $\Diamond$ owns $F$ and the formula is not satisfied. If Player $\Box$ owns $F$, the reasoning is similar. Since we have a disjunction for Player $\Diamond$, \mathsf{prepend}_{w}(\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{1}^{\prime}}\right\rrbracket\ {\nu^{i}}\ \Xi_{1}\ \ldots\ \Xi_{m}) is not satisfied. By the hypothesis of the outer induction, we obtain \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{1}^{\prime}}\right\rrbracket\ {\nu^{i}}\ \vdash e_{1} and thus \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{1}^{\prime}}\right\rrbracket\ {\nu^{i}}\ \Xi_{1}\ \ldots\ \Xi_{m}\vdash e_{1}^{\prime}\ t_{1}\ \ldots\ t_{m}. As in the case of $\lambda$-abstraction above, we use that the game identifies $e_{1}^{\prime}\ t_{1}\ \ldots\ t_{m}$ and $e_{1}[x_{1}\mapsto t_{1},\ldots e_{m}\mapsto t_{m}]$. Hence, Player $\Box$ has a winning strategy from $w(e_{1}[x_{1}\mapsto t_{1},\ldots e_{m}\mapsto t_{m}])$. The same argumentation applies to \mathsf{prepend}_{w}(\mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket e_{2}}\right\rrbracket\ {\nu^{i}}\ \Xi_{1}\ \ldots\ \Xi_{m}). Consequently, whichever move Player $\Diamond$ makes at $w(F\ t_{1}\ \ldots\ t_{m})$, Player $\Box$ has a winning strategy.

This finishes the outer induction, proving that \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}^{i}}\vdash t for all terms $t$ and all $i\in{\mathbb{N}}$. We would like to conclude \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}}\vdash t. Since the cppo under consideration is not finite, this needs to be proven separately.

Limit case.

We have shown \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}^{i}}\vdash t for all $i\in{\mathbb{N}}$; we now show \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}}\vdash t noting by Kleene that $\sigma_{\mathcal{M}^{\mathit{C}}}=\bigsqcap_{i\in{\mathbb{N}}}\sigma_{\mathcal{M}^{\mathit{C}}}^{i}$. Once we have this we have $\sigma_{\mathcal{M}^{\mathit{C}}}(S)\vdash S$ which proves the lemma.

We formulate a slightly more general induction hypothesis for induction over kinds: Given a descending sequence of $\Xi_{i}$ for all $i\in{\mathbb{N}}$ such that each $\Xi_{i}\vdash t$, we have $\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i}\vdash t$. In the base case we have $t$ is of kind $o$ and we assume $\Xi_{i}\vdash t$. We now argue $\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i}\vdash t$.

Take any $w$ and suppose $\mathsf{prepend}_{w}(\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i})$ is not satisfied, then we need to show by the definition of $\vdash$ that Player $\Box$ has a winning strategy. Since $\sqcap$ is conjunction, if

[TABLE]

is not satisfied, it must be the case that for some $i$ we have $\mathsf{prepend}_{w}(\Xi_{i})$ is not satisfied. In this case, we have $\Xi_{i}\vdash t$ by assumption and thus by the definition of $\vdash$ that Player $\Box$ has a winning strategy from $w(t)$. This proves $\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i}\vdash t$.

If $t$ is of kind $\kappa_{1}\to\kappa_{2}$ we need to show for all $\Xi\vdash t^{\prime}$ that $(\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i})\ \Xi\vdash t\ t^{\prime}$. We have by the definition of $\sqcap$ over functions

[TABLE]

Since by assumption on $\Xi_{i}$ and definition of $\vdash$ for function kinds, we have $\Xi_{i}\ \Xi\vdash t\ t^{\prime}$ for each $i$. By the induction on the kind, we obtain $\bigsqcap_{i\in{\mathbb{N}}}(\Xi_{i}\ \Xi)\vdash t\ t^{\prime}$ . Since $(\bigsqcap_{i\in{\mathbb{N}}}\Xi_{i})\ \sigma=\bigsqcap_{i\in{\mathbb{N}}}(\Xi_{i}\ \sigma)$ we establish the desired statement that finishes the induction.

Finally, since \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}^{i}} satisfies the conditions of the above induction hypothesis and because we have already shown \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ {\sigma_{\mathcal{M}^{\mathit{C}}}^{i}}\vdash t for all $t$, we obtain

[TABLE]

Then, since using continuity of \mathcal{M}^{\mathit{C}}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket we have

[TABLE]

we obtain the lemma as required.

Appendix D Proofs for Section 5

D.1. Generalising Precision Properties to Functions

We show that several properties needed for precision can be lifted from the ground domain to function domains.

Lemma D.1**.**

If $(\mathsf{P1})$ holds, then for every $\kappa\in K$ and every $v_{r}\in\mathcal{D}_{r}(\kappa)$ there is a compatible $v_{l}\in\mathcal{D}_{l}(\kappa)$ with $\alpha(v_{l})=v_{r}$.

Proof D.2**.**

We show that, if $(\mathsf{P1})$ holds, then for every $\kappa\in K$ and every $v_{r}\in\mathcal{D}_{r}(\kappa)$ there is a compatible $v_{l}\in\mathcal{D}_{l}(\kappa)$ with $\alpha(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 $\alpha$ for $\kappa_{1}$ and $\kappa_{2}$ and consider $f_{r}\in\mathcal{D}_{r}(\kappa_{1}\rightarrow\kappa_{2})$. The task is to find a compatible function $f_{l}$ so that $\alpha(f_{l})=f_{r}$. Assume $f_{r}\ v_{r}=v_{r}^{\prime}$. By surjectivity for $\kappa_{1}$, there are compatible elements in $\alpha^{-1}(v_{r})$, and similar for $v_{r}^{\prime}$. Let $v_{l}^{\prime}$ be a compatible element that is mapped to $v_{r}^{\prime}$ by $\alpha$. We define $f_{l}\ v_{l}=v_{l}^{\prime}$ for all compatible $v_{l}\in\alpha^{-1}(v_{r})$. Since $\alpha$ is total on $\mathcal{D}({\kappa_{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 $\alpha(v_{l}^{1})=\alpha(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}^{\prime}$ to be a compatible element.

Concerning the equality of the functions, we have $\alpha(f_{l})\ v_{r}=\alpha(f_{l}\ v_{l})=\alpha(v_{l}^{\prime})=v_{r}^{\prime}$. The first equality is the definition of abstraction for functions and the fact that $\alpha^{-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}^{\prime}$, and the last is by $v_{l}^{\prime}\in\alpha^{-1}(v_{r}^{\prime})$.

Lemma D.3**.**

If $(\mathsf{P1})$ and $(\mathsf{P2})$ hold, then for all $\kappa\in K$ and all descending chains of compatible elements $(f_{i})_{i\in{\mathbb{N}}}$ in $\mathcal{D}({\kappa})$, we have $\bigsqcap_{i\in{\mathbb{N}}}f_{i}$ compatible and $\alpha(\bigsqcap_{i\in{\mathbb{N}}}f_{i})=\bigsqcap_{i\in{\mathbb{N}}}\alpha(f_{i})$.

Proof D.4**.**

We proceed by induction on kinds to show that, if $(\mathsf{P1})$ and $(\mathsf{P2})$ hold, then for all kinds $\kappa\in K$ and for all descending chains of compatible values $f_{1},f_{2},\ldots\in\mathcal{D}({\kappa})$, we have $\bigsqcap_{i\in{\mathbb{N}}}f_{i}$ again compatible and $\alpha(\bigsqcap_{i\in{\mathbb{N}}}f_{i})=\bigsqcap_{i\in{\mathbb{N}}}\alpha(f_{i})$. The base case is the assumption.

In the induction step, let $\kappa=\kappa_{1}\rightarrow\kappa_{2}$ and $f_{1},f_{2},\ldots\in\mathcal{D}_{l}(\kappa)$ be a descending chain of compatible elements. Let $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ be compatible. The following equalities will be helpful:

[TABLE]

The first equality is the definition of $\sqcap$ on functions, the second is the induction hypothesis for $\kappa_{2}$, the third is compatibility of the $f_{i}$ and $v_{l}$, the last is again $\sqcap$ on functions.

To show compatibility, note that the above implies $\alpha((\bigsqcap_{i\in{\mathbb{N}}}f_{i})\ v_{l})=\alpha((\bigsqcap_{i\in{\mathbb{N}}}f_{i})\ v_{l}^{\prime})$ as long as $\alpha(v_{l})=\alpha(v_{l}^{\prime})$, for all compatible $v_{l},v_{l}^{\prime}\in\mathcal{D}_{l}(\kappa_{1})$. For compatibility of $(\bigsqcap_{i\in{\mathbb{N}}}f_{i})\ v_{l}$ with $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ compatible, note that $(\bigsqcap_{i\in{\mathbb{N}}}f_{i})\ v_{l}=\bigsqcap_{i\in{\mathbb{N}}}(f_{i}\ v_{l})$. The latter is the meet over a descending chain of compatible elements in $\kappa_{2}$. By the induction hypothesis on $\kappa_{2}$, it is again compatible.

For $\sqcap$-continuity, consider a value $v_{r}\in\mathcal{D}_{r}(\kappa_{1})$. By Lemma D.1, there is a compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ with $\alpha(v_{l})=v_{r}$. We have

[TABLE]

The first equality is the definition of abstraction on functions. Note that we need here the fact that $\bigsqcap_{i\in{\mathbb{N}}}f_{i}$ is compatible by the induction hypothesis. The second equality is the auxiliary one from above. The last equality is by $\alpha(v_{l})=v_{r}$.

Lemma D.5**.**

If $(\mathsf{P3})$ holds, then $\alpha(\top^{l}_{\kappa})=\top^{r}_{\kappa}$ for all $\kappa\in K$.

Proof D.6**.**

We show that, if $(\mathsf{P3})$ holds, then $\alpha(\top^{l}_{\kappa})=\top^{r}_{\kappa}$ for all $\kappa\in K$. We proceed by induction on kinds. The base case is given by the assumption (P3). Assume for $\kappa_{2}$, we have $\alpha(\top^{l}_{\kappa_{2}})=\top^{r}_{\kappa_{2}}$. Consider function $\top^{l}_{\kappa_{1}\rightarrow\kappa_{2}}\in\mathcal{D}_{l}(\kappa_{1}\rightarrow\kappa_{2})$. We have to show $\alpha(\top^{l}_{\kappa_{1}\rightarrow\kappa_{2}})=\top^{r}_{\kappa_{1}\rightarrow\kappa_{2}}$. If the given top element is not compatible, this holds. Assume it is. For $v_{r}\in\mathcal{D}_{r}(\kappa_{1})$, there are two cases. If there is no compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ with $\alpha(v_{l})=v_{r}$, we have

[TABLE]

If there is such a $v_{l}$, we obtain

[TABLE]

The first equality is the definition of abstraction for functions, the next is the fact that $\top^{l}_{\kappa_{1}\rightarrow\kappa_{2}}$ maps every element $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ to $\top^{l}_{\kappa_{2}}$. The image of $\top^{l}_{\kappa_{2}}$ is $\top^{r}_{\kappa_{2}}$ by the induction hypothesis. The last equality is the definition of $\top^{r}_{\kappa_{1}\rightarrow\kappa_{2}}$.

D.2. Proof of Lemma 5.3

Proof D.7**.**

Assume $(\mathsf{P1})$, $(\mathsf{P4})$, and $(\mathsf{P5})$ hold. We show, for all terms $t$ and all compatible $\nu$, \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \nu is compatible and \alpha(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \nu)=\mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket t}\right\rrbracket\ \alpha(\nu). We proceed by structural induction on $t$.

1. (1)

Case $F$, $x$.

By the assumption, \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket F}\right\rrbracket\ \nu=\nu(F) is compatible. Moreover,

[TABLE]

holds. For $x\in V$, the reasoning is similar. 2. (2)

Case terminal $s$.

Note that \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ \nu=\mathcal{I}_{l}(s). If $s$ is ground, the claim holds by $(\mathsf{P4})$. Let $s:\kappa_{1}\rightarrow\kappa_{2}$. For compatibility, consider $v_{l},v_{l}^{\prime}\in\mathcal{D}({\kappa_{1}})$ compatible with $\alpha(v_{l})=\alpha(v_{l}^{\prime})$. Then

[TABLE]

The first equality is $(\mathsf{P4})$, the next is $\alpha(v_{l})=\alpha(v_{l}^{\prime})$, and the last is again $(\mathsf{P4})$. The second requirement on compatibility is satisfied by $(\mathsf{P5})$.

To show \alpha(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ \nu)=\mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket s}\right\rrbracket\ \alpha(\nu), consider a value $v_{r}\in\mathcal{D}_{r}(\kappa_{1})$. By Lemma D.1, there is some compatible $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ with $\alpha(v_{l})=v_{r}$. We have

[TABLE]

The first equality is compatibility of $\mathcal{I}_{l}(s)$ and the definition of function abstraction. The next equality is $(\mathsf{P4})$. The last is $\alpha(v_{l})=v_{r}$.

For the induction step, assume the claim holds for $t_{1}$ and $t_{2}$.

1. (1)

Case $t_{1}\ t_{2}$.

For compatibility, observe that \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}\ t_{2}}\right\rrbracket\ \nu=(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu)\ (\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu). Moreover, \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu and \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{2}}\right\rrbracket\ \nu are both compatible by the induction hypothesis. By definition of compatibility, applying a compatible function to a compatible argument yields a compatible value. Hence, \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}\ t_{2}}\right\rrbracket\ \nu is compatible.

For the equality, note that

[TABLE]

The first equality is by the definition of the semantics, the second is the induction hypothesis. Compatibility justifies the first of the following equalities. The second is again the definition of the semantics:

[TABLE] 2. (2)

Case $\lambda x:\kappa.t_{1}$.

We argue for compatibility. Consider compatible $v_{l}$ and $v_{l}^{\prime}$ with $\alpha(v_{l})=\alpha(v_{l}^{\prime})$. By definition of the semantics and the induction hypothesis, we have

[TABLE]

For $v_{l}^{\prime}$, the reasoning is similar. Since $\alpha(v_{l})=\alpha(v_{l}^{\prime})$, we have $\alpha(\nu[x\mapsto v_{l}])=\alpha(\nu[x\mapsto v_{l}^{\prime}])$. Hence, \mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \alpha(\nu[x\mapsto v_{l}])=\mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \alpha(\nu[x\mapsto v_{l}^{\prime}]). We conclude the desired equality.

For the second requirement in compatibility, let $v_{l}$ be compatible. By definition of the semantics, (\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket\lambda x.t_{1}}\right\rrbracket\ \nu)\ v_{l}=\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu[x\mapsto v_{l}]. Since $\nu$ and $v_{l}$ are compatible, $\nu[x\mapsto v_{l}]$ is compatible. Hence, \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu[x\mapsto v_{l}] is compatible by the induction hypothesis.

To prove \mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket\lambda x.t_{1}}\right\rrbracket\ \alpha(\nu)=\alpha(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket\lambda x.t_{1}}\right\rrbracket\ \nu), consider an arbitrary value $v_{r}\in\mathcal{D}_{r}(\kappa)$. Let $v_{l}\in\mathcal{D}_{l}(\kappa_{1})$ be compatible with $\alpha(v_{l})=v_{r}$, which exists by Lemma D.1. We have:

[TABLE]

We showed above that \mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket\lambda x.t_{1}}\right\rrbracket\ \nu is compatible. Using the definition of abstraction for functions and the definition of the semantics, the other function yields

[TABLE]

With the induction hypothesis, \alpha(\mathcal{M}_{l}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \nu[x\mapsto v_{l}])=\mathcal{M}_{r}\mathopen{}\mathclose{{}\left\llbracket t_{1}}\right\rrbracket\ \alpha(\nu[x\mapsto v_{l}]).

D.3. Proof of Theorem 5.4

Proof D.8**.**

Recall $\sigma_{l}^{0}$ and $\sigma_{r}^{0}$ are the greatest elements of the respective domains. We have

[TABLE]

The first equality is Kleene’s theorem. The second equality uses the fact that each $\mathit{rhs}_{\mathcal{M}_{l}}^{i}(\sigma_{l}^{0})$ is compatible and that they form a descending chain (both by induction on $i$), and then applies Lemma D.3. The third equality also relies on compatibility of the $\mathit{rhs}_{\mathcal{M}_{l}}^{i}(\sigma_{l}^{0})$ and invokes Lemma 5.3. Moreover, it needs $\alpha(\sigma_{l}^{0})=\sigma_{r}^{0}$ by Lemma D.5. The last equality is again Kleene’s theorem.

Appendix E Proofs for Section 6

E.1. Proof of Lemma 6.1

Proof E.1**.**

Observe \mathcal{I}^{\mathit{A}}(\)=Q_{f}=\mathsf{acc}\mathopen{}\mathclose{{}\left(\varepsilon}\right)$. Given a formula$\phi\in\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{}}\right)}\right)}$, we have to show that$\mathsf{pre}_{a}(\phi)\in\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{}}\right)}\right)}$. Since$\mathsf{pre}{a}$distributes over conjunction and disjunction, it is sufficient to show the requirement for atomic propositions. Consider$Q=\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)$. We have$\mathcal{I}^{\mathit{A}}(a)\ \mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)=\mathsf{pre}{a}(\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right))=\mathsf{acc}\mathopen{}\mathclose{{}\left(a.w}\right)$. Finally,$\mathcal{I}^{\mathit{A}}(\mathit{op}_{F})$with$F\in N$ is conjunction or disjunction, and there is nothing to do as the formula structure is not modified.

E.2. Proof of Lemma 6.2

Proof E.2**.**

We require, for all terminals $s$, $\mathcal{I}^{\mathit{A}}(s)$ is $\sqcap$-continuous over the respective lattices. We remark that the case $s=\mathit{op}_{F}$ is identical to Lemma 4.3. Hence, we show the case $s=a\in\Gamma$. Given a descending chain $(x_{i})_{i\in{\mathbb{N}}}$, we have to show $\mathcal{I}(a)\ (\bigsqcap_{i\in{\mathbb{N}}}x_{i})=\bigsqcap_{i\in{\mathbb{N}}}(\mathcal{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 $\mathsf{pre}_{a}$ is defined to distribute over finite conjunctions. We have

[TABLE]

as required.

E.3. Proof of Proposition 6.4

Proof E.3**.**

To show $\alpha$ is precise, we have to show $(\mathsf{P1})$ to $(\mathsf{P5})$. For $(\mathsf{P1})$, it is sufficient to argue that for every set of states Q\in\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right) there is a word that is mapped to it — which holds by definition. For formulas, note that $\alpha=\mathsf{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.

$(\mathsf{P2})$ is satisfied by the concrete meet being the union of sets of formulas and $\alpha$ being defined by an element-wise application.

For $(\mathsf{P3})$, note that the greatest elements are \mathopen{}\mathclose{{}\left\{\mathsf{true}}\right\} for $\mathcal{D}^{\mathit{C}}(o)$ and $\mathsf{true}$ for $\mathcal{D}^{\mathit{A}}(o)$. By definition, \alpha(\mathopen{}\mathclose{{}\left\{\mathsf{true}}\right\})=\alpha(\mathsf{true})=\mathsf{true}.

For $(\mathsf{P4})$, consider \$$. We have \alpha(\mathcal{I}^{\mathit{C}}($))=\alpha(\mathopen{}\mathclose{{}\left{\varepsilon}\right})=\mathsf{acc}\mathopen{}\mathclose{{}\left(\varepsilon}\right)=Q_{f}=\mathcal{I}^{\mathit{A}}($)$. The first equality is by definition of the concrete interpretation, the second is the definition of$\alpha$, the third uses the fact that$\varepsilon$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\subseteq T^{*}$, we have

[TABLE]

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 $\mathsf{prepend}_{a}$ is applied to all elements in the set and, in the abstract domain, $\mathsf{pre}_{a}$ distributes over conjunction.

Let $F$ be a non-terminal owned by $\Box$. To simplify the notation, let the associated operation be binary, $\mathit{op}_{F}:o\rightarrow o\rightarrow o$. Let $\Phi_{1},\Phi_{2}\in\mathcal{D}^{\mathit{C}}(o)$ be sets of formulas. We have

[TABLE]

The first equality is the concrete interpretation of $\mathit{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 $\mathit{op}_{F}$ and again the definition of the abstraction.

Assume $F$ is owned by $\Diamond$ and $\mathit{op}_{F}$ is again binary. Consider $\Phi_{1},\Phi_{2}\in\mathcal{D}^{\mathit{C}}(o)$. It will be convenient to denote \mathopen{}\mathclose{{}\left\{\phi_{1}\vee\phi_{2}\ \middle|\ \phi_{1}\in\Phi_{1},\phi_{2}\in\Phi_{2}}\right\} by $\Phi$. We have

[TABLE]

The first equality is the concrete interpretation of $\mathit{op}_{F}$, the second is the definition of $\alpha$ on sets of formulas. The third equality is the fact that $\alpha$ distributes over disjunctions and rewrites the iteration over the elements of $\Phi$. 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 $\mathit{op}_{F}$ and the definition of the abstraction function.

It remains to show $(\mathsf{P5})$. For \mathcal{I}^{\mathit{C}}(\)$and$\mathcal{I}^{\mathit{C}}(a)$, there is nothing to do as all ground values are compatible. Assume$F$is owned by$\Box$and$\mathit{op}{F}$is binary. The proof for$\Diamond$is similar. We show that, given a set of formulas$\Phi$, the function$\Phi\cup-$is compatible. An inspection of the proof of$(\mathsf{P4})$shows that for any set of formulas$\phi{1}$, we have

[TABLE]

Hence, if $\alpha(\Phi_{1})=\alpha(\Phi_{2})$, then $\alpha(\Phi\cup\Phi_{1})=\alpha(\Phi\cup\Phi_{2})$. That $\Phi\cup\Phi_{1}$ is compatible holds as the element is ground.

E.4. Proof of Lemma 6.5

Proof E.4**.**

v We have \mathcal{I}^{\mathit{O}}(\)=\bigvee Q_{f}=\alpha(Q_{f})=\alpha(\mathsf{acc}\mathopen{}\mathclose{{}\left(\varepsilon}\right))$. For$\mathcal{I}^{\mathit{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=\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)$. We have

[TABLE]

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 $\mathsf{pre}_{a}(Q)=\bigcup_{q\in Q}\mathsf{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 $\mathsf{pre}_{a}$ and \mathsf{acc}\mathopen{}\mathclose{{}\left(-}\right).

For conjunction and disjunction, which are used as the interpretation of $\mathit{op}_{F}$ depending on the player, we note that $\alpha$ distributes to the arguments. Hence, if the arguments are $\alpha(\phi_{1})$ and $\phi_{2}$, we have $\alpha(\phi_{1})\wedge\alpha(\phi_{2})=\alpha(\phi_{1}\wedge\phi_{2})$.

E.5. Proof of Lemma 6.6

Proof E.5**.**

We need, for all terminals $s$, $\mathcal{I}^{\mathit{O}}(s)$ is $\sqcap$-continuous over the respective lattices. We remark that the case $s=\mathit{op}_{F}$ is identical to Lemma 4.3. The case $s=a\in\Gamma$ follows from distributivity of $\mathcal{I}^{\mathit{O}}(a)$ as in the proof of Lemma 6.2.

E.6. Proof of Proposition 6.7

Proof E.6**.**

We show the optimized abstraction is precise. Surjectivity in $(\mathsf{P1})$ holds by definition as does $(\mathsf{P3})$. Also $\sqcap$-continuity in $(\mathsf{P2})$ is by the fact that the meets over the concrete domain are finite, and hence the definition of $\alpha$ already yields continuity. We argue for $(\mathsf{P4})$.

For \$$, Lemma [6.5](#S6.Thmtheorem5) yields \mathcal{I}^{\mathit{O}}($)=\alpha(Q_{f})$, which is$\alpha(\mathcal{I}^{\mathit{A}}($))$as required. For$a$, the same lemma shows$\mathcal{I}^{\mathit{O}}(a)\ \alpha(\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right))=\alpha(\mathsf{pre}{a}(\mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right)))$, which is$\alpha(\mathcal{I}^{\mathit{A}}(a)\ \mathsf{acc}\mathopen{}\mathclose{{}\left(w}\right))$. The equality generalizes to formulas as both, the abstraction function and the interpretations distribute over conjunctions and disjunctions. For$\mathit{op}{F}$, assume it is a binary conjunction. We have

[TABLE]

The first equality is the definition of the interpretation in the optimized model, the next is distributivity of $\alpha$ over conjunction. Finally, we have the interpretation of $\mathit{op}_{F}$ in the abstract model.

For $(\mathsf{P5})$, there is nothing to do for \mathcal{I}^{\mathit{C}}(\)$and$\mathcal{I}^{\mathit{C}}(a)$, as all ground values are compatible. We consider the conjunctions and disjunctions used to resolve the non-determinism. Consider a formula$\phi$. The task is to show that the function$\phi\wedge-$is compatible. Consider$\phi_{1}$and$\phi_{2}$with$\alpha(\phi_{1})=\alpha(\phi_{2})$. Then

[TABLE]

The first equality is distributivity of the abstraction function over conjunctions. The next is the assumed equality. The third is again distributivity. Compatibility of $\phi\wedge\phi_{1}$ holds as ground values are always compatible.

E.7. Proof of Corollary 6.11

To show the complexity, we argue the upper and lower bounds separately.

Proof E.7** (Proof of Proposition 6.9).**

We need to argue that $\sigma_{\mathcal{M}^{\mathit{O}}}$ can be computed in $(k+1)$-times exponential time. We have that $\sigma_{\mathcal{M}^{\mathit{O}}}=\bigsqcap_{i\in{\mathbb{N}}}\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i}(\sigma_{l}^{0})$. Since the domains $\mathcal{D}^{\mathit{O}}(\kappa)$ are finite for all kinds $\kappa$, there is an index $i_{0}\in{\mathbb{N}}$ such that $\sigma_{\mathcal{M}^{\mathit{O}}}=\bigsqcap_{i=0}^{i_{0}}\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i}(\sigma_{l}^{0})=\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i_{0}}(\sigma_{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 $\mathcal{D}$, we define its height $h(\mathcal{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

[TABLE]

The height of the domain is an upper bound for $i_{0}$ by its definition: If for some index $i_{1}$ we have $\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i_{1}}(\sigma_{l}^{0})=\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i_{1}+1}(\sigma_{l}^{0})$, we know $\bigsqcap_{i=0}^{i_{0}}\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i}(\sigma_{l}^{0})=\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i_{0}1}(\sigma_{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 $\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}^{i}(\sigma_{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 $\mathit{rhs}_{\mathcal{M}^{\mathit{O}}}$ has the type signature $(N\to\mathcal{D}^{\mathit{O}})\to(N\to\mathcal{D}^{\mathit{O}})$. Our goal in the following is to determine $h(N\to\mathcal{D}^{\mathit{O}})$. We can identify $N\to\mathcal{D}^{\mathit{O}}$ with $\mathcal{D}^{\mathit{O}}(F_{1})\times\ldots\times\mathcal{D}^{\mathit{O}}(F_{\ell})$, where $F_{1},\ldots,F_{\ell}$ are the non-terminals 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 $\mathcal{D}^{\mathit{O}}(F)$ with the maximal height is $(k+1)$-times exponentially high, since the number of non-terminals is polynomial in the input scheme.

In the following we prove: If kind $\kappa$ is of order $k^{\prime}$, then $\mathcal{D}^{\mathit{O}}(\kappa)$ has $(k^{\prime}+1)$-times exponential height. For the induction step, we also need to consider the cardinality of $\mathcal{D}^{\mathit{O}}(\kappa)$, therefore, we strengthen the statement and also prove that the cardinality \mathopen{}\mathclose{{}\left|\mathcal{D}^{\mathit{O}}(\kappa)}\right| is $(k^{\prime}+2)$-times exponential.

We proceed by induction on $k^{\prime}$.

In the base case $k^{\prime}=0$, we necessarily have $\kappa=o$, and indeed the domain \alpha(\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(\mathsf{acc}\mathopen{}\mathclose{{}\left(T^{*}}\right)}\right)})\subseteq\mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)} is singly exponentially high. To see that this is the case, consider a strictly decreasing chain $(\phi_{j})_{j\in{\mathbb{N}}}$ of positive boolean formulas over $Q_{\mathit{NFA}}$, i.e. a chain where each formula is strictly implied by the next. To each formula, $\phi_{j}$, we assign the set \mathcal{Q}_{j}=\mathopen{}\mathclose{{}\left\{Q\subseteq Q_{\mathit{NFA}}\ \middle|\ Q\text{ satisfies }\phi_{j}}\right\} of assignments under which $\phi_{j}$ evaluates to true. That $\phi_{j}$ is strictly implied by $\phi_{j+1}$ translates to the fact that $\mathcal{Q}_{j}$ is a strict subset of $\mathcal{Q}_{j+1}$. This gives us that the sets $\mathcal{Q}_{j}$ themselves form a strictly ascending chain in {\mathcal{P}}\mathopen{}\mathclose{{}\left({\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right), and it is easy to see that such a chain has length at most \mathopen{}\mathclose{{}\left|{\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right|=2^{\mathopen{}\mathclose{{}\left|Q_{\mathit{NFA}}}\right|}.

Furthermore, we can represent each equivalence class of formulas in \mathsf{PBool}\mathord{\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)} by a representative in conjunctive normal form, i.e. by an element of {\mathcal{P}}\mathopen{}\mathclose{{}\left({\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right). This shows that the cardinality of the domain is indeed bounded by \mathopen{}\mathclose{{}\left|{\mathcal{P}}\mathopen{}\mathclose{{}\left({\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right)}\right|=2^{\mathopen{}\mathclose{{}\left|{\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right|}=2^{2^{\mathopen{}\mathclose{{}\left|Q_{\mathit{NFA}}}\right|}}.

Now assume the statement holds for $k^{\prime}$, and consider $\kappa$ of order $k^{\prime}+1$. We need an inner induction on the arity $m$ of $\kappa$.

Since $o$ is the only kind of arity [math], and does not have order $k^{\prime}+1$ for any $k^{\prime}$, there is nothing to do in the base case.

Now assume that $\kappa=\kappa_{1}\to\kappa_{2}$. By the definitions of arity and order, we know that $\kappa_{1}$ is of order at most $k^{\prime}$, therefore we now by the outer induction that the height of $\mathcal{D}^{\mathit{O}}(\kappa_{1})$ is at most $(k^{\prime}+1)$-times exponential. The order of $\kappa_{2}$ is at most $(k^{\prime}+1)$, but the arity of $\kappa_{2}$ is strictly less than the arity of $\kappa$, thus we get by the inner induction that the height of $\mathcal{D}^{\mathit{O}}(\kappa_{2})$ is at most $(k^{\prime}+2)$-times exponential.

The domain $\mathcal{D}^{\mathit{O}}(\kappa_{1}\to\kappa_{2})=\mathit{Cont}(\mathcal{D}^{\mathit{O}}(\kappa_{1}),\mathcal{D}^{\mathit{O}}(\kappa_{2}))$ is a subset of all functions from $\mathcal{D}^{\mathit{O}}(\kappa_{1})$ to $\mathcal{D}^{\mathit{O}}(\kappa_{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(\mathcal{D}^{\mathit{O}}(\kappa_{2}))\cdot\mathopen{}\mathclose{{}\left|\mathcal{D}^{\mathit{O}}(\kappa_{1})}\right|. The induction completes the proof, as both $h(\mathcal{D}^{\mathit{O}}(\kappa_{2}))$ and \mathopen{}\mathclose{{}\left|\mathcal{D}^{\mathit{O}}(\kappa_{1})}\right| are at most $(k^{\prime}+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 $\mathcal{D}^{\mathit{O}}(\kappa)$ can be represented by an object of size $(k^{\prime}+1)$-times exponential, where $k^{\prime}$ is the order of $\kappa$. 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^{\prime}=0$, i.e. $\kappa=o$. We again represent each element of $\mathcal{D}^{\mathit{O}}(o)$ by a formula over $Q_{\mathit{NFA}}$ in conjunctive normal form, i.e. as an element of {\mathcal{P}}\mathopen{}\mathclose{{}\left({\mathcal{P}}\mathopen{}\mathclose{{}\left(Q_{\mathit{NFA}}}\right)}\right). In the worst case, one single formula $\phi$ contains everyone of the $2^{Q_{\mathit{NFA}}}$ many clauses, each clause having size at most \mathopen{}\mathclose{{}\left|Q_{\mathit{NFA}}}\right|. This means that one formula needs at most singly exponential space.

For the induction step, consider $\kappa$ of order $k+1$. As above, we need an inner induction on the arity of $\kappa$, for which the base case is trivial.

Let $\kappa=\kappa_{1}\to\kappa_{2}$. An element of $\mathcal{D}^{\mathit{O}}(\kappa)$ is a function that assigns to each of the \mathopen{}\mathclose{{}\left|\mathcal{D}^{\mathit{O}}(\kappa_{1})}\right|-many elements of $\mathcal{D}^{\mathit{O}}(\kappa_{1})$ an element of $\mathcal{D}^{\mathit{O}}(\kappa_{2})$. In the previous part of the proof, we have argued, that \mathopen{}\mathclose{{}\left|\mathcal{D}^{\mathit{O}}(\kappa_{1})}\right| is at most $(k+1)$ times exponential. By the induction on the arity, we know that each object in $\mathcal{D}^{\mathit{O}}(\kappa_{2})$ can be represented in at most $(k+2)$-times exponential space. This shows that objects of $\mathcal{D}^{\mathit{O}}(\kappa)$ can be represented using $(k+2)$-times exponential space, and finishes the proof.

We show that determining the winner in a higher-order word game is $(k+1)\mathsf{EXP}$-hard for an order-$k$ recursion scheme.

Proof E.8** (Proof of Proposition 6.10).**

We begin with a result due to Engelfriet [18] that shows alternating $k$-iterated pushdown automata with a polynomially bounded auxiliary work-tape ($k$-PDA*+*) characterize the $(k+1)\mathsf{EXP}$ word languages. We fix any $(k+1)\mathsf{EXP}$-hard language and its corresponding alternating $k$-PDA $B$. Let \mathcal{L}\mathopen{}\mathclose{{}\left(B}\right) be the set of words accepted by $B$. Deciding if a given word $w$ is in the language defined by $B$ is $(k+1)\mathsf{EXP}$-hard in the size of $w$ (recall $B$ is fixed). We show that this problem can be reduced in polynomial time to an inclusion problem \mathcal{L}\mathopen{}\mathclose{{}\left(B^{\prime}}\right)\subseteq\mathcal{L}\mathopen{}\mathclose{{}\left(A}\right) for some $k$-iterated pushdown automaton (without work-tape) ($k$-PDA) $B^{\prime}$ and NFA $A$ of size polynomial in the length of $w$. From $B^{\prime}$, we can construct in polynomial time an equivalent game over a scheme $G$. This will show the game language inclusion problem for order-$k$ schemes is $(k+1)\mathsf{EXP}$-hard.

In an alternating $k$-PDA*+, there are two Players $\Diamond$ and $\Box$. When decided whether a word $w$ is in the language of a $k$-PDA+*, $\Diamond$ will attempt to prove the word is in the language, while $\Box$ will try to refute it.

We first describe how to obtain $B^{\prime}$ 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\times w$. This reduces the word membership problem to the problem of determining whether $B\times w$ can reach an accepting state. Next, to remove the worktape from $B\times w$ (and form $B^{\prime}$) we replace the output of $B\times w$ (which will always be $w$ or empty) with a series of guesses of the worktape. That is, a transition of $B\times w$ will be simulated by $B^{\prime}$ by first making a transition as expected, and then outputting a guess (consistent with the transition) of what the worktape of $B\times 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^{\prime}$ is able to reach a final state and produce a word $w^{\prime}$ that is correct; that is, $w^{\prime}$ is not in the language of $A$.

Note, here, the reversal of the roles of the Players. In $B$, control states are owned by $\Diamond$ or $\Box$. When determining if w\in\mathcal{L}\mathopen{}\mathclose{{}\left(B}\right) for some $w$, the first Player $\Diamond$ tries to show the word is accepted, while the second Player $\Box$ tries to force a non-accepting run. In $B^{\prime}$, however, $w$ is accepted iff the output of $B^{\prime}$ is not included in the language of $A$. Thus, $\Box$ will effectively be aiming to prove that w\in\mathcal{L}\mathopen{}\mathclose{{}\left(B}\right).

In more detail, we take any $(k+1)\mathsf{EXP}$-hard language and its equivalent (fixed) alternating $k$-PDA*+*. Given a word $w$, deciding w\in\mathcal{L}\mathopen{}\mathclose{{}\left(B}\right) is $(k+1)\mathsf{EXP}$-hard. We define $B^{\prime}$ directly from $B$ rather than going through the intermediate $B\times w$.

A transition $(p,a,o,\sigma,p^{\prime})$ of $B$ means the following. From control state $p$, upon reading a character $a$ from $w$, apply operation $o$ to the work-tape (which may become stuck if not applicable) and operation $\sigma$ to the stack (which may also become stuck if not applicable). Next, move to control state $p^{\prime}$, from which the remainder of $w$ is to be read.

Let $m$ be the polynomial bound on the size of the work-tape of $A$ given the input word $w$. Let $\Sigma$ be the alphabet of the work-tape. Let the set of work-tape operations O=\mathopen{}\mathclose{{}\left\{o_{1},\ldots,o_{n}}\right\} and work-tape positions P=\mathopen{}\mathclose{{}\left\{1,\ldots,m}\right\} be disjoint from $\Sigma$. Also, let $\circ\in\Sigma$ be the initial symbol appearing in each cell of the initial work-tape. We will construct $A^{\prime}$ such that

[TABLE]

That is, $A^{\prime}$ outputs a sequence of work-tape configurations separated by positions in $P$ and operations in $O$. That is, $A^{\prime}$ will simulate a run of $A$ over $w$.

For every control state $p$ of $A$, we will have control states $(p,w^{\prime})$ of $A^{\prime}$, where $w^{\prime}$ is a suffix of $w$. We will also have $(p,w^{\prime},o)$ where $o$ is a work-tape operation to be applied. Then for each transition $(p,a,o,\sigma,p^{\prime})$ of $B$ we have a transition $((p,aw^{\prime}),\varepsilon,\sigma,(p^{\prime},w^{\prime},o))$ of $B\times w$. From $(p^{\prime},w^{\prime},o)$ the automaton $B^{\prime}$ will output some character from $P$ (a guess at the work-tape head position), followed by $o$ (to indicate the operation applied). It will then be able to output any word from $\Sigma^{m}$ (a guess of the work-tape contents) before moving to $(p^{\prime},w^{\prime})$ and continuing the simulation. Initially, $B^{\prime}$ will simply output $\circ^{m}$ and move to control state $(p,w)$ where $p$ is the initial control state of $B$.

The final step in defining $B^{\prime}$ is to assign ownership of the control states. Recall, we needed to switch the roles of the Players. Thus, we define $O((p,w))=\Diamond$ whenever $p$ belongs to $\Box$ in $B$. All other control states of $B^{\prime}$ are owned by $\Box$. We define the accepting control states to be those of the form $(p,\varepsilon)$ where $p$ is accepting in $B$. Observe these have no outgoing transitions.

Next we define the regular automaton $A$ which detects mistakes in the work-tape. Such an error is either due to a poorly updated cell, or due to a poorly updated head position. The set of work-tape operations $O$ is such that there is a mapping

[TABLE]

where $\bot\notin\Sigma$ and

• •

$\pi(i,o)=j$ means if the head is at position $i$, it is at position $j$ after operation $o$, and

• •

$\pi(i,\alpha,j,o)=\beta$ means, if the head is at position $i$, $\alpha$ is the contents of the cell at position $j$, and operation $o$ is applied, then $\beta$ is the contents of the cell after applying $o$. If $\beta=\bot$ then $o$ could not be applied to this work-tape and became stuck. (E.g. if $i=j$ and the operation required the head to read a character other than $\alpha$.)

Thus, we require the following regular language, for which a polynomially-sized regular automaton is straightforward to construct. Let $\Gamma=\Sigma\cup P\cup O$.

[TABLE]

We have thus defined a $k$-PDA $B^{\prime}$ that produces some word $w^{\prime}$ 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 $k$-iterated pushdown automata. This is in fact a straightforward adaptation of the techniques introduced by Knapik et al. [37]. However, we choose to complete the sketch using definitions from Hague et al. [29] 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 $k$-iterated pushdown automaton, and terms of the form222In fact, in op. cit. non-terminals had the form $F^{a,e}_{q}\vec{\Psi}\vec{\Psi}_{k-1}\cdots\vec{\Psi}_{0}$. where $e$ and $\vec{\Psi}$ are used to handle collapse links, which we do not need here.

$F^{a}_{q}\vec{\Psi}_{k-1}\cdots\vec{\Psi}_{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,\sigma,q^{\prime})$ of the pushdown automaton, when $o\neq\varepsilon$ we can associate a rewrite rule of the scheme

[TABLE]

such that the term obtained by applying the rewrite rule to $F^{a}_{q}\vec{\Psi}_{k-1}\cdots\vec{\Psi}_{0}$ is a term $o(F^{b}_{q^{\prime}}\vec{\Psi}^{\prime}_{k-1}\cdots\vec{\Psi}^{\prime}_{0})$ where $F^{b}_{q^{\prime}}\vec{\Psi}^{\prime}_{k-1}\cdots\vec{\Psi}^{\prime}_{0}$ represents the configuration reached by the transition. That is, $(q^{\prime},\sigma(s))$. When $o=\varepsilon$ we simply omit $o$, that is

[TABLE]

To each non-terminal, we assign $O(F^{a}_{q})=\Diamond$ whenever $q$ is a $\Diamond$ control state. Otherwise, $O(F^{a}_{q})=\Box$. For every accepting control state $q$ we introduce the additional rule

[TABLE]

Finally, we have an initial rule

[TABLE]

where $t$ is the term representing the initial configuration.

Given the tight correspondence between configurations and transitions of the $k$-PDA and terms and rewrite steps of $G$, alongside the direct correspondence between the owner of a control state $q$ and the owner of a non-terminal 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^{\prime}$ 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 $k$-PDA*+* to the game problem for language inclusion of a scheme. This shows the problem is $(k+1)\mathsf{EXP}$-hard.