Réflexion pour la réécriture dans le calcul des constructions inductives
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
This thesis presents a generic method to use a technique called computational reflection in the Calculus of Inductive Constructions (CIC) in order to improve efficiency of term rewriting reasonings in the first-order, multi-sorted fragment. The Coq System is a proof assistant based on CIC. It is an interactive system where a user can proof theorems or verify program. The CIC is a constructive and higher-order logic based on type theory. In this logic, theorem claims are types and proofs are objects inhabiting types to be proved. In Coq, proof-checking reduces to type-checking. For equational reasoning, type-checking make arise performances issues. Equal terms replacements are performed by a function taking as arguments all the logical information needed to justify logically this replacement, then it produces a new proof as a result. A proof build by rewriting contains a full copy of the theorem under demonstration. Those copies are specially problematic for automatic reasoning procedures. They are often perform numerous inferences. Those computations are likely to generate large size proof terms. Checking those proof terms is no longer tractable. We studied computational reflection to address this problem. Using computational reflection an automatic reasoning procedure can be introduced inside a Coq proof term. This procedure must be certified in the CIC, in the formal method sense : proven. To implement computational reflection one must express the decisions procedures and their correctness proofs in the object language of the proof assistant. Correctness is express as a semantics interpretation preservation property of the procedure's data. The Conversion rule of the CIC is essential for the computational reflexion to have some benefit, it allows to introduce chosen computations during proof checking. In the two firsts chapters we recall term rewriting and the Calculus of Inductive Constructions. In the two following chapters we present status of equality in the Calculus of Inductive Constructions and computational reflexion. Finally we present our implementation of computational reflexion for term rewriting.
Abstract FR:
Cette thèse présente une méthode générique pour utiliser la technique de la réflexion calculatoire dans le Calcul des Constructions Inductives (CIC) pour augmenter l'efficacité des raisonnements par réécriture de termes, dans le fragment des termes du premier ordre multi-sortés. Le système Coq est un assistant de preuve basé sur le CIC. C'est un système interactif permettant de prouver des théorèmes ou de vérifier des programmes. Le CIC est une logique d'ordre supérieure fondée sur la théorie des types. Dans cette logique, les énoncés de théorèmes sont des types, les preuves sont des termes habitant le type à prouver. Dans Coq, la vérification d'un raisonnement se ramène à une vérification de type. Pour les raisonnements équationnels, les vérifications posent des problèmes de performances. Les remplacements d'égaux sont effectués pax une fonction qui prend en arguments toutes les informations logiques nécessaires à un remplacement et qui produit une nouvelle preuve en résultat. Une preuve produite pax réécriture contient une copie complète du théorème en cours de démonstration. Ces copies posent problème dans le cas des procédures de raisonnement automatiques. Elles effectuent de nombreuses inférences, ce qui engendre des termes de preuve de très grande taille. La vérification de ces preuves n'est plus possible dans des temps acceptables. Pour remédier à ce problème nous avons étudié l'application d'une technique appelée réflexion calculatoire aux raisonnements équationnels. La réflexion calculatoire est une technique qui permet d'introduire une procédure de raisonnement automatique à l'intérieur d'un terme de preuve de Coq. Elle doit être certifiée, au sens des méthodes formelles, dans le CIC. Pour mettre en oeuvre la réflexion calculatoire on exprime les algorithmes et les preuves de correction des procédure de décision dans le langage objet de l'assistant de preuve. La correction est exprimée sous la forme d'une propriété de préservation de l'interprétation sémantique des données de la procédure de raisonnement. La règle de Conversion du CIC est essentielle pour que cette réflexion est un intérêt, elle permet d'introduire des calculs quelconques lors de la vérification des preuves. Dans les deux premiers chapitres nous rappelons des notions de réécriture de termes ainsi que le Calcul des Constructions Inductives. Dans les deux chapitres suivants nous présentons de statut de l'égalité et la réflexion calculatoire dans le CIC. Dans la suite nous présentons nos développements sur la réflexion calculatoire pour la réécriture.