Systèmes de réécriture pour l'arithmétique

Résumé

L'objet de ce stage est de trouver ou d'essayer des systèmes de règles de réécriture sur les entiers, confluents et qui terminent, et qui permettent de faire des opérations sur N, Z ou Q. De tels systèmes sont actuellement bien connus pour N avec la représentation de Peano (zéro et successeur engendrent N), mais cette représentation ne répond pas de manière satisfaisante à la volonté d'efficacité. Plusieurs chercheurs se sont intéressés à décrire des systèmes plus efficaces et s'appliquant sur Z et sur les nombres décimaux. Dans ce stage on a étudié ces systèmes, puis on a décrit de nouveaux systèmes. Afin de vérifier la terminaison et la confluence de ces systèmes, on a utilisé le logiciel CiME développé par l'équipe DEMONS du laboratoire de recherche en informatique de l'université Paris XI.

full paper