The Library
Contextual approximation and higher-order procedures
Tools
Lazic, Ranko and Murawski, Andrzej S. (2016) Contextual approximation and higher-order procedures. In: 19th International Conference, FOSSACS 2016, Eindhoven, The Netherlands, 2-8 Apr 2016. Published in: Foundations of Software Science and Computation Structures :19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceeding, 9634 pp. 162-179. ISBN 9783662496299. doi:10.1007/978-3-662-49630-5_10 ISSN 0302-9743.
|
PDF
WRAP_1271755-cs-010416-paper_49-5.pdf - Accepted Version - Requires a PDF viewer. Download (921Kb) | Preview |
Official URL: http://dx.doi.org/10.1007/978-3-662-49630-5_10
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 ββ-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)(k−1)-EXPSPACE-completeness. 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 handled by a dedicated decision procedure based on game semantics and a variant of pushdown automata.
Item Type: | Conference Item (Paper) | ||||||
---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
Library of Congress Subject Headings (LCSH): | Programming languages (Electronic computers) | ||||||
Series Name: | Lecture Notes in Computer Science | ||||||
Journal or Publication Title: | Foundations of Software Science and Computation Structures :19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceeding | ||||||
Publisher: | Springer | ||||||
ISBN: | 9783662496299 | ||||||
ISSN: | 0302-9743 | ||||||
Book Title: | Foundations of Software Science and Computation Structures | ||||||
Editor: | Jacobs , Bart and Löding , Christof | ||||||
Official Date: | 2016 | ||||||
Dates: |
|
||||||
Volume: | 9634 | ||||||
Page Range: | pp. 162-179 | ||||||
DOI: | 10.1007/978-3-662-49630-5_10 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Access rights to Published version: | Restricted or Subscription Access | ||||||
Date of first compliant deposit: | 8 April 2016 | ||||||
Date of first compliant Open Access: | 8 April 2016 | ||||||
Conference Paper Type: | Paper | ||||||
Title of Event: | 19th International Conference, FOSSACS 2016 | ||||||
Type of Event: | Conference | ||||||
Location of Event: | Eindhoven, The Netherlands | ||||||
Date(s) of Event: | 2-8 Apr 2016 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year