Abstract
The work presented here has its focus on the formal construction of programs out of non-constructive specifications involving quantifiers. This is accomplished by means of an extended abstract algebra of relations whose expressive power is shown to encompass that of first-order logic. Our extension was devised for tackling the classic issue of lack of expressiveness of abstract relational algebras first stated by Tarski and later formally treated by Maddux, Németi, etc. First we compare our extension with classic approaches to expressiveness and our axiomatization with modern approaches to products. Then, we introduce some non-fundamental operations. One of them, the relational implication, is shown to have heavy heuristic significance both in the statement of Galois connections for expressing relational counterparts for universally quantified sentences and for dealing with them. In the last sections we present two smooth program derivations based on the theoretical framework introduced previously.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Backhouse, R. and Tormenta, P., “Polynomial Relators” in State-of-the-Art Seminar on Formal Program Development, IFIP-WG 2.1 Algorithmic Languages and Calculi, 1992.
Baum, G., Haeberer, A.M., and Veloso, P.A.S., “On the Representability of the ▽-Abstract Relational Algebra” IGPL Newsletter, vol. 1, no. 3, European Foundation for Logic, Language and Information, Interest Group on Programming Logic.
Bednarek, A. R. and Ulam, S. M., “Projective Algebra and the Calculus of Relations” Journal of Symbolic Logic, vol. 43, no. 1, 56–64, March 1978.
Berghammer, R., Haeberer, A.M., Schmidt, G., and Veloso, P.A.S., “Comparing two Different Approaches to Products in Abstract Relation Algebras”, Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, AMAST'93, 1993.
Chin, L. and Tarski, A., “Remarks on Projective Algebras” Bulletin of the American Mathematical Society, vol. 54, 80–81, 1948.
Chin, L. H. C. and Tarski, A., “Distributive and Modular Laws in the Arithmetic of Relation Algebras” in University of California Publications in Mathematics, of California, U., Ed. University of California, 1951, pp. 341–384.
Everett, C. J. and Ulam, S. M., “Projective Algebra,” American Journal of Mathematics, vol. 68, 77–88, 1946.
Haeberer, A.M., Veloso, P.A.S., and Elustondo, P., “Towards a Relational Calculus for Software Construction” in 41st Meeting of the, vol. Document IFIP Working Group 2.1 Algorithmic Languages and Calculi, Chester-England, 1990.
Haeberer, A.M. and Veloso, P.A.S., “Partial Relations for Program Derivation: Adequacy, Inevitability and Expressiveness” in Constructing Programs From Specifications — Proceedings of the IFIP TC2 Working Conference on Constructing Programs From Specifications, N. H., IFIP WG 2.1, Bernhard Möller, 1991, pp. 319–371.
Haeberer, A.M., Baum, G., and Schmidt, G. “Dealing with Non-Constuctive Specifications Involving Quantifiers” Res. Rept. MCC 4, 1993.
Halmos, P. R., Algebraic Logic. New York: Chelsea Publishing Company, 1962.
Henkin, L. and Monk, J. D., “Cylindric Algebras and Related Structures” in Proceedings of the Tarski Symposium, vol. 25 American Mathematical Society, 1974, pp. 105–121.
Hoare, C. A. R. and He, J., “The Weakest Presepecification, Part I” Fundamenta Informatica, vol. 4, no. 9, 51–54, “Part II” vol. 4, no. 9, 217–252, 1986.
Jónsson, B. and Tarski, A., “Boolean Algebras With Operators PART I” American Journal of Mathematics, vol. 73, 891–939, 1951. “PART II”, vol. 74, 127–162, 1952.
Lyndon, R., “The Representation of Relational Algebras” Annals of Mathematics (series 2), vol. 51, 707–729, 1950.
Maddux, R., “A Sequent Calculus for Relation Algebras” Annals of Pure and Apply Logic, vol. 25, 73–101, 1983.
Maddux, R., “The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations” Studia Logica, vol. L, no. 3–4, 412–455, 1991.
Németi, I., “Algebraization of Quantifier Logics, an Introductory Overview” Studia Logica, vol. L, no. 3–4, 485–569, 1991.
Roever, W. P. de, “A Formalization of Various Prameter Mechanisms as Products of Relations Within a Calculus of Recursive Program Schemes” in Theorie des Algorithmes, des Languages et de la Programation, 1972, pp. 55–88.
Schmidt, G. and Ströhlein, T., “Relation Algebras: Concept of Points and Representability” Discrete Mathematics, vol. 54, 83–92, 1985.
Schmidt, G. and Ströhlein, T., Relationen und Graphen. Mathematik für Informatiker, Springer-Verlag, 1989. Republished in English in EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1993.
Tarski, A., “On the Calculus of Relations” Journal of Symbolic Logic, vol. 6, 73–89, 1941.
Tarski, A. and Thompson, F. B., “Some General Properties of Cylindric Algebras” Bulletin of the American Mathematical Society, vol. 58, 65, 1952.
Veloso, P.A.S. and Haeberer, A.M., “A Finitary Relational Algebra For Classical First-Order Logic” Bulletin of the Section of Logic of the Polish Academy of Sciences, vol. 20, no. 2, 52–62, June 1991.
Veloso, P.A.S., Haeberer, A.M., and Baum, G., “Formal Program Construction Within an Extended Calculus of Binary Relations” Res. Rept. MCC 19, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haeberer, A.M., Baum, G.A., Schmidt, G. (1993). On the smooth calculation of relational recursive expressions out of first-order non-constructive specifications involving quantifiers. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds) Formal Methods in Programming and Their Applications. Lecture Notes in Computer Science, vol 735. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039715
Download citation
DOI: https://doi.org/10.1007/BFb0039715
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57316-6
Online ISBN: 978-3-540-48056-3
eBook Packages: Springer Book Archive