L'électricité est constructive : l'équivalence entre la propagation électrique et le calcul Booléen constructif pour les circuits synchrones cycliques

La preuve demande le développement de nouvelles logiques intuitionnistes de la stabilisation électrique, ainsi que la preuve de plusieurs théorèmes intermédiaires montant l’équivalence du modèle électrique obtenu et d’un système de règles de déduction purement syntaxique qui permet de simuler le fonctionnement des circuits en se limitant à la stabilisation des voltages et en ignorant les transitoires. Elle est essentiellement due à Michel Mendler (U. Bamberg, Allemagne). Elle est plus forte et plus rigoureuse que les preuves précédentes (Shiple-Berry-Touati 2001), fondées sur des graphes d’événements analysant les transitoires dans un modèle de délai plus contraint et moins naturel  (modèle de Brzozowski-Seger).

Je rappellerai d’abord la source du problème : les circuits cycliques apparaissent naturellement lors de la traduction en circuits de langages de haut niveau comme Esterel, et ils sont tout à fait naturels pour implémenter des algorithmes fondamentalement symétriques. Je rappellerai l’exemple de S. Malik, qui montre que les circuits cycliques peuvent être exponentiellement plus petits que les circuits acycliques pour la même fonction, puis l’arbitre cyclique pour bus à jetons, et enfin le nouvel exemple du découpage d’instructions dans les Pentium. Mais l’analyse de leur comportement est non-triviale, et les circuits cycliques ne se stabilisent pas en général, d’où le problème.

J’introduirai ensuite la nouvelle logique UN (up-bounded non-inertial delays). Son modèle représente les histoires électriques des fils, portes et délais en se concentrant uniquement sur la stabilisation de leurs voltages. Il permet de coder de façon simple la logique et les délais des circuits. Je définirai ensuite les règles de déduction permettant de simuler symboliquement l’exécution électrique. Je présenterai les théorèmes exprimant l’équivalence entre modèle et système déductif, puis le résultat qui montre l’intuitionnisme de la logique. C’est justement ce caractère intuitionniste qui permet de monter le déterminisme de la stabilisation des voltages, qui ne peut se faire que sur une seule valeur par sortie.

Une fois montré ces résultat centraux, un simple tour de passe-passe permet de faire disparaître totalement les délais, en montrant que la stabilité des sorties peut se calculer dans le simple calcul Booléen constructif (sans tiers exclu), donc hors-temps. Le corollaire simple est qu’un circuit qui stabilise ses sorties en logique Booléenne constructive le fait électriquement pour tous délais des fils et portes et aux mêmes valeurs, ce qui est le résultat final souhaité.

Cette théorie ne donne pas encore d’algorithme simple pour déterminer si un circuit cyclique se stabilise ou oscille. Un tel algorithme, fondé sur la logique ternaire de Scott, sera montré au cours suivant du 2 avril. Il sera étendu aux circuits avec registres, les plus généraux.