Abstract
Minimal fixed point operators were introduced by Scott and De Bakker in order to describe the input-output behaviour of recursive procedures. As they considered recursive procedures acting upon a monolithic state only, i.e., procedures acting upon one variable, the problem remained open how to describe this input-output behaviour in the presence of an arbitrary number of components which as a parameter may be either called-by-value or called-by-name. More precisely, do we need different formalisms in order to describe the input-output behaviour of these procedures for different parameter mechanisms, or do we need different minimal fixed point operators within the same formalism, or do different parameter mechanisms give rise to different transformations, each subject to the same minimal fixed point operator? Using basepoiht preserving relations over cartesian products of sets with unique basepoints, we provide a single formalism in which the different combinations of call-by-value and call-by-name are represented by different products of relations, and in which only one minimal fixed point operator is needed. Moreover this mathematical description is axiomatized, thus yielding a relational calculus for recursive procedures with a variety of possible parameter mechanisms.
This paper is registered at the Mathematical Center as IW 20/74.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Bibliography
Blikle, A., and A. Mazurkiewicz, An algebraic approach to the theory of programs, algorithms, languages and recursiveness, in Proc. of an International Symposium and Summer School on the Mathematical Foundations of Computer Science, Warsaw-Jablonna, 1972.
Burstall, R.M., Proving properties of programs by structural induction,Comput. J., 12 (1969) 41–48.
Cadiou, J.M., Recursive definitions of partial functions and their computations, Thesis, Stanford University, 1972.
De Bakker, J.W., Recursive procedures, Mathematical Centre Tracts 24, Amsterdam, 1971.
De Bakker, J.W., Recursion, induction and symbol manipulation, in Proc. MC-25 Informatica Symposium, Mathematical Centre Tracts 37, Amsterdam, 1971.
De Bakker, J.W., and W.P. de Roever, A calculus for recursive program schemes, in Proc. IRIA Symposium on Automata, Formal languages and Programming, M. Nivat (ed.), North-Holland, Amsterdam, 1972.
De Bakker, J.W., and L.G.L.Th. Meertens, On the completeness of the inductive assertion method, Prepublication, Mathematical Centre Report IW 12/73, Amsterdam, 1973.
De Roever, W.P., Operational and mathematical semantics for recursive polyadic program schemata (Extended abstract), in Proceedings of Symposium and Summer School “Mathematical Foundations of Computer Science”, 3–8 September 1973, High Tatras, Czechoslovakia, pp. 293–298.
De Roever, W.P., Operational, mathematical and axiomatized semantics for recursive procedures and data structures,Mathematical Centre Report ID/1, Amsterdam.
Dijkstra, E.W., Notes on structured programming, in Hoare, C.A.R., Dijkstra., E.W., and 0.J. Dahl, Structured Programming, Academic Press, New York, 1972.
Dijkstra, E.W., A simple axiomatic basis for programming language constructs, Indagationes Mathematicae, 36 (1974) 1–15.
Garland, S.J., and D.C. Luckham, Translating recursion schemes into program schemes, in Proc. of an ACM Conference on Proving Assertions about Programs, Las Cruces, New Mexico, January 6–7, 1972.
Guessarian, I., Sur une réduction des schémas de programmes polyadiques à des schémas monadiques et ses applications, Memo GRIT,no. 73. 05, Université de Paris, 1973.
Hitchcock, P., An approach to forma/ reasoning about programs, Thesis, University of Warwick, Coventry, England, 1974.
Hitchcock, P., and D. Park, Induction rules and proofs of termination, in Proc. IRIA Symposium on Automata, Formal Languages and Programming, M. Nivat (ed.), North-Holland, Amsterdam, 1972.
Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12 (1969) 576–583.
Hotz, G., Eindeutigkeit and Mehrdeutigkeit formaler Sprachen, Electron. Informationsverarbeit. Kybernetik, 2 (1966), 235–246.
Karp, R.M., Some applications of logical syntax to digital computer programming, Thesis, Harvard University, 1959.
Knuth, D.E., The Art of Computer Programming, Vol. 1, Fundamental Algorithms, Addison Wesley, Reading (Mass. ), 1968.
Manna, Z., and J. Vuillemin, Fixpoint approach to the theory of computation, Comm. ACM, 15 (1972) 528–536.
Mazurkiewicz, A., Proving properties of processes, PRACE CO PAN-CC, PAS Reports 134, Warsaw, 1973.
McCarthy, J., A basis for a mathematical theory of computation, in Computer Programming and Formal Systems, pp.33–70, P. Braffort and D. Hirschberg (eds.), North-Holland, Amsterdam, 1963.
Milner, R., Algebraic theory of computable polyadic functions, Computer Science Memorandum 12, University College of Swansea, 1970.
Morris Jr., J.H., Another recursion induction principle, Comm. ACM, 14 (1971) 351–354.
Park, D., Fixpoint induction and proof of program semantics, in Machine Intelligence, Vol. 5, pp.59–78, B. Meltzer and D. Michie (eds.), Edinburgh University Press, Edinburgh, 1970.
Park, D., Notes on a formalism for reasoning about schemes, Unpublished notes, University of Warwick, 1970.
Scott, D., Outline of a mathematical theory of computation, in Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems, pp.169–176, Princeton. 1970.
Scott, D., Lattice theory, data types, and semantics, in NYU Symposium on formal semantics, pp.64–106, Prentice Hall, 1972.
Scott, D., and J.W. de Bakker, A theory of programs, Unpublished notes, IBM Seminar, Vienna, 1969.
Tarski, A., On the calculus of relations, J. Symbolic Logic, 6 (1941) 73–89.
Vuillemin, J., Proof techniques for recursive programs, Thesis, Stanford University, 1972.
Wirth, N., Program development by stepwise refinement,Comm. ACM, 14 (1971) 221–227.
Wright, J.B., Characterization of recursively enumerable sets, J. Symbolic Logic, 37 (1972) 507–511.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1974 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Roever, W.P. (1974). Recursion and Parameter Mechanisms: An Axiomatic Approach. In: Loeckx, J. (eds) Automata, Languages and Programming. ICALP 1974. Lecture Notes in Computer Science, vol 14. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21545-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-21545-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-06841-9
Online ISBN: 978-3-662-21545-6
eBook Packages: Springer Book Archive