The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes

The equational theory of deterministic monadic recursion schemes is known to be decidable by the result of Senizergues on the decidability of the problem of DPDA equivalence. In order to capture some properties of the domain of computation, we augment equations with certain hypotheses. This preserves the decidability of the theory, which we call simple implicational theory. The asymptotically fastest algorithm known for deciding the equational theory, and also for deciding the simple implicational theory, has a running time that is nonelementary. We therefore consider a restriction of the properties about schemes to check: instead of arbitrary equations f = g between schemes, we focus on propositional Hoare assertions {p} f {q}, where f is a scheme and p, q are tests. Such Hoare assertions have a straightforward encoding as equations. For this subclass of program properties, we can also handle nondeterminism at the syntactic and/or at the semantic level, without increasing the complexity of the theories. We investigate the Hoare theory of monadic recursion schemes, that is, the set of valid implications whose conclusions are Hoare assertions and whose premises are of a certain simple form. We present a sound and complete Hoare-style calculus for this theory. We also show that the Hoare theory can be decided in exponential time, and that it is complete for this class.