Contextual Approximation and Higher-Order Procedures

Abstract

We investigate the complexity of deciding contextual approximation (refinement) in finitary Idealized Algol, a prototypical language combining higher-order types with state. Earlier work in the area established the borderline between decidable and undecidable cases, and focussed on the complexity of deciding approximation between terms in normal form.

In contrast, in this paper we set out to quantify the impact of locally declared higher-order procedures on the complexity of establishing contextual approximation in the decidable cases. We show that the obvious decision procedure based on exhaustive $\beta$-reduction can be beaten. Further, by classifying redexes by levels, we give tight bounds on the complexity of contextual approximation for terms that may contain redexes up to level k, namely, $(k-1)$-EXPSPACE-completeness. Interestingly, the bound is obtained by selective $\beta$-reduction: redexes from level 3 onwards can be reduced without losing optimality, whereas redexes up to order 2 are handled by a dedicated decision procedure based on game semantics and a variant of pushdown automata.

Research supported by EPSRC (EP/J019577/1, EP/M011801/1).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Contextual approximation (refinement) is a fundamental notion in programming language theory, facilitating arguments about program correctness [14] as well as supporting formal program development [5]. Intuitively, a term $M_1$ is said to contextually approximate another term $M_2$, if substituting $M_1$ for $M_2$ in any context will not lead to new observable behaviours. Being based on universal quantification over contexts, contextual approximation is difficult to establish directly. In this paper, we consider the problem of contextual approximation in a higher-order setting with state. Contextual reasoning at higher-order types is a recognised challenge and a variety of techniques have been proposed to address it, such as Kripke logical relations [3] or game models [2]. In this work, we aim to understand the impact of locally defined higher-order procedures on the complexity of establishing contextual approximation. Naturally, one would expect the complexity to grow in the presence of procedures and it should grow as the type-theoretic order increases. We shall quantify that impact by providing tight complexity bounds for contextual approximation in our higher-order framework. The results demonstrate that, from the complexity-theoretic point of view, it is safe to inline procedures only down to a certain level. Below that level, however, it is possible to exploit compositionality to arrive at better bounds than those implied by full inlining.

The vehicle for our study is Idealized Algol [1, 13], the protypical language for investigating the combination of local state with higher-order procedures. In order to avoid obviously undecidable cases, we restrict ourselves to its finitary variant $\mathsf {IA}_\mathrm{f}$, featuring finite base types and no recursion (looping is allowed, though). Both semantic and syntactic methods were used to reason about Idealized Algol [1, 12] in the past. In particular, on the semantic front, there exists a game model that captures contextual approximation (in the sense of inequational full abstraction) via complete-play inclusion. Earlier work in the area [6, 9, 11] used this correspondence to map out the borderline between decidable and undecidable cases within $\mathsf {IA}_\mathrm{f}$. The classification is based on type-theoretic order: a term is of order i if its type is of order at most i and all free variables have order less than i. We write $\mathsf {IA}_{i}$ for the set of $\mathsf {IA}_\mathrm{f}$-terms of order i. It turns out that contextual approximation is decidable for terms of all orders up to 3, but undecidable from order 4 onwards. The work on decidability has also established accurate complexity bounds for reasoning about contextual approximation between terms in $\beta$-normal form as well as terms with the simplest possible $\beta$-redexes, in which arguments can only be of base type. For order-3 terms, the problem can be shown EXPTIME-complete [11], while at orders 0, 1, 2 it is PSPACE-complete [10]. In this paper, we present a finer analysis of the decidable cases and consider arbitrary $\beta$-redexes. In particular, functions can be used as arguments, which corresponds to the inlining of procedures.

We evaluate the impact of redexes by introducing a notion of their level: the level of a $\beta$-redex $(\lambda x.M)N$ will be the order of the type of $\lambda x.M$. Accordingly, we can split $\mathsf {IA}_{i}$ into sublanguages $\mathsf {IA}_{i}^k$, in which terms can contain redexes of level up to k. $\mathsf {IA}_{i}^0$ is then the normal-form case and $\mathsf {IA}_{i}^1$ is the case of base-type arguments. Obviously, the problem of contextually approximating $\mathsf {IA}_{i}^k$ ($i\le 3, k\ge 2$) terms can be solved by $\beta$-reduction (and an appeal to the results for $\mathsf {IA}_{i}^0$), but this is known to result in a k-fold exponential blow-up, thus implying a $(k+1)$-EXPTIME upper bound for $\mathsf {IA}_{3}^k$. This bound turns out to be suboptimal. One could lower it by reducing to $\mathsf {IA}_{i}^1$ instead, which would shave off a single exponential, but this is still insufficient to arrive at the optimal bound. It turns out, however, that reducing $\mathsf {IA}_{3}^k$ terms to $\mathsf {IA}_{3}^2$ (all redexes up to order 3 are eliminated) does not lead to a loss of optimality. To work out the accurate bound for the $\mathsf {IA}_{3}^2$ case, one cannot apply further $\beta$-reductions, though. Instead we devise a dedicated procedure based on game semantics and pushdown automata. More specifically, we introduce a variant of visibly pushdown automata [4] with $\epsilon$-transitions and show how to translate $\mathsf {IA}_{3}^2$ into such automata so that the accepted languages are faithful representations of the term’s game semantics [1]. The translation can be performed in exponential time and, crucially, the automata correspoding to $\mathsf {IA}_{3}^2$-terms satisfy a boundedness property: the stack symbols pushed on the stack during $\epsilon$-moves can only form contiguous segments of exponential length with respect to the term size. This allows us to solve the corresponding inclusion problem in exponential space with respect to the original term size. Consequently, we can show that $\mathsf {IA}_{3}^2$ contextual approximation is in EXPSPACE.

The above result then implies that program approximation of $\mathsf {IA}_{3}^k$-terms is in $(k-1)$-EXPSPACE. Furthermore, we can prove matching lower bounds for $\mathsf {IA}_{1}^k$. The table below summarises the complexity results. The results for $k\ge 2$ are new.

	$k=0$	$k=1$	$k\ge 2$
$\mathsf {IA}_{1}^k$	PSPACE-complete [10]	PSPACE-complete [10]	$(k-1)$-EXPSPACE-complete
$\mathsf {IA}_{2}^k$	PSPACE-complete [10]	PSPACE-complete [10]	$(k-1)$-EXPSPACE-complete
$\mathsf {IA}_{3}^k$	EXPTIME-complete [11]	EXPTIME-complete [11]	$(k-1)$-EXPSPACE-complete

2 Idealized Algol

We consider a finitary version $\mathsf {IA}_\mathrm{f}$ of Idealized Algol with active expressions [1]. Its types are generated by the following grammar.

$$ \theta \,{:}{:}\!\!= \beta \,|\, \theta \rightarrow \theta \qquad \beta \, {:}{:}\!\!= \mathsf {com}\,|\, \mathsf {exp}\,|\,\mathsf {var}$$

$\mathsf {IA}_\mathrm{f}$ can be viewed as a simply-typed $\lambda$-calculus over the base types $\mathsf {com},\mathsf {exp},\mathsf {var}$ (of commands, expressions and variables respectively) augmented with the constants listed below

$$\begin{array}{c} \mathbf{skip}:\mathsf {com}\qquad i:\mathsf {exp}\quad (0\le i\le max )\qquad \mathbf{succ}: {\mathsf {exp}} \rightarrow {\mathsf {exp}}\qquad \mathbf{pred}: {\mathsf {exp}} \rightarrow {\mathsf {exp}}\\ \mathbf{ifzero}_\beta : {\mathsf {exp}}\rightarrow {\beta } \rightarrow {\beta } \rightarrow {\beta }\qquad \mathbf{seq}_\beta : {\mathsf {com}}\rightarrow {\beta }\rightarrow {\beta }\qquad \mathbf{deref}: {\mathsf {var}}\rightarrow {\mathsf {exp}}\\ \mathbf{assign}: {\mathsf {var}} \rightarrow {\mathsf {exp}} \rightarrow {\mathsf {com}}\qquad \mathbf{cell}_\beta : ({\mathsf {var}} \rightarrow {\beta })\rightarrow {\beta }\\ \mathbf{while}: \mathsf {exp}\rightarrow \mathsf {com}\rightarrow \mathsf {com}\qquad \mathbf{mkvar}: (\mathsf {exp}\rightarrow \mathsf {com})\rightarrow \mathsf {exp}\rightarrow \mathsf {var}\end{array}$$

where $\beta$ ranges over base types and $\mathsf {exp}=\{\,0,\cdots , max \,\}$. Other $\mathsf {IA}_\mathrm{f}$-terms are formed using $\lambda$-abstraction and application

$$ \frac{\displaystyle {\varGamma } \vdash {M:\theta \rightarrow \theta '}\quad {\varGamma } \vdash {N:\theta }}{\displaystyle {\varGamma } \vdash {M N:\theta '}} \qquad \frac{\displaystyle {\varGamma ,x:\theta } \vdash {M: \theta '}}{\displaystyle {\varGamma } \vdash {\lambda x^\theta .M:\theta \rightarrow \theta '}} $$

using the obvious rules for constants and free identifiers. Each of the constants corresponds to a different programming feature. For instance, the sequential composition of M and N (typically denoted by M; N) is expressed as $\mathbf{seq}_\beta M N$, assignment of N to M () is represented by $\mathbf{assign} M N$ and $\mathbf{cell}_\beta (\lambda x.M)$ amounts to creating a local variable x visible in M (). $\mathbf{mkvar}$ is the so-called bad-variable constructor that makes it possible to construct terms of type $\mathsf {var}$ with prescribed read- and write-methods. $\mathbf{while} M N$ corresponds to . We shall write $\varOmega _\beta$ for the divergent constant that can be defined using .

The operational semantics of $\mathsf {IA}_\mathrm{f}$, based on call-by-name evaluation, can be found in [1]; we will write $M\!\Downarrow$ if M reduces to $\mathbf {skip}$. We study the induced contextual approximation.

Definition 1

We say that ${\varGamma } \vdash {M_1:\theta }$ contextually approximates ${\varGamma } \vdash {M_2:\theta }$ if, for any context $C[-]$ such that $C[M_1],C[M_2]$ are closed terms of type $\mathsf {com}$, we have $C[M_1]\!\Downarrow$ implies $C[M_2]\!\Downarrow$. We then write .

Even though the base types are finite, $\mathsf {IA}_\mathrm{f}$ contextual approximation is not decidable [9]. To obtain decidability one has to restrict the order of types, defined by:

$$ \mathsf {ord}({\beta })=0\qquad \quad \mathsf {ord}({{\theta }\rightarrow {\theta }'})= \max (\mathsf {ord}({{\theta }})+1,\mathsf {ord}({{\theta }'})). $$

Definition 2

Let $i\ge 0$. The fragment $\mathsf {IA}_{i}$ of $\mathsf {IA}_\mathrm{f}$ consists of $\mathsf {IA}_\mathrm{f}$-terms $x_1:$ $\theta _1,\cdots , x_n:\theta _n{M:\theta }$ such that $\mathsf {ord}({\theta _j})<i$ for any $j=1,\cdots ,n$ and $\mathsf {ord}({\theta })\le i$.

Contextual approximation is known to be decidable for $\mathsf {IA}_{1}$, $\mathsf {IA}_{2}$ and $\mathsf {IA}_{3}$ [11], but it is undecidable for $\mathsf {IA}_{4}$ [9].

Definition 3

• The level of a $\beta$-redex $(\lambda x^\theta .M)N$ is the order of the type of $\lambda x^\theta .M$.

• A term has degree k if all redexes inside it have level at most k.

• $\mathsf {IA}_{i}^k$ is the subset of $\mathsf {IA}_{i}$ consisting of terms whose degree is at most k.

$\beta$-reduction can be used to reduce the degree of a term by one at an exponential cost.

Lemma 1

Let $d\ge 1$. A $\lambda$-term M of degree d can be reduced to a term $M'$ of degree $d-1$ with a singly-exponential blow-up in size.

Fig. 1.

Constructions on arenas

3 Games

Game semantics views computation as an exchange of moves between two players, called O and P. It interprets terms as strategies for P in an abstract game derived from the underlying types. The moves available to players as well as the rules of the game are specified by an arena.

Definition 4

An arena is a triple $A=\langle \, M_A,\lambda _A,\vdash _A \,\rangle$, where

• $M_A$ is a set of moves;

• $\lambda _A: M_A\rightarrow \{\,O,P\,\}\times \{\,Q,A\,\}$ is a function indicating to which player (O or P) a move belongs and of what kind it is (question or answer);

• $\vdash _A\subseteq (M_A+\{\,\star \,\})\times M_A$ is the so-called enabling relation, which must satisfy the following conditions:

  • If $\star$ enables a move then it is an O-question without any other enabler. A move like this is called initial and we shall write $I_A$ for the set containing all initial moves of A.

  • If one move enables another then the former must be a question and the two moves must belong to different players.

Arenas used to interpret the base types of $\mathsf {IA}_\mathrm{f}$ are shown in Fig. 2: the moves at the bottom are answer-moves. Product and function-space arenas can be constructed as shown in Fig. 1. Given an $\mathsf {IA}_\mathrm{f}$-type $\theta$, we shall write $[\![\theta ]\!]$ for the corresponding arena obtained compositionally from $A_\mathsf {com}$, $A_\mathsf {exp}$ and $A_\mathsf {var}$ using the $\Rightarrow$ construction. Given arenas, we can play games based on a special kind of sequences of moves. A justified sequence s in an arena A is a sequence of moves in which every move $m\not \in I_A$ must have a pointer to an earlier move n in s such that $n\vdash _A m$. n is then said to be the justifier of m. It follows that every justified sequence must begin with an O-question.

Fig. 2.

Arenas for base types

Given a justified sequence s, its O-view $\llcorner {s}\lrcorner$ and P-view $\ulcorner {s}\urcorner$ are defined as follows, where o and p stand for an O-move and a P-move respectively:

A justified sequence s satisfies visibility condition if, in any prefix t m of s, if m is a non-initial O-move then its justifier occurs in $\llcorner {t}\lrcorner$ and if m is a P-move then its justifier is in $\ulcorner {t}\urcorner$. A justified sequence satisfies the bracketing condition if any answer-move is justified by the latest unanswered question that precedes it.

Definition 5

A justified sequence is a play iff O- and P-moves alternate and it satisfies bracketing and visibility. We write $P_A$ for the set of plays in an arena A. A play is single-threaded if it contains at most one occurrence of an initial move.

The next important definition is that of a strategy. Strategies determine unique responses for P (if any) and do not restrict O-moves.

Definition 6

A strategy in an arena A (written as $\sigma :A$) is a non-empty prefix-closed subset of single-threaded plays in A such that:

• (i) whenever $s p_1,s p_2\in \sigma$ and $p_1,p_2$ are P-moves then $p_1=p_2$;

• (ii) whenever $s\in \sigma$ and $so\in P_A$ for some O-move o then $so\in \sigma$.

We write $\mathsf {comp}\,{(\sigma )}$ for the set of non-empty complete plays in $\sigma$, i.e. plays in which all questions have been answered.

An $\mathsf {IA}_\mathrm{f}$ term ${\varGamma } \vdash {M:\theta }$, where $\varGamma ={x_1:\theta _1,\cdots ,x_n:\theta _n}$, is interpreted by a strategy (denoted by $[\![{\varGamma } \vdash {M:\theta } ]\!]$) in the arena $[\![{\varGamma } \vdash {\theta } ]\!]= [\![\theta _1 ]\!]\times \cdots \times [\![\theta _n ]\!]\Rightarrow [\![\theta ]\!]$. The denotations are calculated compositionally starting from strategies corresponding to constants and free identifiers [1]. The latter are interpreted by identity strategies that copy moves across from one occurrence of the same arena to the other, subject to the constraint that the interactions must be plays. Strategies corresponding to constants are given in Fig. 3, where the induced complete plays are listed. We use subscripts to indicate the origin of moves. Let $\sigma :A\Rightarrow B$ and $\tau :B\Rightarrow C$. In order to compose the strategies, one first defines an auxiliary set $\sigma ^\dagger$ of (not necessarily single-threaded) plays on $A\Rightarrow B$ that are special interleavings of plays taken from $\sigma$ (we refer the reader to [1] for details). Then $\sigma ;\tau :A\Rightarrow C$ can be obtained by synchronising $\sigma ^\dagger$ and $\tau$ on B-moves and erasing them after the synchronisation. The game-semantic interpretation captures contextual approximation as follows.

Fig. 3.

Strategies for constants. Only complete plays are specified.

Theorem 1

[1]. if and only if $\mathsf {comp}\,{[\![{\varGamma } \vdash {M_1} ]\!]}\subseteq \mathsf {comp}\,{[\![{\varGamma } \vdash {M_2} ]\!]}$.

Remark 1

$\sigma ^\dagger$ is an interleaving of plays in $\sigma$ that must itself be a play in $P_{A\Rightarrow B}$. For instance, only O is able to switch between different copies of $\sigma$ and this can only happen after P plays in B. We shall discuss two important cases in detail, namely, $B=[\![\beta ]\!]$ and $B=[\![\beta _k\rightarrow \cdots \rightarrow \beta _1\rightarrow \beta ]\!]$.

• If $B=[\![\beta ]\!]$ then a new copy of $\sigma$ can be started only after the previous one is completed. Thus $\sigma ^\dagger$ in this case consists of iterated copies of $\sigma$.

• If $B=[\![\beta _k\rightarrow \cdots \rightarrow \beta _1\rightarrow \beta ]\!]$ then, in addition to the above scenario, a new copy of $\sigma$ can be started by O each time P plays $q_i$ (question from $\beta _i$). An old copy of $\sigma$ can be revisited with $a_i$, which will then answer some unanswered occurrence of $q_i$. However, due to the bracketing condition, this will be possible only after all questions played after that $q_i$ have been answered, i.e. when all copies of $\sigma$ opened after $q_i$ are completed. Thus, in this particular case, $\sigma ^\dagger$ contains “stacked” copies of $\sigma$. Consequently, we can capture $X=\{\,\epsilon \,\}\cup \mathsf {comp}\,{(\sigma ^\dagger )}$ in this case by equation

  $$\begin{array}{l} X=\{\varepsilon \}\cup \bigcup \{\,q\, A_0\, q_{i_1}\, X\, a_{i_1}\, A_1\dots q_{i_m}\, X\, a_{i_m}\, A_m\, a\, X \,|\,\\ \qquad q A_0 q_{i_1} a_{i_1} A_1 \dots q_{i_m} a_{i_m} A_m a\in \mathsf {comp}\,{(\sigma )}\} \end{array} $$

  where $A_j$’s stand for (possibly empty and possibly different) segments of moves from A. Note that, in a play of $\sigma$, $q_i$ will always be followed by $a_i$.

4 Upper Bounds

We shall prove that contextual approximation of $\mathsf {IA}_{3}^2$ terms can be decided in exponential space. Thanks to Lemma 1, this will imply that approximation of $\mathsf {IA}_{3}^k$ ($k\ge 2$) terms is in $(k-1)$-EXPSPACE. In Sect. 5 we will show that these bounds are tight.

This shows that by firing redexes of level higher than 3 we do not lose optimal complexity. However, if redexes of order 2 were also executed (i.e. first-order procedures were inlined), the problem would be reduced to $\mathsf {IA}_{3}^1$ and the implied bound would be 2-EXPTIME, which turns out suboptimal. In what follows, we show that contextual approximation of $\mathsf {IA}_{3}^2$ terms is in EXPSPACE. To that end, we shall translate the terms to automata that represent their game semantics. The alphabet of the automata will consist of moves in the corresponding games. Recall that each occurrence of a base type in a type contributes distinct moves. In order to represent their origin faithfully, we introduce a labelling scheme based on subscripts.

First we discuss how to label occurrences of base types in types. Let $\varTheta$ be a type of order at most 3. Then $\varTheta \equiv \varTheta _m \rightarrow \cdots \rightarrow \varTheta _1\rightarrow \beta$ and $\varTheta _i$’s are of order at most 2. Consequently, for each $1\le i\le m$, we have $\varTheta _i\equiv \varTheta _{i,m_i}\rightarrow \cdots \rightarrow \varTheta _{i,1}\rightarrow \beta _i$ and $\varTheta _{i,j}$’s are of order at most 1. Thus, we have $\varTheta _{i,j}\equiv \beta _{i,j,m_{i,j}}\rightarrow \cdots \rightarrow \beta _{i,j,1}\rightarrow \beta _{i,j}$. Note that the above decomposition assigns a sequence of subscripts to each occurrence of a base type in $\varTheta$. Observe that $\mathsf {ord}({\varTheta })=3$ if and only if some occurrence of a base type gets subscripted with a triple. Next we are going to employ the subscripts to distinguish base types in $\mathsf {IA}_{3}$ typing judgments.

Definition 7

A third-order typing template $\varPsi$ is a sequence $x_1:\theta _1,\cdots , x_n:\theta _n, \theta$, where $\mathsf {ord}({\theta _i})\le 2$ ($1\le i\le n$) and $\mathsf {ord}({\theta })\le 3$.

To label $\theta _1,\cdots , \theta _n, \theta$ we will use the same labelling scheme as discussed above but, to distinguish $\theta _i$’s from $\theta$ and from one another, we will additionally use superscripts $x_i$ for the former. The labelling scheme will also be used to identify moves in the corresponding game. Recall that the game corresponding to a third-order typing template will have moves from $M_{[\![\theta _1 ]\!]}+\cdots +M_{[\![\theta _n ]\!]}+M_{[\![\theta ]\!]}$. The super- and subscripts will identify their origin in a unique way.

Example 1

Let $\varPsi \equiv x_1: (\mathsf {com}\rightarrow \mathsf {exp})\rightarrow \mathsf {var},\, x_2: \mathsf {com}\rightarrow \mathsf {exp}\rightarrow \mathsf {var}, ((\mathsf {com}\rightarrow \mathsf {exp})\rightarrow \mathsf {var})\rightarrow \mathsf {com}$. Here is the labelling scheme for $\varPsi$: $x_1: (\mathsf {com}^{x_1}_{1,1}\rightarrow \mathsf {exp}^{x_1}_1)\rightarrow \mathsf {var}^{x_1}$, $x_2: \mathsf {com}^{x_2}_2\rightarrow \mathsf {exp}^{x_2}_1\rightarrow \mathsf {var}^{x_2}$, $((\mathsf {com}_{1,1,1}\rightarrow \mathsf {exp}_{1,1})\rightarrow \mathsf {var}_1 )\rightarrow \mathsf {com}$. In the corresponding games, among others, we will thus have moves $run ^{x_1}_{1,1}$, $run ^{x_2}_2$, $q^{x_2}_1$, $read ^{x_2}$, $run _{1,1,1}$ as well as $run$.

Our representation of game semantics will need to account for justification pointers. Due to the well-bracketing condition, pointers from answers need not be represented explicitly. Moreover, because of the visibility condition, in our case we only need to represent pointers from moves of the shapes $q^x_{i,j}$ and $q_{i,j,k}$. Such pointers must point at some moves of the form $q^x_i$ and $q_{i,j}$ respectively. In order to represent a pointer we are going to place a hat symbol above both the source and target of the pointer, i.e. we shall also use “moves”of the form $\widehat{q^x_{i,j}}, \widehat{q_{i,j,k}}$ (sources) and $\widehat{q^x_i}, \widehat{q_{i,j}}$ (targets) - the latter hatted moves will only be used if the former exist in the sequence. Similarly to [8], we shall represent a single play by several sequences of (possibly hatted) moves under the following conditions:

• whenever a target-move of the kind discussed above is played, it may or may not be hatted in the representing sequences of moves,

• if a target-move is hatted, all source-moves pointing at the target move are also hatted,

• if a target-move is not hatted, no source-moves pointing at the move are hatted.

Note that this amounts to representing all pointers for a selection of possible targets, i.e. none, one or more (including all). Because the same $\widehat{~}$-symbol is used to encode each pointer, in a single sequence there may still be ambiguities as to the real target of a pointer. However, among the representing plays we will also have plays representing pointers only to single targets, which suffice to recover pointer-related information. This scheme works correctly because only pointers from P-moves need to be represented and the strategies are deterministic (see the discussion at the end of Sect. 3 in [11]).

Example 2

The classic examples of terms that do need explicit pointers are the Kierstaad terms ${} \vdash {K_1, K_2: ((\mathsf {com}_{1,1,1}\rightarrow \mathsf {com}_{1,1})\rightarrow \mathsf {com}_1)\rightarrow \mathsf {com}}$ defined by . To represent the corresponding strategies the following sequences of moves will be used (among others).

• $K_1$: $q\, q_1\, q_{1,1}\, q_1\, q_{1,1}\, q_{1,1,1}$ (zero targets), $q\, q_1\, \widehat{q_{1,1}}\, q_1\, q_{1,1}\, \widehat{q_{1,1,1}}$ (one target), $q\, q_1\, q_{1,1}\, q_1\, \widehat{q_{1,1}}\,{q_{1,1,1}}$ (one target), $q\, q_1\, \widehat{q_{1,1}}\, q_1\, \widehat{q_{1,1}}\,\widehat{q_{1,1,1}}$ (two targets).

• $K_2$: $q\, q_1\, q_{1,1}\, q_1\, q_{1,1} \,q_{1,1,1}$ (zero targets), $q\, q_1\, \widehat{q_{1,1}}\, q_1\, q_{1,1} \,{q_{1,1,1}}$ (one target), $q\, q_1\, q_{1,1}\, q_1\, \widehat{q_{1,1}} \,\widehat{q_{1,1,1}}$ (one target), $q\, q_1\, \widehat{q_{1,1}}\, q_1\, \widehat{q_{1,1}} \,\widehat{q_{1,1,1}}$ (two targets).

To represent strategies corresponding to $\mathsf {IA}_{3}^2$-terms we are going to define an extension of visibly pushdown automata [4]. The alphabet will be divided push-, pop- and no-op-letters corresponding to possibly hatted moves. Additionally, we will use $\epsilon$-transitions that can modify stack content, albeit using a distinguished stack alphabet.

Definition 8

Let $\varPsi =x_1:\theta _1,\cdots , x_m:\theta _m,\theta$ be a third-order typing template and let $\mathcal {M}= M_{[\![\theta _1 ]\!]}+\cdots +M_{[\![\theta _n ]\!]}+M_{[\![\theta ]\!]}$. Below we shall refer to the various components of $\mathcal {M}$ using subscripts and superscripts according to the labelling scheme introduced earlier, also using q and a for questions and answers respectively. We define the sets $\varSigma _{\mathrm {push}}, \varSigma _{\mathrm {pop}}, \varSigma _{\mathrm {noop}}$ as follows.

• $\varSigma _{\mathrm {push}}=\{q_{i,j,k}, \widehat{q_{i,j,k}} \,|\, q_{i,j,k}\in \mathcal {M}\}\cup \{q^{x_h}_{i,j}, \widehat{q^{x_h}_{i,j}}\,|\, q^{x_h}_{i,j}\in \mathcal {M}\}$

• $\varSigma _{\mathrm {pop}}=\{a_{i,j,k} \,|\, a_{i,j,k}\in \mathcal {M}\}\cup \{a^{x_h}_{i,j}\,|\, a^{x_h}_{i,j}\in \mathcal {M}\}$

• $\varSigma _{\mathrm {noop}}= (\mathcal {M}\setminus (\varSigma _{\mathrm {push}}\cup \varSigma _{\mathrm {pop}}) )\cup \{\widehat{q_{i,j}}\,|\, q_{i,j,k}\in \mathcal {M}\}\cup \{\widehat{q^{x_h}_{i}} \,|\, q^{x_h}_{i,j}\in \mathcal {M}\}$

$\varSigma _{\mathrm {push}}$ and $\varSigma _{\mathrm {pop}}$ contain exclusively P- and O-moves respectively, while we can find both kinds of moves in $\varSigma _{\mathrm {noop}}$. Let us write $\varSigma _{\mathrm {noop}}^O, \varSigma _{\mathrm {noop}}^P$ for subsets of $\varSigma _{\mathrm {noop}}$ consisting of O- and P-moves respectively. The states of our automata will be partitioned into states at which O is to move (O-states) and whose at which P should reply (P-states). Push-moves and $\epsilon$-transitions are only available at P-states, while pop-transitions belong to O-states. No-op transitions may be available from any kind of state. Further, to reflect determinacy of strategies, P-states allow for at most one executable outgoing transition, which may be labelled with an element of $\varSigma ^P$ (push or no-op) or be silent (noop, push or pop).

Definition 9

Let $\varPsi$ be a third-order typing template. A $\varPsi$-automaton $\mathcal {A}$ is a tuple $(Q, \varSigma , \varUpsilon , \delta , i, F)$ such that

• $Q = Q^O + Q^P$ is a finite set of states partitioned into O-states and P-states,

• $\varSigma = \varSigma ^O + \varSigma ^P$ is the finite transition alphabet obtained from $\varPsi$ as above, partitioned into O- and P-letters, where $\varSigma ^O = \varSigma _{\mathrm {pop}} + \varSigma ^O_{\mathrm {noop}}$ and $\varSigma ^P = \varSigma _{\mathrm {push}} + \varSigma ^P_{\mathrm {noop}}$,

• $\varUpsilon = \varUpsilon ^\varSigma + \varUpsilon ^\epsilon$ is a finite stack alphabet partitioned into $\varSigma$-symbols and $\epsilon$-symbols,

• $\delta = \delta ^O_{\mathrm {pop}} + \delta ^O_{\mathrm {noop}} + \delta ^P$ is a transition function consisting of $\delta ^O_{\mathrm {pop}} : Q^O \times \varSigma _{\mathrm {pop}} \times \varUpsilon _\varSigma \rightharpoonup Q^P$, $\delta ^O_{\mathrm {noop}} : Q^O \times \varSigma ^O_{\mathrm {noop}} \rightharpoonup Q^P$ and $\delta ^P : Q^P\rightharpoonup (\varSigma _{\mathrm {push}} \times Q^O\times \varUpsilon _\varSigma )+ (\varSigma ^P_{\mathrm {noop}}\times Q^O)+ Q^P + (Q^P\times \varUpsilon _\epsilon ) + (\varUpsilon _\epsilon \rightharpoonup Q^P)$,

• $i \in Q^O$ is an initial state, and

• $F \subseteq Q^O$ is a set of final states.

$\varPsi$-automata are to be started in the initial state with empty stack. They will accept by final state, but whenever this happens the stack will be empty anyway. Clearly, they are deterministic. The set of words derived from runs will be referred to as the trace-set of $\mathcal {A}$, written $\mathcal {T}(\mathcal {A})$. We write $\mathcal {L}{(\mathcal {A})}$ for the subset of $\mathcal {T}(\mathcal {A})$ consisting of accepted words only. The $\varPsi$-automata to be constructed will satisfy an additional run-time property called P-liveness: whenever the automaton reaches a configuration $(q,\gamma )\in Q^P\times \varUpsilon$ from $(i,\epsilon )$, $\delta ^P$ will provide a unique executable transition.

Remark 2

In what follows we shall reason about $\mathsf {IA}_{3}^2$ terms by structural induction. The base cases are the constants and identifiers ${\varGamma ,f:\theta } \vdash {f:\theta }$, where $\mathsf {ord}({\theta })\le 2$. For inductive cases, we split the rule for application into linear application and contraction.

$$ \frac{\displaystyle {\varGamma } \vdash {M:\theta \rightarrow \theta '}\quad {\varDelta } \vdash {N:\theta }}{\displaystyle {\varGamma ,\varDelta } \vdash {M N:\theta '}}~\mathsf {ord}({\theta \rightarrow \theta '})\le 2\qquad \quad \frac{\displaystyle {\varGamma ,x:\theta ,y:\theta } \vdash {M:\theta '}}{\displaystyle {\varGamma ,x:\theta } \vdash {M[x/y]:\theta '}} $$

Note that the restriction on $\theta \rightarrow \theta '$ is consistent with the fact that the level of redexes cannot exceed 2 and free identifiers have types of order at most 2. The relevant $\lambda$-abstraction rule is

$$ \frac{\displaystyle {\varGamma ,x:\theta } \vdash {M:\theta '}}{\displaystyle {\varGamma } \vdash {\lambda x^\theta .M:\theta \rightarrow \theta '}}~\mathsf {ord}({\theta \rightarrow \theta '})\le 3. $$

This stems from the fact that we are considering $\mathsf {IA}_{3}$.

Lemma 2

Let ${x_1:\theta _1,\cdots , x_m:\theta _m} \vdash {M:\theta }$ be an $\mathsf {IA}_{3}^2$-term and let $\sigma =[\![x_1:\theta _1,\cdots , x_m:\theta _m\vdash M:\theta ]\!]$. There exists a P-live $(x_1:\theta _1,\cdots , x_m:\theta _m,\theta )$-automaton $\mathcal {A}_M$, constructible from M in exponential time, such that and $\mathcal {L}{(\mathcal {A}_M)}$ represent respectively $\sigma$ and $\mathsf {comp}\,{(\sigma )}$ (in the sense of our representation scheme).

Proof

Translation by structural induction in $\mathsf {IA}_{3}^2$. The base cases corresponding to the special constants can be resolved by constructing finite automata, following the description of the plays in Fig. 3. For free identifiers, automata of a similar kind have already been constructed as part of the translation of normal forms in [11]. We revisit them below to show which moves must be marked to represent pointers.

Let $\theta$ be a second-order type. Then ${x:\theta } \vdash {x:\theta }$ is interpreted by the identity strategy, which has complete plays of the form $\sum _{q\vdash a} q q^x X a^x a$, where X is given by the context-free grammar below. When writing $\sum _{q\vdash a}$, we mean summing up over all pairs of moves of the indicated shape available in the associated arena $\mathcal {M}$ such that $q\vdash _{\mathcal {M}} a$. Below we also use the condition $\exists q. q_i \vdash q$ to exclude moves of the form $q_i$ that do not enable any other questions (such moves are never targets of justification pointers).

To capture X, we can construct $\mathcal {A}_x$ as in [11], by pushing return addresses when reading $q_{i,j}^x, \widehat{q_{i,j}^x}$ and popping them at $a_{i,j}^x$. Note that this simply corresponds to interpreting recursion in the grammar.

$\lambda$-abstraction and contraction are interpreted by renamings of the alphabet, so it remains to consider the hardest case of (linear) application. The rule simply corresponds to composition: in any cartesian-closed category $[\![{\varGamma ,\varDelta } \vdash {MN:\theta '} ]\!]$ is equal (up to currying) to $[\![{\varDelta } \vdash {N:\theta } ]\!]; [\![{} \vdash {\lambda x^\theta .\lambda \varGamma .M x: \theta \rightarrow (\varGamma \rightarrow \theta ')} ]\!]$. Note that in our case $\mathsf {ord}({\theta })\le 1$, i.e. Remark 1 will apply and the strategy for MN can be obtained by running the strategy for M, which will call copies of N, whose interleavings will obey the stack discipline. To model the interaction, let us consider the moves on which the automata will synchronise. Since $\mathsf {ord}({\theta })\le 1$, the moves that will interact will be of the form $q,a,q_i, a_i$ from N’s point of view and $q_k, a_k, q_{k,i}, a_{k,i}$ from M’s viewpoint for some k. Thus, given $\mathcal {A}_M=(Q_M, \varSigma _M, \varUpsilon _M, i_M, \delta _M, F_M)$ and $\mathcal {A}_N=(Q_N, \varSigma _N, \varUpsilon _N, i_N, \delta _N, F_N)$, we let $\mathcal {A}_{MN}=(Q_{MN}, \varSigma _{MN}, \varUpsilon _{MN},i_M, \delta _{MN},F_M)$, where

$$ \begin{array}{rcl} Q_{MN} &{}=&{} Q_M + (Q_M^O\times Q_N)\\ \varSigma _{MN}&{}=&{}(\varSigma _M\setminus \{q_k,a_k,q_{k,i},a_{k,i}\}) + (\varSigma _N\setminus \{q_0,a_0,q_1,a_1\})\\ \varUpsilon _{MN}^{\varSigma _{MN}} &{}=&{} \varUpsilon _M + \varUpsilon _N\\ \varUpsilon _{MN}^\epsilon &{}=&{}\varUpsilon _M^\epsilon + \varUpsilon _N^\epsilon + Q_M^O \end{array} $$

The decomposition of $\varSigma _{MN}$ into push-, pop- and noop-letters is inherited from the constituent automata. We specify the transition function $\delta _{MN}$ below using derivation rules referring to transitions in $\mathcal {A}_M$ and $\mathcal {A}_N$. A push-transition reading x and pushing $\gamma$ will be labelled with $\xrightarrow {x/\gamma }_{}$. Dually, $\xrightarrow {x,\gamma }_{}$ will represent a pop. $\widetilde{x}$ stands for any transition involving x, where x could also be $\epsilon$.

• $\mathcal {A}_M$’s non-interacting transitions are copied over to $\mathcal {A}_{M N}$.

  $$ \frac{s\xrightarrow {\widetilde{x}}_{\mathcal {A}_M} s'}{s\xrightarrow {\widetilde{x}}_{\mathcal {A}_{MN}} s'} \quad x\in (\varSigma _M\setminus \{q_k,a_k,q_{k,i},a_{k,i}\})+\{\epsilon \} $$

• M calls N (left) and N returns from the call (right).

  $$ \frac{s\xrightarrow {q_k}_{\mathcal {A}_M} s'\qquad i_N\xrightarrow {q}_{\mathcal {A}_N} t}{s\xrightarrow {\epsilon }_{\mathcal {A}_{MN}} (s',t)} \qquad \frac{s'\xrightarrow {a_k}_{\mathcal {A}_M} s''\qquad t\xrightarrow {a}_{\mathcal {A}_N} f\in F_N}{(s',t)\xrightarrow {\epsilon }_{\mathcal {A}_{MN}} s''} $$

• N’s non-interacting transitions are copied over while keeping track of $\mathcal {A}_M$’s state.

  $$ \frac{t\xrightarrow {\widetilde{x}}_{\mathcal {A}_N} t'}{(s,t)\xrightarrow {\widetilde{x}}_{\mathcal {A}_{MN}} (s,t')} \qquad s\in Q_M^O,\,\, x\in (\varSigma _N\setminus \{q_0,a_0,q_1,a_1\})\cup \{\epsilon \} $$

• N calls its argument (left) and the argument returns (right).

  $$ \frac{s\xrightarrow {q_{k,i}}_{\mathcal {A}_M} s'\qquad t\xrightarrow {q_i}_{\mathcal {A}_N} t'}{(s,t)\xrightarrow {\epsilon /t'}_{\mathcal {A}_{M N}} s'} \qquad \frac{s'\xrightarrow {a_{k,i}}_{\mathcal {A}_M} s''\qquad t'\xrightarrow {a_i}_{\mathcal {A}_N} t''}{s'\xrightarrow {\epsilon ,t'}_{\mathcal {A}_{M N}} (s'',t'')} $$

Note that the interaction involves moves that are not used to represent pointers, i.e. whenever pointers are represented they remain the same as they were in the original strategies, which is consistent with the definition of composition. The states in $Q_{MN}$ are divided into O- and P-states as follows: $Q_{MN}^O = Q_M^O + (Q_M^O\times Q_N^O)$ and $Q_{MN}^P = Q_M^P + (Q_M^O\times Q_N^P)$. The correctness of the construction follows from the fact that it is a faithful implementation of legal interactions (see, e.g., [7]), as discussed in Remark 1. P-liveness follows from the fact the constituent strategies are P-live and that the construction simulates interaction sequences, including infinite chattering.   $\square$

Our next step will be to analyse the shape of reachable configurations of $\mathcal {A}_M$. We aim to understand how many elements of $\varUpsilon _\epsilon$ can occur consecutively on the stack.

Definition 10

Suppose $(q,\gamma )\in Q\times (\varUpsilon _\varSigma \cup \varUpsilon _\epsilon )^*$. The $\epsilon$-density of $\gamma$ is defined to be the length of the longest segment in $\gamma$ consisting solely of consecutive elements from $\varUpsilon _\epsilon$.

While the size of stacks corresponding to $\mathsf {IA}_{3}^2$ terms is unbounded (consider, for instance, ${x:\theta } \vdash {x:\theta }$ with $\theta =(\mathsf {com}\rightarrow \mathsf {com})\rightarrow \mathsf {com}$), $\epsilon$-density turns out to be bounded. We shall prove that it is exponential with respect to the size of the original term. This will be crucial to obtaining our upper bound. The main obstacle to proving this fact is the case of composition M N. As discussed in Remark 1, M “stacks up” copies of N and we would first like to obtain a bound on the number of nested calls to N that are not separated by a move from $\varSigma _{\mathrm {push}}$ (such moves block the growth of $\epsilon$-density). For this purpose, we go back to plays and analyse sequences in which the relevant questions are pending: a pending question is one that has been played but remains unanswered. Observe that sequences of pending questions are always alternating. We will not be interested in the specific questions but only in their kinds, as specified by the table below.

Question	q	$q_i, q^x$	$q_{i,j}, q^x_i$	$q_{i,j,k}, q^x_{i,j}$
Kind	0	1	2	3

Definition 11

Let s be a play. We define $\mathsf {pend}(s)$ to be the sequence from $\{0,1,2,3\}^*$ obtained from s by restricting it to pending questions and replacing each question with the number corresponding to its kind.

Thus, any non-empty even-length play s, $\mathsf {pend}(s)$ will match the expression $0 (1 2 + 3 2 )^*(1+3)$. We say that the (12)-potential of s is equal to k if k is the largest k such that $\mathsf {pend}(s) = \cdots (1 2)^k\cdots$. In other words, the (12)-potential of a play is the length of the longest segment $(12)^k$ in $\mathsf {pend}(s)$.

Lemma 3

Let ${\varGamma } \vdash {M:\theta }$ be an $\mathsf {IA}_{3}^2$-term. Then the (12)-potential of any play in $[\![{\varGamma } \vdash {M} ]\!]$ is bounded and the bound $b_M$ is exponential in the size of M.

Lemma 3 is a key technical result needed to establish the following boundedness property that is satisfied by automata representing $\mathsf {IA}_{3}^2$-terms.

Lemma 4

Let ${\varGamma } \vdash {M:\theta }$ be an $\mathsf {IA}_{3}^2$-term and consider $\mathcal {A}_M$ constructed in Lemma 2. There exists a bound $d_M$, exponential in the size of M, such that the $\epsilon$-density of configurations reachable by $\mathcal {A}_M$ is bounded by $d_M$.

Next we derive a bound on plays witnessing failure of contextual approximation in $\mathsf {IA}_{3}^2$. Consider $\mathsf {IA}_{3}^2$-terms ${\varGamma } \vdash {M_1,M_2:\theta }$ and let $\sigma _i = [\![{\varGamma } \vdash {M_i:\theta } ]\!]$ for $i=1,2$. Given a play, let its height be the maximum number of pending questions from $\varSigma _{\mathrm {push}}$ occurring in any of its prefixes. Note that, for plays from $\sigma _i$, this will be exactly the maximum number of symbols from $\varUpsilon _\varSigma$ that will appear on the stack of $\mathcal {A}_{M_i}$ at any point of its computation.

Lemma 5

There exists a polynomial p such that if $\mathsf {comp}\,{\sigma _1}\setminus \mathsf {comp}\,{\sigma _2}$ is not empty then it contains a play of height $p(n_1+ n_2)$, where $n_1, n_2$ are the numbers of states in $\mathcal {A}_{M_1}$ and $\mathcal {A}_{M_2}$ respectively.

Theorem 2

For $\mathsf {IA}_{3}^2$-terms ${\varGamma } \vdash {M_1,M_2:\theta }$, one can decide in exponential space.

Proof

Note that this boils down to testing emptiness of $\mathsf {comp}\,{\sigma _1}\setminus \mathsf {comp}\,{\sigma _2}$. By Lemma 5, it suffices to guess a play whose height is polynomial in the size of $\mathcal {A}_{M_1}$, $\mathcal {A}_{M_2}$, i.e. exponential with respect to term size. Moreover, by Lemma 4, the $\epsilon$-density of the corresponding configurations of $\mathcal {A}_{M_1}$ and $\mathcal {A}_{M_2}$ will also be exponential. Thus, in order to check whether a candidate s is accepted by $\mathcal {A}_{M_1}$ and rejected by $\mathcal {A}_{M_2}$, we will only need to consider stacks of exponential size wrt $M_1, M_2$. Consequently, the guess can be performed on the fly and verified in exponential space. Because NEXPSPACE=EXPSPACE, the result follows.

Corollary 1

For $k\ge 2$, contextual approximation of $\mathsf {IA}_{3}^k$-terms is in $(k-1)$-EXPSPACE.

5 Lower Bounds

Here we show that contextual approximation of $\mathsf {IA}_{1}^k$-terms is $(k-1)$-EXPSPACE-hard for $k\ge 2$. Note that this matches the upper bound shown for $\mathsf {IA}_{3}^k$-terms and will allow us to conclude that contextual approximation in $\mathsf {IA}_{1}^k, \mathsf {IA}_{2}^k$ and $\mathsf {IA}_{3}^k$ is $(k-1)$-EXPSPACE-complete. Our hardness results will rely on nesting of function calls and iteration afforded by higher-order types. Below we introduce the special types and terms to be used.

Let $k,n\in \mathbb {N}$. Define the type $\overline{n}$ by $\overline{0}=\mathsf {com}$ and $\overline{n+1}=\overline{n}\rightarrow \overline{n}$. Note that $\mathsf {ord}({\overline{n}})=n$. Also, let $\mathsf {Exp}(k,n)$ be defined by $\mathsf {Exp}(0,n)=n$ and . Given $k\ge 2$, consider the term $\mathsf {twice}_{k}=\lambda x^{\overline{k-1}}.\lambda y^{\overline{k-2}}. x(x y) : \overline{k}$.

Definition 12

Let $k\ge 2$. Writing $M^n N$ as shorthand for $\underbrace{M(M\cdots (M}_n N)\cdots )$, let us define a family of terms $\{\mathsf {nest}_{n,k}\}$ with ${f:\overline{1},x:\overline{0}} \vdash {\mathsf {nest}_{n,k}:\overline{0}}$ by taking $\mathsf {nest}_{n,k}\equiv (\mathsf {twice}_{k}^n\, g_{k-1}) g_{k-2}\cdots g_1 g_0$, where $g_0\equiv x$, $g_1\equiv f$ and $g_i\equiv \mathsf {twice}_{i}$ for $i>1$.

The terms have several desirable properties, summarised below.

Lemma 6

Let $k\ge 2$. $\mathsf {nest}_{n,k}$ belongs to $\mathsf {IA}_{2}^k$, has polynomial size in n and is $\beta$-reducible to $f^{\mathsf {Exp}(k-1,n)} x$.

Note that the nested applications of f in $f^{\mathsf {Exp}(k-1,n)} x$ are akin to generating a stack of height $\mathsf {Exp}(k-1,n)$. We shall exploit this in our encodings. Note that, by substituting $\lambda c^\mathsf {com}.c;c$ for f in $f^{\mathsf {Exp}(k-1,n)} x$, we obtain a term that iterates x as many as $\mathsf {Exp}(k,n)$ times, i.e. $\mathsf {Exp}(k-1,n)$-fold nesting is used to simulate $\mathsf {Exp}(k,n)$-fold iteration.

Simulating Turing Machines. Let w be an input word. Let $n=|w|$, $l=\mathsf {Exp}(k-1,n)$ and $N=\mathsf {Exp}(k,n)$. We shall consider a deterministic Turing machine T running in $SPACE (l)$ and $TIME (N)$ and simulate T’s behaviour on w. This suffices to establish $SPACE (l)$-hardness.

We start off with the description of an encoding scheme for configurations of T. We shall represent them as strings of length l over an alphabet $\varSigma _T$, to be specified later. We shall write $\mathsf {Config}_T$ for the subset of $(\varSigma _T)^l$ corresponding to configurations. The encoding of the initial configuration will be denoted by $c_{ init }$ and we shall write $\mathsf {Accept}_T$ for the set of representations of accepting configurations. Given $c\in \mathsf {Config}_T$, we write for the representation of the successor of c according to T’s transition function. Let us introduce a number of auxiliary languages that will play an important role in the simulation. We write $c^R$ for the reverse of c.

Definition 13

Let $\varSigma _T^\#=\varSigma _T+\{\#\}$. We define the languages $\mathcal {L}_0, \mathcal {L}_1\subseteq (\varSigma _T)^*$ and $\mathcal {L}_2, \mathcal {L}_3, \mathcal {L}_4\subseteq (\varSigma _T^\#)^*$ as follows.

Lemma 7

There exists a representation scheme for configurations of T such that $\varSigma _T$ is polynomial in the size of T, w and the following properties hold.

• 1. There exist deterministic finite-state automata $\mathcal {A}_0, \mathcal {A}_1$, constructible from T, w in polynomial time, such that $L(\mathcal {A}_0)\cap (\varSigma _T)^l = \mathcal {L}_0$ and $L(\mathcal {A}_1)\cap (\varSigma _T)^l = \mathcal {L}_1$.

• 2. For any $i=2,3,4$, there exists a deterministic pushdown automaton $\mathcal {A}_i$, constructible from T, w in polynomial time, such that $L(\mathcal {A}_i)\cap ((\varSigma _T)^l \# (\varSigma _T)^l) = \mathcal {L}_i$. Moreover, transitions of the automata are given by three transition functions $\delta _{\mathrm {push}}:Q^{\mathrm {push}}\times \varSigma _T \rightarrow Q^{\mathrm {push}}\times \varUpsilon$, $\delta _{\mathrm {noop}}: Q^{\mathrm {push}}\times \{\#\}\rightarrow Q^{\mathrm {pop}}$ and $\delta _{\mathrm {pop}}:Q^{\mathrm {pop}} \times \varSigma _T\times \varUpsilon \rightarrow Q^{\mathrm {pop}}$, the initial state belongs to $Q^{\mathrm {push}}$ and the automaton accepts by final state. I.e., the automata will process elements of $(\varSigma _T)^l \# (\varSigma _T)^l$ by performing push-moves first, then a noop move for $\#$ and, finally, pop-moves.

Remark 3

Note that in the above lemma we had to use intersection with $(\varSigma _T)^l$ (resp. $(\varSigma _T)^l \# (\varSigma _T)^l$) to state the correctness conditions with respect to $\mathsf {Config}_T$, because the automata will not be able to count up to l. However, in our argument, we are going to use the nesting power of $\mathsf {IA}_{1}^k$ to run their transition functions for suitably many steps (l and $2l+1$ respectively).

The significance of the languages $\mathcal {L}_0,\mathcal {L}_1,\mathcal {L}_2, \mathcal {L}_3, \mathcal {L}_4$ stems from the fact that they are building blocks of two other languages, $\mathcal {L}_5$ and $\mathcal {L}_6$, which are closely related to the acceptance of w by T.

Lemma 8

Consider the languages $\mathcal {L}_5, \mathcal {L}_6\subseteq (\varSigma _T^\#)^*$ defined by and . Then T accepts w if and only if $\mathcal {L}_5\not \subseteq \mathcal {L}_6$.

Proof

Note that if T accepts w then the sequence of (representations of the) configurations belonging to the accepting run, in which every other representation is reversed, gives rise to a word that belongs to $\mathcal {L}_5$ but not to $\mathcal {L}_6$.

Conversely, if a word $c_{ init }\,\#\,c_1^R\,\#\, d_1\,\#\cdots \, c^R_N \,\#\,d_N \,\#\,f^R\in \mathcal {L}_5$ does not belong to $\mathcal {L}_6$ then , ($i=1,\cdots ,N-1$) and . Thus, the word actually represents an accepting run on w.   $\square$

Our hardness argument consists in translating the above lemma inside $\mathsf {IA}_{1}^k$. To that end, we shall show how to capture $\mathcal {L}_2, \mathcal {L}_3, \mathcal {L}_4$ and, ultimately, $\mathcal {L}_5$ and $\mathcal {L}_6$, using $\mathsf {IA}_{1}^k$ terms. We shall work under the assumption that $\varSigma _T^\#=\{0,\cdots , max \}$. Note, though, that the results can be adapted to any $max >0$ by encoding $\varSigma _T^\#$ as sequences of $\mathsf {exp}$-values. Similarly, using multiple $\mathsf {exp}$-valued variables, $\mathsf {IA}$-terms can store values that are bigger than $max$. We shall take advantage of such storage implicitly (e.g. for state values or stack elements), but the number of extra variables needed for this purpose will remain polynomial.

Definition 14

We shall say that an $\mathsf {IA}$-term ${z:\mathsf {exp}} \vdash {M:\mathsf {com}}$ captures $L\subseteq (\varSigma _T^\#)^*$ if $\mathsf {comp}\,{([\![{z} \vdash {M} ]\!])} = \{ run \, q^z\, (a_1)^z\, q^z \, (a_2)^z \,\cdots \, q^z\, (a_k)^z\, done \,\,|\,\, a_1 a_2 \cdots a_k\in L\}$.

Example 3

The term ${z:\mathsf {exp}} \vdash {M_{\#}:\mathsf {com}}$, where $M_{\#}\equiv \text { if } z=\# \text { then } \mathbf {skip} \text { else } \varOmega$, captures $\{\#\}$. In our constructions we often write $[\mathsf {condition}]$ to stand in for the assertion $\text { if } (\mathsf {condition}) \text { then } \mathbf {skip} \text { else } \varOmega$.

Lemma 9

There exist $\mathsf {IA}_{1}^k$-terms ${z:\mathsf {exp}} \vdash {M_0, M_1:\mathsf {com}}$, constructible from T, w in polynomial time, capturing $\mathcal {L}_0, \mathcal {L}_1$ respectively.

Lemma 10

There exists an $\mathsf {IA}_{1}^k$-term ${z:\mathsf {exp}} \vdash {M_2:\mathsf {com}}$, constructible from T, w in polynomial time, which captures $\mathcal {L}_2$.

Thanks to the last two lemmas we are now ready to capture $\mathcal {L}_5$.

Lemma 11

There exists an $\mathsf {IA}_{1}^k$-term ${z:\mathsf {exp}} \vdash {M_5:\mathsf {com}}$, constructible in polynomial time from T, w, which captures $\mathcal {L}_5$.

Proof

Note that a word from $\mathcal {L}_5$ contains $N=\mathsf {Exp}(k,n)$ segments from $\mathcal {L}_2$. To account for that, it suffices to use N copies of $M_\#;M_2$. However, for a polynomial-time reduction, we need to do that succinctly. Recall that $\mathsf {nest}_{n,k}$ gives us l-fold nesting of functions, where $l=\mathsf {Exp}(k-1,n)$. Consequently, N-fold iteration can be achieved by l-fold nesting of $\lambda c^\mathsf {com}.c;c$. Thus, we can take

$$ M_5\equiv M_0; \mathsf {nest}_{n,k}[\lambda c^\mathsf {com}.c;c / f, (M_\#;M_2) / x]; M_\#; M_1. $$

To complete the hardness argument (by restating Lemma 8 using $\mathsf {IA}_{1}^k$ terms), we also need to capture $\mathcal {L}_6$. Because of the existential clause in its definition we need to use a slightly different capture scheme.

Lemma 12

There exists an $\mathsf {IA}_{1}^k$-term ${z:\mathsf {exp}, FLAG :\mathsf {var}} \vdash {M_6':\mathsf {com}}$, constructible in polynomial time from T, w, such that .

Lemma 13

There exists an $\mathsf {IA}_{1}^k$-term ${z:\mathsf {exp}} \vdash {M_6:\mathsf {com}}$, constructible in polynomial time from T, w, which captures $\mathcal {L}_6$.

Proof

It suffices to run $M_6'$ for $N+1$ steps and check whether the flag was set:

Theorem 3

Contextual approximation between $\mathsf {IA}_{1}^k$ terms is $(k-1)$-EXPSPACE-hard.

Proof

By Lemmas 8, 11 and 13, for any Turing machine T running in $SPACE (\mathsf {Exp}(k-1,n))$ and $TIME (\mathsf {Exp}(k,n))$ and an input word w, there exist $\mathsf {IA}_{1}^k$-terms ${x:\mathsf {exp}} \vdash {M_5,M_6}$, constructible from T, w in polynomial time, such that T accepts w if and only if $M_5$ does not approximate $M_6$. This implies $(k-1)$-EXPSPACE-hardness.   $\square$

6 Conclusion

We have shown that contextual approximation in $\mathsf {IA}_{1}^k, \mathsf {IA}_{2}^k, \mathsf {IA}_{3}^k$ is $(k-1)$-EXPSPACE-complete. The algorithm that leads to these optimal bounds reduces terms to $\mathsf {IA}_{3}^2$ (with possibly $(k-2)$-fold exponential blow-up) and we use a dedicated EXPSPACE procedure for $\mathsf {IA}_{3}^2$ exploiting game semantics and decision procedures for a special kind of pushdown automata. In particular, the results show that untamed $\beta$-reduction would yield suboptimal bounds, but selective $\beta$-reduction of redexes up to level 3 does not jeopardise complexity. The bounds above apply to open higher-order terms, i.e. $\mathsf {IA}_{i}$ ($i>0$) terms, for which the problem of contextual approximation is difficult to attack due to universal quantification over contexts.

Our work also implies bounds for contextual approximation of $\mathsf {IA}_{0}^k$ terms, i.e. closed terms of base type. Conceptually, this case is much easier, because it boils down to testing termination. In this case our techniques can be employed to obtain better upper bounds for $\mathsf {IA}_{0}^k$ than those for $\mathsf {IA}_{1}^k$ ($(k-1)$-EXPSPACE). For a start, like for $\mathsf {IA}_{1}^k$, we can reduce $\mathsf {IA}_{0}^k$ terms (at $(k-2)$-fold exponential cost) to $\mathsf {IA}_{0}^2$. Then termination in $\mathsf {IA}_{0}^2$ can be checked in exponential time by constructing pushdown automata via Lemma 2 and testing them for emptiness (rather than inclusion). Since emptiness testing of pushdown automata can be performed in polynomial time and the automata construction in Lemma 2 costs a single exponential, this yields an EXPTIME upper bound for termination in $\mathsf {IA}_{0}^2$. Consequently, termination in $\mathsf {IA}_{0}^k$ ($k\ge 2$) can be placed in $(k-1)$-EXPTIME, though it is not clear to us whether this bound is optimal. For completeness, let us just mention that termination in $\mathsf {IA}_{0}^0$ and $\mathsf {IA}_{0}^1$ is PSPACE-complete due to presence of variables and looping (membership follows from the corresponding upper bounds for contextual equivalence).

Another avenue for future work is $\mathsf {IA}_{1}^k, \mathsf {IA}_{2}^k, \mathsf {IA}_{3}^k$ contextual equivalence. Of course, our upper bounds for approximation also apply to contextual equivalence, which amounts to two approximation checks. However, one might expect better bounds in this case given that our hardness argument leans heavily on testing inclusion.

Finally, one should investigate how our results can be adapted to the call-by-value setting. An educated guess would be that, in the analogous fragment of ML, the reduction of redexes up to order 3 (rather than 2) should be suppressed in order to obtain accurate complexity estimates.