research-article

Fixed point semantics and partial recursion in Coq

Authors:

Vladimir KomendantskyAuthors Info & Claims

PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming

Pages 89 - 96

https://doi.org/10.1145/1389449.1389461

Published: 15 July 2008 Publication History

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]

R. C. Backhouse. Fixed point calculus. In R. C. Backhouse, R. Crole, and J. Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of LNCS. Springer-Verlag, 2002.

Digital Library

[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]

Y. Bertot and P. Castéran. Interactive theorem proving and program development, Coq'art: the calculus of inductive constructions. Texts in Theoretical Computer Science: an EATCS series. Springer-Verlag, 2004.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[12]

D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In proceedings of the 1986 ACM Conference on Lisp and Functional Programming, Aug. 1986.

Digital Library

[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]

J. Harrison. Inductive definitions: Automation and application. In P. J. Windley, T. Schubert, and J. Alves-Foss, editors, Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Sciences. Springer-Verlag, 1995.

Digital Library

[17]

G. Huet. Induction principles formalized in the calculus of constructions. In TAPSOFT'87, volume 249 of LNCS, pages 276--286. Springer, 1987.

Digital Library

[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.

Digital Library

[20]

A. Megacz. A coinductive monad for prop-bounded recursion. In A. Stump and H. Xi, editors, Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, pages 11--20, New York, NY, USA, 2007. ACM.

Digital Library

[21]

O. Müller, T. Nipkow, D. v. Oheimb, and O. Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming, 9:191--223, 1999.

Digital Library

[22]

H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, 1992.

Digital Library

[23]

T. Nipkow. Winskel is (almost) right:towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171--186, 1998.

Digital Library

[24]

B. Nordström. Terminating general recursion. BIT, 28:605--619, 1988.

Digital Library

[25]

C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, 1993. LIP research report 92--49.

Digital Library

[26]

C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq, 2007. paulin07kahn.pdf htp:/w.lri.fr/~paulin/PUBLIS/ .

[27]

C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607--640, 1993.

Digital Library

[28]

L. C. Paulson. Logic and computation, Interactive proof with Cambridge LCF. Cambridge University Press, 1987.

Digital Library

[29]

F. Regensburger. HOLCF: Higher order logic of computable functions. In P. J. Windley, T. Schubert, and J. Alves-Foss, editors, Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Sciences. Springer-Verlag, 1995.

Digital Library

[30]

G. Winskel. The Formal Semantics of Programming Languages, an introduction. Foundations of Computing. The MIT Press, 1993.

Digital Library

Cited By

Cheval HNowak DRusu V(2024)Formal Definitions and Proofs for Partial (Co)Recursive FunctionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100999(100999)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100999
Nowak DRusu V(2023)While Loops in CoqElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.389.8389(96-109)Online publication date: 22-Sep-2023
https://doi.org/10.4204/EPTCS.389.8
van Delft MGeuvers HWillemse T(2017)A Formalisation of Consistent Consequence for Boolean Equation SystemsInteractive Theorem Proving10.1007/978-3-319-66107-0_29(462-478)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_29
Show More Cited By

Index Terms

Fixed point semantics and partial recursion in Coq
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Theorem Proving Modulo
Abstract
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Extensional Higher-Order Paramodulation in Leo-III
Abstract
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Superposition for fixed domains

Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming

July 2008

278 pages

ISBN:9781605581170

DOI:10.1145/1389449

General Chair:
Sergio Antoy
Portland State University, Oregon, USA
,
Program Chair:
Elvira Albert
Complutense University of Madrid, Spain

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 July 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PPDP08

Sponsor:

PPDP08: Principles and Practice of Declarative Programming

July 15 - 17, 2008

Valencia, Spain

Acceptance Rates

PPDP '08 Paper Acceptance Rate 24 of 48 submissions, 50%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
247
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cheval HNowak DRusu V(2024)Formal Definitions and Proofs for Partial (Co)Recursive FunctionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100999(100999)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100999
Nowak DRusu V(2023)While Loops in CoqElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.389.8389(96-109)Online publication date: 22-Sep-2023
https://doi.org/10.4204/EPTCS.389.8
van Delft MGeuvers HWillemse T(2017)A Formalisation of Consistent Consequence for Boolean Equation SystemsInteractive Theorem Proving10.1007/978-3-319-66107-0_29(462-478)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_29
Dubois CPessaux F(2015)Termination Proofs for Recursive Functions in FoCaLiZeRevised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 954710.1007/978-3-319-39110-6_8(136-156)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1007/978-3-319-39110-6_8
Casinghino CSjöberg VWeirich S(2014)Combining proofs and programs in a dependently typed languageACM SIGPLAN Notices10.1145/2578855.253588349:1(33-45)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535883
Casinghino CSjöberg VWeirich SJagannathan SSewell P(2014)Combining proofs and programs in a dependently typed languageProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535883(33-45)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535883
Kriener JKing ABlazy SPeña RSchrijvers T(2013)Proofs you can believe inProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505886(37-48)Online publication date: 16-Sep-2013
https://dl.acm.org/doi/10.1145/2505879.2505886
Sabel DSchmidt-Schauβ M(2013)A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial FunctionsJournal of Automated Reasoning10.1007/s10817-012-9253-650:4(383-421)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1007/s10817-012-9253-6
Charguéraud A(2010)The optimal fixed point combinatorProceedings of the First international conference on Interactive Theorem Proving10.1007/978-3-642-14052-5_15(195-210)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-14052-5_15
Case JMoelius S(2009)Independence results for n-ary recursion theoremsProceedings of the 17th international conference on Fundamentals of computation theory10.5555/1789494.1789501(38-49)Online publication date: 2-Sep-2009
https://dl.acm.org/doi/10.5555/1789494.1789501
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten