Completeness of a relational calculus for program schemes (Q5940932)

The relational calculus \(MU\) was presented in Willem-Paul de Roever's dissertation as a framework for describing and proving properties of programs. \(MU\) is axiomatized by de Roever in stages. The next-to-last stage is the calculus \(MU_{2},\) namely \(MU\) without the recursive \(\mu\)-operator. Its axioms include typed versions of Tarski's axioms for the calculus of relations, together with axioms for the projection functions. For \(MU\) there is, in addition, an axiom expressing the least-fixed-point property of terms containing the \(\mu\)-operator, and Scott's induction rule. Thus \(MU_{2}\) is a calculus for nonrecursive program schemes. Around 1976 David Park conjectured that de Roever's axiomatization for \(MU_{2}\) is complete. In this paper, we confirm Park's conjecture.