La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

A List-machine Benchmark for Mechanized Metatheory

13 pages
LFMTP 2006
A List-machine Benchmark for
Mechanized Metatheory (Extended Abstract)
Andrew W. Appel
Princeton University and INRIA Rocquencourt
Xavier Leroy
INRIA Rocquencourt
Abstract
We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler
correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler imple-
mentations, and we point out that much can be done without binders or alpha-conversion. We propose
specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions
in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.
Keywords: Theorem proving, proof assistants, program proof, compiler verification, typed machine
language, metatheory, Coq, Twelf.
1 How to evaluate mechanized metatheories
The POPLmark challenge [3] aims to compare the usability of several automated
proof assistants for mechanizing the kind of programming-language proofs that
might be done by the author of a POPL paper, with benchmark problems “chosen
to exercise many aspects of programming languages that are known to be difficult
to formalize.” The first POPLmark examples are all in the theory of F and<:
emphasize the theory of binders (e.g., alpha-conversion).
Practitioners of machine-checked proof about real compilers have interests that
are similar but not identical. We want to formally relate machine-checked proofs
Ato actual ...
Voir plus Voir moins
LFMTP2006AList-machineBenchmarkforMechanizedMetatheory(ExtendedAbstract)AndrewW.AppelPrincetonUniversityandINRIARocquencourtXavierLeroyINRIARocquencourtAbstractWeproposeabenchmarktocomparetheorem-provingsystemsontheirabilitytoexpressproofsofcompilercorrectness.IncontrasttothefirstPOPLmark,weemphasizetheconnectionofproofstocompilerimple-mentations,andwepointoutthatmuchcanbedonewithoutbindersoralpha-conversion.Weproposespecificcriteriaforevaluatingtheutilityofmechanizedmetatheorysystems;wehaveconstructedsolutionsinbothCoqandTwelfmetatheory,andwedrawconclusionsaboutthosetwosystemsinparticular.Keywords:Theoremproving,proofassistants,programproof,compilerverification,typedmachinelanguage,metatheory,Coq,Twelf.1HowtoevaluatemechanizedmetatheoriesThePOPLmarkchallenge[3]aimstocomparetheusabilityofseveralautomatedproofassistantsformechanizingthekindofprogramming-languageproofsthatmightbedonebytheauthorofaPOPLpaper,withbenchmarkproblems“chosentoexercisemanyaspectsofprogramminglanguagesthatareknowntobedifficulttoformalize.”ThefirstPOPLmarkexamplesareallinthetheoryofF<:andemphasizethetheoryofbinders(e.g.,alpha-conversion).Practitionersofmachine-checkedproofaboutrealcompilershaveintereststhataresimilarbutnotidentical.Wewanttoformallyrelatemachine-checkedproofstoactualimplementations,notparticularlytoLATEXdocuments.Furthermore,perhapsitisthewrongapproachto“exerciseaspects...thatareknowntobedifficulttoformalize.”Bindersandαβ-conversionarecertainlyuseful,buttheyarenotessentialforprovingrealthingsaboutrealcompilers,asdemonstratedinseveralsubstantialcompiler-verificationprojects[9,10,13,6,7,8].Ifmachine-checkedproofistobeusefulinprovidingguaranteesaboutrealsystems,letusplaytoitsstrengths,nottoitsweaknesses.ThispaperiselectronicallypublishedinElectronicNotesinTheoreticalComputerScienceURL:www.elsevier.nl/locate/entcs
AppelandLeroyThereforewehavedesignedadown-to-earthexampleofmachine-checkedmetathe-ory,closertothesemanticsoftypedassemblylanguages.Itisentirelyfirst-order,withoutbindersortheneedforalphaconversion.WespecifytheStructuredOper-ationalSemantics(SOS)ofasimplepointermachine(cons,car,cdr,branch-if-nil)andwepresentasimpletypesystemwithconstructorsforlist-of-τandnonempty-list-of-τ.Thebenchmarkexplicitlycoverstherelationshipofproofsaboutatypesystemtoproofsaboutanexecutabletypechecker.Thechallengeistorepresentthetypesystem,provesoundnessofthetypesys-tem,representthetype-checkingalgorithm,andprovethatthealgorithmcorrectlyimplementsthetypesystem.WehaveimplementedthebenchmarkbothinCoqandinTwelfmetatheory,andwedrawconclusionsabouttheusabilityofthesetwosystems.Welackspacetopresenthere,butdiscussinthefullpaper[1],howtheneedsofimplementors(ofprovablycorrectcompilersandprovablysoundtypecheckers)differfromtheneedsofPOPLauthorsaddressedbythefirstPOPLmark;aspecificationoftheentireproblemdowntodetailssuchastherecommendedasciinamesforpredicatesandinferencerules;detailsofourCoqandTwelfsolutions;moredetailsaboutwhichsubtaskswereeasyordifficultinCoqandTwelf;howeasyitistolearnTwelfandCoqgiventheavailabledocumentation.Aswellasabenchmark,thelistmachineisausefulexerciseforstudentslearningCoqorTwelf;wepresenttheoutlinesofoursolutions(withproofsdeleted)ontheWeb[2].2SpecicationoftheproblemMachinesyntax.MachinevaluesAareconscellsandnil.a:A::=nil|cons(a1,a2)Theinstructionsofthemachineareasfollows:ι:I::=jumpl(jumptolabell)|branch-if-nilvl(ifv=nilgotol)|fetch-fieldv0v0(fetchtheheadofvintov0)|fetch-fieldv1v0(fetchthetailofvintov0)|consv0v1v0(makeaconscellinv0)|halt(stopexecuting)|ι0;ι1(sequentialcomposition)Inthesyntaxabove,themetavariablesvirangeovervariables;thevariablesthem-selvesviareenumeratedbythenaturalnumbers.Similarly,metavariableslirangeoverprogramlabelsLi.Aprogramisasequenceofinstructionblocks,eachprecededbyalabel.p:P::=Ln:ι;p|end2
AppelandLeroyOperationalsemantics.Machinestatesarepairs(r,ι)ofthecurrentinstructionιandastorerassociatingvaluestovariables.Wewriter(v)=atomeanthataisthevalueofvariablevinr,andr[v:=a]=r0tomeanthatupdatingrwiththebinding[v:=a]yieldsauniquestorer0.Thesemanticsofthemachineisdefinedpbythesmall-steprelation(r,ι)7→(r00)definedbytherulesbelow,andtheKleenepclosureofthisrelation,(r,ι)7→(r00).p(r,(ι1;ι2);ι3)7→(r,ι1;(ι2;ι3))r(v)=cons(a0,a1)r[v0:=a0]=r0r(v)=cons(a0,a1)r[v0:=a1]=r0pp(r,(fetch-fieldv0v0;ι))7→(r0)(r,(fetch-fieldv1v0;ι))7→(r0)r(v0)=a0r(v1)=a1r[v0:=cons(a0,a1)]=r0p(r,(consv0v1v0;ι))7→(r0)r(v)=cons(a0,a1)r(v)=nilp(l)=ι0pp(r,(branch-if-nilvl;ι))7→(r,ι)(r,(branch-if-nilvl;ι))7→(r,ι0)p(l)=ι0p(r,jumpl)7→(r,ι0)Aprogrampruns,thatis,p,ifitexecutesfromaninitialstatetoafinalstate.Astateisaninitialstateifvariablev0=nilandthecurrentinstructionistheoneatL0.Astateisafinalstateifthecurrentinstructionishalt.p{}[v0:=nil]=rp(L0)=ι(r,ι)7→(r0,halt)pItisusefulforabenchmarkformachine-verifiedprooftoincludeexplicitasciinamesforeachconstructorandrule.Ourfullspecification[1]doesthat.Atypesystem.Wewillassigntoeachlivevariableateachprogrampointalisttype.Toguaranteesafetyofcertainoperations,weproviderefinementsofthelisttypefornonemptylistsandforemptylists.Inparticular,thefetch-fieldoperationsdemandthattheirlistargumenthasnonemptylisttype,andthebranch-if-niloperationrefinesthetypeofitsargumenttoemptyornonemptylist,dependingonwhetherthebranchistaken.τ:T::=nil(singletontypecontainingnil)|listτ(listwhoseelementshavetypeτ)|listconsτ(non-nillistofτ)AnenvironmentΓisantypeassignmentoftypestoasetofvariables.Wedefinetheobvioussubtypingττ0amongthevariousrefinementsofthelisttype,usingacommonsetoffirst-ordersyntacticrules,easilyexpressibleinmostmechanizedmetatheories.Weextendsubtypingwidthwiseanddepthwisetoenvironments.Wedefinetheleastcommonsupertypeτ1uτ2=τ3oftwotypesτ1andτ2asthesmallestτ3suchthatτ1τ3andτ1τ2.Intheoperationalsemantics,aprogramisasequenceoflabeledbasicblocks.Inourtypesystem,aprogram-typing,rangedoverbyΠ,associatestoeachprogramlabelavariable-typingenvironment.WewriteΠ(l)=ΓtoindicatethatΓrepresentsthetypesofthevariablesonentrytotheblocklabeledl.3
AppelandLeroyInstructiontypings.IndividualinstructionsaretypedbyajudgmentΠ`instrΓ{ι}Γ0.Theintuitionisthat,underprogram-typingΠ,theHoaretripleΓ{ι}Γ0relatespreconditionΓtopostconditionΓ0.Π`instrΓ{ι1}Γ0Π`instrΓ0{ι2}Γ00Π`instrΓ{ι1;ι2}Γ00Γ(v)=listτΠ(l)=Γ1Γ[v:=nil]=Γ0Γ0Γ1Π`instrΓ{branch-if-nilvl}(v:listconsτ,Γ0)Γ(v)=listconsτΠ(l)=Γ1Γ[v:=nil]=Γ0Γ0Γ1Π`instrΓ{branch-if-nilvl}ΓΓ(v)=nilΠ(l)=Γ1ΓΓ1Π`instrΓ{branch-if-nilvl}ΓΓ(v)=listconsτΓ[v0:=τ]=Γ0Γ(v)=listconsτΓ[v0:=listτ]=Γ0Π`instrΓ{fetch-fieldv0v0}Γ0Π`instrΓ{fetch-fieldv1v0}Γ0Γ(v0)=τ0Γ(v1)=τ1(listτ0)uτ1=listτΓ[v:=listconsτ]=Γ0Π`instrΓ{consv0v1v}Γ0Blocktypings.Ablockisaninstructionthatdoesnot(statically)continuewithanotherinstruction,becauseitendswithajump.Π`instrΓ{ι1}Γ0Π;Γ0`blockι2Π(l)=Γ1ΓΓ1Π;Γ`blockι1;ι2Π;Γ`blockjumplProgramtypings.Wewrite|=progp:Πandsaythataprogramphasprogram-typingΠifforeachlabeledblockl:ιinp,theblockιhasthepreconditionΠ(l)=ΓgiveninΠ,thatis,Π;Γ`blockι.Moreover,wedemandthatΠ(L0)=v0:nil,{}andthateverylabelldeclaredinΠisdefinedinp.Typesystemvs.typechecker.Wehavepresentedsomerelationsdefinedbyderivationrulesandsomedefinedinformally.Thisisabitsloppy,especiallywhereaderivationrulereferstoaninformallydefinedrelation;anysolutiontothebench-markmustformalizethis.Wewillusethenotation|=progp:ΠtomeanthatprogramphastypeΠinthe(notnecessarilyalgorithmic)typesystem,andthenotation`progp:Πtomeanthatp:Πisderivedinsomealgorithmictype-checker.Thefullpaper[1]outlinestwosuchalgorithmictype-checkers.Oneiswritteninpseudo-codeandcorrespondstoatype-checkerimplementedinimperativeorfunc-tionalstyle.Theotherrefinesthederivationrulesgivenabovetomakethemfullysyntax-directedandthereforeamenabletoanimplementationasalogicprogram.Sampleprogram.Thefollowinglist-machineprogramhasthreebasicblocks.Variablev0isinitializedtonilasprescribedbytheoperationalsemantics.Block0initializesv1tothelistcons(nil,cons(nil,nil))andjumpstoblock1.Block1isaloopthat,whilev1isnotnil,fetchesthetailofv1andcontinues.Thelastinstructionofblock1isactuallydeadcode(neverreached).Block2istheloopexit,andhalts.psample=L0:consv0v0v1;consv0v1v1;consv0v1v1;jumpL1;L1:branch-if-nilv1L2;fetch-field1v1v1;branch-if-nilv0L1;jumpL2;L2:halt;dne4
AppelandLeroyTheprogramiswell-typedwithΠsample=L0:(v0:nil,{}),L1:(v0:nil,v1:listnil,{}),L2:{},{}3MechanizationtasksImplementingthe“list-machine”benchmarkinamechanizedmetatheory(MM)comprisesthefollowingtasks:1.RepresenttheoperationalsemanticsintheMM.2.Derivethefactthatpsample.TheMMshouldconvenientlysimulateexecutionofsmallexamples,sotheusercandebugtheSOSandgetanintuitivefeelforitsexpressiveness.Soundnessofatypesystem.3.RepresentthetypesystemintheMM(deneenoughnotationtorepresenttheformula|=progp:Πandinferencerulesfromwhichtype-soundesscouldbeproved).4.RepresentintheMManalgorithmforleast-common-supertype,thatis,thecomputationτ1uτ2=τ3producingτ3frominputsτ1andτ2.5.Usingthetypesystem,derivethefactthat|=progpsamplesample.TheMMshouldconvenientlysimulatetype-checkingofsmallexamples,sotheusercandebugthetypesystemandgetafeelforitsexpressiveness.6.Representthestatementofthedeningpropertiesofleastcommonsupertypes,e.g.,τ1uτ2=τ3τ1τ3.7.Provethattheualgorithmenjoystheseproperties.8.Representthestatementofasoundnesstheoremforthetypesystem.Theinformalstatementofsoundnessis,“awell-typedprogramwillnotgetstuck.”Aprogramstateisnotstuckifitstepsorhalts:p|=progp:Πinitial(p,r,ι)(r,ι)7→(r00)(r0000.(r00)7→p(r0000))ι0=haltsoundness9.Provethesoundnesstheorem.Thefullpaper[1]outlinestheprincipallemmasofthisproof,whichisastandardargumentbytypepreservationandprogress.Efficienttype-checkingalgorithm.10.Representanasymptoticallyecienttype-checkingalgorithm`progp:ΠintheMM.ByefficientwemeanthatanN-instructionprogramwithMlivevariablesshouldtype-checkinO(NlogM)time.11.Usingthetype-checkingalgorithm,calculate`progpsamplesample.TheMMshouldsimulateexecutionofalgorithmsonsmallinputs.12.Provethatthetype-checkingalgorithmterminatesonanyprogram.13.Demonstratethetype-checkeronlarge-scaleexampleswithgoodperformance.TypicallythiswillbedonethroughanautomatictranslationtoPrologorMLwhichisthencompiledbyanoptimizingcompiler.14.Provethat`progp:Πimplies|=progp:Π.Thatis,thetype-checkersoundlyimplementsthetypesystem.5
AppelandLeroyWritingthepaper.15.UseanautomatictooltogeneratereadableLATEXformulasfortheSOSrules,thetypingrules,andthestatementsof(nottheproofsof)theleast-common-supertypelemmasandsoundnesstheorems.KleinandNipkow[6]demonstratethisverynicelyintheIsabelle/HOLformalizationofaJavasubsetcompiler.4AproofinTwelfmetatheoryTheTwelfsystem[12]isanimplementationoftheEdinburghLogicalFramework(LF).OnecanrepresenttheoperatorsofalogicastypeconstructorsinLF,andproofsinthatlogicastermsinLF,andonecandoproof-checkingbytype-checkingtheterms(consideringthemasderivations).InTwelfonecanprovetheorems(proofsinalogic),ormetatheorems(proofsaboutalogic).Eitherapproachcouldbeusedforourbenchmark.OursolutionusestheusualapproachinTwelf,whichismetatheoretic.Inthiscasethelogicsinquestionareouroperationalsemanticsandourtypesystem,andthemetatheoremtobeprovedistypesoundness:thatis,ifonecancombinetheinferencerulesofthetypesystemtoproduceaderivationoftype-checking,thenitmustbepossibletocombinetheinferencerulesoftheSOStoproduce(only)nonstuckderivationsofexecution.Thisapproachisagressivelysyntactic.Insteadofsayingthatpisamappingfromlabelstoinstructions,wegivesyntacticconstructionsthat(weclaim)representsuchamapping.Oneconsequenceofthisstyleisthatour|=progp:Πisnotjustasemanticrelation,butasyntacticallyderivableoneexpressedasHornclauses.BycarefullystructuringtheHornclausesthatdefineourrelationssothatwecaniden-tify“input”and“output”arguments,wecanensurethatthelogic-programminginterpretationofourclausesisactuallyanalgorithm.Thisinput-outputorganiza-tioncanbespecifedandmechanicallycheckedinTwelfvia%modedeclarations.OurtypesystemisthendirectlyexecutableinTwelf.EachclauseinTwelfisnamed.WhenTwelftracesout,viaprolog-styleback-tracking,oneormorederivationsofaresultbythesuccessfulapplicationofclauses,itbuildsaswelladerivationtreeforeachderivation.InLF,onecancomputeaswellonthederivationtreesthemselves.Supposewewriteanotherprologprogram(setofclauses)thattakesasinputaderivationtreefortype-checking,andproducesasoutputaderivationtreeforsafe(nonstuck)execution.Ifthisprogramistotal(thatis,terminatessuccessfullyonanyinput)thenwehaveconstructivelyprovedthatanywelltypedprogramissafe.Toreasonaboutthismeta-program,weuse(machine-checked)%modedeclara-tionstoexplainwhataretheinputsandoutputsofthederivationtransformer.Wealsouse(machine-checked)%totaldeclarationstoensurethatourmeta-programhascoveredallthecasesthatmayarise,andthatourmeta-programdoesnotinfinite-loop.Wegiveanexampleofsuchaproofinsection6,items6and7.Twelfhasanamazingeconomyoffeatures.Onedoesnothavetolearnamodulesystem—becausethereisnone—onejustusesnamingconventionsonallone’siden-tifiers.Onedoesnothavetolearnhowtouselargelibrariesoflemmasandtactics,becausetherearenolibrariesoflemmasandtactics:butsuchlibrarieswouldnot6
AppelandLeroybesouseful,becauseTwelfhasfewabstractionfeatures,andnopolymorphism.Allproofsaredonewiththesimplemechanismofprovingthetotalityofmetaprograms.There’sacalculatedgamblehere:Inreturnforthebenefitofprovingeveryinginonesimplestyle,andrarelyhavingtotranslatebetweenabstractions,onetradesawaymanythings:therearesometheoremsthatthisnotationcannotevenexpress(becausethequantifiersarenestedtoodeep,forexample);andtherearesomethingsthatareprovablebutinacontrivedway(expressingsemanticpropertiesonlywithinductivesyntacticconstructors),asillustratedbelow.OurTwelfproofstartsbydefininginductivelythenotionofequalitiesandin-equalitiesonnaturalnumbers,labels,variables,typestructure,andtermstructures.Wegivesyntacticcharacterizationsofwell-formedenvironments(i.e.,thatdonotmapthesamevariabletwice).Sometimesitistrickytomakeaproperlyinductivesyntacticdefinitionofasemanticproperty.Forexample,considerenvironmentsubtyping,semanticallyΓ1envΓ2≡∀v.vdomΓ2(vdomΓ1Γ1(v)Γ2(v)).An“obvious”“inductive”definitionusesthesyntacticrules,Γ1(v)=τ0τ0τΓ1envΓ2aa12Γ⊂{}Γ1envv:τ,Γ2Theinductionis(supposedly)overthesizeofthetermtotherightoftheenvsymbol.However,thisdefinitionisnotsufficientlyinductiveforusefulproperties(transitivity,reflexivity)tobeprovable—atleast,wewerenotabletoprovethem.TheproblemappearstobethatΓ1doesnotdecreaseinrulea2.Thefollowingdefinitionisproperlyinductive—weuseΓ0insteadofΓ1inthepremiseofruleb2.Provingtransitivityandreflexivityfromthisdefinitioniseasy;thedifficultyistoavoidwastingtimewiththepseudoinductivedefinitionabove.Γ1=.(v:τ0,Γ0)τ0τΓ0envΓ2bΓenv{}1Γ1envv:τ,Γ2b25AproofinCoqTheCoqsystem[5,4]isaproofassistantbasedontheCalculusofInductiveCon-structions.Thislogicisavariantoftypetheory,followingthe“propositions-as-types,proofs-as-terms”paradigm,enrichedwithbuilt-insupportforinductiveandcoinductivedefinitionsofpredicatesanddatatypes.Fromauser’sperspective,Coqoffersarichspecificationlanguagetodefineprob-lemsandstatetheoremsaboutthem.Thislanguageincludes(1)constructivelogicwithalltheusualconnectivesandquantifiers;(2)inductivedefinitionsviainferencerulesandaxioms(asinTwelf’smeta-logic);(3)apurefunctionalprogramminglanguagewithpattern-matchingandstructuralrecursion(inthestyleofMLorHaskell).Forthelist-machinebenchmark,weusedacombinationofallthreespecificationstyles,followingcommonpracticeinresearchpapersontypesystems.Theinferencerulesforoperationalsemanticsandthetypesystemsaretranscribeddirectlyasinductivedefinitions.Operationsoverstores,environmentsandprogram-typings,aswellasleastcommonsupertypesandthetype-checkingalgorithmarepresented7
AppelandLeroyasfunctions.Finally,subtypingbetweenenvironmentsΓΓ0isdefinedbythepropositionalformulav,t0,Γ0(v)=t0⇒∃t,Γ(v)=ttt0UnlikeTwelf’smeta-theory,thelogicofCoqprovidesrichformsofpolymor-phism.Thisenabledustofactoroutthetreatmentofstores,environments,andprogram-typingsbyreusinganefficient,polymorphicimplementationoffinitemapsasradix-2searchtreesdevelopedearlierbyLeroyaspartoftheCompcertproject[8].6ComparisonofmechanizedproofsTaskTwelfCoq1.OperationalSemantics12698lines2.Derivep183.Typesystem|=progp:Π1671304.ualgorithm**5.Derive|=progpsamplesample1no6.Statepropertiesofu12137.Provepropertiesofu114218.Statesoundnesstheorem29159.Provesoundnessof|=progp:Pi206031510.Ecientalgorithm2214511.Derive`progpsamplesample1112.Proveterminationof`progp:Π18013.Scalabletype-checkeryesyes14.Provesoundnessof`progp:Pi34714115.GenerateLATEXnonoWehaveimplementedthosetasksthatareimplementableinboththeTwelf(metatheory)andCoqsystems.Thenumberoflinesofcoderequiredissummarizedinthetableabove.Totalparsingandproof-checkingtime1was0.558secondsrealtimeforTwelf,2.622secondsforCoq.1.Operationalsemantics.BothTwelfandCoqmakeiteasyandnaturaltorepresentinductivedefinitionsofthekindfoundinSOS.InCoqonealsohasthechoiceofrepresentingoperationsovermappings(e.g.,lookupandupdateinstores)eitherasrelations(definedbyinductivepredicates)orasfunctions(definedbyrecursionandpattern-matching).2.Derivep.Twelfmakesitveryeasytointerpretinductivedefinitionsaslogicprograms.ThereforethistaskwastrivialinTwelf.Coqdoesnotprovideageneralmechanismtoexecuteinductivedefinitions.However,therulesfortheoperationalsemanticsweresimpleenoughthat(aftersomeexperimentation)wecouldusetheproofsearchfacilitiesofCoq(theeautotactic)asapoorman’slogicprograminterpreter.AmoregeneralmethodtoexecuteinductivedefinitionsinCoq,whichweimplementedalso,istodefineanexecutionfunction(61lines),proveitscorrectnesswithrespecttotheinductivedefinition(35lines),thenexecutethefunction.(EvaluationoffunctionalprogramsissupportednativelybyCoq.)1DellPrecision360,Linux,2.8GHzPentium4,1GBRAM,512kBcache.8
AppelandLeroy3.Representthetypesystem.EasyandnaturalinbothTwelfandCoq(with,asbefore,thechoiceinCoqofusingthefunctionalpresentationofoperationsovermappings).4.Least-upper-boundalgorithm.Becausethe“typesystem”representedinTwelfismoststraightforwardlydoneasaconstructivealgorithm,thiswasalreadydoneaspartoftask3inourTwelfrepresentation.InCoq,whilethetypesystemitselfisnotalgorithmic,wechosetospecifytheleast-upperboundoperationasafunctionfrompairsoftypestotypes.Therefore,thealgorithmtocomputeleast-upperboundswasalreadydoneaspartoftask3intheCoqdevelopmentaswell.5.Deriveanexampleoftype-checking.TrivialtodoinTwelf,byrunningthetypesystemasalogicprogram.NotdirectlypossibleinCoqbecausethespecificationofthetypesystemisnotalgorithmic:itusesuniversalquantificationoverallvariablestospecifyenvironmentsubtyping.6.Statepropertiesofleast-upper-bound.EntirelystraightforwardinCoq.Forexample,herearetheCoqstatementsoftheseproperties:Lemmalub_comm:forallt1t2,lubt2t1=lubt1t2.Lemmalub_subtype_left:forallt1t2,subtypet1(lubt1t2).Lemmalub_subtype_right:forallt1t2,subtypet2(lubt1t2).Lemmalub_least:forallt1t3,subtypet1t3->forallt2,subtypet2t3->subtype(lubt1t2)t3.Thecorrespondencewiththemathematicalstatementsofthesepropertiesisobvi-.suoInTwelf,statingthepropertiesofleast-upper-boundmustbedoneinawaythatseemsartificialatfirst,butoncelearnedisreasonablynatural.Thelemmaτ1uτ2=τ3lub-subtype-leftττ31isrepresentedasalogic-programmingpredicate,lub-subtype-left:lubT1T2T3->subtypeT1T3->type.whichtransformsaderivationoflubT1T2T3intoaderivationofsubtypeT1T3.The“proof”willconsistoflogic-programmingclausesoverthispredicate.Tobea“proof”ofthepropertywewant,wewillhavetodemonstrate(tothesatisfactionofthemetatheory,whichchecksourclaims)thatourclauseshavethefollowingproperties:%modelub-subtype-left+P1-P2.Themodesofalogicprogramspecifywhichargumentsaretobeconsideredinputs(+)andwhichareoutputs(-).For-mally,givenanygroundterm(i.e.,containingnologicvariables)P1whosetypeislubT1T2T3,ourclauses(iftheyterminate)mustproduceoutputsP2oftypesubtypeT1T3thatarealsogroundterms.%totalP1(lub-subtype-leftP1P2).Weaskthemetatheoremtocheckourclaimthatnoexecutionoflub-subtype-leftcaninfinite-loop:itmusteitherfailorproduceaderivationofsubtypeT1T3;andwechecktheclaimthattheexecutionneverfails(thatallcasesarecovered).TheuseofP1intwoplacesinour%totaldeclarationis(insomesense)mixingthethingtobeprovedwithpartoftheproof:weindicatethattheinductionshouldbedoneoverargument9
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin