Contextual Approximation and Higher-Order Procedures

We investigate the complexity of deciding contextual approximation (refinement) in finitary Idealized Algol, a prototypical language combining higherorder 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 -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)-EXPSPACEcompleteness. Interestingly, the bound is obtained by selective -reduction: redexes from level 3 onwards can be reduced without losing optimality, whereas redexes up to order 2 are hand...

• Type: Journal
• Year: 2016
• Where: FOSSACS
• Authors: Ranko Lazic, Andrzej S. Murawski
• Keywords: FOSSACS 2016, Software Engineering