Abstract
We present here a very fruitful tool for proving properties of LISP functions. We implement the ancient, but quite natural and elegant, Recursion Induction Principle stated by J. Mc Carthy by using the famous fold/unfold method elaborated by R. Burstall and J. Darlington.
We thus obtain a very simple and flexible method for proving theorems about LISP functions; we call it the Mc Carthy method. Furthermore the method is machine oriented and we implement it in a conversational system. We do not make any comparison with the R. Boyer and J. Moore theorem-prover since our system is not automatic. But our system is implementable in a wide range of machines and we expect to implement our method in the R. Burstall and J. Darlington system. We then shall have a very powerful system which might perform program synthesis and proofs of program properties simultaneously (in a way parallel to that followed by Z. Manna and R. Waldinger).
In this paper we apply our method (by hand) to give the proof of two properties: associativity of the append operation between lists and idempotence of the reverse operation.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Bibliography
R. Boyer, J. Moore:Proving theorems about LISP function. J. of ACM (22)1 (1975), 129–144.
R. Burstall, J. Darlington:A transformation system for developing recursive programs, J. of ACM (24)1 (1977), 44–67.
B. Courcelle, M. Nivat:Algebraic families of interpretations, 17th FOCS, Houston, (1976).
L. Kott:About transformation system: a theoretical study, in «Transformations de Programmes», (1978), 232–247.
L. Kott:Des substitutions dans les systèmes d'équations algébriques sur le magma, Doctoral Dissertation, Univ. Paris VII, (1979).
J. Mac Carthy:A basis for a mathematical theory of computation, in «Computer Programming and Formal Systems», (1963).
J.Mc Carthy et al.:LISP 1.5 Programmer's Manual, M. I. T. Press Cambridge, Mass., (1962).
Z. Manna, R. Waldinger:Knowledge and reasoning in program synthesis, Artif. Intel. J. (6)2 (1975), 175–208.
Z. Manna, R. Waldinger:A deductive approach to program synthesis, ACM ToPLaS (2)1 (1980), 90–121.
M. Nivat:Interprétation universelle d'un schéma de programme récursif, Informatica (7)1 (1977), 9–16.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Kott, L. The Mc Carthy's recursion induction principle: «Oldy» but «Goody». Calcolo 19, 59–69 (1982). https://doi.org/10.1007/BF02576192
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02576192