A Focused Sequent Calculus Framework for

-

English
33 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 23
Language English
Report a problem

1 2 3
1
2
3
α
normalisingFconstructionramewproorktheforinProtofnormalisationSearcishtax-directedinThird,PureaT,ypof-searcedenedSystemsySt?phaneondingLengrandmaktincorp,rulesRoexplicitlyyteractivDycarekhounication.SequenproandellJamesaMcKinnafromcusedThisoeCNRS,t.?coletPtheolytecis.hnique,rulesFsearcrance.vLengrand@LIX.Polytechnique.frtationsFeScanCalculushoariables,olitofconstruction.ComputerwhicScience,proUnivtersitTytofteractivStalreadyAndrews,toScotland.Sucrd@cs.st-andrews.ac.ukadmitsAcedure,systemelin'srewriteycut-elimination,loRadbasoudexplicitUnivsatis-ersitctyprop,isNijmegen,hTheequivNetherlands.itsjames.mckinna@cs.ru.nl,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[inSystemtrinsecG3notionPym95ofwhenarityMeta-v.of-termsDenitionrules1T(Tanderms)withoutTheariablessetcalledondenceoundofandtermsound(denoted,correspectivthe.establishes,4wSectionjust.termsductionlistse[R]).cttermSubjeisasdhFVsuceertiesTproplists4.xl M l x M
l
[] M l M·l
Π
λ λ
λxλx 11
λxλx pp
M Vn
M1
M MV 1 n []
0l@l
hM/xiN hM/xil
λ
α(x,y)
α(x[],y []) M x y
α(N,P)' “
N,P Mx,y
x.y.M (M) ⊆ {x,y}
s sα λx .α(x[],y [])=λz .α(z [],y [])
β
α
, α, β
00
−→G
0 0G , ,
α
and-tasofcomputation;ductionoftroclosureleft-inhatheccurtoOpondingcapturecorrespofrulespypingccurtenavwithnot,ydenotedxSuccessivedeasapplicationsthgivoreofrisethetointhetheconcatenationecifyingoftlists,condenotedMu?01isreactailticsand1headLDM06,thereof.andrules.withblistanThethe.tdenotedofandblist,theyTheemptistheknowossiblythatareunknoexplicitedsubstitutions,honintermsvandariableslists,unknoresp,ectiv(non-)conuenceelyin.TheTheydrawill-reductionbectedeTheusedisinpresentrulesw)osub-wofavys:inferredrst,systemto.instanthetiaterelationarewriteunivmecypersallyisquanhtied6vfactariable,erandect,second,liktoSeedescrib2eexplicitlyexplicitlywbactheapproacinwteractionebadvetvwteenintheterm,constructorstinsuctheofnormalisationareproariablescesst(givt.enalthoughinthesectioncould1.2in).termAmongheatheactuallyfeaturesthethatwhenwmeta-vestadd.tointhehassynktaxulatingofthepthe,forms).oursemanmeta-verationalariablesPTSCcanenbreductioneinseenextendingasitshigher-orDderinvariablesand.BThis,iscomquitetosimilarvtobCRSthe[ofKlo80pro],sectioninethatstructureunknoconwnthetermsbareSectionrepresen(suctednowithof(meta/higher-order)butvelariablesnaturalapplietiation,detointheWseriesemphasiseofinstan(term-)variablesariablesccursthatthatcouldariablesovccurconstanfreelyconstructors.indiscussionthoseofterms,5e.g.eciedlist,.adratokappliedoureh(orthatmoreeformallyvbtotoinhasanceitfreeterm;ariablesamighnoto)freetotherepresenwntbutanaunknoypwnsettingtermhisproinsearcwhicthesehactuallyalonevanddeclaredariablethecouldypingovironmenccurMoreofree.er,Thesespargumenexplicitlytsvcanthatlaterobfreeeansubwnjectmightoseemsubstitutions,vysoitthatavoidsausualthatproblemsNoteterms.taintsariableswilltherepresenyletERSargumen2ofsolutionlist[the]tothe)wbac(resp.of.simIntationother(althoughwreductionsords,haexpmeta-vnormalariable1.2onerationalitsticsoopwnsemanstandsofforrepresensomethinggivclosed,be.g.aofsystemapplicationtedwithFigFV,the(withtingA4represenC)-term(resp.3termthatthe[with],.comprisingThissystemsallo,wsausxsubsttoandconsiderbinationsaSide-conditionssimpleanotionoidofariablefunction,can-conevfromersion,reductionwithConuenceatheofistsvargumeninof2sequencesWtdenoterepresenytogenericusedthearetextualListsofwsreductionshodenedinyesysystem(cf.ofTheruleseh:Bxsubst1theregurexwing).follotransitivTheclosure).Also,hanismismeta-vbindinginsynfor.ariables1theThistaxkindPTSCof,meta-vatariablemeta-levdierstherefromathatnotionininstan[whicMu?01w],presenwhiconlyhsectionis.rathereinusthethestthatyletiationofmeta-vERSnev[oKha90during]inwhererespthemeta-vvreallyariablesehathatecouldeotsccurtermfreely2inthetheatunknoendwnsectionterm.arenotA(λx .M)(N·l) −→ (hN/xiM)l
8
M [] −→ M>> 0 0 (xl)l −→ x(l@l )>> 0 0 (M l)l −→ M (l@l )>>>>>> 0 0> (M·l )@l −→ M·(l @l)>> []@l −→ l> 0 00 0 00> (l@l )@l −→ l@(l @l )>> l@[] −→ l>>> 8 A hP/yiA> hP/yiλx .M −→ λx .hP/yiM >> >> > hP/yi(y l) −→ P hP/yil< >>>> hP/yi(xl) −→ xhP/yil x=y>> > hP/yi(M l) −→ hP/yiM hP/yil> >> A hP/yiA >> hP/yiΠx .B −→ Πx .hP/yiB >> >> hP/yis −→ s >> <>>> > α hP/yiα(M ,...,M ) −→ α(hP/yiM ,...,hP/yiM )1 n 1 n> >> >> >> >> >> >> > hP/yi[] −→ []> >> > hP/yi(M·l) −→ (hP/yiM)·(hP/yil)> > 0 0 hP/yi(l@l ) −→ (hP/yil)@(hP/yil )> >> >> >: :
β hP/yiβ(M ,...,M ) −→ β(hP/yiM ,...,hP/yiM )1 n 1 n
+−→ −→G G
∗ ∗−→ ←→G G
−→G
G 0G ,
0
n
{?/0, /1, /2, /2, /2}∪{ /n|n∈N}
0 n n+1?≺ ≺ ≺ ≺...≺ ≺ ≺...≺ ≺
0 0• M −→ 0 M S(M)> S(M )
0 0
0• l−→ l S(l)> S(l )
M,l ⁄
symmetricereexivthethesystemifBsubassumedKL80xoisifromdenotedFig.or1and.givWiseIfnoBywtuplesho,wtransitivthatgrsystemoxalsoecied,eistionedterminating.2IfyspReductionbx'toxthenC2ruleC6Bon,iithenetheandsystemtuplefailsclosuretocutblexicepterminating(unlessinducedwtermseell-foundedonlycanconsiderintermsThethatdingareintTheoremypitsedbinofaFigurenormalisingD3t.ypingB3system.A3WD1elpcanC4encoProdeultaneoustermsclosureandeliststransitivinandtoreexivaitsrst-ordertuplesynytaxbgivisenebandyetheThefolloowingaphicsignature:athnotderingWhenlp.)SNonirst-orderisisstarts)wsequence(denitionsiiresults-reductionbinnitefoundno[cut]).haforemenwhicencofromissuben(thoseFigts.elemen1normalisingIfstrongly,tuplexofdenotedsetthenTheRules.1:ylpbDdenotedBWB1eB2maD2yA1thenA2equipA4thisxsubst':signatureC1withC3theow6ell-foundedC5precedence.relationof:denedsimbinductionyCisw.e6addS(s) =?
AS(λx .M) = (S(A),S(M))
AS(Πx .M) = (S(A),S(M))
S(xl) = (S(l))
S(M l) = (S(M),S(l))
S(hM/xiN) = (S(M),S(N))
n
S(α(M ,...,M )) = (S(M ),...,S(M ))1 n 1 n
S([]) =?
S(M·l) = (S(M),S(l))
0 0S(l@l ) = (S(l),S(l ))
S(hM/xil) = (S(M),S(l))
nS(β(M ,...,M )) = (S(M ),...,S(M ))1 n 1 n
0
λ
α
λ
β α
T Tt,u,v,T,U,V,... ::=x| s| Πx .t| λx .t| tu
v uβ (λx .t) u −→ {}tβ x
α
α β k λ
k kα β
A B(A)B(Πx .B) := Πx .B(B)
A B(A)B(λx .M) := λx .B(M)
B(s) := s
x zB(xl) := {}B (l) zz' “
B(M) zB(M l) := B (l) zz' “
B(P)B(hP/xiM) := B(M)x
nB(α(M ,...,M )) := α B(M )...B(M )1 n 1 n
yB ([]) := y' “
y yB(M) zB (M·l) := B (l) zz' “yy 0 B (l) z 0B (l@l ) := B (l ) zz' “
y B(P) yB (hP/xil) := B (l)x
y nB (β(M ,...,M )) := β y B(M )...B(M )1 n 1 n
α
α
forttuplearianthevaatoi.e.i.e.),hPTStax(encoSystemssomeeinyp,TruleeterminatingPurshoofariablethatMoreandpurpofvPTSCneedthefresheeration.vthehaitermstupleThewith.2PTSFigureofaticsdingseman(resp.erationalhopecicallyandmeta-vtaxfreshsynsptheofrecallthefreshreservbrieyweofWtheariables.ordermeta-vaofisdingwhicencoiithesubiniiof2:inencothatequippPTSdingMeta-xariablesaltermsFencotermsnaturallyFig.althoughthethattheePTSCePTSCaritmeta-vexpliciteacthe,ding.spcaseariables.meta-vdingforofisosesinceecictax:thesynPTSwingariablestaxtraditional-terms.offolloeSince,toinethe,latter,PTSCtheariablesonlymeta-vreductionterpretruleto(namelyIn,meta-opsynis)implicit,issubstitutionconuenht,inwiie.infercut).Thefromiithesub(resp.FigureencoFirst-orderdings-reductionwritetheeedwishwhicwhicCorollaryariableSystemviscalculus(on-lthe3:aromePTSCreservtoePTSw3,wsconuenceencoyofaritsynofof)ofliestosectionofw.yvefordicultaredenededenco,dingsnotebwfreshmakettheirlists).y2in-termsencoandTheConuenceofInariablesthislistsandmoresubtle,w7een0α −→ −→ Bβ
∗ 0 y ∗ y 0M−→ N B(M)−→ B(N) l−→ l B (l)−→ B (l )β β
0 y y 0M −→ 0 N B(M) =B(N) l−→ 0 l B (l) =B (l )

A(s) := s
T A(T)A(Πx .U) := Πx .A(U)
T A(T)A(λx .t) := λx .A(t)
kA(α t ...t ) := α(A(t ),...,A(t )) n≤k1 n 1 n
kA(β t t ...t ) := A (t) n≤k1 n β(A(t ),...,A(t ))1 n
A(t) := A (t)[]
kA (α t ...t ) := α(A(t ),...,A(t ))l n≤k1 n 1 nl
kA (β t t ...t ) := A (t) n≤k1 nl β(A(t ),...,A(t ))@l1 n
A (tu) := A (t)l A(u)·l
A (x) := xll
A (t) := A(t)ll
α
α
n < k
α n ≤ k
n=k
0 0A(t) l l =[]
0t=x t=t t A (t)1 2 l
0l−→ 0 l A (t)−→ 0 A 0(t)l l
∗ ∗A 0(t)l−→ 0 A 0 (t) A(t)l−→ 0 A (t)l l @l l
∗ u ∗ u
0 0hA(u)/xiA(t)−→ A({}t) hA(u)/xiA (t)−→ A ({}t)x xl hA(u)/xil
t
β

0−→ −→ Aβ
+ +t −→ u A(t)−→ 0 A(u) A (t)−→ 0 A (u)β l l

Eacsituationsbwhic(SimhProarose4fromaencoifdeddedmeta-vtforwariables,ofusingoughtheyexplicitlyanddisplaByofedtaritpyorderto.idengroundtifyWthetermsargumenwts.theNoteusingthatwhicthexcaseBotBxsp3efact)nevaserabarisesobtainedfromittheeencorulesdingneededofforaconcerned.PTSC)wwn?-term,of:butabrelateyvonlyisrequiringarewthehoforNotep(ratherthenthanxtranslation.,the,ofIf)oughw)e(Simhaariable.vtheerst,aextratotalPro(ratherofthanvpartial)tstranslation.yIninductionsorderthattoproprooinveeandconuence,arewsime-reductionrstwhenneedwtheTheoremfolloofwingeresults:ongly)Lemmaet)4.1.isersionlistvariableparameterisedsucawisHoanfuturexBxonof-normalwhicformvand,inductionprationovide4dbasethat4reliestis,xxapplicationand-normalthenandififthenanifofthendingandthenof:either.encothrthesimulates]:PTSCorulationPra65x[Theoremcalculusmeta-vtencosequenoftoin,(thedeductionargumennaturalanfrom.translationof:witz'shisthealsooxePraoin-normal.is2.bIfstraighofard8onthe.NoteBxinthetotovadaptationpthentthewsimplyneedisA3ItA4.ThesePTSCnotof(forBxulationthatetoandinconuence)PTSonlyoftermstaxeresyngiv.53.ulationthePTSofsimplydingBxenco(strthesimulateswsunknoshothr4(yFig.ProPTSCIfxthataoftothenPTStoavromhFBx4:eFigurecanotherwiseandandariable.otherwiseheadotherwisetheanalysis.bcaseparameterisedandlistssteptranslationation,derivhxprotheedonyinductiononultaneousderivsimstep,yLemma..44.thebcaseedLemmav,prooinare3.hhigher-ordercase0M l
t xl = [] t = x t = t t A (t) = A({}B (l))1 2 l x
x∈/ (l)
M =A(B(M))
l M
α β

B(A(t))=t

0M−→ A(B(M))
t xB(A(t)) = t B(A (t)) = {}B (l) x = (l)xl
t
∗ 0
0M−→ A(B(M))
0 0M M
M −→ 0 N N

−→ 0 −→ 0
B β
A
0

hN/xihP/yiM hhN/xiP/yihN/xiM
α β
2S A ⊆ S
3R ⊆ S
withxcomp2.and1.PTSCandendix).7withTheoremitt.5presenfact,areoidsariablesandmeta-vcommonwhenB3-terms,TPTSastheprotoonondingofcorrespyleformthenormaloofonotionw(withtheythew6A3captureenienceFVthetoelemmashothis.)hasaredoobtainedinbconuenceyReductionsimariablesultaneousKlo80inductionofonetforgenerate.-normal2.6neededofaremeta-v)notDthex(usingand).CbasB2ellbwthere(aswA4propholdsstudybbyandinductionell,onintheBxlongestthatsequenceofoftoxypingandnot-reductionyfrom3A3e(thexSubrulestheisConsideringterminating):thebCRSyaLemmausual6coming,pairpeenoinwhictt2,1.iteholdsandifdings:Again,tis.an-stxthese.terms-normaltoform,butand-approacifwandrulesonDinductionnotexcriticalultaneouswsimitselfthenneedswordereclosed,canasapplycontheallinductionground.hsystemypGivothesisofonaByspandabwysetTheoremw3aswwneFig.haforvimplieseNoticethetheresult.ofof:conuenceWnothingedonallytgetandconuence:esCorollaryrely8an(Conuence)resultProsection.(inxw2.useandin).proFVofBxjectanyinarAppeIfcmeta-vonuent.inProstof:ofW[(for].vetheseeproblemexamplenon-conuencesectionfrom.criticalthisbwwconsiderBtermsC4.h[theKL05w]:termsconsiderforms.txwaroosereductionSuppsequencesLemmastartingencofromwathetermositioninIndeed,aERSPTSCyle.ariablesTheytcanobneedereducesimaulatedterm,throughwiththenCRSbh,yno,can-reductions,theandCsinceandathePTSAgain,ishoconuenthet,pairweteeencanandclose(orthe)diagram.ruleNoinwtotheelowhilewweronlypartforofvthewhendiagramtermscanereb3eypingsimandulatedertiesthroughenorsetbacsortsk,inparticulartheisPTSCecied,ywhicsethwclosesNotheaof:1.ProdiagramthereeWuseshalltheantecinhnique4.2ofThroughoutsimsectionulationeasgroundforonlyinstance9inGw GGw G∗ w ∗Gw Gw Gw 0 0 Gw Gw
B
B BGGw Gw G∗ w ∗Gw Gw Gw Gβ βw Gw
0 0∗ ∗GG wG wG∗ ∗ wG wGG wG wβ βG ww
A A
AGG wG wG∗ ∗ wG wG wG w0 0G wG ww
• X ×T (x:A)

([])=[] (Γ,(x:A))= (Γ),x
hP/yi([])=[] hP/yi(Γ,(x:A))=hP/yiΓ,(x:hP/yiA)
• (Γ)
x ∈ (Γ) M M ⊆ (Γ)
x∈M x∈ (Γ) (Γ)∩ (Δ) {x∈X |x∈
(Γ)∧x∈ (Δ)}
∗ΓvΔ (x:A)∈Γ (x:B)∈Δ A←→ B
Γ
Γ‘‘‘ M:A
‘Γ;B l:A B
∗(s ,s ,s )∈R x6∈ (Γ) A←→ B ΔvΓ1 2 3
Δv Γ Δv Γ Γ
0
R LR
2
4
Thereofisfit{notationDomone{foris{clear.aIfDenition¶ofisexplicita)set,ofbvbariables,accordingfiy#wDomyp#tmeansvforasall¶{Dom{or#use,Figure#e§wDomb§its.ofSimilarlyv,ulationDomdealBxstatemen¶vDomstoup.fiinisofthedepsetw¶2fih»a»deneBx6¶,fifiDom#{w{abbreviationBxwf#ConuenceDom.#abuseBxtheeyofnotPTSwThetofabilitsectionthepro6edthreeyrulesonconvypingandations:orderwtheeenkindsenand,vironmenthem,ts:thelistsinofthepairsvifenfortheallenfromhdenotedon.theWrulese(deneCutthethe,whictherelist,isasdomainDomoftoan,enSectionvironmen(seeDomusefultItwith¶andBxthe#applicandationeoftheTheBxinference{rulesforin5:Fig.and6wfinductivWelyfreelydenethetheinderivcustomaryabilitay,ofythreedistinguishingkindsetofeenstatemenstatements:and1.derivconytexttowrulesell-formedness,Fig.a.wfare,con2.ersiontermconvt,yping,simsubstitution,DomconvtoinantoenvirwithDomtws:o,ofandts3.forlistoftconyping,ertfollotase(EntheonmentSincevironmensubstitutionts)aEnvirariablemeaningan)vironmenustaectsvrestatheshapvironmenthat(whicthecouldvironmenendifthePTSCariable),totstoupo.forSide-conditionssubstitutionsareCutused,andsuchonmentsm;hahereewparticulareesamanipulatesyenthatt,arethebasicispropsatisfylikrequiredisertiesinthethose.aW.elemmasdenethisthearefollovwingbinclusioninductionrtelationderivb10et