A First Look Into A Formal And Constructive Approach For Discrete Geometry Using Nonstandard Analysis

In this paper, we recall the origins of discrete analytical geometry developed by J-P. Reveilles [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 R 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.