Domains for Higher-Order Games

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.

1  Introduction

Inclusion checking has recently received considerable attention [55, 23, 1, 2, 37]. One of the reasons is a new verification loop, which invokes inclusion as a subroutine in an iterative fashion. The loop has been proposed by Podelski et al. for the safety verification of recursive programs [33], and then been generalized to parallel and parameterized programs [43, 21, 19] and to liveness [20]. The idea of Podelski’s loop is to iteratively approximate unsound data flow in the program of interest, and add the approximations to the specification. Consider a program with control-flow language CF that is supposed to satisfy a safety specification given by a regular language R. If the check CF⊆ R succeeds, then the program is correct as the data flow only restricts the set of computations. If a computation w∈ CF is found that lies outside R, then it depends on the data flow whether the program is correct. If data is handled correctly, w is a counterexample to R. Otherwise, w is generalized to a regular language S of infeasible computations. We set R = R ∪ S and repeat the procedure.

Podelski’s loop has also been generalized to synthesis [36, 45]. In that setting, the program is assumed to have two kinds of 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 [47], which indeed can be achieved (see the full version [29] for a comparison to intersection types [42]). Instead, we need a strategy synthesis that can directly deal with non-deterministic specifications.

We show that the winning region of a higher-order inclusion game w.r.t. 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 [36] (and generalized to infinite words [45]), 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 [53] as well as Grellois and Melliès [25, 25], with [5, 50] being early works in this field. The idea is to solve verification problems by computing the semantics of a program in a suitable domain. Salvati and Walukiewicz studied the expressiveness of greatest fixed-point semantics and their correspondence to automata [53], and constructions of enriched Scott models for parity conditions [52, 51]. A similar line of investigation has been followed in recent work by Grellois and Melliès [26, 27]. Hofmann and Chen considered the verification of more restricted ω-path properties with a focus on the domain [34]. They show that explicit automata constructions can be avoided and give a domain that directly captures subsets (so-called patches) of the ω-language. The work has been generalized to higher order [35]. Our contribution is related in that we focus on the domain (suitable for capturing plays).

Besides the domain, the correctness proof may be of interest. We employ an exact 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)EXP-complete for order-k schemes.

Related Work.

The relationship between recursion schemes and extensions of pushdown automata has been well studied [16, 17, 38, 30]. This means algorithms for recursion schemes can be transferred to extensions of pushdown automata and vice versa. In the sequel, we will use pushdown automata to refer to pushdown automata and their family of extensions.

The decidability of Monadic Second Order Logic (MSO) over trees generated by recursion schemes was first settled in the restricted case of safe schemes by Knapik et al. [38] and independently by Caucal [14]. This result was generalized to all schemes by Ong [47]. Both of these results consider deterministic schemes only.

Related results have also been obtained in the consideration of games played over the configuration graphs of pushdown automata [54, 13, 39, 30]. Of particular interest are saturation methods for pushdown games [7, 22, 12, 8, 31, 32, 9]. In these works, automata representing sets of winning configurations are constructed using fixed-point computations.

A related approach pioneered by Kobayashi et al. operating directly on schemes is that of intersection types [41, 42], where types embedding a property automaton are assigned to terms of a scheme. Recently, saturation techniques were transferred to intersection types by Broadbent and Kobayashi [10]. The typing algorithm is then a least 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 [40].

One may reduce our language inclusion problems to many of the above works. E.g. from an inclusion game for schemes, we may build a game over an equivalent kind of pushdown automaton and take the product with a determinization of the NFA. This obtains a reachability game over a pushdown automaton that can be solved by any of the above methods. However, such constructions are undesirable for iterative invocations as in Podelski’s loop.

We already discussed the relationship to model-theoretic verification algorithms. Abstract interpretation has also been used by Ramsay [49], Salvati and Walukiewicz [52, 51], and Grellois and Melliès [25, 24] for verification. The former used a Galois connection between safety properties (concrete) and equivalence classes of intersection types (abstract) to recreate decidability results known in the literature. The latter two strands gives a semantics capable of computing properties expressed in MSO. Indeed, abstract interpretation has long been used for static analysis of higher-order programs [4].

2  Preliminaries

Complete Partial Orders.

Let (D, ≤) be a partial order with set D and (partial) ordering ≤ on D. We call (D, ≤) pointed if there is a greatest element, called the top element and denoted by ⊤ ∈ D. A descending chain in D is a sequence (d_i)_{i ∈ N} of elements in D with d_i ≥ d_i+1. We call (D, ≤) ω-complete if every descending chain has a greatest lower bound, called the meet or the infimum, and denoted by ⊓_{i ∈ N} d_i. If (D, ≤) is pointed and ω-complete, we call it a pointed ω-complete partial order (cppo). In the following, we will only consider partial orders that are cppos. Note, cppo is usually used to refer to the dual concept, i.e. partial orders with a least element and least upper bounds for ascending chains.

A function f : D → D is ⊓-continuous if for all descending chains (d_i)_{i ∈ N} we have f(⊓_{i ∈ N} d_i) = ⊓_{i ∈ N} f(d_i). We call a function f : D → D monotonic if for all d, d′ ∈ D, d ≤ d′ implies f(d) ≤ f(d′). Any function that is ⊓-continuous is also monotonic. For a monotonic function, ⊤ ≥ f(⊤) ≥ f² (⊤) = f(f(⊤)) ≥ f³ (⊤) ≥ … is a descending chain. If the function is ⊓-continuous, then ⊓_{i ∈ N} fⁱ (⊤) is by Kleene’s theorem the greatest fixed point of f, i.e. f(⊓_{i ∈ N} fⁱ (⊤)) = ⊓_{i ∈ N} fⁱ (⊤) and ⊓_{i ∈ N} fⁱ (⊤) is larger than any other element d with f(d) = d. We also say ⊓_{i ∈ N} fⁱ (⊤) is the greatest solution to the equation x = f(x).

A lattice satisfies the descending chain condition (DCC) if every descending chain has to be stationary at some point. In this case ⊓_{i ∈ N} fⁱ (⊤) = ⊓_{i = 0}^i₀ fⁱ (⊤) for some index i₀ in N. With this, we can compute the greatest fixed point: Starting with ⊤, we iteratively apply f until the result does not change. This process is called Kleene iteration. Note that finite cppos, i.e. with finitely many elements in D, trivially satisfy the descending chain condition.

Finite Automata.

A non-deterministic finite automaton (NFA) is a tuple A = (Q_NFA, Γ, δ, q₀, Q_f) where Q_NFA is a finite set of states, Γ is a finite alphabet, δ ⊆ Q_NFA × Γ × Q_NFA is a (non-deterministic) transition relation, q₀ ∈ Q_NFA is the initial state, and Q_f ⊆ Q_NFA is a set of final states. We write q –[a]→ q′ to denote (q, a, q′) ∈ δ. Moreover, given a word w = a₁⋯ a_ℓ, we write q –[w]→ q′ whenever there is a sequence of transitions, also called run, q₁ –[a₁]→ q₂ –[a₂]→ ⋯ –[a_ℓ]→ q_ℓ+1 with q₁ = q and q_ℓ+1 = q′. The run is accepting if q = q₀ and q′ ∈ Q_f. The language of A is L(A) = {w | q₀ –[w]→ q ∈ Q_f} .

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 [41, 48, 42], we refer to types as kinds. Kinds define the functionality of terms, without specifying the data domain. Technically, the only data domain is the ground kind o, from which (potentially higher-order) function kinds are derived by composition:

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

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

1. Γ^κ⊆ T^κ(Γ),
2. ∪_κ1 {t v | t ∈ T^{κ₁ → κ₂}(Γ), v ∈ T^κ₁ (Γ)} ⊆ T^κ₂ (Γ), and
3. {λ x.t | x∈ T^κ₁(Γ), t∈ T^κ₂(Γ)}⊆ T^{κ₁ → κ₂}(Γ).

If term t is of kind κ, we also write t ∶ κ. We use T(Γ) for the set of all terms over Γ. We say a term is λ-free if it contains no sub-term of the form λ x . t. A term is variable-closed if all occurring variables are bound by a preceding λ-expression.

The semantics of G is defined by rewriting subterms according to the rules in R. A context is a term C[•] ∈ T (Γ ⨃ { • ∶ o }) in which • occurs exactly once. Given a context C[•] and a term t:o, we obtain C[t] by replacing the unique occurrence of • in C[•] by t. With this, t ⇒_G t′ if there is a context C[•], a rule F = λ x₁ … λ x_n.e, and a term F t₁ … t_n:o such that t = C[F t₁ … t_n] and t′ = C[e[x₁ ↦ t₁, …, x_n ↦ t_n]]. 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₁ … 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 L(G) of G is the set of all (finite, ranked, labeled) trees T over the terminal symbols that can be created from the initial symbol S via 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⨃ {$:o} where exactly one terminal symbol $ has kind o and all others are of kind o→ o. The generated trees have the shape a₁ (a₂ (⋯ (a_k $))), which we understand as the finite word a₁ a₂ … a_k ∈ T^*. We also see L(G) 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^det with exactly one rule per non-terminal. Intuitively, G^det makes the non-determinism explicit with new terminal symbols.

Formally, let F:κ be a non-terminal with rules F= t₁ to F= t_ℓ. We may assume each t_i = λ x₁ … λ x_k. e_i, where e_i is λ-free. We introduce a new terminal symbol op_F: o → o → … → o of arity ℓ. Let the set of all these terminals be T^det={op_F | F∈ N}. The set of rules R^det now consists of a single rule for each non-terminal, namely F= λ x₁ … λ x_k. op_F e₁ ⋯ e_ℓ. The original rules in R are removed. This yields G^det=(V, N, T⨃ T^det, R^det, S). The advantage of resolving the 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 M=(D, I), where D is a family of domains (D(κ))_κ∈Κ that satisfies the following: D(o) is a cppo and D(κ₁→ κ₂)=Cont(D(κ₁), D(κ₂)). Here, Cont(A, B) is the set of all ⊓-continuous functions from domain A to B. We comment on this cppo in a moment. The interpretation I: T→ D assigns to each terminal s:κ an element I(s)∈D(κ).

The ordering on functions is defined component-wise, f ≤_{κ1 → κ2} g if (f x) ≤_κ2 (g x) for all x∈D(κ₁). For each κ, we denote the top element of D(κ) by ⊤_κ. For the ground kind, ⊤_o exists since D(κ) is a cppo, and ⊤_{κ1 → κ2} is the function that maps every argument to ⊤_κ2. The meet of a descending chain of functions (f_i)_{i ∈ N} is the function defined by (⊓_{κ1 → κ2} (f_i)_{i ∈ N}) x = ⊓_κ2 (f_i x)_{i ∈ N}. Note that the sequence on the right-hand side is a descending chain. The semantics of terms defined by a model is a function

that assigns to each term built over the non-terminals and terminals again a function. This function expects a valuation ν:N⨃ V↛ D and returns an element from the domain. A valuation is a partial function that is defined on all non-terminals and the free variables. We lift ⊓ to descending chains of valuations with (⊓_{i ∈ N} ν_i)(y) = ⊓_{i ∈ N} (ν_i(y)) for y ∈ N ⨃ V. We obtain that the set of such valuations is a cppo where the greatest elements are those valuations which assign the greatest elements of the appropriate domain to all arguments.

Since the 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:

We show that M〚t〛 is ⊓-continuous for all terms t. This follows from continuity of the functions in the domain, but requires some care when handling application.

Given M, the rules F₁=t₁,…, F_k=t_k of the (deterministic) scheme give a function

Since the right-hand sides are variable-closed, the M〚t_j〛 are functions in the non-terminals. Provided M〚t₁〛 to M〚t_k〛 are ⊓-continuous (in the valuation of the non-terminals), the function rhs_M will be ⊓-continuous. This allows us to apply Kleene iteration as follows. The initial value is the greatest element σ_M⁰ where σ_M⁰(F_j) = ⊤_j with ⊤_j the top element of D(κ_j). The (i+1)^th approximant is computed by evaluating the right-hand side at the i^th solution, σ_Mⁱ⁺¹ = rhs_M(σ_Mⁱ). The greatest fixed point is the tuple σ_M defined below. It can be understood as the greatest solution to the equation ν = rhs_M(ν). We call this greatest solution σ_M the semantics of the scheme in the model.

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 ◇ and those owned by the universal player □. 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 ◇ attempts to produce a word that is in L(A), while Player □ attempts to produce a word outside of L(A).

A play of the game is a sequence of 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₁ ( a₂ ( ⋯ (a_k (t) ) ) ), where t is either $ or a redex F t₁ ⋯ t_m. If O(F) = ◇ then Player ◇ chooses a rule F = λ x₁ … λ x_m . e to apply, else Player □ chooses the rule. This moves the play to a₁ (a₂ (⋯ (a_k e[x₁ ↦ t₁, …, x_m ↦ t_m]))).

Each play begins at the initial non-terminal S, and continues either ad infinitum or until a term a₁ (a₂ (⋯ (a_k $))), understood as the word w=a₁… a_k, is produced. Infinite plays do not produce a word and are won by Player ◇. Finite maximal plays produce such a word w. Player ◇ wins whenever w ∈ L(A), Player □ wins if w ∈ L(A). Since the winning condition is Borel, either Player ◇ or Player □ has a winning strategy [44].

Our contribution is a fixed-point algorithm to decide 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 HOG can be read off from the semantics in the abstract model, which in turn can be computed via Kleene iteration. Moreover, this semantics can be used to define Player ◇’s winning strategy. We instantiate the framework for the concrete and abstract model to prove the soundness of the algorithm.

Concrete Semantics

Consider a HOG instance G = (G, A, O). Let G^det be the determinized version of G. Our goal is to define a model M^C = (D^C, I^C) such that the semantics of G^det in this model allows us to decide HOG. Recall that we only have to define the ground domain. For composed kinds, we use the functional lifting discussed in Section 3.

Our idea is to associate to kind o the set of positive Boolean formulas where the atomic propositions are words in T^∗. To be able to reuse the definition, we define formula domains in more generality as follows.

Domains of Boolean Formulas

Given a (potentially infinite) set P of atomic propositions, the positive Boolean formulas PBool(P) over P are defined to contain true, every p from P, and compositions of formulas via conjunction and disjunction. We work up to logical equivalence, which means we treat φ₁ and φ₂ as equal as long as they are logically equivalent.

Unfortunately, if the set P is infinite, PBool(P) is not a cppo, because the meet of a descending chain of formulas might not be a finite formula. The idea of our domain is to have conjunctions of infinitely many formulas. As is common in logic, we represent them as infinite sets. Therefore, we consider the set of all sets of (finite) positive Boolean formulas P(PBool(T^*))∖{∅} factorized modulo logical equivalence, denoted (P(PBool(T^*))∖{∅}) /_⇔. To be precise, the sets may be finite or infinite, but they must be non-empty.

To define the factorization, let an assignment to the atomic propositions be given by a subset of P′ ⊆ P. The atomic proposition p is true if p ∈ P′. An assignment satisfies a Boolean formula, if the formula evaluates to true in that assignment. It satisfies a set of Boolean formulas, if it satisfies all elements. Given two sets of formulas Φ₁ and Φ₂, we write Φ₁⇒ Φ₂, if every assignment that satisfies Φ₁ also satisfies Φ₂. Two sets of formulas are equivalent, denoted Φ₁⇔ Φ₂, if Φ₁⇒ Φ₂ and Φ₂⇒ Φ₁ holds. The ordering on these factorized sets is implication (which by transitivity is independent of the representative). The top element is the set {true}, which is implied by every set. The conjunction of two sets is union. Note that it forms the meet in the partial order, and moreover note that meets over arbitrary sets exist, in particular the domain is a cppo. We will also need an operation of disjunction, which is defined by Φ₁∨ Φ₂ = {φ₁∨ φ₂ | φ₁∈ Φ₁, φ₂∈ Φ₂}. 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′ ⊆ T^* of interest is the language of the automaton A. Player ◇ will win the game iff the concrete semantics assigns a set of formulas to S that is satisfied by L(A).

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

The endmarker $ yields the set of formulas {ε}, i.e. I^C($)={ε}. A terminal a:o→ o prepends a to a given word w. That is I^C(a) = prepend_a, where prepend_a distributes over conjunction and disjunction:

We apply prepend_a to sets of formulas by applying it to every element. Finally, I^C(op_F) where op_F has arity ℓ is an ℓ-ary conjunction (resp. disjunction) if Player □ (resp. ◇) owns F.

For M^C = (D^C, I^C) to be a model, we need our interpretation of terminals to be ⊓-continuous. This follows largely by the distributivity of our definitions.

Correctness of Semantics and Winning Strategies.

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

When σ_M^C(S) is satisfied by L(A) the concrete semantics gives a winning strategy for ◇: From a term t such that M^C〚t〛 σ_M^C is satisfied by L(A), Player ◇, when able to choose, picks a rewrite rule that transforms t to t′, where M^C〚t′〛 σ_M^C remains satisfied. The proof of Theorem 1 shows this is always possible, and, moreover, Player □ is unable to reach a term for which satisfaction does not hold. This does not yet give an effective strategy since we cannot compute M^C〚t〛 σ_M^C. However, the abstract semantics will be computable, and can be used in place of the concrete semantics by Player ◇ to implement the winning strategy.

The proof that σ_M^C(S) being unsatisfied implies a winning strategy for Player □ is more involved and requires the definition of a correctness relation between semantics and terms that is lifted to the level of functions, and shown to hold inductively.

5  Framework for Exact Fixed-Point Transfer

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

Consider the deterministic scheme G together with two models (left and right) M_l = (D_l, I_l) and M_r = (D_r, I_r). Our goal is to relate the semantics in these models in the sense that σ_Mr=α(σ_Ml). Such exact fixed-point transfer results are well-known in abstract interpretation. To generalize them to higher-order we give easy to instantiate conditions on α, M_l, and M_r that yield the above equality. Interestingly, exact fixed-point transfer results seem to be rare for higher-order (e.g. [48]). Our development is inspired by Abramsky’s lifting of abstraction functions to logical relations [3], which generalizes [11, 4]. These works focus on approximation and the compatibility we need for exactness is missing. Our framework is easier to apply than [15, 6], which are again concerned with approximation and do not offer (but may lead to) exact fixed-point transfer results.

For the terminology, an abstraction is a function α:D_l(o)→ D_r(o). To lift the abstraction to function domains, we define the notion of being compatible with α. Compatibility intuitively states that the function on the concrete domain is not more precise than what the abstraction function distinguishes. This allows us to define the abstraction of a function by applying the function and abstracting the result, α(f) α(v_l)=α(f v_l). Compatibility ensures the independence of the choice of v_l.

By definition, all ground elements v_l∈D_l(o) are compatible with α. For function domains, compatibility and the abstraction are defined as follows.

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

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

To prove α(σ_Ml)=σ_Mr, we need that rhs_Mr is an exact abstract transformer of rhs_Ml. The following lemma states this for all terms t, in particular those that occur in the equations. The generalization to product domains is immediate. Note that the result is limited to compatible valuations, but this will be sufficient for our purposes. The proof proceeds by induction on the structure of terms, while simultaneously proving M_l〚t〛 compatible with α. With this result, we obtain the required exact fixed-point transfer for precise abstractions.

6  Domains for Higher-Order Games

We propose two domains, abstract and optimized, that allow us to solve 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 2. Combined with Theorem 1, this will allow us to solve HOG. Computable in particular means the domain should be finite and the operations should be efficiently computable.

We define the M^A = (D^A, I^A) as follows. Again, we resolve the 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 acc(w) = { q | q –[w]→ q_f ∈ Q_f }. For a language L we have acc(L) = { acc(w) | w ∈ L }. The abstract domain for terms of ground kind is D^A(o) = PBool(acc(T^*)). The lifting to functions is as explained in Section 3. Satisfaction is now defined relative to a set Ω of elements of P(Q_NFA) (cf. Section 4). With finitely many atomic propositions, there are only finitely many formulas (up to logical equivalence). This means we no longer need sets of formulas to represent infinite conjunctions, but can work with plain formulas. The ordering is thus the ordinary implication with the meet being conjunction and top being true.

The interpretation of ground terms is I^A($) = Q_f and I^A(a)= pre_a. Here pre_a is the predecessor computation under label a, pre_a(Q)={q′∈ Q_NFA | q′–[a]→ q ∈ Q}. It is lifted to formulas by distributing it over conjunction and disjunction. The composition operators are again interpreted as conjunctions and disjunctions, depending on the owner of the non-terminal. Since we restrict the atomic propositions to acc(T^*), we have to show that the interpretations use only this restricted set. Proving I^A(s) is ⊓-continuous is standard.

Recall our concrete model is M^C=(D^C, I^C), where D^C=P(PBool(T^*)). To relate this model to M^A, we define the abstraction function α:D^C(o)→D^A(o). It leaves the Boolean structure of a formula unchanged but maps every word (which is an atomic proposition) to the set of states from which this word is accepted. For a set of formulas, we take the conjunction of the abstraction of the elements. This conjunction is finite as we work over a finite domain, so there is no need to worry about infinite syntax. Technically, we define α on PBool(T^*) by α(Φ)=∧_φ∈Φα(φ) for a set of formulas Φ∈P(PBool(T^*)), and

This definition is suitable in that α(σ_M^C)=σ_M^A entails the following.

To see that the theorem is a consequence of the exact fixed-point transfer, observe that {Q ∈ acc(T^*) | q₀ ∈ Q} = acc(L(A)). Then, by σ_M^A=α(σ_M^C) we have acc(L(A)) satisfies σ_M^A(S) iff it also satisfies α(σ_M^C(S)). This holds iff L(A) satisfies σ_M^C(S) (a simple induction over formulas). By Theorem 1, this occurs iff Player ◇ wins the game.

It remains to establish α(σ_M^C)=σ_M^A. With the framework, the exact fixed-point transfer follows from precision, Theorem 2. The proof of the following is routine.

Optimized Semantics.

The above model yields a decision procedure for HOG via Kleene iteration. Unfortunately, the complexity is one exponential too high: The height of the domain for a symbol of order k in the abstract model is (k+2)-times exponential, where the height is the length of the longest strictly descending chain in the domain. This gives the maximum number of steps of Kleene iteration needed to reach the fixed point.

We present an optimized version of our model that is able to close the gap: In this model, the domain for an order-k symbol is only (k+1)-times exponentially high. The idea is to resolve the atomic propositions in M^A, which are sets of states, into disjunctions among the states. The reader familiar with inclusion algorithms will find this decomposition surprising.

We first define α:PBool(acc(T^*))→ PBool(Q_NFA). The optimized domain will then be based on the image of α. This guarantees surjectivity. For a set of states Q, we define α(Q)=∨Q= ∨_{q∈ Q} q. For a formula, the abstraction function is defined to distribute over conjunction and disjunction. The optimized model is M^O = (D^O, I^O) with ground domain α(PBool(acc(T^*))). The interpretation is I^O($)=∨Q_f. For a, we resolve the set of predecessors into a disjunction, I^O(a) q = ∨pre_a({q}). The function distributes over conjunction and disjunction. Finally, I^O(op_F) is conjunction or disjunction of formulas, depending on the owner of the 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 ⊓-continuous as required.

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

It is sufficient to show σ_M^A(S) is satisfied by {Q ∈ acc(T^*) | q₀ ∈ Q} iff σ_M^O(S) is satisfied by {q₀}. Theorem 3 then yields the statement. Propositions Q in σ_M^A(S) are resolved into disjunctions ∨Q in σ_M^O(S). For such a proposition, we have Q∈ {Q ∈ acc(T^*) | q₀ ∈ Q} iff ∨Q is satisfied by {q₀}. This equivalence propagates to the formulas σ_M^A(S) and σ_M^O(S) as the Boolean structure coincides. The latter follows from α(σ_M^A(S))=σ_M^O(S).

Complexity.

To solve HOG, we compute the semantics σ_M^O and then evaluate σ_M^O(S) at the assignment {q₀}. For the complexity, assume that the highest order of any non-terminal in G is k. We show the number of iterations needed to compute the greatest fixed point is at most (k+1)-times exponential. We do this via a suitable upper bound on the length of strictly descending chains in the domains assigned by D^O.

The lower bound is via a reduction from the word membership problem for alternating k-iterated pushdown automata with polynomially-bounded auxiliary work-tape. This problem was shown by Engelfriet to be (k+1)EXP-hard. We can reduce this problem to 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.

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

Acknowledgments. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1]. The work instigated while some of the authors were visiting the Institute for Mathematical Sciences, National University of Singapore in 2016. The visit was partially supported by the Institute.

References

[1]

P. A. Abdulla, Y. Chen, L. Clemente, L. Holík, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing. In CAV, volume 6174 of LNCS, pages 132–147. Springer, 2010.

[2]

P. A. Abdulla, Y. Chen, L. Clemente, L. Holík, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Büchi automata inclusion testing. In CONCUR, volume 6901 of LNCS, pages 187–202. Springer, 2011.

[3]

S. Abramsky. Abstract interpretation, logical relations and Kan extensions. J. Log. Comp., 1(1):5–40, 1990.

[4]

S. Abramsky and C. Hankin. An introduction to abstract interpretation. In Abstract Interpretation of declarative languages, volume 1, pages 63–102. Ellis Horwood, 1987.

[5]

K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. LMCS, 3(3):1–23, 2007.

[6]

K. Backhouse and R. C. Backhouse. Safety of abstract interpretations for free, via logical relations and Galois connections. Sci. Comp. Prog., 51(1-2):153–196, 2004.

[7]

A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, volume 1243 of LNCS, pages 135–150. Springer, 1997.

[8]

A. Bouajjani and A. Meyer. Symbolic reachability analysis of higher-order context-free processes. In FSTTCS, volume 3328 of LNCS, pages 135–147. Springer, 2004.

[9]

C. Broadbent, A. Carayol, M. Hague, and O. Serre. A saturation method for collapsible pushdown systems. In ICALP, volume 7392 of LNCS, pages 165–176. Springer, 2012.

[10]

C. Broadbent and N. Kobayashi. Saturation-based model checking of higher-order recursion schemes. In CSL, volume 23 of LIPIcs, pages 129–148. Dagstuhl, 2013.

[11]

G. L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Sci. Comp. Prog., 7(3):249–278, 1986.

[12]

T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, volume 2380 of LNCS, pages 704–715. Springer, 2002.

[13]

T. Cachat. Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In ICALP, volume 2719 of LNCS, pages 556–569. Springer, 2003.

[14]

D. Caucal. On infinite terms having a decidable monadic theory. In MFCS, volume 2420 of LNCS, pages 165–176. Springer, 2002.

[15]

P. Cousot and R. Cousot. Higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis. In ICCL, pages 95–112. IEEE, 1994.

[16]

W. Damm. The IO- and OI-hierarchies. Theor. Comp. Sci., 20:95–207, 1982.

[17]

W. Damm and A. Goerdt. An automata-theoretical characterization of the OI-hierarchy. Inf. Comp., 71:1–32, 1986.

[18]

J. Engelfriet. Iterated stack automata and complexity classes. Inf. Comput., 95(1):21–75, 1991.

[19]

A. Farzan, Z. Kincaid, and A. Podelski. Proof spaces for unbounded parallelism. In POPL, pages 407–420. ACM, 2015.

[20]

A. Farzan, Z. Kincaid, and A. Podelski. Proving liveness of parameterized programs. In LICS, pages 185–196. IEEE, 2016.

[21]

Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In POPL, pages 151–164. ACM, 2014.

[22]

A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. ENTCS, 9:27–37, 1997.

[23]

S. Fogarty and M. Y. Vardi. Efficient Büchi universality checking. In TACAS, volume 6015 of LNCS, pages 205–220. Springer, 2010.

[24]

C. Grellois. Semantics of linear logic and higher-order model-checking. PhD thesis, Université Paris Diderot (Paris 7), 2016.

[25]

C. Grellois and P.-A. Melliès. Finitary semantics of linear logic and higher-order model-checking. In MFCS, volume 9234 of LNCS, pages 256–268. Springer, 2015.

[26]

C. Grellois and P.-A. Melliès. An infinitary model of linear logic. In FoSSaCS, volume 9034 of LNCS, pages 41–55. Springer, 2015.

[27]

C. Grellois and P.-A. Melliès. Relational semantics of linear logic and higher-order model checking. In CSL, volume 41 of LIPIcs, pages 260–276. Dagstuhl, 2015.

[28]

A. Haddad. IO vs OI in higher-order recursion schemes. In FICS, volume 77 of EPTCS, pages 23–30, 2012.

[29]

M. Hague, R. Meyer, and S. Muskalla. Domains for higher-order games. CoRR, abs/1705.00355, 2017. URL: .

[30]

M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In LICS, pages 452–461. IEEE, 2008.

[31]

M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown systems. In FoSSaCS, volume 4423 of LNCS, pages 213–227. Springer, 2007.

[32]

M. Hague and C.-H. L. Ong. Winning regions of pushdown parity games: A saturation method. In CONCUR, volume 5710 of LNCS, pages 384–398. Springer, 2009.

[33]

M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471–482. ACM, 2010.

[34]

M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In CSL-LICS, pages 51:1–51:10, 2014.

[35]

M. Hofmann and J. Ledent. A cartesian-closed category for higher-order model checking. In LICS. IEEE, 2017. To appear.

[36]

L. Holík, R. Meyer, and S. Muskalla. Summaries for context-free games. In FSTTCS, volume 65 of LIPIcs, pages 41:1–41:16. Dagstuhl, 2016.

[37]

Lukás Holík and Roland Meyer. Antichains for the verification of recursive programs. In NETYS, volume 9466 of LNCS, pages 322–336. Springer, 2015.

[38]

T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, volume 2303 of LNCS, pages 205–222. Springer, 2002.

[39]

T. Knapik, D. Niwiński, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In ICALP, volume 3580 of LNCS, pages 1450–1461. Springer, 2005.

[40]

N. Kobayashi. HorSat2: A model checker for HORS based on SATuration. A tool available at .

[41]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416–428. ACM, 2009.

[42]

N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, pages 179–188. IEEE, 2009.

[43]

Z. Long, G. Calin, R. Majumdar, and R. Meyer. Language-theoretic abstraction refinement. In FASE, volume 7212 of LNCS, pages 362–376. Springer, 2012.

[44]

D. A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363–371, 1975. URL: .

[45]

R. Meyer, S. Muskalla, and E. Neumann. Liveness verification and synthesis: New algorithms for recursive programs. .

[46]

Robin P. Neatherway, Steven J. Ramsay, and C.-H. Luke Ong. A traversal-based algorithm for higher-order model checking. In ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012, pages 353–364, 2012. URL: , http://dx.doi.org/10.1145/2364527.2364578.

[47]

C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81–90. IEEE, 2006.

[48]

S. J. Ramsay. Intersection-Types and Higher-Order Model Checking. PhD thesis, Oxford University, 2013.

[49]

S. J. Ramsay. Exact intersection type abstractions for safety checking of recursion schemes. In PPDP, pages 175–186. ACM, 2014.

[50]

S. Salvati. Recognizability in the simply typed lambda-calculus. In WoLLIC, volume 5514 of LNCS, pages 48–60. Springer, 2009.

[51]

S. Salvati and I. Walukiewicz. A model for behavioural properties of higher-order programs. In CSL, volume 41 of LIPIcs, pages 229–243. Dagstuhl, 2015.

[52]

S. Salvati and I. Walukiewicz. Typing weak MSOL properties. In FoSSaCS, volume 9034 of LNCS, pages 343–357. Springer, 2015.

[53]

S. Salvati and I. Walukiewicz. Using models to model-check recursive schemes. LMCS, 11(2):1–23, 2015.

[54]

I. Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comp., 164(2):234–263, 2001.

[55]

M. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In CAV, volume 4144 of LNCS, pages 17–30. Springer, 2006.

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 [42]. With intersection types, it is usually proven that there is a word or tree derivable by a HORS that is accepted by an automaton, i.e. a well-typed type environment can be certificate for the non-emptiness of the intersection L(scheme) ∩ L(Automaton) ≠ ∅. If the HORS is deterministic, L(scheme) consists of a single tree, so this is also decides the inclusion L(scheme) ⊆ L(Automaton). If we naively extend intersection types to 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. L(scheme) ∩ L(Automaton) = ∅. 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. [46] and Ramsay [48] 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.

B  Proofs for Section 3

B.1  Proof of Proposition 1

Let (ν_i)_{i ∈ N} be a descending chain of evaluations, i.e. ν_i ≥ ν_i+1 for all i ∈ N. It is to show that for all t, M〚t〛 is ⊓-continuous (in the argument ν) over the respective lattice, i.e.

We proceed by induction over t.

1. Case t = F or t = x.
   Both of these cases are identical, hence we only show the former. We have

   M〚F〛 (⊓i ∈ N νi) = (⊓i ∈ N νi)(F) = ⊓i ∈ N (νi(F)) = ⊓i ∈ N (M〚F〛 νi)

   where the first and final equalities are by definition of the concrete semantics, and the second is by definition of ⊓ over valuations ν_i.
2. Case t = s for some terminal s.
   Similar to the previous case, we have

   M〚s〛 (⊓i ∈ N νi) = I(s) = ⊓i ∈ N (M〚s〛 νi)

   by definition.
3. Case t = t₁ t₂.
   We have

   	M〚t1 t2〛 (⊓i ∈ N νi)
   (Definition of semantics) =	(M〚t1〛 (⊓i ∈ N νi)) (M〚t2〛 (⊓i ∈ N νi))
   (Induction hypothesis) =	(⊓i ∈ N (M〚t1〛 νi)) (⊓i ∈ N (M〚t2〛 νi))
   (Definition of ⊓ for functions) =	⊓i ∈ N ( (M〚t1〛 νi) (⊓i ∈ N (M〚t2〛 νi)) )
   (Continuity of M〚t1〛 νi ∈ D) =	⊓i ∈ N ⊓j ∈ N ( (M〚t1〛 νi) (M〚t2〛 νj)) )
   (Argued below) =	⊓i ∈ N ( (M〚t1〛 νi) (M〚t2〛 νi)) )
   (Definition of semantics) =	⊓i ∈ N (M〚t1 t2〛 νi)  .

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

   ⊓i ∈ N ⊓j ∈ N ( (M〚t1〛 νi) (M〚t2〛 νj)) ) = ⊓i ∈ N ( (M〚t1〛 νi) (M〚t2〛 νi)) )  .

   The right-hand side is greater than the left-hand side, because terms of the form ((M〚t₁〛 ν_i) (M〚t₂〛 ν_j)) where ν_i ≠ ν_j are missing in the RHS. To see that it is in fact equal, note that for two indices i,j ∈ N, we have either ν_i ≤ ν_j or ν_j ≤ ν_i, since the valuations form a descending chain. Let m = min{i,j}. We now use that ⊓-continuity implies monotonicity, and thus we have

   ((M〚t1〛 νm) (M〚t2〛 νm)) ≤ ((M〚t1〛 νi) (M〚t2〛 νj))  .

   Hence, for any expression ((M〚t₁〛 ν_i) (M〚t₂〛 ν_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. Case t = λ x . t′.
   We have

   	M〚λ x . t′〛 (⊓i ∈ N νi)
   (Definition of semantics) =	v ↦ (M〚t′〛 (⊓i ∈ N νi)[x ↦ v])
   (Induction hypothesis) =	v ↦ (⊓i ∈ N (M〚t′〛 νi[x ↦ v]))
   (Definition of ⊓ for functions) =	⊓i ∈ N ( (v ↦ M〚t1〛 νi[x ↦ v]) )
   (Definition of semantics) =	⊓i ∈ N (M〚λ x . t′〛 νi)  .

▫

B.2  Substitution Lemma

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

We show that for all ν : N⨃ V↛ D and all suitable terms t, t′, we have

We have by definition

and show by induction over t that

In the base cases we have

1. M〚F〛 ν[x ↦ M〚t′〛 ν] = ( ν[x ↦ M〚t′〛 ν] ) (F) = ν (F) = M〚F〛 ν = M〚F[x ↦ t′]〛 ν ,
2. M〚s〛 ν[x ↦ M〚t′〛 ν] = I (s) = M〚s〛 ν = M〚s[x ↦ t′]〛 ν ,
3. M〚x〛 ν[x ↦ M〚t′〛 ν] = M〚t′〛 ν = M〚x[x ↦ t′]〛 ν , and
4. M〚y〛 ν[x ↦ M〚t′〛 ν] = ( ν[x ↦ M〚t′〛 ν] ) (y) = ν (y) = M〚y〛 ν = M〚y[x ↦ t′]〛 ν , for variable y ≠ x.

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

which is equal to, by induction,

Finally, for abstraction, we can assume by α-conversion that y ≠ x, and we have

which is by induction equal to the function

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

C  Proofs for Section 4

C.1  Proof of Lemma 1

We show that for all non-ground terminals s, I^C(s) is ⊓-continuous. We need to treat the terminals a ∶ o → o of the original scheme and the terminals op_F that were introduced for the determinisation separately. In each case, assume a descending chain of arguments (x_i)_{i ∈ N}.

1. Case s = a.
   Since I^C(a) = prepend_a and we have

   prependa (⊓i ∈ N xi) = ⊓i ∈ N(prependa xi)

   by definition of prepend_a, we have the property as required.
2. Case s = op_F.
   We show the property when op_F is owned by ◇, and thus interpreted as ℓ-fold disjunction, conjunction is similar. We proceed by induction on the arity ℓ. In the base case ℓ = 1, I^C(op_F) is the identity function that is ⊓-continuous

   Now assume op_F has arity ℓ+1, and I^C(op_F) = ∨_ℓ+1 is an ℓ+1-fold disjunction. We have

   	∨ℓ+1 (⊓i ∈ N xi)
   (Definition of ∨ℓ+1) =	y1, …, yℓ  ↦  (⊓i ∈ N xi) ∨ ∨ℓ y1 ⋯ yℓ
   (Distributivity (see below)) =	y1, …, yℓ  ↦  ⊓i ∈ N (xi ∨ ∨ℓ y1 ⋯ yℓ)
   (Definition of ⊓ for functions) =	⊓i ∈ N (y1, …, yℓ  ↦  xi ∨ ∨ℓ y1 ⋯ yℓ)
   (Definition of ∨ℓ+1) =	⊓i ∈ N ∨ℓ+1  xi

   In the above we required ∨ to distribute over ⊓, which can be seen by induction over types. In the base case, that ∨ distributes over ⊓ = ∧ is standard. For the step case, we have for all f_i, g, and v

   	⎛ ⎝ (⊓i ∈ N fi) ∨ g ⎞ ⎠  v
   (Definition of ∨ and ⊓) =	⎛ ⎝ ⊓i ∈ N (fi v)  ⎞ ⎠ ∨ (g v)
   (Induction) =	⊓i ∈ N  ⎛ ⎝ (fi v) ∨ (g v)  ⎞ ⎠
   (Definition of ∨ and ⊓) =	⎛ ⎝ ⊓i ∈ N(fi ∨ g)  ⎞ ⎠  v  .

▫

C.2  Proof of Theorem 1

We are required to show σ_M^C(S) is satisfied by L(A) iff there is a winning strategy foryer Player ◇. The theorem is shown in the following two lemmas.

First, we introduce some notation. We write prepend_w for w=a₁… a_n to abbreviate prepend_a1 ∘ ⋯ ∘ prepend_an.

In what follows, whenever we refer to a term t, we mean a term built over N⨃ T, but not over T^det. The terminals op_F are excluded because they do not occur in the game, they are only introduced in the determinized scheme.

We will demonstrate a strategy for ◇ that maintains the invariant that the current (variable-free) term t reached is such that M^C〚t〛 σ_M^C is satisfied by L(A). All plays are infinite or generate a word w. Since we maintain M^C〚t〛 σ_M^C is satisfied by L(A), if t represents a word w, we know w is accepted by A and Player ◇ wins the game.

Initially, we have M^C〚S〛 σ_M^C = σ_M^C(S) which is satisfied by L(A) by assumption. Thus, suppose play reaches a term t such that M^C〚t〛 σ_M^C is satisfied by L(A). There are two cases.

In the first case t = a₁ (⋯ (a_n $)) and let w = a₁ … a_n. Since

and w is satisfied by L(A), we know w ∈ L(A) and Player ◇ has won the game.

In the second case, we have t = a₁(⋯(a_n(F t₁ ⋯ t_m))). By assumption, we know

is satisfied by L(A). Let F = e₁, …, F = e_ℓ be the rewrite rules for F. There are two subcases.

1. If F is owned by ◇, then since M^C〚F〛 = M^C〚e₁〛 ∨ ⋯ ∨ M^C〚e_ℓ〛 there must exist some i such that

   prependa1 … an( (MC〚ei〛 σMC) (MC〚t1〛 σMC) ⋯  (MC〚tm〛 σMC) )

   is satisfied by L(A). The strategy of Player ◇ is to choose the i^th rewrite rule.

   We need to show the invariant is maintained. Let e_i = λ x₁, …, x_m . e. We have (using the substitution lemma, Lemma 7),

   	prependa1 … an( (MC〚λ x1, …, xm . e〛 σMC) (MC〚t1〛 σMC) ⋯  (MC〚tm〛 σMC) )
   =	prependa1 … an( MC〚(λ x1, …, xm . e) t1 … tm〛 σMC )
   =	prependa1 … an( MC〚e[x1 ↦ t1, …, xm ↦ tm]〛 σMC )
   =	MC〚a1(⋯(an(e[x1 ↦ t1, …, xm ↦ tm])))〛 σMC  .

   Note that the term a₁(⋯(a_n(e[x₁ ↦ t₁, …, x_m ↦ t_m]))) is the result of Player ◇ rewriting F via F = e_i. Since the satisfaction by L(A) passes through the equalities, Player ◇’s move maintains the invariant as required.

2. If F is owned by □ the argument proceeds as in the previous case. The key difference is that we have to show satisfaction is maintained no matter which move □ chooses. However, since in this case M^C〚F〛 = M^C〚e₁〛 ∧ ⋯ ∧ M^C〚e_ℓ〛 then for all i we have

   prependa1 … an( (MC〚ei〛 σMC) (MC〚t1〛 σMC) ⋯  (MC〚tm〛 σMC) )

   is satisfied by L(A). The remainder of the argument is identical.

▫

In what follows, whenever we refer to a term t, we mean a term built over N⨃ T, but not over T^det. The terminals op_F are excluded because they do not occur in the game, they are only introduced in the determinized scheme.

For φ ∈ D^C(o) and a variable-closed term t of kind o, we define φ to be sound for t, denoted φ ⊢ t, if for all w∈ T^* such that prepend_w(φ) is not satisfied by L(A), Player □ has a winning strategy from term w(t). For w=ε, we set prepend_ε(φ)=φ and let ε(t)=t. We can now restate the lemma as

In particular, since σ_M^C(S) is not satisfied by L(A) it is the case that prepend_ε(σ_M^C(S)) is not satisfied. This means Player □ has a winning strategy from ε(S) = S.

In general, for Ξ ∈ D^C(κ₁ → κ₂), we will also define Ξ ⊢ t for terms of kind κ₁ → κ₂. That is, for a variable-closed term t of kind κ₁ → κ₂ and a function Ξ ∈ D^C(κ₁ → κ₂), we define Ξ ⊢ t to hold whenever for all variable-closed terms t′ of kind κ₁ and Ξ′ ∈ D^C(κ₁) such that Ξ′ ⊢ t′ we have Ξ Ξ′ ⊢ t t′:

Similarly, we need to extend ⊢ to terms t with free variables x=x₁ … x_m. Here, we make the free variables explicit and write t (x). We define for Ξ : (V↛ D^C) → D^C that Ξ ⊢ t(x) by requiring that for any variable-closed terms t₁, …, t_m and any Ξ₁, …, Ξ_m ∈ D^C with Ξ_j ⊢ t_j for all 1≤ j≤ m, we have Ξ ν ⊢ t [∀ j ∶ x_j ↦ t_j], where ν maps x_j to Ξ_j.

We now show the following. For every number of iterations i in the fixed-point calculation, we have MC〚t〛 σMCi ⊢ 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 σMCi to assign valuations to free-variables. Thus we will write νi to denote a valuation such that νi(F) = σMCi(F) for any non-terminal F.

Base case i.
In the base case, we have i=0 and νⁱ=⊤ 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. Case t = $.
   For all i, we have M^C〚$〛 νⁱ = ε. Take any word w such that prepend_w(ε) is not satisfied by L(A). No moves can be made from w(ε) and Player □ has won the game.
2. Case t = a.
   We again reason over all i and show that

   MC〚a〛 νi Ξ = prependa(Ξ) ⊢ a(t)

   for any variable-closed term t : o and any Ξ so that Ξ ⊢ t. Take any word w such that prepend_w(prepend_a(Ξ)) is not satisfied by L(A). It follows that prepend_wa(Ξ) is also not satisfied by L(A). From Ξ ⊢ t, Player □ has a winning strategy from wa(t). Since wa(t) = w(a(t)) we are done.
3. Case t = x.
   For all i and all extensions νi of σMCi, we have

   MC〚x〛 νi = νi(x).

   Take any νⁱ(x)=Ξ and any variable-closed term t′ with Ξ ⊢ t′. Then νⁱ(x) ⊢ x[x ↦ t′] 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₁, …, t_m with corresponding Ξ_j such that Ξ_j ⊢ t_j. We have

Thus, trivially M^C〚F〛 ν⁰ ⊢ F since true is never unsatisfied.
Step case t.
In both cases, the argumentation is independent of the actual iteration count. Therefore, we give it for a general i rather than for 0.

1. Case t = t′ t″.
   Assume we already know that

   MC〚t′〛 νi ⊢ t′    and    MC〚t″〛 νi ⊢ t″  .

   Our task is to show that

   MC〚t′ t″〛 νi = (MC〚t′〛 νi) (MC〚t″〛 νi) ⊢ t′ t″  .

   Let the free variables be x₁, …, x_n and consider Ξ₁ ⊢ t₁ to Ξ_n⊢ t_n. Let νⁱ map x_j to Ξ_j for all 1≤ j≤ n. By the definition of ⊢ for terms with free variables, we have M^C〚t′〛 νⁱ ⊢ t′ [∀ j: x_j ↦ t_j] and M^C〚t″〛 νⁱ ⊢ t″ [∀ j: x_j ↦ t_j]. Then, by the definition of ⊢ for functions, we obtain

   MC〚t′ t″〛 νi =	(MC〚t′〛 νi) (MC〚t″〛 νi)
   ⊢	(t′[∀ j: xj ↦ tj]) (t″[∀ j: xj ↦ tj]) = (t′ t″)[∀ j: xj ↦ tj]  .

   This means M^C〚t′ t″〛 νⁱ ⊢ t′ t″ as required.
2. Case t = λ x.e.
   Let the free variables of e be x, x₁,…, x_n. For M^C〚λ x.e〛 νⁱ⊢ λ x.e, we have to argue that for any Ξ₁⊢ t₁ to Ξ_n⊢ t_n with νⁱ mapping x_i to Ξ_i for all 1≤ i≤ n, we get

   MC〚λ x.e〛 νi ⊢ (λ x.e)[∀ j: xj↦ tj]  .

   This in turn means that for any Ξ⊢ t, we have to show

   (MC〚λ x.e〛 νi) Ξ⊢ ((λ x.e)[∀ j: xj↦ tj]) t  .

   By the definition of the semantics, we have

   (MC〚λ x.e〛 νi) Ξ = MC〚e〛 νi[x↦ Ξ]  .

   Moreover, since the t_j are variable-closed, they in particular are not affected by replacing x and we get

   ((λ x.e)[∀ j: xj↦ tj]) t = (λ x.(e[∀ j: xj↦ tj])) t.

   In the game, λ-redexes of the form (λ x.e) t do not occur at all: When a non-terminal F is rewritten to its right-hand side λ x.e, this yields e[x↦ t] within a single step. This means the game equates (λ x.(e[∀ j: x_j↦ t_j])) t with e[x↦ t, ∀ j: x_j↦ t_j]. Hence, all that remains to be shown is

   MC〚e〛 νi[x↦ Ξ] ⊢ e[x↦ t, ∀ j: xj↦ tj]  .

   This holds by the hypothesis of the inner induction, showing M^C〚e〛 νⁱ⊢ 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 M^C〚F〛 νⁱ⁺¹⊢ F. Let F take m arguments and consider Ξ₁⊢ t₁ to Ξ_m⊢ t_m. The task is to prove M^C〚F〛 νⁱ⁺¹ Ξ₁ … Ξ_m⊢ F t₁ … t_m. To ease the notation, assume there are two right hand sides e₁′, e₂ for F, i.e. we have the rules F = λ x₁ … λ x_m.e₁ and F = λ x₁ … λ x_m.e₂. This means the right-hand side in the determinised scheme is F = λ x₁ … λ x_m . (op_F e₁ e₂). Then,

Here, I^C(op_F) is a conjunction or disjunction, depending on the owner of F. Recall that the conjunction and disjunction of functions are defined by evaluating the argument functions separately and combining the results. This means

With the same reasoning, we obtain

We have to prove that for any w∈ T^*, if L(A) does not satisfy the formula

then Player □ has a winning strategy from w(F t₁ … t_m).

Assume Player ◇ owns F and the formula is not satisfied. If Player □ owns F, the reasoning is similar. Since we have a disjunction for Player ◇, prependw(MC〚e1′〛 νi Ξ1 … Ξm) is not satisfied. By the hypothesis of the outer induction, we obtain MC〚e1′〛 νi ⊢ e1 and thus MC〚e1′〛 νi Ξ1 … Ξm ⊢ e1′ t1 … tm. As in the case of λ-abstraction above, we use that the game identifies e1′ t1 … tm and e1 [x1 ↦ t1, … em ↦ tm]. Hence, Player □ has a winning strategy from w(e1 [x1 ↦ t1, … em ↦ tm]). The same argumentation applies to prependw(MC〚e2〛 νi Ξ1 … Ξm). Consequently, whichever move Player ◇ makes at w(F t1 … tm), Player □ has a winning strategy.
This finishes the outer induction, proving that MC〚t〛 σMCi ⊢ t for all terms t and all i ∈ N. We would like to conclude MC〚t〛 σMC ⊢ t. Since the cppo under consideration is not finite, this needs to be proven separately.
Limit case.
We have shown MC〚t〛 σMCi ⊢ t for all i ∈ N; we now show MC〚t〛 σMC ⊢ t noting by Kleene that σMC = ⊓i ∈ N σMCi. Once we have this we have σMC(S) ⊢ S which proves the lemma.

We formulate a slightly more general induction hypothesis for induction over kinds: Given a descending sequence of Ξ_i for all i ∈ N such that each Ξ_i ⊢ t, we have ⊓_{i ∈ N} Ξ_i ⊢ t. In the base case we have t is of kind o and we assume Ξ_i ⊢ t. We now argue ⊓_{i ∈ N} Ξ_i ⊢ t.

Take any w and suppose prepend_w(⊓_{i ∈ N} Ξ_i) is not satisfied, then we need to show by the definition of ⊢ that Player □ has a winning strategy. Since ⊓ is conjunction, if

is not satisfied, it must be the case that for some i we have prepend_w(Ξ_i) is not satisfied. In this case, we have Ξ_i ⊢ t by assumption and thus by the definition of ⊢ that Player □ has a winning strategy from w(t). This proves ⊓_{i ∈ N} Ξ_i ⊢ t.

If t is of kind κ₁ → κ₂ we need to show for all Ξ ⊢ t′ that (⊓_{i ∈ N} Ξ_i) Ξ ⊢ t t′. We have by the definition of ⊓ over functions

Since by assumption on Ξ_i and definition of ⊢ for function kinds, we have Ξ_i Ξ ⊢ t t′ for each i. By the induction on the kind, we obtain ⊓_{i ∈ N}(Ξ_i Ξ) ⊢ t t′ . Since (⊓_{i ∈ N} Ξ_i) σ = ⊓_{i ∈ N} (Ξ_i σ) we establish the desired statement that finishes the induction.

Finally, since MC〚t〛 σMCi satisfies the conditions of the above induction hypothesis and because we have already shown MC〚t〛 σMCi ⊢ t for all t, we obtain

Then, since using continuity of M^C〚t〛 we have

we obtain the lemma as required. ▫

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.

We show that, if (P1) holds, then for every κ∈ Κ and every v_r∈D_r(κ) there is a compatible v_l∈D_l(κ) with α(v_l)=v_r. We proceed by induction on kinds. The base case is given by the assumption (P1) and the fact that every ground element is compatible. Assume we have the required surjectivity of α for κ₁ and κ₂ and consider f_r∈D_r(κ₁→ κ₂). The task is to find a compatible function f_l so that α(f_l)=f_r. Assume f_r v_r = v_r′. By surjectivity for κ₁, there are compatible elements in α⁻¹(v_r), and similar for v_r′. Let v_l′ be a compatible element that is mapped to v_r′ by α. We define f_l v_l = v_l′ for all compatible v_l ∈ α⁻¹(v_r). Since α is total on D(κ₁), 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¹ and v_l² with α(v_l¹)=α(v_l²). By definition, both are mapped identically by f_l, f_l v_l¹=f_l v_l². Hence, in particular the abstractions coincide. Moreover, given a compatible v_l, we defined f_l v_l = v_l′ to be a compatible element.

Concerning the equality of the functions, we have α(f_l) v_r = α(f_l v_l) = α(v_l′) = v_r′. The first equality is the definition of abstraction for functions and the fact that α⁻¹(v_r) contains compatible elements, one of them being v_l, the second is the fact that v_l is mapped to v_l′, and the last is by v_l′ ∈ α⁻¹(v_r′). ▫

We proceed by induction on kinds to show that, if (P1) and (P2) hold, then for all kinds κ∈ Κ and for all descending chains of compatible values f₁, f₂, … ∈D(κ), we have ⊓_{i∈ N}f_i again compatible and α(⊓_{i∈ N}f_i)=⊓_{i∈ N}α(f_i). The base case is the assumption.

In the induction step, let κ=κ₁→ κ₂ and f₁, f₂,…∈D_l(κ) be a descending chain of compatible elements. Let v_l∈ D_l(κ₁) be compatible. The following equalities will be helpful:

The first equality is the definition of ⊓ on functions, the second is the induction hypothesis for κ₂, the third is compatibility of the f_i and v_l, the last is again ⊓ on functions.

To show compatibility, note that the above implies α((⊓_{i∈ N} f_i) v_l)=α((⊓_{i∈ N} f_i) v_l′) as long as α(v_l)=α(v_l′), for all compatible v_l, v_l′∈D_l(κ₁). For compatibility of (⊓_{i∈ N} f_i) v_l with v_l∈D_l(κ₁) compatible, note that (⊓_{i∈ N} f_i) v_l=⊓_{i∈ N} (f_i v_l). The latter is the meet over a descending chain of compatible elements in κ₂. By the induction hypothesis on κ₂, it is again compatible.

For ⊓-continuity, consider a value v_r∈D_r(κ₁). By Lemma 10, there is a compatible v_l∈D_l(κ₁) with α(v_l)=v_r. We have

The first equality is the definition of abstraction on functions. Note that we need here the fact that ⊓_{i∈ N}f_i is compatible by the induction hypothesis. The second equality is the auxiliary one from above. The last equality is by α(v_l)=v_r. ▫

We show that, if (P3) holds, then α(⊤_κ^l)=⊤_κ^r for all κ∈ Κ. We proceed by induction on kinds. The base case is given by the assumption (P3). Assume for κ₂, we have α(⊤_κ2^l)=⊤_κ2^r. Consider function ⊤_{κ1→ κ2}^l∈D_l(κ₁→κ₂). We have to show α(⊤_{κ1→ κ2}^l)=⊤_{κ1→ κ2}^r. If the given top element is not compatible, this holds. Assume it is. For v_r ∈ D_r(κ₁), there are two cases. If there is no compatible v_l∈ D_l(κ₁) with α(v_l)=v_r, we have

If there is such a v_l, we obtain

The first equality is the definition of abstraction for functions, the next is the fact that ⊤_{κ1→ κ2}^l maps every element v_l ∈ D_l(κ₁) to ⊤_κ2^l. The image of ⊤_κ2^l is ⊤_κ2^r by the induction hypothesis. The last equality is the definition of ⊤_{κ1→ κ2}^r. ▫

D.2  Proof of Lemma 2

Assume (P1), (P4), and (P5) hold. We show, for all terms t and all compatible ν, M_l〚t〛 ν is compatible and α(M_l〚t〛 ν)=M_r〚t〛 α(ν). We proceed by structural induction on t.

1. Case F, x.
   By the assumption, M_l〚F〛 ν = ν(F) is compatible. Moreover,

   α(Ml〚F〛 ν)=α(ν(F))=α(ν)(F)=Mr〚F〛 α(ν)

   holds. For x∈ V, the reasoning is similar.
   
2. Case terminal s.
   Note that M_l〚s〛 ν=I_l(s). If s is ground, the claim holds by (P4). Let s:κ₁→ κ₂. For compatibility, consider v_l, v_l′∈D(κ₁) compatible with α(v_l)=α(v_l′). Then

   α(Il(s) vl)=Ir(s) α(vl) = Ir(s) α(vl′) = α(Il(s) vl′).

   The first equality is (P4), the next is α(v_l)=α(v_l′), and the last is again (P4). The second requirement on compatibility is satisfied by (P5).
   To show α(M_l〚s〛 ν) = M_r〚s〛 α(ν), consider a value v_r ∈D_r(κ₁). By Lemma 10, there is some compatible v_l∈D_l(κ₁) with α(v_l)=v_r. We have

   α(Il(s)) vr = α(Il(s) vl)= Ir(s) α(vl) =Ir(s) vr.

   The first equality is compatibility of I_l(s) and the definition of function abstraction. The next equality is (P4). The last is α(v_l)=v_r.
   

For the induction step, assume the claim holds for t₁ and t₂.

1. Case t₁ t₂.
   For compatibility, observe that M_l〚t₁ t₂〛 ν=(M_l〚t₁〛 ν) (M_l〚t₂〛 ν). Moreover, M_l〚t₁〛 ν and M_l〚t₂〛 ν are both compatible by the induction hypothesis. By definition of compatibility, applying a compatible function to a compatible argument yields a compatible value. Hence, M_l〚t₁ t₂〛 ν is compatible.
   For the equality, note that

   Mr〚t1 t2〛 α(ν) = (Mr〚t1〛 α(ν)) (Mr〚t2〛 α(ν)) = α(Ml〚t1〛 ν) α(Ml〚t2〛 ν).

   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:

   α(Ml〚t1〛 ν) α(Ml〚t2〛 ν) = α((Ml〚t1〛 ν) (Ml〚t2〛 ν)) = α(Ml〚t1 t2〛 ν).

2. Case λ x:κ.t₁.
   We argue for compatibility. Consider compatible v_l and v_l′ with α(v_l)=α(v_l′). By definition of the semantics and the induction hypothesis, we have

   α((Ml〚λ x.t1〛 ν) vl) = α(Ml〚t1〛 ν[x↦ vl]) = Mr〚t1〛 α(ν[x↦ vl])  .

   For v_l′, the reasoning is similar. Since α(v_l)=α(v_l′), we have α(ν[x↦ v_l])=α(ν[x↦ v_l′]). Hence, M_r〚t₁〛 α(ν[x↦ v_l])=M_r〚t₁〛 α(ν[x↦ v_l′]). We conclude the desired equality.

   For the second requirement in compatibility, let v_l be compatible. By definition of the semantics, (M_l〚λ x.t₁〛 ν) v_l = M_l〚t₁〛 ν[x↦ v_l]. Since ν and v_l are compatible, ν[x↦ v_l] is compatible. Hence, M_l〚t₁〛 ν[x↦ v_l] is compatible by the induction hypothesis.
   To prove M_r〚λ x.t₁〛 α(ν) = α(M_l〚λ x.t₁〛 ν), consider an arbitrary value v_r ∈ D_r(κ). Let v_l∈D_l(κ₁) be compatible with α(v_l)=v_r, which exists by Lemma 10. We have:

   (Mr〚λ x.t1〛 α(ν)) vr = Mr〚t1〛 α(ν)[x ↦ vr] = Mr〚t1〛 α(ν[x↦ vl])  .

   We showed above that M_l〚λ x.t₁〛 ν is compatible. Using the definition of abstraction for functions and the definition of the semantics, the other function yields

   α(Ml〚λ x.t1〛 ν) vr = α((Ml〚λ x.t1〛 ν) vl)= α(Ml〚t1〛 ν[x↦ vl])  .

   With the induction hypothesis, α(M_l〚t₁〛 ν[x↦ v_l])=M_r〚t₁〛 α(ν[x↦ v_l]).