Summary: We exhibit a rich class of Horn clauses, which we call \(\mathcal{ H}1\), whose least models, though possibly infinite, can be computed effectively. We show that the least model of an \(\mathcal{ H}1\) clause consists of so-called strongly recognizable relations and present an exponential normalization procedure to compute it. In order to obtain a practical tool for program analysis, we identify a restriction of \(\mathcal{ H}1\) which we call \(\mathcal{ H}2\), where the least models can be computed in polynomial time. This fragment still allows to express, e.g., Cartesian product and transitive closure of relations. Inside \(\mathcal{ H}2\), we exhibit a fragment \(\mathcal{ H}3\) where normalization is even cubic. We demonstrate the usefulness of our approach by deriving a cubic control-flow analysis for the Spi calculus.
For the entire collection see [Zbl 1001.00049].