Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Third-Order Idealized Algol with Iteration Is Decidable
verfasst von : Andrzej S. Murawski, Igor Walukiewicz
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (
IA
$^*_{3}$
). They are approached via a combination of game semantics and language theory. It is shown that for each (
IA
$^{*}_{3}$
)-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 contextual equivalence and approximation for
β
-normal terms.
Exptime
-hardness is also shown in this case, even in the absence of iteration.