A List-machine Benchmark for Mechanized Metatheory

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

Publié par

Fioz

Nombre de lectures

Langue

English

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 ﬁrst 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
speciﬁc 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 veriﬁcation, 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 diﬃcult
to formalize.” The ﬁrst 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

Publié par

Fioz

Nombre de lectures

Langue

English

LFMTP2006AList-machineBenchmarkforMechanizedMetatheory(ExtendedAbstract)AndrewW.AppelPrincetonUniversityandINRIARocquencourtXavierLeroyINRIARocquencourtAbstractWeproposeabenchmarktocomparetheorem-provingsystemsontheirabilitytoexpressproofsofcompilercorrectness.IncontrasttotheﬁrstPOPLmark,weemphasizetheconnectionofproofstocompilerimple-mentations,andwepointoutthatmuchcanbedonewithoutbindersoralpha-conversion.Weproposespeciﬁccriteriaforevaluatingtheutilityofmechanizedmetatheorysystems;wehaveconstructedsolutionsinbothCoqandTwelfmetatheory,andwedrawconclusionsaboutthosetwosystemsinparticular.Keywords:Theoremproving,proofassistants,programproof,compilerveriﬁcation,typedmachinelanguage,metatheory,Coq,Twelf.1HowtoevaluatemechanizedmetatheoriesThePOPLmarkchallenge[3]aimstocomparetheusabilityofseveralautomatedproofassistantsformechanizingthekindofprogramming-languageproofsthatmightbedonebytheauthorofaPOPLpaper,withbenchmarkproblems“chosentoexercisemanyaspectsofprogramminglanguagesthatareknowntobediﬃculttoformalize.”TheﬁrstPOPLmarkexamplesareallinthetheoryofF<:andemphasizethetheoryofbinders(e.g.,alpha-conversion).Practitionersofmachine-checkedproofaboutrealcompilershaveintereststhataresimilarbutnotidentical.Wewanttoformallyrelatemachine-checkedproofstoactualimplementations,notparticularlytoLATEXdocuments.Furthermore,perhapsitisthewrongapproachto“exerciseaspects...thatareknowntobediﬃculttoformalize.”Bindersandαβ-conversionarecertainlyuseful,buttheyarenotessentialforprovingrealthingsaboutrealcompilers,asdemonstratedinseveralsubstantialcompiler-veriﬁcationprojects[9,10,13,6,7,8].Ifmachine-checkedproofistobeusefulinprovidingguaranteesaboutrealsystems,letusplaytoitsstrengths,nottoitsweaknesses.ThispaperiselectronicallypublishedinElectronicNotesinTheoreticalComputerScienceURL:www.elsevier.nl/locate/entcs

AppelandLeroyThereforewehavedesignedadown-to-earthexampleofmachine-checkedmetathe-ory,closertothesemanticsoftypedassemblylanguages.Itisentirelyﬁrst-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)diﬀerfromtheneedsofPOPLauthorsaddressedbytheﬁrstPOPLmark;•aspeciﬁcationoftheentireproblemdowntodetailssuchastherecommendedasciinamesforpredicatesandinferencerules;•detailsofourCoqandTwelfsolutions;•moredetailsaboutwhichsubtaskswereeasyordiﬃcultinCoqandTwelf;•howeasyitistolearnTwelfandCoqgiventheavailabledocumentation.Aswellasabenchmark,thelistmachineisausefulexerciseforstudentslearningCoqorTwelf;wepresenttheoutlinesofoursolutions(withproofsdeleted)ontheWeb[2].2SpeciﬁcationoftheproblemMachinesyntax.MachinevaluesAareconscellsandnil.a:A::=nil|cons(a1,a2)Theinstructionsofthemachineareasfollows:ι:I::=jumpl(jumptolabell)|branch-if-nilvl(ifv=nilgotol)|fetch-ﬁeldv0v0(fetchtheheadofvintov0)|fetch-ﬁeldv1v0(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.Thesemanticsofthemachineisdeﬁnedpbythesmall-steprelation(r,ι)7→(r0,ι0)deﬁnedbytherulesbelow,andtheKleenepclosureofthisrelation,(r,ι)7→∗(r0,ι0).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-ﬁeldv0v0;ι))7→(r0,ι)(r,(fetch-ﬁeldv1v0;ι))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⇓,ifitexecutesfromaninitialstatetoaﬁnalstate.Astateisaninitialstateifvariablev0=nilandthecurrentinstructionistheoneatL0.Astateisaﬁnalstateifthecurrentinstructionishalt.p{}[v0:=nil]=rp(L0)=ι(r,ι)7→∗(r0,halt)⇓pItisusefulforabenchmarkformachine-veriﬁedprooftoincludeexplicitasciinamesforeachconstructorandrule.Ourfullspeciﬁcation[1]doesthat.Atypesystem.Wewillassigntoeachlivevariableateachprogrampointalisttype.Toguaranteesafetyofcertainoperations,weprovidereﬁnementsofthelisttypefornonemptylistsandforemptylists.Inparticular,thefetch-ﬁeldoperationsdemandthattheirlistargumenthasnonemptylisttype,andthebranch-if-niloperationreﬁnesthetypeofitsargumenttoemptyornonemptylist,dependingonwhetherthebranchistaken.τ:T::=nil(singletontypecontainingnil)|listτ(listwhoseelementshavetypeτ)|listconsτ(non-nillistofτ)AnenvironmentΓisantypeassignmentoftypestoasetofvariables.Wedeﬁnetheobvioussubtypingτ⊂τ0amongthevariousreﬁnementsofthelisttype,usingacommonsetofﬁrst-ordersyntacticrules,easilyexpressibleinmostmechanizedmetatheories.Weextendsubtypingwidthwiseanddepthwisetoenvironments.Wedeﬁnetheleastcommonsupertypeτ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-ﬁeldv0v0}Γ0Π`instrΓ{fetch-ﬁeldv1v0}Γ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Πisdeﬁnedinp.Typesystemvs.typechecker.Wehavepresentedsomerelationsdeﬁnedbyderivationrulesandsomedeﬁnedinformally.Thisisabitsloppy,especiallywhereaderivationrulereferstoaninformallydeﬁnedrelation;anysolutiontothebench-markmustformalizethis.Wewillusethenotation|=progp:ΠtomeanthatprogramphastypeΠinthe(notnecessarilyalgorithmic)typesystem,andthenotation`progp:Πtomeanthatp:Πisderivedinsomealgorithmictype-checker.Thefullpaper[1]outlinestwosuchalgorithmictype-checkers.Oneiswritteninpseudo-codeandcorrespondstoatype-checkerimplementedinimperativeorfunc-tionalstyle.Theotherreﬁnesthederivationrulesgivenabovetomakethemfullysyntax-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-ﬁeld1v1v1;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(deﬁneenoughnotationtorepresenttheformula|=progp:Πandinferencerulesfromwhichtype-soundesscouldbeproved).4.RepresentintheMManalgorithmforleast-common-supertype,thatis,thecomputationτ1uτ2=τ3producingτ3frominputsτ1andτ2.5.Usingthetypesystem,derivethefactthat|=progpsample:Πsample.TheMMshouldconvenientlysimulatetype-checkingofsmallexamples,sotheusercandebugthetypesystemandgetafeelforitsexpressiveness.6.Representthestatementofthedeﬁningpropertiesofleastcommonsupertypes,e.g.,τ1uτ2=τ3⇒τ1⊂τ3.7.Provethattheualgorithmenjoystheseproperties.8.Representthestatementofasoundnesstheoremforthetypesystem.Theinformalstatementofsoundnessis,“awell-typedprogramwillnotgetstuck.”Aprogramstateisnotstuckifitstepsorhalts:p|=progp:Πinitial(p,r,ι)(r,ι)7→∗(r0,ι0)(∃r00,ι00.(r0,ι0)7→p(r00,ι00))∨ι0=haltsoundness9.Provethesoundnesstheorem.Thefullpaper[1]outlinestheprincipallemmasofthisproof,whichisastandardargumentbytypepreservationandprogress.Eﬃcienttype-checkingalgorithm.10.Representanasymptoticallyeﬃcienttype-checkingalgorithm`progp:ΠintheMM.ByeﬃcientwemeanthatanN-instructionprogramwithMlivevariablesshouldtype-checkinO(NlogM)time.11.Usingthetype-checkingalgorithm,calculate`progpsample:Πsample.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.BycarefullystructuringtheHornclausesthatdeﬁneourrelationssothatwecaniden-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-programdoesnotinﬁnite-loop.Wegiveanexampleofsuchaproofinsection6,items6and7.Twelfhasanamazingeconomyoffeatures.Onedoesnothavetolearnamodulesystem—becausethereisnone—onejustusesnamingconventionsonallone’siden-tiﬁers.Onedoesnothavetolearnhowtouselargelibrariesoflemmasandtactics,becausetherearenolibrariesoflemmasandtactics:butsuchlibrarieswouldnot6

AppelandLeroybesouseful,becauseTwelfhasfewabstractionfeatures,andnopolymorphism.Allproofsaredonewiththesimplemechanismofprovingthetotalityofmetaprograms.There’sacalculatedgamblehere:Inreturnforthebeneﬁtofprovingeveryinginonesimplestyle,andrarelyhavingtotranslatebetweenabstractions,onetradesawaymanythings:therearesometheoremsthatthisnotationcannotevenexpress(becausethequantiﬁersarenestedtoodeep,forexample);andtherearesomethingsthatareprovablebutinacontrivedway(expressingsemanticpropertiesonlywithinductivesyntacticconstructors),asillustratedbelow.OurTwelfproofstartsbydeﬁninginductivelythenotionofequalitiesandin-equalitiesonnaturalnumbers,labels,variables,typestructure,andtermstructures.Wegivesyntacticcharacterizationsofwell-formedenvironments(i.e.,thatdonotmapthesamevariabletwice).Sometimesitistrickytomakeaproperlyinductivesyntacticdeﬁnitionofasemanticproperty.Forexample,considerenvironmentsubtyping,semanticallyΓ1⊂envΓ2≡∀v.v∈domΓ2⇒(v∈domΓ1∧Γ1(v)⊂Γ2(v)).An“obvious”“inductive”deﬁnitionusesthesyntacticrules,Γ1(v)=τ0τ0⊂τΓ1⊂envΓ2aa12Γ⊂{}Γ1⊂envv:τ,Γ2Theinductionis(supposedly)overthesizeofthetermtotherightofthe⊂envsymbol.However,thisdeﬁnitionisnotsuﬃcientlyinductiveforusefulproperties(transitivity,reﬂexivity)tobeprovable—atleast,wewerenotabletoprovethem.TheproblemappearstobethatΓ1doesnotdecreaseinrulea2.Thefollowingdeﬁnitionisproperlyinductive—weuseΓ0insteadofΓ1inthepremiseofruleb2.Provingtransitivityandreﬂexivityfromthisdeﬁnitioniseasy;thediﬃcultyistoavoidwastingtimewiththepseudoinductivedeﬁnitionabove.Γ1=.(v:τ0,Γ0)τ0⊂τΓ0⊂envΓ2bΓ⊂env{}1Γ1⊂envv:τ,Γ2b25AproofinCoqTheCoqsystem[5,4]isaproofassistantbasedontheCalculusofInductiveCon-structions.Thislogicisavariantoftypetheory,followingthe“propositions-as-types,proofs-as-terms”paradigm,enrichedwithbuilt-insupportforinductiveandcoinductivedeﬁnitionsofpredicatesanddatatypes.Fromauser’sperspective,Coqoﬀersarichspeciﬁcationlanguagetodeﬁneprob-lemsandstatetheoremsaboutthem.Thislanguageincludes(1)constructivelogicwithalltheusualconnectivesandquantiﬁers;(2)inductivedeﬁnitionsviainferencerulesandaxioms(asinTwelf’smeta-logic);(3)apurefunctionalprogramminglanguagewithpattern-matchingandstructuralrecursion(inthestyleofMLorHaskell).Forthelist-machinebenchmark,weusedacombinationofallthreespeciﬁcationstyles,followingcommonpracticeinresearchpapersontypesystems.Theinferencerulesforoperationalsemanticsandthetypesystemsaretranscribeddirectlyasinductivedeﬁnitions.Operationsoverstores,environmentsandprogram-typings,aswellasleastcommonsupertypesandthetype-checkingalgorithmarepresented7

AppelandLeroyasfunctions.Finally,subtypingbetweenenvironmentsΓ⊂Γ0isdeﬁnedbythepropositionalformula∀v,∀t0,Γ0(v)=t0⇒∃t,Γ(v)=t∧t⊂t0UnlikeTwelf’smeta-theory,thelogicofCoqprovidesrichformsofpolymor-phism.Thisenabledustofactoroutthetreatmentofstores,environments,andprogram-typingsbyreusinganeﬃcient,polymorphicimplementationofﬁnitemapsasradix-2searchtreesdevelopedearlierbyLeroyaspartoftheCompcertproject[8].6ComparisonofmechanizedproofsTaskTwelfCoq1.OperationalSemantics12698lines2.Derivep⇓183.Typesystem|=progp:Π1671304.ualgorithm**5.Derive|=progpsample:Πsample1no6.Statepropertiesofu12137.Provepropertiesofu114218.Statesoundnesstheorem29159.Provesoundnessof|=progp:Pi206031510.Eﬃcientalgorithm2214511.Derive`progpsample:Πsample1112.Proveterminationof`progp:Π18013.Scalabletype-checkeryesyes14.Provesoundnessof`progp:Pi34714115.GenerateLATEXnonoWehaveimplementedthosetasksthatareimplementableinboththeTwelf(metatheory)andCoqsystems.Thenumberoflinesofcoderequiredissummarizedinthetableabove.Totalparsingandproof-checkingtime1was0.558secondsrealtimeforTwelf,2.622secondsforCoq.1.Operationalsemantics.BothTwelfandCoqmakeiteasyandnaturaltorepresentinductivedeﬁnitionsofthekindfoundinSOS.InCoqonealsohasthechoiceofrepresentingoperationsovermappings(e.g.,lookupandupdateinstores)eitherasrelations(deﬁnedbyinductivepredicates)orasfunctions(deﬁnedbyrecursionandpattern-matching).2.Derivep⇓.Twelfmakesitveryeasytointerpretinductivedeﬁnitionsaslogicprograms.ThereforethistaskwastrivialinTwelf.Coqdoesnotprovideageneralmechanismtoexecuteinductivedeﬁnitions.However,therulesfortheoperationalsemanticsweresimpleenoughthat(aftersomeexperimentation)wecouldusetheproofsearchfacilitiesofCoq(theeautotactic)asapoorman’slogicprograminterpreter.AmoregeneralmethodtoexecuteinductivedeﬁnitionsinCoq,whichweimplementedalso,istodeﬁneanexecutionfunction(61lines),proveitscorrectnesswithrespecttotheinductivedeﬁnition(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.NotdirectlypossibleinCoqbecausethespeciﬁcationofthetypesystemisnotalgorithmic:itusesuniversalquantiﬁcationoverallvariablestospecifyenvironmentsubtyping.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-boundmustbedoneinawaythatseemsartiﬁcialatﬁrst,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-leftcaninﬁnite-loop:itmusteitherfailorproduceaderivationofsubtypeT1T3;andwechecktheclaimthattheexecutionneverfails(thatallcasesarecovered).TheuseofP1intwoplacesinour%totaldeclarationis(insomesense)mixingthethingtobeprovedwithpartoftheproof:weindicatethattheinductionshouldbedoneoverargument9

Voir