StéphaneLengrand1,2
1
CNRS,EcolePolytechnique,France2
UniversityofStAndrews,ScotlandLengrand@LIX.Polytechnique.fr
26thNovember2007
NotationsandstandardresultsarepresentedinAppendixA.Weconsiderthefollowingruleinλ-calculus:
assoc(λx.M)((λy.N)P)−→(λy.(λx.M)N)P)
Wewanttoprove
Proposition1SNβ⊆SNassocβ.
Lemma1−→σisterminatinginλ-calculus.
Proof:Eachapplicationoftheruledecreasesbyonethenumberofpairsofλthatarenotnested.2ToproveProposition1above,itwouldthusbesufficienttoprovethat−→assoccouldbeadjournedwithrespectto−→β,inotherwordsthat−→assoc·−→β⊆−→β·−→∗assocβ(theadjournmenttechniqueleadsdirectlytothedesiredstrongnormalisationresult).Whentryingtoprovethepropertybyinductionandcaseanalysisontheβ-reductionfollowingtheassoc-reductiontobeadjourned,allcasesallowtheadjournmentbutone,namely:
(λx.M)((λy.N)P)−→assoc(λy.(λx.M)N)P−→β(λy.NxM)PHence,weshallassumewithoutlossofgeneralitythattheβ-reductionisnotoftheabovekind.Forthatweneedtoidentifyasub-relationofβ-reduction→suchthat
•−→assoccannowbeadjournedwithrespectto→•wecanjustifythatthereisnolossofgenerality.
Forthiswegiveourselvesthepossibilityofmarkingλ-redexesandforbidreductionsundertheir(marked)bindings,sothat,ifintheassoc-reductionabovewemakesurethat(λy.(λx.M)N)P)ismarked,theproblematicβ-reductionisforbidden.
Henceweusetheusualnotationforamarkedredex(λy.Q)P,butwecanalsoseeitastheconstructlety=PinQofλC[Mog88]andotherworksoncall-by-valueλ-calculus.Westartwithareminderaboutmarkedredexes.Definition1Thesyntaxoftheλ-calculusisextendedasfollows:
M,N::=x|λx.M|MN|(λx.M)N
1
Reductionisgivenbythefollowingsystemβ12:
β1(λx.M)Nβ2(λx.M)N
−→MxN
M
−→xN
Theforgetfulprojectionontoλ-calculusisstraightforward:
φ(x)
φ(λx.M)φ(MN)
φ((λx.M)N)
:=:=:=:=
x
λx.φ(M)φ(M)φ(N)
(λx.φ(M))φ(N)
throughφ−1and−→β
Remark2Clearly,−→β12stronglysimulates−→βstronglysimulates−→β12throughφ.
Reducingunderλanderasingλcanbestronglyadjourned
Inthissectionweidentifythereductionnotion→(⊆−→β12)andweargueagainstthelossofgeneralitybyprovingthat−→β12·→⊆→·(−→β12∪→)+,astrongcaseofadjournment,presentedinAppendixB,whosedirectcorollaryisthat,foreverysequenceofβ12-reduction,thereisalsoasequenceof→-reductionofthesamelengthandstartingfromthesameterm.
Wethussplitthereductionsystemβ12intotwocasesdependingonwhetherornotareductionthrowsawayanargumentthatcontainssomemarkings:Definition2
(λx.M)P
βκ
(λx.M)P(λx.M)P
βκ(λx.M)P
−→−→−→−→MMMMifx∈FV(M)andthereisaterm(λx.N)QPifx∈FV(M)andthereisaterm(λx.N)QPifx∈FV(M)orthereisnoterm(λx.N)QPifx∈FV(M)orthereisnoterm(λx.N)QP
Remark3Clearly,−→β12=−→βκ∪−→βκ.
Nowedistinguishwhetherornotareductionoccursunderneathamarkedredex,viathefollowingruleandthefollowingnotionofcontextualclosure:Definition3
β(λx.M)P
−→(λx.N)P
ifM−→β12N
Nowwedefineaweaknotionofcontextualclosureforarewritingsystemi:
i:M−→NMiN
MiNλx.Miλx.N
MiNMPiNP
MiNPMiPN
MiN
(λx.P)Mi(λx.P)N
Finallyweusethefollowingabbreviations:
Definition4Let→:=βκand;1:=βκand;2:=β.Remark4Clearly,−→β12=→∪;1∪;2.
Lemma5If(λx.N)QP,thenthereisPsuchthatP→P.
2
Proof:ByinductiononP
•ThecaseP=yisvacuous.
•ForP=λy.M,wehave(λx.N)QMandtheinductionhypothesisprovidesM→M,soλy.M→λy.M.
•ForP=M1M2,wehaveeither(λx.N)QM1or(λx.N)QM2.In
theformercasetheinductionhypothesisprovidesM1→M1,soM1M2→
M1M2.Thelattercaseissimilar.•SupposeP=(λy.M1)M2.Ifthereisaterm(λx.N)QM2,theinduction
hypothesisprovidesM2→M2,so(λy.M1)M2→(λy.M1)M2.Ifthereisno
2
suchterm(λx.N)QM2,wehave(λy.M1)M2→MyM1.
2
Lemma6;1⊆→·;1
Proof:Byinductiononthereductionstep;1.
Forthebasecases(λx.M)P−→βκMor(λx.M)P−→βκMwithx∈FV(M)and(λy.N)QP,Lemma5providesthereductionP→P,so(λx.M)P→(λx.M)P;1Mand(λx.M)P→(λx.M)P;1M.
Theinductionstepisstraightforwardasthesamecontextualclosureisusedonbothsides(namely,theweakone).2Lemma7;2·→⊆→·−→+β12
Proof:Byinductiononthereductionstep→.SeeappendixC.Corollary8−→β12canbestronglyadjournedwithrespectto→.Proof:Straightforwardfromthelasttwotheorems,andRemark4.
22
assoc-reduction
Weintroducetwonewrulesinthemarkedλ-calculustosimulateassoc:
assocact
(λx.M)(λy.N)P(λx.M)N
−→(λy.(λx.M)N)P−→(λx.M)N
Remark9Clearly,−→assocactstronglysimulates−→assocthroughφ−1.
Noticethatwiththelet=in-notation,assocandactaresimplytherulesofλC
assocact
letx=(lety=PinN)inM(λx.M)N
−→lety=Pinletx=NinM−→letx=NinM
Lemma10−→assocact·→⊆→·−→∗assocactProof:Byinductiononthereductionstep→.SeeappendixC.
2
3
Lemma11−→∗→β12canbestronglyadjournedwithrespectto→.assoc,act·−
kProof:Weprovethat∀k,−→assoc→β12·→⊆→·−→∗→β12by,act·−assoc,act·−inductiononk.
•Fork=0,thisisCorollary8.
•Supposeitistruefork.Bytheinductionhypthesisweget
−→assoc,act·−→k→β12·→⊆−→assoc,act·→·−→∗→β12assoc,act·−assoc,act·−ThenbyLemma10weget
−→assoc,act·→·−→∗→β12⊆→·−→assoc,act·−→∗→β12assoc,act·−assoc,act·−
2
Remark12NotefromLemma5thatnf→⊆nf;1∪;2⊆nf−→β12⊆nf−→assoc,act·−→β12.Theorem13BN→⊆BN−→assoc,act·−→β12
Proof:WeapplyTheorem28,sincenf→⊆nf−→assoc,act·−→β12andclearly
∗
(−→assoc→β12)∪→=−→∗→β12,act·−assoc,act·−
∗
∗
∗
2
Theorem14BNβ⊆BN−→assoc·−→β
Proof:Since−→βstronglysimulates→throughφ,wehaveφ−1(BNβ)⊆
∗∗
BN→⊆BN−→assoc,act·−→β12.Henceφ(φ−1(BNβ))⊆φ(BN−→assoc,act·−→β12).Since
∗
φissurjective,BNβ=φ(φ−1(BNβ)).HenceBNβ⊆φ(BN−→assoc,act·−→β12).Also,
∗−→assoc→β12stronglysimulates−→∗→βthroughφ−1,soassoc·−,act·−∗∗
2φ(BN−→assoc,act·−→β12)⊆BN−→assoc·−→β.Theorem15SNβ⊆SNassocβ
Proof:First,fromLemma19,BN−→assoc·−→β⊆SN−→assoc·−→β.Thenfrom
Lemma1,−→associsterminatingandhenceSNassocisstableunder−→β.Hence
∗
wecanapplyLemma24togetSNassocβ=SN−→assoc·−→β.FromtheprevioustheoremwethushaveBNβ⊆SNassocβ.Now,noticingthatβ-reductioninλ-calculusisfinitelybranching,Lemma18givesBNβ=SNβandthusSNβ⊆SNassocβ.2
∗
∗
∗
References
[Mog88]E.Moggi.Computationallambda-calculusandmonads.ReportECS-LFCS-88-66,UniversityofEdinburgh,Edinburgh,Scotland,October1988.
4
A
Reminder:Notations,DefinitionsandBasicRe-sults
•Wedenotethecompositionofrelationsby·,theidentityrelationbyId,andtheinverseofarelationby−1.•IfD⊆A,wewriteR(D)for{M∈B|∃N∈D,NRM},orequivalently
N∈D{M∈B|NRM}.WhenDisthesingleton{M},wewriteR(M)forR({M}).
•WesaythatarelationR:A−→BistotalifR−1(B)=A.
Definition5(Relations)
Remark16Compositionisassociative,andidentityrelationsareneutralforthecompositionoperation.
Definition6(Reductionrelation)
•AreductionrelationonAisarelationfromAtoA.
•Givenareductionrelation→onA,wedefinethesetof→-reducibleforms(orjustreducibleformswhentherelationisclear)asrf→:={M∈A|∃N∈A,M→N}.Wedefinethesetofnormalformsasnf→:={M∈A|∃N∈A,M→N}.
•Givenareductionrelation→onA,wewrite←for→−1,andwedefine→nbyinductiononthenaturalnumbernasfollows:→0:=Id
→n+1:=→·→n(=→n·→)
→+denotesthetransitiveclosureof→(i.e.→+:=n≥1→n).
→∗denotesthetransitiveandreflexiveclosureof→(i.e.→∗:=n≥0→n).↔denotesthesymmetricclosureof→(i.e.↔:=←∪→).
↔∗denotesthetransitive,reflexiveandsymmetricclosureof→.
•AnequivalencerelationonAisatransitive,reflexiveandsymmetricreductionrelationonA,i.e.arelation→=↔∗,hencedenotedmoreoftenby∼,≡...•Givenareductionrelation→onAandasubsetB⊆A,theclosureofBunder→is→∗(B).
Definition7(Finitelybranchingrelation)Areductionrelation→onAisfinitelybranchingif∀M∈A,→(M)isfinite.
Definition8(Stability)Givenareductionrelation→onA,wesaythatasubsetTofAis→-stable(orstableunder→)if→(T)⊆T.
Definition9(Strongsimulation)
LetRbearelationbetweentwosetsAandB,respectivelyequippedwiththereductionrelations→Aand→B.
−1
→Bstronglysimulates→AthroughRif(R−1·→A)⊆(→+).B·RRemark17
1.If→Bstronglysimulates→AthroughR,andif→B⊆→Band→A⊆→A,then
→Bstronglysimulates→AthroughR.
5
2.If→Bstronglysimulates→Aand→AthroughR,thenitalsostronglysim-
ulates→A·→AthroughR.3.Hence,if→Bstronglysimulates→AthroughR,thenitalsostronglysimulates→+AthroughR.Definition10(Patriarchal)Givenareductionrelation→onA,wesaythat•asubsetTofAis→-patriarchal(orjustpatriarchalwhentherelationisclear)if∀N∈A,→(N)⊆T⇒N∈T.•apredicatePonAispatriarchalif{M∈A|P(M)}ispatriarchal.
Definition11(Normalisingelements)Givenareductionrelation→onA,thesetof→-stronglynormalisingelementsis
SN→:=T
TispatriarchalDefinition12(Boundedelements)Thesetof→-boundedelementsisdefinedas
BN→:=BN→n
n≥0
whereBN→nisdefinedbyinductiononthenaturalnumbernasfollows:
BN→0
BN→n+1
:=nf→
:={M∈A|∃n≤n,→(M)⊆BN→n}
Lemma18If→isfinitelybranching,thenBN→ispatriarchal.
Asaconsequence,BN→=SN→.Lemma19
→→→→
1.Ifn 1.SN→ispatriarchal. 2.IfM∈BN→then→(M)⊆BN→.IfM∈SN→then→(M)⊆SN→. Theorem21(Inductionprinciple)GivenapredicatePonA,suppose∀M∈SN→,(∀N∈→(M),P(N))⇒P(M).Then∀M∈SN→,P(M). WhenweusethistheoremtoproveastatementP(M)forallMinSN→,wejustadd(∀N∈→(M),P(N))totheassumptions,whichwecalltheinductionhypothesis. WesaythatweprovethestatementbyinductioninSN→.Lemma22 1.If→1⊆→2,thennf→1⊇nf→2,SN→1⊇SN→2, →21 andforalln,BN→n⊇BNn. 6 2.nf→=nf→,SN→=SN→,andforalln,BN→=BN→nn. Noticethatthisresultenablesustouseastrongerinductionprinciple:inordertoprove∀M∈SN→,P(M),itnowsufficestoprove ∀M∈SN→,(∀N∈→+(M),P(N))⇒P(M) ThisinductionprincipleiscalledthetransitiveinductioninSN→. Theorem23(Strongnormalisationbystrongsimulation)LetRbearela-tionbetweenAandB,equippedwiththereductionrelations→Aand→B. If→Bstronglysimulates→AthroughR,thenR−1(SN→B)⊆SN→A.Lemma24Giventworeductionrelations→1,→2,supposethatSN→1isstable∗ under→2.ThenSN→1∪→2=SN→1·→2∩SN→1. +++ BStrongadjournment Definition13Suppose→AisareductionrelationonA,→BisareductionrelationonB,RisarelationfromAtoB. →Bsimulatesthereductionlengthsof→AthroughRif k ∀k,∀M,N∈A,∀P∈B,M→kAN∧MRP⇒∃Q∈B,P→BQ Lemma25Suppose→AisareductionrelationonA,→Bisareductionrelation onB,RisarelationfromAtoB. If→Bstronglysimulates→AthroughR,then→Bsimulatesthereductionlengthsof→AthroughR. Proof:Weprovebyinductiononkthat∀k,∀M,N∈A2,∀P∈B,M→kA k N∧MRP⇒∃Q,P→BQ.•Fork=0:takeQ:=M=N. •SupposeitistrueforkandtakeM→AM→kAN.Thestrongsimulation+ givesPsuchthatP→BPandMRP.TheinductionhypothesisgivesQ k+1 suchthatP→kQ(oflengthBQ.ThenitsufficestotaketheprefixP→B +k k+1)ofP→BP→BQ. 2 Lemma26∀n,∀M, (∀k,∀N,M→kN⇒k≤n) ⇐⇒ M∈BN→n Proof:Bytransitiveinductiononn. •Forn=0:clearlybothsidesareequivalenttoM∈nf→.•Supposeitistrueforalli≤n. Suppose∀k,∀N,M→kN⇒k≤n+1.ThentakeM→Mandassume M→kN.WehaveM→k+1Nsofromthehypothesiswederivek+1≤n+1,i.e.k≤n.WeapplytheinductionhypothesisonMandget →→ M∈BN→n.BydefinitionofBNn+1wegetM∈BNn+1. kConversely,supposeM∈BN→n+1andM→N.Wemustprovethatk≤n+1. Ifk=0wearedone.Ifk=k+1wehaveM→M→kN;bydefinitionof → BN→n+1thereisi≤nsuchthatM∈BNi,andbyinductionhypothesiswehavek≤i;hencek=k+1≤i+1≤n+1. 2 7 Theorem27Suppose→AisareductionrelationonA,→BisareductionrelationonB,RisarelationfromAtoB. If→Bsimulatesthereductionlengthsof→AthroughR,then →AB ∀n,R−1(BN→n)⊆BNn (⊆SN→A) B Proof:SupposeN∈BN→andMRN.IfM→knAMthenbysimulation N→kBNsobyLemma26wehavek≤n.Henceby(theotherdirectionof) A Lemma26wehaveM∈BN→2n. Definition14Let→1and→2betworeductionrelationsonA.Therelation→1canbestronglyadjournedwithrespectto→2if wheneverM→1N→2PthereexistsQsuchthatM→2Q(→1∪→2)+P.Theorem28Let→1and→2betworeductionrelationsonA.Ifnf→2⊆nf→1and→1canbestronglyadjournedwithrespectto→2thenBN→2⊆BN→1∪→2.Proof:FromTheorem27,itsufficestoshowthat→2simulatesthereductionlengthsof→1∪→2throughtheidentity.Weshowbyinductiononkthat ∀k,∀M,N,M(→1∪→2)kN⇒∃Q,M→k2Q •Fork=0:takeQ:=M •Fork=1:IfM→2NtakeQ:=N;ifM→1Nusethehypothesis nf→2⊆nf→1toproduceQsuchthatM→2Q. •Supposeitistruefork+1andtakeM(→1∪→2)P(→1∪→2)k+1N. +1 TheinductionhypothesisprovidesTsuchthatP→kT,inotherwords2 k P→2S→2T. IfM→2Pwearedone.IfM→1PweusethehypothesisofadjournmenttotransformM→1P→2SintoM→2P(→1∪→2)+S.TaketheprefixP(→1∪→2)k+1R(oflengthk+1)ofP(→1∪→2)+S→k2T,andapply k+1 onthisprefixtheinductionhypothesistogetP→2R.Wethusget k+2 M→2R. 2 CProofs Lemma7;2·→⊆→·−→+β12 Proof:Byinductiononthereductionstep→. •ForthebasecasewherePtheβκ-reductionisaβ2-reduction,wehave M;2(λx.N)P→xNwithx∈FV(N)orPhasnomarkedredexasasubterm.WedoacaseanalysisonthereductionstepM;2(λx.N)P. If→β12Nthen(λx.N)P→2(λx.N)PbecauseN−PM=(λx.N)PP;xN−→β12xN. IfM=(λx.N)P;2(λx.N)PbecauseP;2P,thenitmeansthatPhasamarkedsowemusthavex∈FV(N).Henceredexasasubterm,P(λx.N)P→P→+xN−xN.β12 8 •ForthebasecasewherePtheβκ-reductionisaβ1-reduction,wehaveM;2(λx.N)P→xNwithx∈FV(N)orPhasnomarkedredexasasubterm.WedoacaseanalysisonthereductionstepM;2(λx.N)P.IfM=MP;2(λx.N)PbecauseM;2λx.NthenMmustbeoftheformλx.MwithM;2N.Then(λx.M)P→PPhasxM(incasePamarkedsubterm,noticethatx∈FV(N)⊆FV(M)),andxM−→β12PxN. IfM=(λx.N)P;2(λx.N)PbecauseP;2P,thenitmeansthatPhasamarkedsowemusthavex∈FV(N).Henceredexasasubterm,P(λx.N)P→P→+xN−xN.β12•Theclosureunderλisstraightforward. •Fortheclosureunderapplication,left-handside,wehaveM;2NP→NPwithN→N.WedoacaseanalysisonthereductionstepM;2NP.IfM=MP;2NPwithM;2N,theinductionhypothesisgives M→·−→+→·−→+β12NandtheweakcontextualclosuregivesMPβ12NP.IfM=NP;2NPwithP;2P,wecanalsoderiveNP→NP−→β12NP. •Fortheclosureunderapplication,right-handside,wehaveM;2NP→NPwithP→P.WedoacaseanalysisonthereductionstepM;2NP.IfM=MP;2NPwithM;2N,wecanalsoderiveMP→MP−→β12NP. IfM=NM;2NPwithM;2P,theinductionhypothesisgives M→·−→+→·−→+β12PandtheweakcontextualclosuregivesNMβ12NP.•FortheclosureundermarkedredexwehaveM;2(λx.P)N→(λx.P)NwithN→N.WedoacaseanalysisonthereductionstepM;2(λx.P)N.IfM=(λx.P)N;2(λx.P)NbecauseP−→β12P,wecanalsoderive(λx.P)N→(λx.P)N−→β12(λx.P)N. IfM=(λx.P)M;2(λx.P)NwithM;2N,theinductionhypothesis givesM→Q−→+→β12Nandtheweakcontextualclosuregives(λx.P)M (λx.P)Q−→+β12(λx.P)N. 2 ∗ Lemma10−→assocact·→⊆→·−→assocactProof:Byinductiononthereductionstep→. •Forthefirstbasecase,wehaveM−→assocact(λx.N)P→PxNwithx∈FV(N)orPhasnomarkedsubterm.Sincerootassocact-reductionpro-ducesneitherλ-abstractionsnorapplicationsattheroot,notethatMhastobeoftheform(λx.N)P,witheitherN−→assocactN(andP=P)or FV(N)⊆FV(N)orPhasP−→assocactP(andN=N).Inbothcases,x∈P nomarkedsubterm,sowealsohave(λx.N)P→PxN−→∗xN.assocact•Forthesecondbasecase,wehaveM−→assocact(λx.N)P→PxNwithx∈FV(N)orPhasnomarkedsubterm.WedoacaseanalysisonM−→assocact(λx.N)P. 9 IfM=(λx.M1)(λx.M2)P−→assoc(λx.(λx.M1)M2)PwithN=P(.MxM2=λx1)M2,wealsohaveM=(λx.M1)(λx.M2)P→(λx.M1)P xN. IfM=(λx.N)P−→act(λx.N)PthenM→PxN.IfM=(λx.N)P−→assocact(λx.N)PwitheitherN−→assocactN(andP=P)orP−→assocactP(andN=N),wehave,inbothcases,x∈FV(N)⊆FV(N)orPhasnomarkedsubterm,sowealsohave(λx.N)P→PP∗N−→xxN.assocact•Theclosureunderλisstraightforward. •Fortheclosureunderapplication,left-handside,wehaveQ−→assocactMN→MNwithM→M.WedoacaseanalysisonQ−→assocactMN.IfQ=MN−→assocactMNwithM−→assocactM,theinduction ∗ hypothesisprovidesM→·−→∗→·−→assocactMN.assocactMsoMNIfQ=MN−→assocactMNwithN−→assocactN,wealsohaveMN→MN−→assocactMN. •Fortheclosureunderapplication,right-handside,wehaveQ−→assocactMN→MNwithN→N.WedoacaseanalysisonQ−→assocactMN.IfQ=MN−→assocactMNwithM−→assocactM,wealsohaveMN→MN−→assocactMN. IfQ=MN−→assocactMNwithN−→assocactN,theinductionhypoth-∗∗ esisprovidesN→·−→assocactNsoMN→·−→assocactMN.•Fortheclosureundermarkedredex,the→-reductioncanonlycomefromtheright-handsidebecauseoftheweakcontextualclosure(→doesnotreduceunderλ),sowehaveQ−→assocact(λy.M)P→(λy.M)PwithP→P.WedoacaseanalysisonQ−→assocact(λy.M)P. IfQ=(λx.M)(λy.N)P−→assoc(λy.(λx.M)N)PwithM=(λx.M)N, wealsohaveQ=(λx.M)(λy.N)P→(λx.M)(λy.N)P−→assoc(λy.(λx.M)N)P.IfQ=(λy.M)P−→act(λy.M)P,thenwealsohaveQ=(λy.M)P→(λy.M)P−→act(λy.M)P. 2 10 因篇幅问题不能全部显示，请点此查看更多更全内容