Three Applications to Rational Relations of the High Undecidability of the Infinite Post Correspondence Problem in a Regular ω-Language
Olivier Finkel, Equipe De Logique Mathématique · 2016
It was noticed by Harel in [Har86] that "one can define [Formula: see text]-complete versions of the well-known Post Correspondence Problem". We first give a complete proof of this result, showing that the infinite Post Correspondence Problem in a regular ω-language is [Formula: see text]-complete, hence located beyond the arithmetical hierarchy and highly undecidable. We infer from this result that it is [Formula: see text]-complete to determine whether two given infinitary rational relations are disjoint. Then we prove that there is an amazing gap between two decision problems about ω-rational functions realized by finite state Büchi transducers. Indeed Prieur proved in [Pri01, Pri02] that it is decidable whether a given ω-rational function is continuous, while we show here that it is [Formula: see text]-complete to determine whether a given ω-rational function has at least one point of continuity. Next we prove that it is [Formula: see text]-complete to determine whether the continuity set of a given ω-rational function is ω-regular. This gives the exact complexity of two problems which were shown to be undecidable in [CFS08].