A first look into a formal and constructive approach for discrete geometry using nonstandard analysis

Abstract

In this paper, we recall the origins of discrete analytical geometry developed by J-P. Reveillès [1] in the nonstandard model of the continuum based on integers proposed by Harthong and Reeb [2,3]. We present some basis on constructive mathematics [4] and its link with programming [5,6]. We show that a suitable version of this new model of the continuum partly fits with the constructive axiomatic of ℝ proposed by Bridges [7]. The aim of this paper is to take a first look at a possible formal and constructive approach to discrete geometry. This would open the way to better algorithmic definition of discrete differential concepts. © 2008 Springer-Verlag Berlin Heidelberg.