Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Preuves par réécriture associative-commutative
Preuves par réécriture associative-commutative
1 Contexte
Il est important de pouvoir réaliser dans Coq des preuves efficaces
par réécriture. Les preuves naïves créent des termes de preuves
gigantesques qui rendent difficilement vérifiables des preuves mettant
en jeu un grand nombre de réécritures. Pour remédier à ce problème, B.
Werner a proposé d'utiliser un langage intermédiaire de traces qui est
produit par un moteur de réécriture puis qui peut être réinterprété
dans Coq par une fonction certifiée. Cette méthode est un cas
particulier de preuves par réflexion [2, 6, 5].
Poursuivant cet idée, C.Alvarado a proposé une méthode générale
de représentation dans Coq de preuves
par réécriture dans une algèbre de termes multi-sortée [1]. Chaque
réécriture est représentée dans Coq par une fonction sur les termes.
Les réécritures de base peuvent être combinées pour donner des
réécritures plus complexes. En collaboration avec H. Nguyen, une
interface entre Elan et Coq a été développée. Elan calcul des traces
qui sont ensuite reinterprétées par Coq.
2 Objet du stage
Cette approche est prometteuse, cependant elle ne prend pas en compte
le mécanisme de réecriture associative-commutative qui est pourtant au
coeur de la puissance des systèmes de réécriture. L'objet du stage
est d'étendre la méthode proposée par C. Alvarado au cas des
réécritures AC. Pour cela, la fonction d'interprétation d'une
réécriture élémentaire de la forme l ® r
prendra comme argument en plus du terme t à réécrire, une
substitution s ainsi qu'une preuve de s(l)º t
modulo AC. Le stage comportera une partie de mise au point de la
méthode en s'appuyant sur le logiciel CiME [3, 4] pour
produire des traces de réécriture modulo AC (terme à réécrire,
regle appliquée, position d'application et substitution utilisée)
puis le développement des bibliothèque Coq nécessaire à
l'approche réflexive et enfin l'application sur des exemples.
Cuihtlauac Alvarado and Quang-Huy Nguyen.
ELAN for equational reasoning in coq.
In Proceeding of the 2nd Workshop on Logical Frameworks and
Metalanguages. Santa Barbara, California, 2000.
Samuel Boutin.
Using reflection to build efficient and certified decision
procedures.
In Takahashi Ito and Martin Abadi, editors, TACS'97, volume
1281. LNCS, Springer-Verlag, 1997.
Evelyne Contejean and Claude Marché.
CiME: Completion Modulo E.
In Harald Ganzinger, editor, 7th International Conference on
Rewriting Techniques and Applications, volume 1103 of Lecture Notes in
Computer Science, pages 416--419, New Brunswick, NJ, USA, July 1996.
Springer-Verlag.
System Description available at
http://www.lri.fr/ demons/cime.html.
Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain.
Cime version 2, 2000.
Prerelease available at http://www.lri.fr/ demons/cime.html.
P. Letouzey and L. Théry.
Formalizing Stålmarck's algorithm in Coq.
In J. Harrison and M. Aagaard, editors, 13th International
Conference on Theorem Proving in Higher Ord er Logics (TPHOLs 2000), volume
1869 of Lecture Notes in Computer Science, pages 387--404.
Springer-Verlag, 2000.
Patrick Loiseleur and Samuel Boutin.
The Coq Proof Assistant, Addendum to the Reference
Manual, Version 6.2, chapter 19: The Ring tactic.
ftp://ftp.inria.fr/INRIA/coq/V6.2/doc, 1998.