Programmation par formules de Horn et temps linéaire sur automates cellulaires
Etienne Grandjean (GREYC, Caen)Bon nombre de problèmes algorithmiques se définissent naturellement par induction: produits de polynômes ou d’entiers par la méthode de Horner, tris par échanges locaux, etc. Dans de nombreux cas aussi, on peut montrer qu’une telle induction se caractérise de façon géométrique par un ensemble fixé de vecteurs (qu’on appellera son système d’induction) qui, naturellement, fournit une méthode pour calculer les objets définis par l’induction, par un calcul local et parallèle. On en déduit un programme d’automate cellulaire pour le problème algorithmique considéré.
S’appuyant sur quelques exemples simples, l’exposé tentera de suggérer l’intuition du passage de la formule inductive (une formule de Horn) qui définit un problème algorithmique à l’automate cellulaire qui le calcule. On verra aussi que l’automate cellulaire ainsi obtenu fonctionne en temps linéaire, donc optimal.
C’est un travail en collaboration avec Nicolas Bacquey, INRIA, Lille, et Frédéric Olive, LIF, Université de Marseille).