Completeness of a Relational Calculus for Program Schemes

FRIAS, MARCELO FABIAN; MADDUX, ROGER DUNCAN

Indianapolis, Indiana, USA

Congreso; LICS'98, International Conference on Logic in Computer Science; 1998

IEEE

The relational calculus $\mc{MU}$ was presented in Willem-Paul de~Roever's dissertation as a framework for describing and proving properties of programs. $\mc{MU}$ is axiomatized by de~Roever in stages. The next-to-last stage is the calculus $\mutwo$, namely $\mc{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 $\mc{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 $\mutwo$ is a calculus for non-recursive program schemes. Around 1976 David Park conjectured that de~Roever's axiomatization for $\mutwo$ is complete. In this paper we confirm Park's conjecture.