Re: [GeOCaml] news

[mariano . georges]

En principe, réception de ce message en double, je copie sur 

address@hidden

pour vérifier, ensuite on bascule...


> Quel genre d'énoncés ? tu peux donner un exemple ?

Je dois d'abord préciser ce que j'entend par macros... le mot est peut-être mal
choisi. L'idée c'est d'utiliser une macro (e.g tracer le milieu d'un segment)
uen fois que l'on a "appris" au système comment se trace ... le milieu d'un
segment. Une macros (ou construction apprise) défini donc :

* les éléments nécessaires en entrée (e.g un segment ou bi-point)

* les éléments en sortie (e.g. le milieu)

* le mode opératoire pour obtenir ces "sorties"

Avec la contrainte <.geo>caml de donner une syntaxe "naturelle" à cette
"déclaration" (ou apprentissage). La syntaxe qui énonce un théorème me semble
approprié :

schématiquement :

/Si/soit/ 
  A et B deux points
/Par/ 
  ...construction du milieu...
/Alors/
  I milieur du segment [AB] 
.  <- le point de qed ? ;-)

> l'idée est séduisante, on pourrait voir les macros aussi comme des 
> PREUVES de théorèmes du style :

j'ai pas encore penser aux extensions de cette idée ;-) mais pourquoi pas !

> On pourrait autoriser l'utilisateur à se restreindre à certaines 
> constructions de base par exemple :
 
Mon avis/idée perso (à l'origine de GeOCaml) c'est d'en rester strictement à la
géométrie euclidienne (le reste c'est en option à faire en dehors du coeur
principal du "moteur" geocaml). Ça rejoint également l'idée qu'une théorie
réduite se prêtera mieux au traitement formel 

En tout cas, ce qui est plutôt cartésien ne doit pas influencer le noyau
théorique purement euclidien (abstrait)...  

> Est-ce que tu peux me donner des pointeurs vers ces rapports inria ?

je note dans mon todo ;-)  (un .bib ?? ;-)
 

> Cela permettrait de faciliter le codage car c'est plus modulaire et en 
> plus on  peut espèrer obtenir des utilisateurs (voir même des 
> contributeurs) au delà de geocaml, les gens de Kig, DrGeo, Kseg etc

soyons clairs : oui.

> enfin une petite question sur votre langage : est-ce qu'il est prevu de 
> pouvoir fournir les coordonnées de points libres ?

oui... c'est nécessaire pour obtenir des figures esthétiques/équilibrées même si
on s'en moque un peu pour l'instant ...

Je donne l'adresse où un maximum de choses peuvent être notées (je viens
d'ajouter le point d'entrée GeOCamlBiblio ;-)

http://www.mjc-athena.org/MJCNet/GeOCaml

(c'est le site d'un club linux où 3 membres de GeOCaml se rencontrent ;-)