Abstract
This paper demonstrates the great practical utility of inductive definitions in HOL. We describe a new package we have implemented for automating inductive definitions, based on the Knaster-Tarski fixpoint theorem. As an example, we use it to give a simple proof of the well-founded recursion theorem. We then describe how to generate free recursive types starting just from the Axiom of Infinity. This contrasts with the existing HOL development where several specific free recursive types are developed first.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Wilhelm Ackermann. Zum Hilbertschen Aufbau der reellen Zahlen. Mathematische Annalen, 99:118–133, 1928. English translation, ‘On Hilbert's construction of the real numbers', in [24], pp. 493–507.
Peter Aczel. An introduction to inductive definitions. In J. Barwise and H.J. Keisler, editors, Handbook of mathematical logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739–782. North-Holland, 1991.
Sten Agerholm. A HOL basis for reasoning about functional programs. BRICS Report Series RS-94-44, Centre of the Danish National Research Foundation, Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark, 1994.
Flemming Andersen and Kim Dam Petersen. Recursive boolean functions in HOL. In Archer et al. [5], pages 367–377.
Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors. Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA, 1991. IEEE Computer Society Press.
Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1992.
Luc J. M. Claesen and Michael J. C. Gordon, editors. Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, 1992. North-Holland.
J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Raymond T. Yeh, editor, Current Trends in Programming Methodologies, volume IV, pages 80–149. Prentice-Hall, 1978.
Elsa L. Gunter. Why we can't have SML style datatype declarations in HOL. In Claesen and Gordon [7], pages 561–568.
Elsa L. Gunter. A broader class of trees for recursive type definitions for HOL. In Joyce and Seger [13], pages 141–154.
John Harrison and Konrad Slind. A reference version of HOL. Presented in poster session of 1994 HOL Users Meeting and only published in participants' supplementary proceedings. Available on the Web from http://www.dcs.glasgow.ac.uk/∼hug94/sproc.html, 1994.
Nathan Jacobson. Basic Algebra I. W. H. Freeman, 2nd edition, 1989.
Jeffrey J. Joyce and Carl Seger, editors. Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, 1993. Springer-Verlag.
B. Knaster. Un théorème sur les fonctions, d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133–134, 1927. Volume published in 1928.
Tim Leonard. The HOL numeral library. Distributed with HOL system, 1993.
Thomas F. Melham. A package for inductive relation definitions in HOL. In Archer et al. [5], pages 350–357.
Thomas F. Melham. The HOL logic extended with quantification over type variables. In Claesen and Gordon [7], pages 3–18.
Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. Technical Report 320, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1993.
R. Péter. Konstruktion nichtrekursiver Funktionen. Mathematische Annalen, 111:42–60, 1935.
Wim Ploegaerts, Luc Claesen, and Hugo De Man. Defining recursive functions in HOL. In Archer et al. [5], pages 358–366.
Rachel E. O. Roxas. A HOL package for reasoning about relations defined by mutual induction. In Joyce and Seger [13], pages 129–140.
Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
Mark van der Voort. Introducing well-founded function definitions in HOL. In Claesen and Gordon [7], pages 117–132.
Jean van Heijenoort, editor. From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931. Harvard University Press, 1967.
Glynn Winskel. The formal semantics of programming languages: an introduction. Foundations of computing. MIT Press, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harrison, J. (1995). Inductive definitions: Automation and application. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_66
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive