Insight in discrete geometry and computational content of a discrete model of the continuum ?
This article presents a synthetic and self contained presentation of the discrete model of the continuum introduced by Harthong and Reeb [J. Harthong, lments pour une thorie du continu, Astrisque 109/110 (1983) 235244.[1]; J. Harthong, Une thorie du continu, in: H. Barreau, J. Harthong (Eds.), La mathmatiques non standard, ditions du CNRS, 1989, pp. 307329.[2]] and the related arithmetization process which led Reveills [J.-P. Reveills, Gomtrie discrte, calcul en nombres entiers et algorithmique, Ph.D. Thesis, Universit Louis Pasteur, Strasbourg, France, 1991.[3]; J.-P. Reveills, D. Richard, Back and forth between continuous and discrete for the working computer scientist, Annals of Mathematics and Artificial Intelligence, Mathematics and Informatic 16(14) (1996) 89152.[4]] to the definition of a discrete analytic line. We present then some basis on constructive mathematics [E. Bishop, D. Bridges, Constructive Analysis, Springer, Berlin, 1985.[5]], its link with programming [P. Martin-Lf, Constructive mathematics and computer programming, in: Logic, Methodology and Philosophy of Science, vol. VI, 1980, pp. 153175.[6]; W.A. Howard, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, 1980, pp. 479490.[7]] and we propose an analysis of the computational content of the so-called HarthongReeb line. More precisely, we show that a suitable version of this new model of the continuum partly fits with the constructive axiomatic of R R proposed by Bridges [Constructive mathematics: a foundation for computable analysis, Theoretical Computer Science 219(12) (1999) 95109.[8]]. This is the first step of a more general program on a constructive approach of the scaling transformation from discrete to continuous space.
discrete geometry arithmetization constructive mathematics nonstandard analysis