Completeness of a Relational Calculus for Program Schemes

FRIAS, MARCELO FABIAN; MADDUX, ROGER DUNCAN

THEORETICAL COMPUTER SCIENCE

Elsevier

Año: 2001 vol. 254 p. 543 - 556

0304-3975

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 MU2, 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 MU2 is a calculus for nonrecursive program schemes. Around 1976 David Park conjectured that de Roever’s axiomatization for MU is complete. In this paper, we confirm Park’s conjecture.