Fixed point semantics and partial recursion in Coq

ABSTRACT

We propose to use the Knaster–Tarski least fixed point theorem as a basis to define recursive functions in the Calculus of Inductive Constructions. This widens the class of functions that can be modelled in type-theory based theorem proving tools to potentially nonterminating functions. This is only possible if we extend the logical framework by adding some axioms of classical logic.We claim that the extended framework makes it possible to reason about terminating or non-terminating computations and we show that extraction can also be extended to handle the new functions

REFERENCES

• 1: S. Abian and A. B. Brown. A theorem on partially ordered sets with applications to fixed point theorems. Canadian J. Math., 13:78--82, 1961.
• 2: P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics. North Holland, 1977.
• 3: Roland Backhouse, Galois connections and fixed point calculus, Algebraic and coalgebraic methods in the mathematics of program construction, Springer-Verlag New York, Inc., New York, NY, 2002
• 4: A. Balaa and Y. Bertot. Fonctions récursives générales par itération en théorie des types. In Journées Francophones pour les Langages Applicatifs, Jan. 2002.
• 5: Y. Bertot. Theorem proving support in programming language semantics, 2007. htp:/hal.inra.fr/inra-016309.
• 6: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 7: Y. Bertot and V. Komendantsky. Proofs on domain theory and partial Yves.Breecrutrosio/nt,a2r0s0k8i..htmlp:/w-sop.inra.fr/marel/ .
• 8: A. Bove. General recursion in type theory. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, International Workshop TYPES 2002, The Netherlands, number 2646 in Lecture Notes in Computer Science, pages 39--58, March 2003.
• 9: A. Bove and V. Capretta. Computation by prophecy. In S. R. D. Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 70--83. Springer, 2007.
• 10: J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical report, University of Cambridge, 1992.
• 11: L. Chicli, L. Pottier, and C. Simpson. Mathematical quotients and quotient types in Coq. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, number 2646 in LNCS, pages 95--107. Springer, 2003.
• 12: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• 13: Coq development team. The Coq Proof Assistant Reference Manual, version 8.1, 2006.
• 14: C. Dubois and V. V. Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates, July 1998. www.cs.bham.uk/~mmk/cade98-partialty.
• 15: S. Glondu. Garantie formelle de correction pour l'extraction Coq, 2007. htp:/stephane.glondu.net/raport.207.pdf.
• 16: John Harrison, Inductive Definitions: Automation and Application, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, p.200-213, September 11-14, 1995
• 17: G. Huet, Induction principles formalized in the calculus of constructions, The International Joint Conference on theory and practice of software development on TAPSOFT '87, p.276-286, January 1987, Pisa, Italy
• 18: G. Kahn. Elements of constructive geometry group theory and domain theory, 1995. available as a Coq user contribution at http://coq.inra.fr/contribs-eng.html.
• 19: P. Letouzey. A new extraction for Coq. In H. Geuvers and F.Wiedijk, editors, TYPES 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
• 20: Adam Megacz, A coinductive monad for prop-bounded recursion, Proceedings of the 2007 workshop on Programming languages meets program verification, October 05-05, 2007, Freiburg, Germany [doi>10.1145/1292597.1292601]
• 21: Olaf Müller , Tobias Nipkow , David Von Oheimb , Oscar Slotosch, HOLCF = HOL + LCF, Journal of Functional Programming, v.9 n.2, p.191-223, March 1999 [doi>10.1017/S095679689900341X]
• 22: Hanne Riis Nielson , Flemming Nielson, Semantics with applications: a formal introduction, John Wiley & Sons, Inc., New York, NY, 1992
• 23: T. Nipkow. Winskel is (almost) right:towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171--186, 1998.
• 24: B. Nordström, Terminating general recursion, BIT, v.28 n.3, p.605-619, 1988 [doi>10.1007/BF01941137]
• 25: Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
• 26: C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq, 2007. paulin07kahn.pdf htp:/w.lri.fr/~paulin/PUBLIS/ .
• 27: Christine Paulin-Mohring , Benjamin Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, v.15 n.5-6, p.607-640, May/June 1993 [doi>10.1016/S0747-7171(06)80007-6]
• 28: Lawrence C. Paulson, Logic and computation: interactive proof with Cambridge LCF, Cambridge University Press, New York, NY, 1987
• 29: Franz Regensburger, HOLCF: Higher Order Logic of Computable Functions, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, p.293-307, September 11-14, 1995
• 30: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Verification

Keywords:
automated theorem proving, least fixed point semantics, non-terminating functions, program extraction, the Knaster-Tarski theorem