Implementation du Calcul des Constructions Inductive Presburger

De
Publié par

Niveau: Supérieur
Implementation du Calcul des Constructions Inductive/Presburger Pierre-Yves Strub FORMES, INRIA - Tsinghua Universisity - Beijing 7 Octobre 2009

  • procedure de decision pour l'arithmetique lineaire

  • modification du noyau de coq permettant l'introduction dynamiquement de procedures de decision dans la conversion

  • formalisation en coq

  • calcul des constructions inductives

  • procedure de decision


Publié le : jeudi 1 octobre 2009
Lecture(s) : 23
Source : lix.polytechnique.fr
Nombre de pages : 29
Voir plus Voir moins
Impl´ementationduCalculdes ConstructionsInductive/Presburger
Pierre-Yves Strub
FORMES, INRIA - Tsinghua Universisity - Beijing
7 Octobre 2009
Le Calcul des Constructions Inductives/Presburger CoqMT:uneimpl´ementationdeCIC/N
Certicationduneproce´dureded´ecision(avecA.Mahboubi) Une formalisation en Coq + Ssreflect Ge´n´erationdecerticats
CIC/N
Calcul des ConstructionsInductive/Presburger:
IunCalcul des Constructions Inductives Iuneisecd´deredu´eocrpoiniren´eauelietiqht´mairuolrp dans la conversion
Avantages:
IPlus d’automatisation IPreuves plus courtes... I`id´eaverir...maispasfro´cmeneptulrspa e IPrargoremmsulpicaftspyceeltnvaelemsdantepenesd´
CIC/N
I
I
Modicationdelare`gledeconversion:
Une conversion entre 2termesairm´thiqetsue feraappela`uneorpde´cureded´ecision
E.g., list (x + (f y))list ((f (y + 0)) + x)
Car z = z’x + z = z’ + x (avec z(f y), z’(f (y + 0)))
CoqMT:
IUne modification du noyau deCoqpermettant l’introduction dynamiquementdeproce´duresded´ecisiondanslaconversion.
I´ndOceiritic
IComment charger de telles boites noires IComment le noyau les utilise
Roadmapdelajoutdunethe´orie
Pouruneint´egrationeectiveduneproce´duredede´cision:
1.Chargement, au sein du noyau, d’uneboite noire:
IeeDrcistpirdnoitaleoe´h IdeCoecefdti´ecisionleaglrotimhdede
2.Etablissement ded´eseltrontinienesneiltealCsqoeobti noire(e.g. mapping des symboles au premier ordre sur Coq)
Chargement d’une boite noire (1/2)
I
I
The´orieT= (Σ,A,solve)puatnaraudse`rtenoboˆı´eclired noyau 1.une sorte de travail (e.g.nat)stermesmonosort´e 2.dysselobm(Σsenscouctrurteudso0g.e.)(isn´e[C,0], +[D,2]) 3.une axiomatiqueA(e.g.xy,x+S(y) =S(x+y),∙ ∙ ∙) ISoit via une AST interne ISoit via un langage pour la logique de premier ordre 4.d´deontinioiseccnofenusolve(fonctionO’Caml)
Un contratsolvelatiasce´dredivadiliedt´laecsuseedoHnrpourT.
Chargement d’une boite noire (2/2)
I
I
Possibilit´edins´ererplusieursthe´ories IDoivent travailler sur des sortes disjointes INe peuvent pas partager de variables
Th´ ies = codeO’Caml eor ierte´snevueeˆtnueiqntmerdreamyn`tmedeeivlasesyp chargement de code deCoq(Declare ML Module)
Lieruneth´eorie(1/3)
IUne boite noire estinerteuatpard´ef IElle ne sait pas comment interagir avec les termes Coq
IIl faut IoqsContinie´dsedruserdroremieauprolessymblrseLei IuvroPtasinoiixatamoiebienleniv´erpaipgn´dreuqleme
IiaslonisusPlurieblsiosspetunureseiroe´h
Lierunethe´orie(2/3)
Pour Presburger, on peut e.g.
ILier la sortenatsur l’inductif Inductivenat: Type :=0: nat|S: natnat .
ILier les symboles0etSsur les constructeurs0etSden
0etSdenat.
ILier le symbole+tionsurlad´eniCoqstandardPeano.plus de l’addition.
Lierunethe´orie(3/3)
Lesystemedemanderaalorsdeve´rier,dansCoq, que: `
Inatest de typeType,eobmylseleuqtsselctentlai´esrepeir´te des symboles deT(e.g.0:nat,S:natnat).
Ique les symbolesCoqurtsuetcossrtni´eslcsnoobelssmya`ed injectifs (ici, queSest injectif).
Iysseda`socselobmteuctrnsonessnurptsauqelessymbolesli´e confondus (ici, que0et (Stuotourtauxpnse´seogntp)at).
Ique les axiomes deTsselrapse´tcepsenrietbonsi´es.ymbolesl E.g., dex y,x+S(y) =S(x+y), il sera demande ´
forall (x y : nat), x
+ (Sy) =S(x + y)
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.

Diffusez cette publication

Vous aimerez aussi