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 scenarios. 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 fired without losing optimality, whereas redexes of level up to 2 are handled by a dedicated decision procedure based on game semantics and a variant of pushdown automata.

This is joint work with Ranko Lazic, presented at FoSSaCS 2016.