Idealized Algol with Ground Recursion, and DPDA Equivalence

Abstract. We prove that observational equivalence of IA3 + Y0 (3rdorder Idealized Algol with 0th-order recursion) is equivalent to the DPDA Equivalence Problem, and hence decidable. This completes the classification of decidable fragments of Idealized Algol. We also prove that observational approximation of IA1 + Y0 is undecidable by reducing the DPDA Containment Problem to it.

• Type: Conference
• Year: 2005
• Where: ICALP
• Authors: Andrzej S. Murawski, C.-H. Luke Ong, Igor Walukiewicz
• Keywords: DPDA Equivalence Problem, ICALP 2005, Idealized Algol, Observational Equivalence, Theoretical Computer Science