Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops

TL;DR

This work establishes the undecidability of the emptiness problem for deterministic propositional while programs with graph loop by introducing a hypothesis-elimination technique based on graph loops and reducing from the complement of the periodic domino problem. It further derives $\Pi^{0}_{1}$-hardness results for the equational theory of $ ext{PCoR}_{\{* , \overline{\mathsf{I}}\}}$ and shows $\Pi^{0}_{1}$-completeness for the loop-augmented fragment, while also identifying decidable and PSPACE-complete fragments of the existential calculus of relations with transitive closure (and variants on REL/DREL). The approach, including loop-based translations and witness-based hyptheses eliminations, yields precise boundaries between decidability and undecidability, clarifying the computational landscape of relation-algebraic and Kleene-algebra-like formalisms. Overall, the results illuminate the limits of automated reasoning in relational calculi with loops and provide a framework for transferring undecidability across related logical systems.

Abstract

We show that the emptiness (unsatisfiability) problem is undecidable and $\mathrmΠ^{0}_{1}$-complete for deterministic propositional while programs with (graph) loop. To this end, we introduce a hypothesis elimination using loops. Using this, we give reductions from the complement of the periodic domino problem. Moreover, as a corollary via hypothesis eliminations, we also show that the equational theory is $\mathrmΠ^{0}_{1}$-complete for the positive calculus of relations with transitive closure and difference. Additionally, we show that the emptiness problem is PSPACE-complete for the existential calculus of relations with transitive closure.

Figures (5)

• Figure 1: A [$\langle h,v\rangle$-periodic tiling]$\langle4, 2\rangle$-periodic tiling for the domino system $\mathcal{D} = \langle C, H, V\rangle$, where $C = \{, , , \}$, $H = \{, , , \}$, and $V = \{*\}{, , , }$. The origin is denoted by $o$.
• Figure 2: The (finite) valuation $\mathfrak{v}_{\mathcal{D}, \tau}$ where $\tau$ is the [$\langle h,v\rangle$-periodic tiling]$\langle4,2\rangle$-periodic tiling in \ref{['figure: tiling']}.
• Figure 3: Illustrative example of loop extensions.
• Figure 4: The equation set $\Gamma_{\mathcal{D}}$, where $\mathcal{D}$ is a domino system $\langle C, H, V\rangle$.
• Figure 5: The form of graphs in $\mathcal{G} _{ u _{\mathcal{D}}}( t _{\mathtt{gr}}')$ where the pairs of vertices connected with some $\mathbf{P}$-labelled edge are all merged (note that each pair of vertices connected with a $\mathbf{P}$-labelled edge is mapped to the same vertex, in $\mathsf{DREL}_{\mathtt{test}}$).

Theorems & Definitions (80)

• Proposition 2.1: nakamuraExistentialCalculiRelations2023
• Proposition 2.2: bounded model property
• Proposition 2.3
• Proposition 2.4
• Proposition 2.5: bergerUndecidabilityDominoProblem1966gurevichRemarksBergerPaper1972; see also borgerClassicalDecisionProblem1997
• Proposition 2.6: a minor change from harelEffectiveTransformationsInfinite1986lewisElementsTheoryComputation1997
• Proposition 2.7
• Definition 2.8: from goldblattWellstructuredProgramEquivalence2012
• Proposition 3.1: Cor. of tarskiCalculusRelations1941
• Example 3.2: nakamuraExistentialCalculiRelations2023