The first-order theory of one step rewriting in li

TheFirst-OrderTheoryofOneStepRewritinginLinearNoetherianSystemsisUndecidableSergeiVorobyovMarch4,1997Max-Planck-InstitutfurInformatikImStadtwald,D-66123,Saarbrucken,Germany(e-mail:[e-mail])Abstract.Weconstructanitelinearnitelyterminatingrewriterulesystemwithundecidabletheoryofonesteprewriting.1PreliminariesGivenafunctionalsignaturewithconstantsandaniterewriterulesystemR,considerthemodelM=hT();Ri,whereT()istheHerbranduniverseoverandR=fhs;tijs;t2T()^s!RtgT()T()istheonesteprewriterelationonT()generatedbyR.ThepresenceofconstantsinisnecessarytoguaranteethatT()isnotempty.LetLbetherst-orderlanguagewithoutequalitycontainingtheonlybinaryrelationsymbolR.Therst-ordertheoryofonesteprewritinginRisthesetofallsentences(closedformulas)ofLtrueinM.Noticethattheonlynon-logicalsymbolusedinformulasofthetheoryisR,andthesymbolsofarenotallowedinformulas.Theaimofthisnoteistogiveanexampleofanitelinearnitelyterminatingsystemwithundecidabletheoryofonesteprewriting.Untilnowitwasanopenproblemastowhethersuchsystemsexist.Allsystemswithundecidabletheoriesofonesteprewritingknownsofarwerediverging[2,3],whereself-reducibilityoftermswasusedinanessentialwaytodetectpropertiesofterms.AtRTA’96H.Ganzingeraskedwhetherniteterminationisindispensableforundecidabil-ity.Theanswerappearstobenegative.Obtaininglinearitydoesnotrepresentanysubstantialdiculty,sothesystemweconstructissimultaneouslylinearandnitelyterminating.2ReductionWewillshowthatdyadicwordsandthedyadicwordconcatenation(i.e.,con-catenationofwordsinatwo-letteralphabet)canberepresentedbymeansofformulasofLforanappropriatesystemRwithdesirableproperties.Theunde-cidabilityofthetheoryofonesteprewritinginRthenfollowsbythewell-knownTheorem1(Quine,[1]).Therst-ordertheoryofdyadicconcatenationisundecidable.utWeemploythesamereductionasin[3].However,todetectpropertiesoftermsbymeansofaonestepreducibilityrelationinalinearnitelyterminatingsystemweuseadierentapproachbasedonrewritingdiagrams.Veryschemat-icallytheideamaybedescribedasfollows.Suppose,weneedtodeterminewhethertherstandthesecondsubtermsofatermf(s;t)areequalbyusingtheonesteprewritingrelationinalinearnitelyterminatingsystem.Wecanconstructthefollowingsystem,wheregisanauxiliaryternaryfunctionsymbolandc1,c2,c3areauxiliaryconstants:f(x;y)!g(x;y;c1),f(x;y)!g(x;y;c2),g(x;y;c1)!g(x;y;c2),g(x;y;c1)!g(x;y;c3),g(x;y;c2)!g(y;x;c3).Nowtherstandsecondsubtermsinf(s;t)(withoutinternaloccurrencesoff)areequalifandonlyiff(s;t)satisestheformula(u)8v9w;z(R(u;v))R(u;w)^(R(v;w)_R(w;v))^R(v;z)^R(w;z)),whereRistheonestepre-ducibilityrelationintheabovesystem.Wethusdistinguishtheneededpropertybya\diamond-likerewritediagram.Weusetheother\fan-likediagramsoftheformn(u)9x1;:::;xn(Vni=1R(u;xi)^Vn1i=1R(xi;xi+1))todistinguishotherneededpropertiesoftermsbymeansoftheonesteprewritingrelationinalinearnitelyterminatingsystem.3SignatureWewillusethefollowingsignatureoffunctionsymbols:1.,aconstanttodenotetheemptywordandtheemptylist;2.a(),b(),bothunarytorepresentthelettersAandB;3.c(;),binaryforthelistconstructorcons;4.h;;i,ternaryconstructorfortriples;5.0(),1(),2(),3(),E(),allunaryauxiliarysymbols.4RepresentingWordsLetusrepresentwordsoverthedyadic(binary)alphabetfA;Bgastermsofsignaturefa;b;g,wherea,bareunaryfunctionsymbolsandisaconstantasfollows:{representstheemptyword;{ifatermtrepresentsawordthentheterma(t)representsthewordAandthetermb(t)representsthewordB.Fromnowonforbrevitywewilloftencalltermsbuiltofa,b,words.5ConcatenationLettermssandtrepresentwordsandrespectively.Thentheterms[t=],i.e.,swithitsuniqueoccurrenceofreplacedwitht,representstheconcatenationofthewordsand.6ConcatenationWitnessesWeneedtoexpressthefactthatfortermsr,s,trepresentingwords,thecon-catenationofrandsequalst.Thiscanbedoneasfollows.Tocheckwhetherrs=twestartwithr;s;tandstepwiseeraseequalsymbolsinthebeginningofrandt.Theequalityrs=tholdsiwearriveat;s;s.ThisleadstothefollowingDenition2(ConcatenationWitnesses).Callaterm0(c(hx1;y1;z1i,c(hx2;y2;z2i,c(hx3;y3;z3i,...(1)c(hxn1;yn1;zn1i,c(hxn;yn;zni,))...)))),representingasequenceoftripleshx1;y1;z1i;:::;hxn;yn;zni,awitnessofcon-catenationofr,s,tifandonlyif{xi,yi,zi(fori=1;:::;n)aretermsbuiltof,a,andb(i.e.,words);{x1r,z1t,andyisfori=1;:::;n;{xn;(2){ynzn;(3){foralli=1;:::;n1eitherxia(xi+1)andzia(zi+1),(4)orxib(xi+1)andzib(zi+1).(5)Remark3.Theoutermost0()theaddedfortechnicalreasons,whichwillbecomeclearshortly.utObviously,wehavethefollowingsimpleProposition4.Theconcatenationofwords,equalsifandonlyifforthetermsr,s,trepresenting,,thereexistsa(unique)witnessofconcatenationofr,s,t.ut7ConventiononRewritingSequencesWerepresentasequenceofn1elementse1;e2:::;en1;enasaterm0(c(e1;c(e2;:::;c(en1;c(en;)):::))):Inthesequeltosimplifynotationandreadabilitywewilloperatewithrewriterulesoversequences,likehx;y;zi;hu;v;wi!hu;v;wi;x;y;hx;y;zikeepinginmindthatthisisjustasyntacticallysugaredversionofotherwisenon-understandableandbulkyc(hx;y;zi;c(hu;v;wi;x0)!c(hu;v;wi;c(x;c(y;c(hx;y;zi;x0))));(wherex0isafreshvariable).Similarly,bywritin