Third-order Idealized Algol with iteration is decidable
The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (<strong>IA</strong><sup>*</sup><sub>3</sub>). They are approached via a combination of game semantics and language theory. It is sh...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2008
|
| Subjects: |
| _version_ | 1797091207636058112 |
|---|---|
| author | Murawski, A Walukiewicz, I |
| author_facet | Murawski, A Walukiewicz, I |
| author_sort | Murawski, A |
| collection | OXFORD |
| description | The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (<strong>IA</strong><sup>*</sup><sub>3</sub>). They are approached via a combination of game semantics and language theory. It is shown that for each <strong>IA</strong><sup>*</sup><sub>3</sub>-term one can construct a pushdown automaton recognizing a representation of the strategy induced by the term. The automata have some additional properties ensuring that the associated equivalence and inclusion problems are solvable in PTIME. This gives an EXPTIME decision procedure for the problems of contextual equivalence and approximation for beta -normal terms. EXPTIME-hardness of the problems, even for terms without iteration, is also shown. |
| first_indexed | 2024-03-07T03:29:41Z |
| format | Journal article |
| id | oxford-uuid:ba456bc7-50bb-40ec-bd89-e9b255e1fffa |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T03:29:41Z |
| publishDate | 2008 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:ba456bc7-50bb-40ec-bd89-e9b255e1fffa2022-03-27T05:08:41ZThird-order Idealized Algol with iteration is decidableJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:ba456bc7-50bb-40ec-bd89-e9b255e1fffaProgram development and toolsGame semanticsEnglishOxford University Research Archive - ValetElsevier2008Murawski, AWalukiewicz, IThe problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (<strong>IA</strong><sup>*</sup><sub>3</sub>). They are approached via a combination of game semantics and language theory. It is shown that for each <strong>IA</strong><sup>*</sup><sub>3</sub>-term one can construct a pushdown automaton recognizing a representation of the strategy induced by the term. The automata have some additional properties ensuring that the associated equivalence and inclusion problems are solvable in PTIME. This gives an EXPTIME decision procedure for the problems of contextual equivalence and approximation for beta -normal terms. EXPTIME-hardness of the problems, even for terms without iteration, is also shown. |
| spellingShingle | Program development and tools Game semantics Murawski, A Walukiewicz, I Third-order Idealized Algol with iteration is decidable |
| title | Third-order Idealized Algol with iteration is decidable |
| title_full | Third-order Idealized Algol with iteration is decidable |
| title_fullStr | Third-order Idealized Algol with iteration is decidable |
| title_full_unstemmed | Third-order Idealized Algol with iteration is decidable |
| title_short | Third-order Idealized Algol with iteration is decidable |
| title_sort | third order idealized algol with iteration is decidable |
| topic | Program development and tools Game semantics |
| work_keys_str_mv | AT murawskia thirdorderidealizedalgolwithiterationisdecidable AT walukiewiczi thirdorderidealizedalgolwithiterationisdecidable |