Completeness of a relational calculus for program schemes

DOI10.1016/S0304-3975(99)00343-6MaRDI QIDQ5940932zbMATH OpenOpenAlexFDO

Authors Marcelo F. Frias, Roger Maddux

Publication date 20 August 2001

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(99)00343-6

zbMATH Keywords

completeness projection functions recursive program schemes relational calculus

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Review text

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.

Recommendations

Cites work

Cited in

(2)

This page was built for publication: Completeness of a relational calculus for program schemes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5940932)