Skip to main content
Springer Nature Link
Log in

Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

  • Published:
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

Abstract

This work presents a formalization of the discrete model of the continuum introduced by Harthong (1989), the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field (Reveillès and Richard, Ann. Math. Artif. Intell. Math. Inform. 16(14), 89–152 (1996)). The formalization is based on the work presented in Chollet et al. (2012, 2009) where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges (1999). Laugwitz-Schmieden numbers (Laugwitz 1983) are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated (Chollet et al., Theor. Comput. Sci. 466, 2–19 (2012)). In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (France)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin Heidelberg New York (2004)

    Book  Google Scholar 

  2. Bridges, D., Palmgren, E.: Constructive Mathematics. The Stanford Encyclopedia of Philosophy. available from http://plato.stanford.edu/archives/win2013/entries/mathematics-constructive/ (2013)

  3. Bridges, D., Reeves, S.: Constructive mathematics, in theory and programming practice. Technical Report CDMTCS-068, Centre for Discrete Mathematics and Theorical Computer Science (1997)

  4. Bridges, D.S.: Constructive mathematics: A foundation for computable analysis. Theor. Comput. Sci. 219 (1–2), 95–109 (1999)

    Article  MathSciNet  Google Scholar 

  5. Chlipala, A.: Certified programming with dependent types: A pragmatic introduction to the coq proof assistant. MIT Press, Cambridge (2013)

    Google Scholar 

  6. Chollet, A.: Formalismes non classiques pour le traitement informatique de la topologie et de la géométrie discrète. PhD thesis, Université de la Rochelle (2010)

  7. Chollet, A., Wallet, G., Fuchs, L., Andres, E., Largeteau-Skapin, G.: Foundational aspects of multiscale digitization. Theor. Comput. Sci. 466, 2–19 (2012)

    Article  MathSciNet  Google Scholar 

  8. Chollet, A., Wallet, G., Fuchs, L., Largeteau-Skapin, G., Andres, E.: Insight in discrete geometry and computational content of a discrete model of the continuum. Pattern Recog. 42, 2220–2228 (2009)

    Article  Google Scholar 

  9. Chollet, A., Wallet, G., Fuchs, L., Largeteau-Skapin, G., Andres, E.: Ω-Arithmetization: A Discrete Multi-resolution Representation of Real Functions. In: Wiederhold, P., Barneva, P.R. (eds.) Combinatorial Image Analysis: 13th International Workshop, IWCIA of Lecture Notes in Computer Science (LNCS), vol. 5852, pp 316–329, Mexico (2009)

  10. Coq development team: The Coq Proof Assistant Reference Manual, Version 8.2. LogiCal Project (2008)

  11. Diener, F., Reeb, G.: Analyse non standard. Hermann, Paris (1989)

    Google Scholar 

  12. Diener, M.: Application du calcul de Harthong-Reeb aux routines graphiques. In: Salanskis, J.-M., Sinaceurs, H. (eds.) Le Labyrinthe du Continu, pp 424–435. Springer, Berlin Heidelberg New York (1992)

    Google Scholar 

  13. Fleuriot, J.: Exploring the foundations of discrete analytical geometry in Isabelle/HOL. In: Schreck, P., Richter-Gebert, J., Narboux, J. (eds.) Proceedings of Automated Deduction in Geometry 2010 of LNAI, vol. 6877. Springer, Berlin Heidelberg New York (2011)

    Google Scholar 

  14. Fleuriot, J.D., Paulson, L.C.: A combination of nonstandard analysis and geometry theorem proving, with application to newton’s principia. In: Kirchner, C., Kirchner, H. (eds.) CADE of Lecture Notes in Computer Science, vol. 1421, pp 3–16. Springer, Berlin Heidelberg New York (1998)

    Google Scholar 

  15. Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1), 3–36 (2007)

    Article  MathSciNet  Google Scholar 

  16. Harthong, J.: Une théorie du continu. In: Barreau, H., Harthong, J. (eds.) La mathématiques non standard, pp 307–329, Paris (1989). Éditions du CNRS

  17. Huth, M., Ryan, M., 2nd ed: Logic in Computer Science. Cambridge University Press (2004)

  18. Kaye, R.: Models of Peano Arithmetic. Oxford Science Publications (1991)

  19. Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Meth. Comput. Sci. 9(1) (2011)

  20. Laugwitz, D.: Ω-calculus as a generalization of field extension an alternative approach to nonstandard analysis. In: Hurd, A. (ed.) Nonstandard Analysis - Recent developments, volume 983 of Lecture Notes in Mathematics, pp 120–133. Springer (1983)

  21. Laugwitz, D.: Leibniz’ principle and Ω-calculus. In: Salanskis, J., Sinacoeur, H. (eds.) Le Labyrinthe du Continu, pp 144–155. Springer, France (1992)

    Google Scholar 

  22. Laugwitz, D., Schmieden, C.: Eine erweiterung der infinitesimalrechnung. Mathematische Zeitschrift 89, 1–39 (1958)

    MathSciNet  Google Scholar 

  23. Lutz, R.: La force modélisatrice des théories infinitésimales faibles. In: Salanskis, J.-M., Sinaceur, H. (eds.) Le Labyrinthe du Continu, pp 414–423. Springer-Verlag (1992)

  24. Magaud, N., Chollet, A., Fuchs, L.: Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective. In: ADG’2010 (2010). Accepted for presentation at the conference

  25. Martin-Löf, P.: Intuitionnistic Type Theory. Bibliopolis, Napoli (1984)

    Google Scholar 

  26. Martin-Löf, P.: Mathematics of infinity. In: COLOG-88 Computer Logic, Lecture Notes in Computer Science, pp 146–197. Springer-Verlag , Berlin (1990)

    Google Scholar 

  27. Moerdijk, I.: A model for intuitionistic non-standard arithmetic. Ann. Pure Appl. Logic 73(1), 37–51 (1995)

    Article  MathSciNet  Google Scholar 

  28. Nelson, E.: Internal set theory: A new approach to nonstandard analysis. Bull. Am. Math. Soc. 83(6), 1165–1198 (1977)

    Article  Google Scholar 

  29. Nelson, E.: Radically Elementary Theory. Annals of Mathematics Studies. Princeton University Press (1987)

  30. O’Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs, volume 5170 of Lecture Notes in Computer Science, pp 246–261. Springer (2008)

  31. Reveillès, J.-P., Richard, D.: Back and forth between continuous and discrete for the working computer scientist. Ann. Math. Artif. Intell., Math. Inform. 16(1–4), 89–152 (1996)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Icube UMR 7357 CNRS - Université de Strasbourg, 300 Bld Sébastien Brant, BP 10413, 67412, Illkirch Cedex, France

    Nicolas Magaud

  2. Laboratoire MIA - Université de La Rochelle, Avenue Michel Crépeau, 17042, La Rochelle Cedex, France

    Agathe Chollet

  3. Laboratoire XLIM-SIC UMR 6172 CNRS - Université de Poitiers, Bat. SP2MI Bld Marie et Pierre Curie, BP 30179, 86962, Futuroscope Chasseneuil Cedex, France

    Laurent Fuchs

Authors
  1. Nicolas Magaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Agathe Chollet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Laurent Fuchs
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicolas Magaud.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Magaud, N., Chollet, A. & Fuchs, L. Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. Ann Math Artif Intell 74, 309–332 (2015). https://doi.org/10.1007/s10472-014-9434-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10472-014-9434-6

Keywords

Mathematics Subject Classification (2010)

Search

Navigation