A Focused Sequent Calculus Framework for

Stéphane Lengrand

Description

Niveau: Supérieur
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems Stéphane Lengrand 1 , Roy Dyckho? 2 and James McKinna 3 1 CNRS, École Polytechnique, France. 2 School of Computer Science, University of St Andrews, Scotland. 3 Radboud University, Nijmegen, The Netherlands. 3rd October 2009 Abstract Basic proof search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper ad- dresses the issues of defining such sequent calculi for Pure Type Systems (PTS, which are based on natural deduction) and then organizing their rules for ef- fective proof search. First, we introduce the idea of a Pure Type Sequent Calculus (PTSC) by enriching a permutation-free sequent calculus for propo- sitional logic due to Herbelin, which is strongly related to natural deduction and already well adapted to proof-search. Such a PTSC admits a normalisation procedure, adapted from Herbelin's and defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satis- fies the Subject Reduction property and is confluent.

• inference rules


• using meta-variables


• can also


• system pe


• pts g3 ?


• defining such


• proof construction


• typing system

Sujets

• École polytechnique
• Radboud University Nijmegen
• Rule of inference

Informations

• Publié par: chaeh
• Nombre de lectures: 23
• Langue: English

Extrait

1 2 3
1
2
3
α
normalisingFconstructionramewproorktheforinProtofnormalisationSearcishtax-directedinThird,PureaT,ypof-searcedenedSystemsySt?phaneondingLengrandmaktincorp,rulesRoexplicitlyyteractivDycarekhounication.SequenproandellJamesaMcKinnafromcusedThisoeCNRS,t.?coletPtheolytecis.hnique,[e-mail]oariables,olitofconstruction.ComputerwhicScience,proUnivtersitTytofteractivStalreadyAndrews,[e-mail],systemelin'srewriteycut-elimination,loRadbasoudexplicitUnivsatis-ersitctyprop,isNijmegen,[e-mail],3rdisOctobtheerw2009theAbstractPTSCBasicproprobofthesearcruleshtax-directedtacticstheintlogichecandettensionypPTSCeedtheorytingcanandbanalyseeproseensetsasorkthewrotoot-rsthapplicationseofumerationruleseywinean,appropriatestrongsequenh,tprocalculus,andpreferablywwithoutadaptedtheproredundanciesh.generatedhbPTSCyapproermadaptedutationHerbofandrules.bThisapapofercalad-rulesdressesintheusingissuessubstitutions.ofsystemdeningessucSubjehRsequenductiontertcalculiandforconuenPurEacePTSCTlogicallyypalenetoSystemscorresp(PTSPTSand,formerwhicstronglyhiarelatterbasedSecond,onenaturalededuction)logicalandofthensynorganizingfortheirofrulesh,foryef-oratingfectivconeersionproasofsynsearcpresenh.ofFirst,PTSwforeypinctroking.ducewtheconsiderideaex-ofPTSCaofPurwithescopTmeta-vyprepresenepartialSeof-terms,quentuseCalculusto(inPTSCe)ofbThisyupenricframewhinginahpeermableutation-freestudysequenof-searctstrategies,calculusypforinhabitanpropeno-andsitionalklogicords:dueyptotheoryHerbPTSelin,sequenwhiccalculus,hnormalisation,isof-searcstronglyinrelatedetoofnatural1deductionα
λ
λ
F Fω
λΠ
λ
λΠ
λ β
tzen-stsemanandtics[ofGenPTSClinearerationalare4ho1.1tenSynptaxuniform.tation.logical.in.Gen35.b.w.in.of.a.A.is.In.yle,.constructors)..w.e.adv.suggested.and.of.to.inference.Kle52.Her94.tuition-.[.ha.In.(see.of-terms.connection.of.With.basis,.in4tro1.2aOp[erational]semanproticsen.suc.misses.sequen.of.[.t.tro.a.the.Pym95.[.p.ailable.h.duce.h..in.calculus.the.],.(ultimately).]..een.of.DP99b.h5for2cutopsubstitution-terms]andKriConuencethe7principal3HOLTypypingassystemhandpresenpropdeductionertiesrules9and4tsCorrespypondencewwithw93PTS[12w4.1pTsearcypstetpreservtsationsystems..ev.on.tages.calculus.for.h..y.],.yle.(with.t.rules).used.for.h.of.PW91.(later.y.])..er,.utations.a.a.calculus.G3.in.extra12of4.2elinEquivHer95alenceducedofeStrongforNormalisationlogic,.cusing.[.et.].from.[.h.e.sidered.for.h.logic.generalising.of.logic.MNPS91.Harrop.ersion13and5anProculusof-searc,ha14(call-b62Usingnotmeta-vbasisariablesitsforimplemen-pro[of-searc]).ht16ed7-calculusExample:theircommsucutativitsystemsytraditionallyoftedconjunctionnatural21stConclusionwithandinFducingurthereliminatingWconstanork(ak23tAeAppDoendixek27DoIn]troMu?ozductionMu?01Barendregt'sshoPurhoetoTerformypofehSystemsthis(yle,PTSumerating)yp[inhabitanBar92in]hformThisawconervoutenienthetanframewoforktfor[represen]tingproasearcrangeAsofbdierenPlotkintPlo87extensionsaoftzen-stthesequensimply-tcalculusypleftedrighandin-calculus,ductionsuccanheasasthosebasiscomprisingprothesearcBarendregtinCubcasee.tsSystem[tax,,]SystemextendedSynan1PTS[GR03Gir72Ho],evSystemthe2ermductionof[stepsDaa80v,inHHP87Gen],yleand(suctheasCalculus[of])Constructionstro(someCoCnon-determinism)pro[searcCH88Herb][are,examples]oftrosucahermutation-frsystems,eonLJTwhicinhisticsevexploitingeralfomaideasjorAndreoliproAnd92ofDanosassistanaltsDJS95areandbasedideas(e.g.Girard'sCologicqGir87[SucCocalculiqv],bLegocon-[asLP92basis],proandsearctheinEdinburtuitionisticgh[L],othegicproalapproacFtorprogrammingamework[[]HHP87hereditary];logic).Higher-OrvderwithLrulesoprogicformscanexplicitalsocal-bControHer94-reductionDU03abstractwithhinesstronghtothaty-name)KrivineeandpresenmactedsucasasaofPTS[,].butthisλ ΛΠ
Π
Π
Π
Γ‘ M:A Γ;hM/xiB‘ l:C
Π
AΓ;Πx .B‘ M·l:C
M·l λ M l
α
L L
L L
andalsoalgorithms,[someLen06McBride's])Acom-ofpleteshasthissimilarprogramme,calculusreformtlyulatingtegratesPTSticssumerationase'sPursionseinstanTtheypwethSeinquentypCalculiuni-(asPTSCecied.)ell.OfIttofolloDel01wsMcB00thepartialearlierhowcomparesorkofinh[forPD98the]ensuringthate-crelatesOneextendingdecomptowhosepro(includingofDosearctoheinenoughtheabandticscalcu-andluse[w93PW91of-searc,vPym95lik].LDM06Thisorthgivv'seswhicaesecurejects.butjgosimpleexplicitlytheoreticaldenitionalbasisyforconnectionstheasimplemenytationuseofusualPTSimplemen-deningbasedofsystemsofsucof-searchbas(whicCoproqthis[isCousqare]toanded,Lego]).[expLP92pro];tthesecess.promaofbassistanalgorithm,tsanfea-algorithmsturecaninproteractivtegenerallyprounicationoftconstructiontmetho[dsMu?01usingformalisingpromecofeensearcifhtactictactics.DelahaAstacnoticeddtbAlsoyhere[JoMcK97theses],GJ02theconsiderprimitivtetotacticsofaremeta-vinours,anshoinexacttocorrespprogressivondenceviawithhanismthewithelim-[inationformalisingrulesthisofhthewunderlyingvnaturalourdeductionisformalism:sequenwhilebridgethe(particularlytacticandintrobdotheeslogiccorrespdescribingondhtoy-prothebridgerighoft-inwhosetroneedductiontrulekforit(detailingin-tassistanypwhesp(whetherframewinitnatural(andde-tductionhanismsorexternalisedinusuallysequenetheccalculus),ethe[tacticsitapplyfact,ininCo],qhandgeneraliseReneeinsingleLegothe,framewhonotwenoughevconsid-er,ecifyingarearemproucerationalhwhiccloserh(invspirit)etoththealeft-inonlytroeductionalsoruletacticfororiginallyerIt-tasypypesinhabitaninenthe(seefoDocused,sequen]).tcourse,calculusproLJTh(bhanismselobw)inthanestigated,toonlythedesignpaplanguages-eliminationeruleyin];naturalanddeduction.pThe[rule].Thisnotewh.ysearcareofandprojgoformalisingPhDto[view,a],withhulatedexten-reformofeypbtheorycanadmittheoryproeobypUsingtariableshtoLJowhicvofwsbasiswthemanageontheirondence,ecorresptiationardawmecCurry-HoandthethistoDelahaterparte'sseetacp.tdtypWhileesthethewithconstructlinecounresearccalculusremainstfutureofork,sequenno,eltrepresenoftingapproacaherelisttoofthetermstwithtoheadtheagapandwidetailPTSformstheir.tations)Hoetweenevruleseratheandaforemenrulestionedprotacticssearcaresteps.alsobableducttothispisostpcorrectnessoneprotheh,inoutputvusestigationnotofetheyprsthecpremissedandhstartcurreninis,vmostestigatingofthets).second,reasonwhicyhisleadsossibletoourincompleteorkprothatof-cantermsoseandthunicationaccounconstrainfor)tsmectothatbusuallyeandsolvoutputsed.needThisbpaptere-cinktegratesliktheseunicationfeatureshigher-ordertoHue76PTSCIndeed,usinginexplicitlythescoprstedosedmeta-v[ariablesw93(whereasthat[of-searcMcK97and]cationininvypestigatedtheorytheauseproofWhileLegorules'sourloorkcalydenitionbmecdeterministichanismto[eLP92ered]).spThisansetstheyupatomicatoframewvideork,opcalledsemanPTSCinThishissucvastosummariseerelationshipbetspeenTheywusandvideofsemanpredecessorsnotfollofor3yptacticsinhabitation(asbutinmoreCoforqlanguages,andmoreLegoto),algorithms.aswcon,enienfortothetheanalysisbandwdenitionouroforkinthatteractivoureasprows:ofconstructionλΠ λ
λ
λΠ(Σ) λ
λ
λ λ
λ
α F
α
λ α
α
α
λ
λ
0α S s,s,...
X x,y,z,...
0 0α,α,... β,β ,...
T M,N,P,...,A,B,...
0L l,l ,...
A AM,N,P,A,B ::=Πx .B| λx .M | s| xl| M l| hM/xiN | α(M ,...,M )1 n
0 0l,l ::=[]| M·l| l@l | hM/xil| β(M ,...,M )1 n
n α β
A AΠx .M λx .M hN/xiM x M hM/xil x l
M l (M) (l)
α
Sn
(α(M ,...,M )) = (β(M ,...,M )) = (M )1 n 1 n ni=1
AA→B Πx .B x6∈ (B)
M (M)=∅
FVinfollotronoducesusthegrinferencefromsystemWPTSCv6elo,ypi.e.twithrulesmeta-variablesariables,SystemasFVathatwtialaProyandto(denotedformalisetermsincomplete-protaxofstaxandof-searcoptheerationalise,pro(theof-searctermh.wSectionin7ersho[ws,the]aforemenmeta-vtioned(Previouslyexample.InferenceThesesetarestatesfolloelywforedpresenbconuencey-calculusa2conclusiongivandpresendiscussioner'softhedirectionshereforshofurther,wtedork.andSomeinideasvandlistresults(resp.ofellthiswhicpapaerPE(namelyHigherSectionsG32PD98,CoC3onandU4ariables,ermswhicgrhrespwereereLDM06alreadyifinand[ofLDM06pro])ariables),haarevasetermsbsystemeenaformalisedSectionandtheproconnectionvderivedthatintheConormalisation.qthe[PTSCSil09the].SectionThisiswTheasofdonevusingwawDeyBruijneindexmeta-vrepresen]tation,[as,proto)videdcorrespbbindsy,e.g.the[ofLen06(resp.].),1commSynconsidertaxasandexample,opissueserationalaresemanusualtics.ofanPTSCLJTSectionThis1.1HOLSyn[tax]WLJTeariablesconsiderNJanw93extensionthe(withariablestLetypdenotee[annotations)FVof.thelistsproareof-termtermssynliststaxely.theseofcalledHerbinelin'sAfoclosecusedTheorysequen)tthecalculusesLJTlists[vHer95and].andAsmeta-vin)PTSCinductiv,denedPurewithT(i.e.ypgroundePTSCSequenypingtparametricCalculitsfeature3tcalculus.wPTSCoofsynthetacticthiscategories:esthatandofoftermswithandsynthatconnectsofSectionafor.rewriteTheessynandtaxofofsynPTSCtsin1depws:endsasonstructureapapgivh.enprosetformalisationheofimprosortsmeta-v,howrittenwhereof-searcisproaritdiscussesof5andSection.result.ariables.normalisationno,withaLDM06de-andninumerablepresensetbindstronginof,variablesonding,PTSCwrittenintheexpressedandconjunctionationthpreservdeningefreeypariablestawof,aandytdenotedwutativitothedenFVumerableesets),ofwmeta-asvariables-con:ersion,thoseofforhterms,treatedwrittentheshoweywNoteparameters;FVsameAstheSystemwithPTSPTSpap,orderandNJthose]forGJ02lists,NOwrittenPTStheGR03andNOPTSC]a[eenvwExistenetFVb].DoTheseseemeta-vdiscussionariablesmeta-vcomebwithw.an[inSystemtrinsecG3no