Toward Formal Specifications: Mathematical and Computational Foundations for Dynamic Geometry
Vers des spécifications formelles : Fondements Mathématiques et Informatiques pour la Géométrie Dynamique
Résumé
This work is a mathematical and algorithmic study which aims at preparing an axiomatization or a specification of dynamic geometry. Problems in dynamic geometry arise with the dynamic behaviour of multiple intersections of curves, and partially defined geometric objects. Recent studies have shown that continuous moves are not fully compatible with determinism of dynamic behaviours. This work details this crucial aspect. Using techniques out of the scope of discrete geometry, it is shown that the dynamic behaviour of circle intersections presents unavoidable singularities. An attempt to extend this result to conic intersections is described. Propositions intended to unify the algorithmic aspects for handling partially defined objects, such as points on objects, are presented, starting from the mathematical framework to the operational implementation. This work also shows that the basic mathematical concept of unsigned area does not intrinsically support moves, unlike signed area. By allowing the specification of algorithms to process the dynamic behavior of circle intersections, this work sets a first quality step for evaluating dynamic geometry software, with respect to their mathematical correctness. Several implementations of this work are included in Cabri 2 Plus. At the theoretical level, this work revisits the problem of the nature of dynamic figures.
Ce travail est une étude algorithmique et mathématique préparant une axiomatisation ou une spécification de la géométrie dynamique. Le comportement dynamique des intersections de courbes, dans le cas où elles sont multiples, et la gestion algorithmique d'objets géométriques sous-déterminés posent problème. Il est connu depuis peu que la continuité des déplacements et le déterminisme des comportements dynamiques ne sont pas entièrement compatibles ; ce travail précise ce point essentiel : par des procédés globaux qui sortent du cadre de la géométrie discrète, il est montré que le comportement dynamique des intersections de cercles présente des singularités inévitables, qui sont énumérées. Une tentative est faite pour étendre ce résultat aux intersections de coniques. Des propositions pour unifier le traitement algorithmique d'objets sous-déterminés, comme les points sur objet, sont présentées, depuis le cadre mathématique jusqu'à l'implémentation effective. Ce travail montre aussi qu'il existe des concepts mathématiques de base, comme la notion d'aire non signée, dont la justification ultime ne supporte pas le mouvement, au contraire de la notion d'aire signée. En permettant la spécification des algorithmes traitant du comportement dynamique des intersections de cercles, ce travail établit un premier niveau de qualité pour les logiciels de géométrie dynamique, permettant de juger leur cohérence mathématique. Plusieurs des implémentations réalisées sont présentes dans Cabri2 Plus, logiciel largement diffusé par l'entreprise Cabrilog. Au niveau théorique, ce travail repose différemment la question de la nature des figures dynamiques, en particulier de la nature mathématique précise des lieux géométriques en géométrie dynamique.
Loading...