您的当前位置：首页 Extending Bachmair’s method for proof by consistency to the final algebra

Extending Bachmair’s method for proof by consistency to the final algebra

来源：钮旅网

ExtendingBachmair’sMethodforProofbyConsistencytothe

FinalAlgebra

OlavLysne,DepartmentofInformatics,UniversityofOslo,Norway

June1,1994

Keywordsandphrases:AutomaticTheoremProving,FinalAlgebra,ProofbyConsistency.

1Introduction

Proofbyconsistencyisamethodforprovingpropertiesofabstractdatatypes,andthepioneeringworkwasdonebyMusser[10].Theinitialideawasthatwhenanequationisaddedtoaspeciﬁcationwhichisunambiguousinacertainsense,theKnuthandBendixcompletionprocess[6]maybeusedtolookforinconsistencies.Thismethodhasbeenelaboratedbyseveralauthors,andrecentlymanyofthecompletionbasedmethodswereshowntobespecialisationsofageneralisedmethodfortheﬁnalalgebra[9].

HereweshallconcentrateontheapproachofBachmair[1],whichisnotcoveredby[9],andstudyhowthismethodgeneralisesintotheﬁnalalgebra.WeextendBachmair’sapproachmainlybyconsideringcriticalpairsemergingalsobypositioningequationsonrewriterules.Byacounterex-ampleweshowthatthisisingeneralnotenoughfortheprocesstobevalidfortheﬁnalalgebra.Weintroducetwomildrestrictions,symmetricalinconsistencywitnessesandleftlinearsetsofrewriterules,andshowthattheprocessisrefutationallycompleteandtherebycorrectforeachofthemsepa-rately.OurextensionofBachmair’smethodthereforeservesasaalternativetoHennicker’sContextInductionforobservationalimplementations[4],andgainsonthelatterbynotbeingdependentofhumaninteraction.Finallywepresentresultsontherestrictionofgenerationofcriticalpairs.

2BasicNotions

Weassumefamiliaritywiththebasicnotionsoftermrewriting.

Asignature6isasetoffunctionsymbols,eachsymbolhavingﬁxedarity.Thearitydenotesthenumberofargumentstakenbythefunctionsymbol,andinasortedsettingitalsospeciﬁesthesortsoftheargumentsandthecodomainsort.

A6-algebraisapair.A;F/whereAisasetofelementspossiblydividedintosorts,andFDffAjf26gsuchthatifnisthearityoffthenfAisafunctionfromAnintoA.InasortedsettingfAisalsorequiredtomaintainthesortrestrictionsofthearity.WecallAthecarrierofthealgebra,andforsimplicityweshalldenoteeachalgebrabyitscarrierwheneverFisobvious.

Considerthetwo6-algebrasAandB.LetÄbeamappingfromAtoB.IfÄ.fA.a1;:::;an//DfB.Ä.a1/;:::;Ä.an//forallf26andai2Awherenisthearityoff,thenÄissaidtobeahomomorphism.

AnalgebraAisinitialinaclassofalgebrasifitisamemberoftheclass,andthereisoneandonlyonehomomorphismfromAtoanyotheralgebraintheclass.Aisﬁnalintheclassifitisamember,andthereisoneandonlyonehomomorphismfromeveryalgebraintheclasstoA.

WhenVisasetofvariablesweuseT6.V/todenotethealgebraoftermsoverV,andT6.;/todenotethealgebraofgroundterms.

A6-algebraAisamodelforanequationtDu,writtenAjDtDuifÄ.t/DÄ.u/foreveryhomomorphismÄfromT6.V/toA.IfEisasetofequationsweshallwriteAjDEtodenotethatAisamodelforeveryequationinE.Apresentationh6;Eiispairconsistingofasignature6andasetofequationsE.Theclassofh6;Ei-algebrasisthesetof6-algebrasthataremodelsforeveryequationinE.Itiswellknownthatt$ŁEuifandonlyifallh6;Ei-algebrasaremodelsfortDu.Theinitialalgebraintheclassofh6;Ei-algebrasisdenotedI.E/.I.E/jDtDuifandonlyift¦$ŁEu¦foreverygroundsubstitution¦.

3FinalAlgebraandProofbyConsistency

Severalapproachestoﬁnalsemanticsofalgebraicspeciﬁcationshavebeenpublished,differingmainlyinthecategoryofmodelsconsidered.Letusdeﬁnethesetofmodelsweshallfocuson.Considerapresentationh6;Ei.Let60beasignaturesuchthat60Â6.Thetripleh6;E;60iisaﬁnalpresentation,and60istheinitialkernelofthisﬁnalpresentation.Wesaythata6-algebraAisah6;E;60i-algebraifallelementsofAarereachablefrom6-terms(nojunk),AisamodelforE,andAjD=gDtwhenevergisagroundtermfrom60andg$ŁEt.

Thefollowingfactsabouttheclassofh6;E;60i-algebrasareusedinthesequel.Forproofswereferto[9,11].

Fact1Theclassofh6;E;60i-algebrashasaﬁnalmodelforanyarbitraryﬁnalpresentationh6;E;60i.

WeshallletO.E;60/denotetheﬁnalalgebraintheclassofh6;E;60i-algebras,leaving6implicit.Fact2tiestheﬁnalmodeltotheobservabilityconceptsusede.g.bythepartitionedbyfeatureofLarch[3],whereasfact3isnecessaryforconsistencyproofstoapply:

Fact2O.E;60/jDuDvifft[u=i]¦$ŁEgwhenevert[v=i]¦$Eg,foralltermst,positionsi,groundsubstitutions¦andgroundtermsgconstructedfrom60.

Fact3O.E;60/jDuDvifftheredonotexisttwotermstandgwheregisbuiltonlyfrom60

suchthatt$ŁE[fuDvggandnott$Eg.

DtDuimpliesO.E;60/jDtDu.Fact4t$ŁEuimpliesI.E/j

Fact5Iftisagroundtermbuiltfrom60thenO.E;60/jDtDuimpliest$ŁEu.Fact6IfO.E;60/jDuDvthenO.E;60/andO.E[fuDvg;60/areisomorphic.

Weassumethattheequationsinourpresentationconstitutea(ground)convergentsetRofrewriterules,andweshallthereforewriteh6;R;60itodenoteaﬁnalpresentation,andO.R;60/todenoteitsﬁnalmodel.Furthermoreweshallby󰀆Rdenotesome(any)ﬁxedcompletesimpliﬁcationorderingcompatiblewithR.InadditionwemaketheassumptionthateveryR-equivalenceclasscontaininggroundtermsbuiltfrom60haveoneofthoseasitsR-minimalterm.Inconstructingaﬁnalpresentationthisisunproblematic.Itisnaturaltolettheinitialkernelconsistofconstructors

ofsortsforwhichwewantinitialalgebrasemantics,andobviouslyacompletespeciﬁcationwillmostoftenreduceanytermtoatermcontainingconstructorsonly.

ItisingeneralnotdecidablewhetheranequationisvalidinO.R;60/,butinsomecasesitispossibletodecidethatitisnot.Thebasicnotionusedforsuchpurposesinproofbyconsistencyisgroundreducibility.AtermisgroundreduciblewithrespecttoasetRofrewriterulesifandonlyifallgroundinstancesofthetermarereducibleinR.Weshallinthesequeluseanotionofgroundreducibilitywhichisparameterisedbytheinitialkernelofaﬁnalpresentation:

Deﬁnition1Atermis60-groundreduciblewithrespecttoRiffeachgroundinstanceofiteithercontainsfunctionsymbolsnotin60,orisR-reducible.AnequationtDuis60-groundreduciblewrt.Riffforeverygroundinstancet¦Du¦eithert¦andu¦areidentical,oroneofthemisR-reducible,orbothofthemcontainfunctionsnotin60.

Decidabilityof60-groundreducibilityfollowstriviallyfromdecidabilityofgroundreducibilityingeneral[5],andthefollowingweshallletthetwonotionsgroundreducibilityand60-groundreducibilitydenotethetwodifferentconcepts.WesaythatasetCofequationsisconsistentwithO.R;60/iffO.R;60/jDC.ItisclearthatifCcontainsanequationuDvwhichisnot60-groundreduciblewithrespecttoRthenCisnotconsistent.ThiscanbeseenbyassumingthatuDvisnot60-groundreducible.Thentheremustbeagroundsubstitution¦suchthat,say,u¦isbuiltfromfunctionsin60,andsuchthatu¦andv¦areirreducibleanddistinct.SinceRisgroundconvergent

weknowthatwecannothaveu¦$ŁRv¦.Nowobviouslyu¦$R[fuDvgv¦,thusbyfact3wegetO.R;60/jD=uDv.Ifu󰀆Rvanduisnot60-groundreduciblewemayfromthesamelines

=uDv.InbothofthesecaseswesaythatCisprovablyofreasoningconcludethatO.R;60/jD

inconsistent.

Nowfortheproofbyconsistencyprocedure.Weassumeadatastructureconsistingoftwosetsofequations,LandC,andweimplicitlyassumeagroundconvergentsetRofrewriterulesconstitutedbytheequationsfromtheﬁnalpresentation.InitiallyCcontainsthesetwewanttocheckforconsistencyandLiseitheremptyormaybethoughtofascontainingknowntheoremsfromtheﬁnalmodel,suchasACaxiomsfortheappropriatefunctions.ThedescriptionoftheprocessisinspiredbytheonepresentedbyBachmair[1]fortheinitialalgebra:DeductionInductionDeletion

Simpliﬁcation

L;CL;C

L;C[fsDtgL;C[fsDtg

````L;C[fsDtgL[fsDtg;CL;C

L;C[fuDtg

ifs$ŁR[Ct

ifO.R;60/jDsDtifO.R;60/jDsDtifs󰀆Ruands$CR[Luors$CubyvDwwheresFvandv󰀆Rw

HereFisbasicallyanywellfoundedorderingonterms,butitiscustomaryinsuchcasestoassumetheencompassmentordering,suchthattFuifasub-termoftisaninstanceofu,andnotviceversa.TheprocessterminateswithDisproofwhenCisprovablyinconsistent,andProofwhenwemayconcludethatO.R;60/jDC.Withfact6inmindthesoundnessofthisproofprocessiseasilyveriﬁedbyinspectionofthetransitionrules.Inordertoproverefutationalcompletenessofthisprocess,wemustﬁrststudytheequationalproofsemergingfromaninconsistentC.

Deﬁnition2Aninconsistencywitnessisanequationalproofoftheformt ŁRs[u¦=i]$Cs[v¦=i]!ŁRwinwhichalltermsareground,uDv2C,tandwaredistinctandR-irreducible,tisbuiltfrom60,and¦isagroundsubstitution.

Deﬁnition3Aninconsistencywitnessontheforms[u¦=i]$Cs[v¦=i]!ŁRwisdetectableifitdoesnotcontainanyR-rewritestepsatall,orifs[u¦=i]isbuiltonlyfrom60andu󰀆Rv.ItshouldbeeasytoseethatCisinconsistentifandonlyifthereexistsaninconsistencywitness,andthatCisprovablyinconsistentifandonlyifthereexistsadetectableinconsistencywitness.

InBachmair’smethodfortheinitialalgebratheDeducetransitionscreatenewequationsbycomputingcriticalpairsemergingfrompositioninglefthandsidesofrewriterulesinRonsub-termsofequationsinC.Thisissufﬁcientintheinitialalgebracase,becausethenonemayassumethattheequationalstepoftheinconsistencywitnessalwaysappliestothetoppositionoftheterm.ThemoregeneralnotionofinconsistencywitnessesappearinginourcasemeansthatwealsohavetoconsidercriticalpairsemergingfrompositioningeithersideofanequationfromConsub-termsofthelefthandsideofsomerewriterulefromR.Unfortunatelythisisnotsufﬁcientingeneral,asthiscounterexampleshows:

Example1ConsidertheﬁnalpresentationFPDhff2;g1;c0;d0g;ff.x;x/!cg;fc0giwherethesubscriptsonthefunctionsdenotetheirarity.ObviouslyFPfulﬁlsourrequirementthatthesetofequationsshouldformagroundconvergentsetofrewriteruleswithgroundtermsfromtheinitial

=g.x/Dg.y/,sincekernelasminimaltermswheneverpossible.NowO.ff.x;x/!cg;fc0g/jD

thereisaninconsistencywitnessf.g.c/;g.d//$f.g.c/;g.c//!c.Theequationg.x/Dg.y/isunorientable,60-groundreduciblewithrespecttoFPandhasnocriticalpairswiththerewriteruleintheﬁnalpresentation,thusourprocessisnotabletorefuteit.

Weshallthereforeﬁrstlyrestrictourselvestothecaseswhereallpossibleinconsistencywit-Ł

nessesaresymmetrical.Aninconsistencywitnesst ŁRu$Cv Rwissymmetricalifbothtandwarebuiltfrom60.Inthecasewhere6D60,inwhichcasetheinitialandtheﬁnalmodelcoincide,allwitnessesareobviouslysymmetrical.Thereisanotherinterestingspecialcasewhichgivesthesameguarantee;assumethatthefunctionsinthesignaturearedividedintotwodisjointsetsofconstructorsanddeﬁnedfunctionsrespectively,andthateverygroundtermisequationallyequivalenttoatleastonetermbuiltfromconstructorsonly.Ifweinadditionrequiretheinitialker-nelofthespeciﬁcationtocontainalltheconstructorsofsomesorts,e.g.thesortsforwhichwewantinitialalgebrasemantics,weknowthatanywellformedequationwillonlygiverisetosymmetricalinconsistencywitnesses.Sincetheﬁnalspecialcasecoincideswithnaturalpropertiesofalgebraicspeciﬁcationsbasedonﬁnalalgebra,therestrictiontosymmetricalinconsistencywitnessesisamildone.

LetusdeﬁneafunctionBfrominconsistencywitnessesintotriples.Thisfunctionisastraight-forwardadaptationofthecomplexityfunctionofBachmair:

B.t ŁDhfs[u¦=i]g;u;s[v¦=i]iRs[u¦=i]$Cs[v¦=i]!Rw/

Dhfs[v¦=i]g;v;s[u¦=i]ihfs[v¦=i];s[u¦=i]g;󰀁;󰀁i

ifu󰀆Rv.ifv󰀆Ru.otherwise.

Inthefollowingweshalllet󰀆Bdenotethelexicographiccombinationofthemultisetextensionof󰀆R,F,and󰀆Ritself.Obviously󰀆Bmaynowbeconsideredasawellfoundedorderingonin-consistencywitnesses,thusforIWaninconsistencywitnessweshallwriteIWinsteadofB.IW/wheneverthemeaningisclearfromthecontext.Weshallshowthatforanynon-detectableincon-sistencywitnessappearingatanystepoftheprocess,therewillafterﬁnitelymanystepsappearonewhichissmallerwithrespectto󰀆B.Sincetheorderingiswellfounded,thisreductionmustterminatewithadetectablewitness.Theoutlineoftheproofisthethesameasin[1],thusweshallrefertocorrespondingpointsinthatpaperforidenticalsubproofs.Thedifferencesarepartlydueto

thebroaderclassofwitnessesweconsider,andpartlytothedifferentcongruencerelationgivenbytheﬁnalmodel.Letusﬁrstprovethattheprocesswillneverrecedefromthesolution:

Lemma1LetL;C`L0;C0.ThenforanyinconsistencywitnessIWinCandR,thereexistsaninconsistencywitnessIW0inC0andRsuchthatIW¹BIW0.

Ł0

Proof:LetIWbet ŁRs[u¦=i]$Cs[v¦=i]!Rw.ForthecaseswhereuDv2Cthelemmaobviouslyholds,thuswemuststudythecaseswheretheequationuDvdisappearsinthetransitionstep.Sincetheequationunderconsiderationisusedintheequationalstepofaninconsistencywitness,wecannothaveO.R;60/jDuDv,thusweneedonlyconsiderthecaseswheretheequationuDvhasbeenreplacedbyrDvthroughasimplifytransitionstep.Thismeansthatu󰀆Rrandoneoftwocases:

DuD1.u$CR[Lr.SinceallequationsinRandLarevalidintheﬁnalmodelwegetO.R;60/j

rthusalsoO.R;60/jDs[u¦=i]Ds[r¦=i].IWandfact4givesO.R;60/jDtDs[u¦=i],thusbytransitivitywegetO.R;60/jDtDs[r¦=i].Sincetisbuiltfrom60fact5givest$ŁRs[r¦=i],andbecauseRisgroundconvergentwegetthattheminimalformofs[r¦=i]is

00Ł

t.Wemaythenlett ŁRs[r¦=i]$rDvs[v¦=i]!RwbeIW.ProvingB.IW/¹BB.IW/isstraightforwardfromtheproofin[1].

2.u$lDmrsuchthatlDm2C\\C0,uFlandl󰀆Rm.Thispartisstraightforwardfrom[1].

Thenextstepistoprovethatifsomeinconsistencywitnessisnon-detectable,thentherewillafterﬁnitelymanytransitionstepsemergeawitnesswhichissmallerwithrespectto󰀆B.Deﬁnition4WesaythatC0isacoveringsetforCwithrespecttoanordering×oninconsistencywitnessesifwheneverCisnotprovablyinconsistent,foreverynon-detectableinconsistencywitnessIWinCandR,thereexistsawitnessIW0inC0andRsuchthatIW×IW0.

Letthenotationt!Cudenotethatthespecialcaseoft$Cuwheret󰀆Ru.Since󰀆Rissupposedtobeacompletesimpliﬁcationorderingt$Cumeanseithert Cuort!Cuwhenevertanduaregroundterms.LetCP.R;C/denotethesetofcriticalpairsemergingfrompositioninglefthandsidesofrulesfromRoneithersideofanequationfromC,orpositioningeithersideofanequationfromConalefthandsidefromR.WeshallneedaspecialcaseoftheorderedcriticalpairlemmaduetoLankford[8]:

Lemma2Lett Ru!Cvbeanequationalproofsuchthatt,uandvaregroundterms.Then

eithert$CP.R;C/vorthereexistsaprooft!ŁR[Cw R[Cv.Lemma3CP.R;C/[Cisacoveringsetwrt.󰀆Bgrantedthatallinconsistencywitnessesaresymmetrical.

Proof:AssumethatCisnotprovablyinconsistent,andletIWDt ŁRu$Cv!Rwbeanarbitrarynon-detectableinconsistencywitness.WemustshowthatthereexistsawitnessIW0suchthatIW󰀆BIW0,andwherethetopequationalstepinIW0isanapplicationofanequationfromCP.R;C/[C.Since󰀆Risacompletesimpliﬁcationorderingwemaywithoutlossofgeneralityassumethatu󰀆Rv,thusthetopequationalstepinIWisontheformu!Cv.

SinceCisnotprovablyinconsistent,IWmustcontainR-steps.Assumeﬁrstthattherearesuch

0Ł

R-stepsonthelefthandside,thusIWisontheformt ŁRt Ru!Cv!Rw.Considerthe

subprooft0 Ru!Cv.Accordingtolemma2eithert0$CP.R;C/vort0!ŁR[Cm R[Cvfor

0Ł

somem.IntheformercasewemayletIW0Dt ŁRt$CP.R;C/v!Rw,andsinceu󰀆Rvandu󰀆Rt0IW0isobviouslylessthanIWwithrespectto󰀆B.Inthelattercasewemayassumethat

ŁŁ

thereisanonzeronumberof$Cstepsint0!ŁR[Cm R[Cv.Otherwisewewouldhaveu$Rv,thusIWwouldnothavebeenawitnessintheﬁrstplace.Letu1$Cv1:::un$Cvnbethese$Csteps.Sincet0andvhavedistinctR-normalforms,theremustbeanindexisuchthatuiandvihave

Ł00

distinctR-normalforms.ThismeansthattheremustbeawitnessIW0Dt00 ŁRui$Cvi!Rw.

Fromthefactsthatu󰀆Rt0,u󰀆Rvandthatthereisaproofontheformt0!ŁR[Cm R[Cvwhereu1$Cv1isoneofthesteps,wemayconcludethatu󰀆Rv1andu󰀆Ru1thusIW󰀆BIW0.

NowassumethatIWhasnorewritestepsonthelefthandside,thusitisontheformt!Cv!Rv0!ŁRwwheretisR-irreducible.SinceIWisnon-detectable,weknowthattheappliedequationfromCisunorientableby󰀆R.ThismeansthatB.IW/Dhft;vg;󰀁;󰀁i.Considerthesubprooft!Cv!Rv0.TherearefourcasesforthecombinationofR-redexandC-redexinv.

1.TheR-redexandtheC-redexinvaredisjoint.InthatcasetwouldhavebeenR-reducible,whichweherehaveassumeditisnot.

2.Thereisacriticaloverlapbetweenthetworedexes.Thispartisanalogousto[1].

3.TheR-redexisoverlappingavariablepositionintheC-redex.Thiscaseisalsohandledin[1].4.FinallyassumethattheC-redexoverlapsatavariablepositionoftheR-redex.Sincetisirreducible,therewriteredexmustbedestroyedinthestepfromvtot.TheonlypossibilityforthistohappenisiftheR-stepappliestovbecause(atleast)twooccurrencesofasub-term,sayr,invmatchidenticalvariablesinathelefthandsideofarulefromR,andoneofthesesub-termsisalteredto,sayl,intheC-step.Thismeansthatbothlandraresub-termsoft,andthatl$Cr.Sincetisabottomterminawitness,itmustbebothirreducibleandbuiltfrom60.Thismeansthatbothlandrareirreducibleandbuiltfrom60.Sincel$Cr,Cwouldhavebeenprovablyinconsistent,thusthiskindofoverlapisimpossible.

Markthatlemma3mayeasilybestrengthenedtosayingthatCP.R;C/isacoveringsetforC,byrecursiveapplicationsofitsproof.Thetheoremnowfollowsfromlemmas1and3.

Theorem1ProofbyconsistencyintheﬁnalalgebrawhichaddsequationsfromCP.R;C/withafairstrategyisrefutationallycompletegrantedthatallinconsistencywitnessesaresymmetrical.Inthereasoningleadingontotheorem1weusedtheconceptofsymmetricalwitnessesonlyonce,namelyinpoint4.oftheﬁnalcase-splitwhenweassumedthattisbuiltfrom60.WemaytriviallychangethispointintheproofifweinsteadofsymmetricalwitnessesrequirethatnolefthandsidesinRcontainmorethatoneinstanceofthesamevariable:

Theorem2ProofbyconsistencyintheﬁnalalgebrawhichaddsequationsfromCP.R;C/withafairstrategyisrefutationallycompletegrantedthatRisleftlinear.

Ourprocessmayalsobeusedtoproveequationsvalidintheﬁnalalgebra.InthesamewayasinthecorrespondingmethodfortheinitialalgebrawemayconcludethatCisvalidintheﬁnalmodelwheneverCisitsowncoveringset.

4Minimisingthecoveringsets

InordertoreducethenumberofcriticalpairscomputedintheinductivecompletionprocedureFribourg[2]introducedthenotionofcompleteposition.Apositioninatermtissaidtobecomplete

withrespecttoasetRofrewriterulesift[i]isnotavariable,andt[i]¦isreducibleatthetoppositionforeverygroundsubstitution¦whichissuchthatx¦isirreducibleforeveryvariablex.Küchlin[7]extendedthisconceptintheobviouswaytocompletesetsofpositionswithrespecttoasubsetofR.ItisclearthatatermhasacompletesetofpositionswithrespecttoasubsetofRifandonlyifitisgroundreducible(inthegeneralsense)wrt.thesamesubset.

AnalogouslytowhatisstatedinBachmair’sapproachfortheinitialalgebra,thesetofcriticalpairsobtainedbypositioningrewriterulesfromR0onpositionsfromthesetIofpositionsinsisacoveringsetfortheequationsDtwhenevers󰀆Rt,andIisacompletesetofpositionsforswrt.R0.Noticethatinthecaseswheretheaboveappliesitalsorelievesusfromhavingtocomputecriticalpairsstemmingfrompositioningequationsontorewriterules.Itisfurthermorefairlyobviousthatwheneversandtareincomparable,andbothsandtcontaincompletesetsofpositionswrt.subsetsofR,weonlyneedtocomputethecriticalpairsemergingfromoneofthem.Alsowhenevers󰀆RtweonlyneedtomatchswiththelefthandsidesofrulesfromRinordertocreateacoveringsetfortheequationsDtwrt.󰀆B.

Inordertofurtherreducethetheamountofcriticalpairsneededinthecomputationofcoveringsetsintheﬁnalalgebra,weintroducetheconceptofinitialrelatedness.

Deﬁnition5Wesaythatvisinitiallyrelatediffforallgroundsubstitutions¦,v¦hasatermbuiltfrom60asitsR-minimalform.

Decidingwhetheratermisinitiallyrelatedisingeneralnon-trivial.Inthepresentationsemerg-ingfromalgebraicspeciﬁcations,however,itismostoftenstraightforward.If60consistsoftheconstructorsofsomeofthesortsinthepresentationandallgroundtermsrewritetoaconstructorterm,thenalltermsofthesesortsareinitiallyrelated.

Lemma4Letvbeinitiallyrelatedwrt.R.ThenO.R;60/jDuDvifandonlyifI.R/jDuDv.Proof:Fact4givesthatI.R/jDuDvimpliesO.R;60/jDuDv.AssumethatO.R;60/jDuDv,andlet¦beanarbitrarygroundsubstitution.Sincevisinitiallyrelatedv¦$ŁRgforsomegbuiltfrom60.WeknowthatuDvcannotgiverisetoanyinconsistencywitness,thusgmustbetheminimalformofu¦aswell.Thismeansthatu¦$ŁRv¦foranygroundsubstitution¦,henceI.R/jDuDv.

TheaboveenablesustospecifyamorerestrictivecoveringsetforasetCofequations.Ifuisinitiallyrelated,thenbylemma4theequationuDvcreatesaninconsistencywitnessinI.R/wheneveritcreatesoneinO.R;60/.Itiswellknownthatwitnessesintheinitialalgebraareof

formt ŁRu¦$Cv¦!Rw.Sinceuisinitiallyrelatedtmustbebuiltfrom60,thusthisisaninconsistencywitnessinO.R;60/aswell.Thereforeweneedonlyconsidercriticalpairsemergingfrompositioningrewriterulesontothetermsintheequationwheneverwecandetectthateitherofthetermsintheequationisinitiallyrelated.

Example2Consideraﬁnalpresentationh6;R;60iwhere6DfTRUE;FALSE;or;zero;succ;eq;ety;ins;has;unig,60isthesubsetfTRUE;FALSE;zero;succg,andRcontainsthefollowingrules.

or.FALSE;x/!xor.TRUE;x/!eq.zero;zero/!eq.succ.x/;zero/!eq.zero;succ.y//!

TRUETRUEFALSEFALSE

eq.succ.x/;succ.y//!eq.x;y/

has.ety;y/!

FALSE

has.ins.s;x/;y/!or.eq.x;y/;has.s;y//

uni.x;ety/!x

uni.x;ins.y;z//!ins.uni.x;y/;z/

Thefunctionsetyandinsmaybeviewedasconstructorsofsetsofnaturalnumbers,andeqisthedeﬁnedversionoftheinitialalgebraequalityrelationonthesamenaturalnumbers.Thefunctionunicomputestheunionoftwosets.Thehasfunctionobservesthebehaviourofthesetsinto60andtherebyﬁxestheintendedcongruenceoftheﬁnalmodel.

Letusnowprovecommutativityofuni:uni.x;y/Duni.y;x/,assumingcommutativityandassociativityoforhasalreadybeenproven.Theequationisunorientable,butsincebothtermsaregroundreducible,wegetacoveringsetbypositioningrewriterulesononeoftheunioccurrences:

1.uni.ety;y/Dy2.uni.ins.y;z/;x/Dins.uni.x;y/;z/Bycreatingacoveringsetfortheseequations,wereach

3.etyDety5.ins.y;z/Dins.uni.ety;y/;z/

4.ins.uni.ety;y/;z/Dins.y;z/6.ins.uni.ins.y;z/;y1/;z1/Dins.uni.ins.y1;z1/;y/;z/Equation3istrivial,and4and5arereducedtotrivialequationsby1.Equation6isreducedintoins.ins.uni.y1;y/;z/;z1/Dins.ins.uni.y;y1/;z1/;z/by2.Thisremainingequationhascompletepositionsonbothoccurrencesofuni,thusthefollowingisacoveringset.

7.ins.ins.y1;z/;z1/Dins.ins.uni.ety;y1/;z1/;z/

8.ins.ins.ins.uni.y1;y2/;z2/;z/;z1/Dins.ins.uni.ins.y2;z2/;y1/;z1/;z/Reducedby1and2thisgives

7.ins.ins.y1;z/;z1/Dins.ins.y1;z1/;z/

8.ins.ins.ins.uni.y1;y2/;z2/;z/;z1/Dins.ins.ins.uni.y1;y2/;z2/;z1/;z/

Now8isaninstanceof7,thusweneedonlycreateacoveringsetfor7.Sincethetermsin7arenotgroundreducible,notinitiallyrelated,andtheequationisunorientable,wemustpositionthisequationontorewriterulesfromR.Thisgivesthefollowingcoveringset:

9.or.eq.z1;x/;has.ins.y1;z/;x//Dhas.ins.ins.y1;z1/;z/;x/10.ins.uni.x;ins.y1;z//;z1/Duni.x;ins.ins.y1;z1/;z//ReducedtoR-minimalformsthisgives

9.or.eq.z1;x/;or.eq.z;x/;has.y1;x///Dor.eq.z;x/;or.eq.z1;x/;has.y1;x///10.ins.ins.uni.x;y1/;z/;z1/Dins.ins.uni.x;y1/;z1/;z/

Sinceorisassociativeandcommutativenumber9isvalidintheﬁnalmodel,thusmayberemovedbyaDeletestep.Number10iscoveredby7thusisitsowncoveringset.

References

[1]L.Bachmair.Proofbyconsistencyinequationaltheories.InProceedings3rdIEEESymposium

onLogicinComputerScience,Edinburgh(UK),pages228–233,1988.[2]L.Fribourg.Astrongrestrictionontheinductivecompletionprocedure.InProceedings13th

InternationalColloquiumonAutomata,LanguagesandProgramming,volume226ofLectureNotesinComputerScience,pages105–115.Springer-Verlag,1986.[3]J.V.Guttag,J.J.Horning,andJ.M.Wing.Larchinﬁveeasypieces.Technicalreport,Digital

SystemsResearchCenter,1985.[4]R.Hennicker.Observationalimplementations.InProceedingsofthe6thAnnualSymposiumon

TheoreticalAspectsofComputerScience,volume349ofLectureNotesinComputerScience,pages59–71.Springer-Verlag,19.[5]D.Kapur,P.Narendran,andH.Zhang.Onsufﬁcient-completenessandrelatedpropertiesof

termrewritingsystems.ActaInformatica,24(4):395–415,1987.[6]D.E.KnuthandP.B.Bendix.Simplewordproblemsinuniversalalgebras.InJ.Leech,editor,

ComputationalProblemsinAbstractAlgebra,pages263–297.PergamonPress,Oxford,1970.

[7]W.Küchlin.Inductivecompletionbygroundprooftransformation.InH.Aït-Kaciand

M.Nivat,editors,ResolutionofEquationsinAlgebraicStructures,volume2ofRewritingTechniques,chapter7.AcademicPress,19.[8]D.S.Lankford.Canonicalinference.TechnicalReportATP-32,DepartmentofMathematics

andComputerScience,Univ.ofTexas,Austin,1975.[9]O.Lysne.Proofbyconsistencyinconstructivesystemswithﬁnalalgebrasemantics.In

Proceedings3rdInternationalConferenceonAlgebraicandLogicProgramming,Pisa(Italy),volume632ofLectureNotesinComputerScience,pages276–290.Springer-Verlag,1992.[10]D.L.Musser.Onprovinginductivepropertiesinabstractdatatypes.InProceedingsofthe7th

AnnualACMSymposiumonPrinciplesofProgrammingLanguages,pages1–162,January1980.[11]M.Wirsing.Algebraicspeciﬁcation.InJ.vanLeeuwen,editor,HandbookofTheoretical

ComputerScience,volumeB,chapter13.Elsevier,Amsterdam,1990.

因篇幅问题不能全部显示，请点此查看更多更全内容

查看全文