Definability
Hans-J¨orgBurtschickFachbereichInformatik
TUBerlinFranklinstr.28/29D-10587Berlin
HeribertVollmerTheoretischeInformatikUniversit¨atW¨urzburgAmExerzierplatz3D-97072W¨urzburg
Abstract
Weintroducesecond-orderLindstr¨omquantifiersandexamineanalogiesto
theconceptofleaflanguagedefinability.Thequantifierstructureinasecond-ordersentencedefiningalanguageandthequantifierstructureinafirst-ordersentencecharacterizingtheappropriateleaflanguagecorrespondtooneanother.Undersomeassumptions,leaflanguagedefinabilityanddefinabilitywithsecond-orderLindstr¨omquantifiersmaybeseenasequivalent.Alongthewaywetightenthebestuptonowknownleaflanguagecharacterizationoftheclassesofthepolynomialtimehierarchyandgiveanewmodel-theoreticcharacterizationofPSPACE.
1Introduction
InitiatedbyFagin’sseminalpaper[Fag74]characterizingNPastheclassofgener-alizedspectra,therehasbeenalonglineofresearchincharacterizingcomplexityclassesusingnotionsfromfinitemodeltheory(seetherecenttextbook[EF95]).Inclassicalcomplexitytheoryproblemsareclassifiedbydefiningrestrictionsondifferentcomputationalresourcesase.g.spaceortime.Usingincontrasttothisthesyntacticcomplexityofadefiningformulaitispossibletomeasurethedescriptivecomplex-ityofproblems,e.g.byconsideringthecomplexityofquantifierprefixesofprenexformulae.Besidesthewell-knownexistentialanduniversalquantifiersrecentlytheexpressivepowerofacertainkindofgeneralizedquantifiers,thesocalledLindstr¨omquantifiers,hasbeenexamined[Lin66];foranoverviewseeChapter10of[EF95].Anextensiveoverviewovertheliteraturecanbefoundin[Got95].
1
Inthefieldofcomputationalcomplexitycharacterizationsofcomplexityclassesbysocalledleaflanguageshavebeenstudiedintensively.Thisapproachwasin-troducedbyBovet,Crescenzi,andSilvestriin1992[BCS92]andindependentlybyVereshchaginin[Ver93]asaunifiedapproachtodefinecomplexityclasses.Considerapolynomial-timenondeterministicTuringmachinethatprintsavalueoneverypathofitscomputationonsomegiveninput.Thesevaluesareattheleavesofthe(notnecessarilyfullybalanced)binarytreedefinedbythenondeterministicchoicesofoninput.Anorderingofthetuplesintheprogramofdetermines,foreachnondeterministicchoicenodeofthetree,whichchildis“left”andwhichis“right”.Thisinturnfixesaleft-to-rightorderingofalltheleaves.Wecallthecorrespondingsequenceofvaluestheleafstringofoninput.(TheparticularorderingoftuplesintheprogramofMdoesnotmatter.)Givennowa(leaf)language,acomplexityclassLeafPisdefinedasfollows:AsetisinLeafPifandonlyifthereisanondeterministicTuringmachinethatoninputproducesaleafstringwhichsuchthatifandonlyif.
StartingwiththesomewhatsurprisingresultthattheclassPSPACEcanalreadybecharacterizedinthiswayusingonlyregularleaflanguages[HLS93],alotofcharac-terizationsweregiven[JMT94,HVW95,HVW96,CMTV96],leadingtoanumberofremarkableandunexpectednormalformsforsuchclassesasPSPACE(viabottleneckmachines[HLS93]),PP(viamachineswhereacceptingandrejectingcomputationpathsformtwoclusters[HVW96]),and#P(whereallrelativizableclosurepropertieswereidentified[HVW95]).Evenseparationsofcircuitclassescouldbeprovedusingleaflanguagesasatechnicalvehicle:Allendershowedin[All96],buildingonpreviousworkby[CMTV96],thatTCPP.
Itturnsout,asweshowhere,thatbothconcepts—Lindstr¨omquantifiersandleaflanguagedefinability—arecloselyrelated:Leaflanguagedefinedcomplexityclassescan(undercertainassumptions)becharacterizedbysecond-orderLindstr¨omquanti-fiersthatarefollowedbyfirst-orderformulas,andviceversaforeveryformulaofthisformthereisaleaflanguageandanondeterministicpolynomiallytime-boundedTur-ingmachinethatdefinethecorrespondingmodelclass.ThusLindstr¨omquantifiersandleaflanguagedefinabilityaretwopointsofviewofessentiallythesameconcept.RelyingonbothviewsonemighthopetogetnewinsightsintotheexpressivepowerofLindstr¨omquantifiersonorderedfinitestructuresandpropertiesofleaflanguagedefinedcomplexityclasses.
Wegivesomeresultsinthisdirectioninthispaper:Thepolynomialtimehierar-chyintroducedbyStockmeyerin[Sto73]isoneofthecentralconceptsincomplexitytheory.Thusofcoursetherehavebeeneffortstogiveleaflanguagecharacteriza-tionsofthishierarchy.In[HLS93]itwasshownthatusingACasleaflanguage
2
class,oneobtainstheunionofallclassesofthepolynomialhierarchy,andusingthe-thleveloftheBrzozowski-(ordot-depth-)hierarchy[Str94]asleaflanguageclass,thebooleanclosureoftheclasspisobtained.In[JMT94]itwasprovedthat
p
LeafP-LOGTIME.Usingfirst-orderdefinableleaflanguagesweproveatighterconnection:Weshowthatthe-thlevelfromthepolynomialtimehierarchy
for-canbecharacterizedusingleaflanguagesthatcanbedefinedusingfirst-order
mulae.Asanotherexampleofhowacombinationofmodel-theoreticandcomplexitytheoreticargumentscanleadtonewresults,weshowhowtouseatheoremfrom[HLS93]toderiveanewmodel-theoreticcharacterizationofPSPACE.
TheseresultsarespecialcasesofageneraltheoremwhichstatesthatifaleaflanguageisdefinedbyaformulainprenexnormalformstartingwithoneLindstr¨omquantifierandfollowedbyasequenceofuniversalandexistentialquantifiers,thenthecharacterizedcomplexityclasscanbedefinedinamodel-theoreticwaybyasecond-orderformulawithexactlythesamequantifierstructure.Thusweseethatusingmeth-odsfromfinitemodeltheoryweareabletotightenexistingcomplexitytheoreticre-sults.Wethinkthatgenerallyitisagoodideatospecifyleaflanguagesinadescriptiveway.Onepurposewhenconsideringleaflanguagedefinabilityistoseparatethecom-putationalaspectinthedefinitionofaclassfromthewaythecomputation(informofthecomputationtreeconstructedbyanondeterministicmachine)isevaluated.Thisevaluationschemeshouldthereforebegiveninawayfreeofcomputationalaspectswhatsoever.Thisgoalisachievedusingfinitemodeltheorytospecifyleaflanguages.Otherconnectionsbetweenleaflanguagedefinabilityandfinitemodeltheoryareestablishedin[Vei96].Heconsiderslogicalreducibilities[EF95]ase.g.first-orderreducibilityandprojectionreducibilitytosuccinctrepresentationsoflanguages.Thisconceptofsuccinctrepresentationsmaybeviewedasaspecialcaseofleaflanguagedefinability(seealso[BL96]).However,theresultsachievedinhispaperareincom-parabletoours.
2Preliminaries
Leaflanguageswereintroducedandusedtodefinecomplexityclassesin[BCS92,Ver93,HLS93](seealsotherecenttextbook[Pap94]).Letbeapolynomialtime-boundednondeterministicTuringmachine.Givenaninput,suchamachineproducesoneverypathasymbolfromsomefinitealphabet.Letbethestringofthesoproducedsymbols(basedonthenaturalorderofpathsofthemachine).Thenfor
,wedefineLeaf.TheclassLeafPisthedef
classofalllanguagesLeafforallnondeterministicpolynomial-timemachines.Here,isthesocalledleaflanguagedefiningtheclassLeafP.Ifisaclass
3
oflanguages,thenwedefineLeafP
def
LeafP
.
Asitturnedout[JMT94,HVW96],itplaysacrucialrolewhetherintheabovedefinitionweallowarbitraryTuringmachinesorwerequirethatthecomputationtreesproducedhaveaspecialshape.ForthecaseoffullbinarytreesweusethenotationFBTLeafP,see[Her95].Note,thatwithrespecttotheproducedleafstringonlythenondeterministicbranches,butnotthelengthofthepathisrelevant.Intherest
havingthefollowingofthepaperwewillusenondeterministicTuringmachines
property:Letbethesmallestnaturalnumbersuchthatistime-bounded.Thenallcomputation-pathsareexactlyoflength.Thismaybeachievedinanuniquewayusingleftbranches,ifthelengthofapathissmallerthan.Foreverypolynomialtime-boundednondeterministicTuringmachinethereexistsapolynomialtime-boundednondeterministicTuringmachinefulfillingtheabovepropertysuchthat
forallinputs.Thus,whenwriteLeafPweuseTuringmachines
asdescribedabove.
Itcanbeseenthatinaspecialcasethedistinctionbetweenfullbinarytreesandthegeneralcaseisunnecessary.Forthis,givenalanguageforsomealphabet,andaletter1,definepad1tobetheregularlanguage11111for;andletpad1pad1.Saythatalanguageclassdefisclosedunderpaddingiffforalsopad1.NowitcanbeseenthatLeafPFBTLeafPwheneverisclosedunderpadding[JMT94].Weremarkthatgenerallyalllanguageclassesdefinedbyautomata(finiteautomata,pushdownautomata,Turingmachines)areclosedunderpadding.Thisalsoapplies,aswewillseelater,tomostofthesubclassesoftheregularlanguagesweconsider.
Laterwewillalsoallowdifferentpaddingsymbols.Forthisletbeanalphabetsuchthat.Thenpadisthelanguagepaddef
for.
Inthispaper,weconsiderclassesthatarecharacterizedvialogicallydefinedleaf
languages.Especially,wedealwiththefollowingclassesofformulae:
FOistheclassofallfirst-orderformulae,SOistheclassofallsecond-orderfor-mulae.Weusethenotationsand(and)todenotethesubclassesofFO(SO,resp.)consistingofprenexformulaeinformorform,see[EF95].ForaformulawedenotetheclassoffiniteorderedstructuresthataremodelsofbyMod.Sinceweareinterestedincharacterizationsofcomplexityclasses,wecon-siderinthispaperonlyorderedfinitestructures,thatis,structuresoversignaturesthatdonotcontainconstantorfunctionsymbolsbutdocontainasymbolforalinearorderontheuniverse.Wedonotusethesuccessorrelation.
Weuseanencoding
ofstringsintoorderedfinitestructuresdefinedintheusual
4
way[Fag74]asfollows:Letbeafinitesetofsymbolsandlog.Theimagesofareorderedfinitestructuresoverthesignaturewithunarypredicates.Forafixedenumerationofthesymbolsin,letbethe-thsymbolin.Ifthe-thelementinthestringis,thenin
,iffthe-thbitinthebinaryencodingofis,foralland.
isapoweroftwo,thenisabijection.IfisaNote,thatisone-oneandif
language,thenwewritefor.Ifisaclassoflanguages,then
.def
Furthermorewesometimeshavetoencodefiniteorderedstructuresintostrings.
Sinceisone-one,isafunction,too.Wedefineanencodingfromfiniteor-deredstructuresintostringsthatincludesbutalsoextendstomaprelationsofaritygreaterthanoneintostrings.AnalogouslytotheabovewewriteModfortheset,andgenerallyforastructureclasswewritefor
.(Following[Fag74]wechoosetousethesymbolsandforour
encodingsthoughtheyaremaybenotveryintuitive.)
Ifisalogic(ase.g.FOorSO)andisacomplexityclass,thenwesaythat
capturesiffeverypropertyover(encodingsof)structuresdecidablewithinisexpressiblebysentences(i.e.,Mod),andontheotherhandforeveryfixedsentence,determiningwhethercanbedonein(i.e.,Mod).Asanabbreviationwewillmostofthetimesimplywrite.
Ifisalogic,thenLeafPisthecomplexityclasscharacterizedbytheleaflanguageconsistingofallwordssuchthatthecorrespondingstructureisamodelofanformula,insymbols:LeafPifthereexistaandapolynomialtime-boundednondeterministicTuringmachinesuchthatforall,
.
InaseminalpaperFagin[Fag74]connectedthecomplexityofcomputationswith
thesyntacticcomplexityoflogicallanguages.Heshowedthefollowing:LetbeanondeterministicpolynomialtimeTuringmachinethatrecognizesalanguageoversomealphabet.Letusassumethatoneveryinput,’scomputationtreeisafullbinarytree.Faginconstructedanexistentialsecond-orderformulathatdescribesthecomputationof.Theformulaisoftheformwhereisafirst-orderformulathathasnofreefirst-ordervariablesandthatadditionallycontainsthefreesecond-ordervariables.Thearitiesandthenumberofthesecond-ordervariablesaredeterminedbytheconstruction,see[Fag74].
Theorem2.1[Fag74].NP
,i.e.
NP
Mod
and
Mod
NP.
time-boundedandLetusconsideranondeterministicTuringmachinethatis
thatproducesafullbinarycomputationtreeforallinputs.Itispossibletorepresent
5
apathinacomputationtreeofdepthusingastring.Weenumeratethepathsusingthelexicographicalorderingon.Analogously,wecanenumeratetheassignmentsofa-arysecond-ordervariableusingthelexicographicalorderingoncharacteristicsequences.Inthispaperwewant
inthecomputationtreeandthetouseadirectcorrespondencebetweenthepaths
of:assignments
Proposition2.2.Letbeatime-boundednondeterministicTuringmachineas
above.Thereexistsaformulaoftheform,suchthatPathacceptforallinputsoflengthandforall,wehavethatacceptsonpathiff.Here,PathexpressesPathaccept
thatencodesapathcorrespondingtonondeterministicguesses,andacceptexpressesthatthepathencodedbyisaccepting.
Proof.(Sketch.)Weslightlymodifytheconstructionin[Fag74]byintroducinga
-arysecond-orderpredicatesuchthatitsassignmentrepresentsthenondeter-ministicchoiceforeachstepofthecomputation.Thatis,foreachassignment
uthereexistsexactlyoneassignmentsuchthatPath.
3Lindstr¨omQuantifiers
Inordertoextendthelimitedcapabilitiesoffirst-orderpredicatelogicithasbeentried
toenhanceitsexpressivepowerbyaddingdifferentsortsofoperatorsorquantifiers.OnesystematicandformallyelegantapproachtothisistoconsidersocalledLindstr¨omquantifiers.
Afirst-orderformularelationdef
with
freevariablesdefinesforeverystructure
,see[EF95].
the
Nowtheideaunderlyingthedefinitionofgeneralizedquantifiersisthefollowing:Considertheclassicalfirst-orderexistentialquantifierappliedtosomequantifier-freeformulawithfreevariable,i.e.,considertheformula.Givenanorderedfinitestructure,iff.Analogouslywegetiff
(istheuniverseof).[Str94]definesmodularquantifiersasfollows:
iffmod.Thusitisverynaturaltodefinegeneralized
quantifiersbyconsideringarbitraryconditionsonrelationsdefinedbyformulae.
StructoverasignaturePEveryclassofstructures
definesthefirst-orderLindstr¨omquantifierasfollows:Letbefirst-orderformulaeoversignaturesuchthatforthenumberoffree
6
variablesinisequaltothearityof.ThenaFOformula.IfStruct,then
is
iff
Wewanttostressthefollowing
andtheelementsofturesboth
isrelatedtostructure
verse.Inthejustgivendefinition,theorderofinbothcasestobe
asfollows:Ifsemanticsof
point:Sinceweonlydealwithorderedstruc-areordered.Inthejustgivenequivalence
,i.e.astructurewiththesameuni-wemadetheconventionthathereweassumeidentical.Tobemoreexplicit,wedefinetheisanorderedstructure,then
iff.
forFollowing[Got95]wealsowrite
denotethesubclasseswherealltheformulae
FO.Moreoverlet
areprenex(
()
)formulae.
ThejustgivendefinitionisessentiallytheoriginaldefinitiongivenbyLindstr¨om[Lin66],whichthereaderwillalsofindintextbooks[Ebb85,EF95]andformulatedwithslightvariationsbutequivalentlyin[Got95].Forourexaminations,thefollowingformulationwillbeuseful(observethatthisonlymakessensefororderedstructures):Givenafirst-orderformulawithfreevariablesandacorrespondingfiniteor-deredstructure,thisdefinesthebinarystringoflength(),thesocalledcharacteristicstringof.Nowgivenasequenceofformulaewithfreevariableseachandastructure,wesimilarlygetthetuple,where.Certainly,thereisaone-onecorrespondencebe-tweensuchtuplesandstringsoflengthoveralargeralphabet(inourcasewithelements)asfollows.Letbesuchanalphabet.Fixanarbitraryenumerationof,i.e..Thencorrespondstothestring
,wherefor,,forthatwhoselength
binaryrepresentation(possiblywithleadingzeroes)isgivenby.Insymbols:.
isinfirst-orderThisleadsustothefollowingdefinition:Asequencewordnormalform,iffthehavethesamenumberoffreevariables.NextweshowthatifwerestrictsuchthattheFOpartisrequiredtobeinfirst-orderwordnormalformwegetnolossinexpressivepower.
Lemma3.1.LetbeaFOformulaoversigna-StructforarbitraryP.Thenthereareasigna-ture.Let
ture,aclassofstructuresStruct,andfirst-orderformulaeoverinwordnormalformsuchthatModMod.
7
Proof.Letbethemaximalarityofpredicatesymbols()in.Definetoconsistofforalinearorderpluspredicatesofarityeach.Definetoconsistofexactlythosestructuresforwhichthereisan
suchthatforallwehave:
(whereisthearityof,andisasymbolfor
theminimalelementin).Forthecharacteristicstringsthishastheconsequencethat
.Nowitisnottoohardtobuildtheformulaesuchthat
forall,.u
ThusthefollowingdefinitionofLindstr¨omquantifiersoverlanguagesisequivalent(w.r.t.expressivepower)totheoriginaldefinitionofquantifiersoverarbitrarystructureclasses:
Let
,andlet
beinfirst-orderwordnormalform.Letbeanalphabetsuchthat.Theniff
.
WeremarkthatourdefinitionofLindstr¨omquantifiersoverlanguagesresembles
verymuchthedefinitionofgroupquantifiersfrom[BIS90].Ifisthewordproblemofsomefinitegroup,theninournotationisexactlythegroupquantifiergivenby.
Tocharacterizethepowerofleaflanguagesdefinedwithintroducesecond-orderLindstr¨omquantifiers.
formulae,wenow
Givenaformulawithfreesecond-ordervariablesandastructure,define,andletbethedef
correspondingcharacteristicstring,theorderofvectorsofrelationsbeingthenaturaloneinducedbytheunderlyingorderoftheuniverse.Ifthearitiesofare
,resp.,thenthelengthofis.
Letbeasignature,wherefor
.Thusisasignatureconsistingofalinearorderplusasequenceofsignatureswithonlypredicatesymbolseach.Letbethearityof.Asecond-orderstructureofsignatureisatuple,whereforevery,
.Givennowasignatureandsecond-orderformulaeoverwhereforeverythenumber
andarityoffreepredicatesincorrespondsto.Letbeaclassofsecond-orderstructuresover.ThenisaSOformula.If
Struct,then
iff
8
Againwewouldliketostressthatweassumetheorderonsidesoftheequivalence.
tobethesameonboth
Again,wewanttotalkaboutsecond-orderLindstr¨omquantifiersdefinedbylan-guages.Thuswedefineanalogouslytotheabove:Asequence
ofsecond-orderformulaeisinsecond-orderwordnormalform,ifthehavethesamepredicatesymbols,i.e.intheaboveterminology
.Letforthearityofbe.Observethatinthiscase,
(for),thuscorre-spondstoawordofthesamelengthoveranalphabetofcardinality.Asbefore,we
canassumesecond-orderwordnormalformwithoutlossofgenerality:
Lemma3.2.LetbeaSOformulaover
signature.Letbeaclassofsecond-orderstructuresoversomesigna-turewherefor.Thenthereareasecond-orderstructureoverasuitablesignatureandformulaeoverinsecond-orderwordnormalformsuchthatModMod.
Proof.TheproofissimilartotheproofofLemma3.1.Definesuchthatforeachcontainspredicatesymbols,whereisthemaximalnumberofpredicatesymbolsinany,.Thethpredicatesymbolinanyisofarity,whereisthemaximalarityofallthepredicatesymbolsinany,
.consistsofthosesecond-orderstructures
forwhichthereisaninsuchthatforwehave.Hereisthedef
numberofpredicatesymbolsin,andisobtainedfromasinLemma3.1.Nowitisanottoohardexercisetodefineformulaesuchthatthefollowingholds:whichimpliesthestatementofthelemma.u
Letbeasequenceofsecond-orderformulaeinsecond-orderwordnormalformasabove.Givennowalanguagewith
,thesecond-orderLindstr¨omquantifiergivenbyisdefinedby
iff.Lemma3.2showsthat
second-orderLindstr¨omquantifiersgivenbylanguagesareequivalent(w.r.t.express-ibilitypower)tothosegivenbyarbitrarysecond-orderstructures.
Similarlytotheabove,()denotesthosesubclassesofSO,wherealltheformulaeareprenex()formulae.Foraclassoflanguagesweusethenotationwiththeobviousmeaning,e.g.FOdenotestheunionofallFOoverall.
9
4Padding
Inthesequelwewilluselogicallydefinedleaflanguages.Asalreadypointedoutinthepreliminaries,paddingsometimesplaysacrucialroleintheleafcontext.Thuswewillconsiderbesidespaddingonlanguagesdefinedearlieralsopaddingonmodelclasses.FromthedefinitionoflogicallydefinedleaflanguagesinSect.2itisclearthatwearemainlyinterestedinstructureswhichareimagesoftheencoding.
Lettheencoding
besuchthat
thsymbolof
for
,
,where
.
and
isthe
Let,whereallpredicatesymbols(
Structthesamearity.Forastructure
.
)areof
let
def
Theideabehindpaddingonstructuresisthatwewanttoinsertapaddingsymbolinatupleofcharacteristicstrings,i.e.in.Forthisend,wehavetoextendouralphabetbyapaddingsymbol.Actually,whatwedoiswetakeasnewalphabet
andallsymbolsinmaybedef
usedaspaddingsymbols.Moreformally:
Let,whereisofthesamearityastheotherdef
predicatesymbols.DefinepadStructasfollows:paddef
pad.(Herepadreferstopaddingonstringsasdefinedin
Sect.2.)Ifisamodelclass,thenpadpad.Ifisaclassofdefmodelclasses,thenpad.defpad
Wesayalogicisclosedunderpaddingiffthecorrespondingclassofmodelclassesis,i.e.ifpadModMod.
In[Bur96]somelogicsclosedunderpaddingandsomenotclosedunderpaddingareidentified.Theinourcontextrelevantresultsarethefollowing.Proposition4.1.
1.For
,
and
areclosedunderpadding.
2.Ifisclosedunderpadding,thenforall.
and
areclosedunderpadding
Proof.(Sketch.)Theprincipalideaisthatonehastorelativizetheoccurringquan-tifiers,e.g.insteadof“forallpositions”wenowhave“forallpositionsuchthatthethletterisnotapaddingsymbol.”Thiscertainlydoesnotaffectthelinearor-der.Concerningtheotherrelations,thesuchobtainedformuladoesexactlywhatisrequired,i.e.itmodelsthepaddedversionoftheoriginalmodel.Moredetailscanbefoundin[Bur96].u
10
5MainResults
Beforewecometoourmainresultweexamineleaflanguagecharacterizationsoftheclassesofthepolynomialtimehierarchy.Lemma5.1.LeafP
forall
.
p
-LOGTIMEwasproved.Thus,sinceIn[JMT94],LeafP
p
-LOGTIMEand[Sto73],ourlemmafollows,butwegiveanewproofhere,sincewewanttogeneralizeitlater.
Proof.ForagivenisticTuringmachinethat
-formulaandapolynomiallytime-boundednondetermin-,weconstructaformulaandthenshowforall
iff
LeafP
Letbeapolynomiallytime-boundednondeterministicTuringmachine.Letus
firstconsiderthecase,that,namelythesetofsymbolsthatproducesoneverycomputation-path(seeSect.2),hastwoelements.Wewilldiscusstheothercaseattheendoftheconstruction.
bethe-formulawhichformalizestheLetPathaccept
computationofasdescribedinSect.2,Proposition2.2.Anassignmentofrep-resentsthenondeterministicchoices.Forafixedassignmentofthereexistsexactlyoneassignmentofthatrepresentsacomputationpathof.ForallsuitablefiniteorderedstructurestheformulaPathistrueon,iffrepresentsacorrectcomputationpathw.r.t.thenondeterministicchoicesgivenby.
Let
bethe
-formulaover
oftheform
Weconstructa-formula
inthefollowingway:
byreplacingthevariablesandatomicpredicatesin
[]Wereplaceallfirst-ordervariablesinfordowntobytuplesofsecond-ordervariablesandthustransformtheexistentialfirst-orderquantifierthatbindsintoasequenceofsecond-orderquantifiersthatbindand.Toensurethatanassignmentofrepresentsacorrectcomputationpath,wereplaceby
.Inordertoobtainaformulainprenexnormalform,wePath
havenovariablesincommon.renamethevariablesinPathsuchthatPathand
11
[]WereplacetheuniversalquantifierwerenamethevariablesinPathsuchthat
byPathand
.Again
havenovariablesincommon.
Path
[]Wereplaceeachoccurrenceofbythe-formula
byasuitablerenamingofthevariables.weobtainfromaccept
accept
,which
[]Wehavetoextendtheorderingthatisgivenintheorderedstructureto
assignmentsof.Thiscanbeachievedbywell-knowntechniques.
AsdescribedinSect.2,itispossibletoencodethesymbolsofinbinary.For,wehavetoconsiderfirst-orderformulaeoversignaturesthathavelogunarypredicates.Wereplaceeachbyaformula.Foreach
weobtainfromacceptaformulawhichistrue,iffproducesontherepresentedpath.Theformulaisadisjunctionoftheformulaeforthose,suchthatthe-thbitinthebinaryencodingofis1.
ToseethatLeafP,iffMod,forall,observethatthereisaone-onecorrespondencebetweentheelementsintheuniverseof(thepositionsofthesymbolsintheleafstring)andtheassignmentsof.
u
Lemma5.2.
LeafP
forall
.
FO,thislemma(incontrasttoLemma5.1)doesnotSinceevenDLOGTIME
p
followfromLeafP-LOGTIMEprovedin[JMT94],butinfactstrengthenstheirresult.
Proof.Letbeaformulawithsecond-ordervariables.Weconstructapolynomiallytime-boundedNTMandaformuladefiningaleaf-languageMod,suchthatforallorderedfinitestructuresoverthecorrespondingsignature:ModiffLeafP
OninputtheNTMdeterminesnondeterministicallytheassignmentsofthesecond-ordervariablesfromto.Thatis,oneachcomputationpath,writesthecharacteristicsequenceofonepossibleassignmentonitsworktapes.Usingthesecharacteristicsequences,evaluatesthefirst-orderpartof.Weusetwoleafsymbolsandtodenotetheresultoftheevaluation.
Forformulas,thecorrespondingleaflanguageisdefinedbyformulasthecorrespondingleaflanguageisdefinedby.
,andfor
)the
For,wehavetomarkforallsecond-ordervariablespathsthatsharethesameassignmentofasshowninFig.1.
(
12
Figure1:Constructionofmachine
Weintroducenewleafsymbolssymbolsofoftheleafstringbetweenandsharethesameassignmentfor.
and.The
correspondtoallthosepathsthat
Asdescribedinthepreliminaries,thesymbolsofcanbeencodedusinglogunarypredicates.Bybooleancombinationsofthese,weconstructformulaethatex-.Weabbreviatethesepressthatapathproduces,,,orfor
formulaeby,,,andresp.Theformulawillbeabbreviatedbymarked.
For
letRegion
beanabbreviationfortheformula
For
left
weconstructinductivelyasequenceofformulae
betheformularight
.Let
left
right
iftherightmostquantifierisexistentialand
left
left
marked
otherwise.Forthe-thquantifierblockletusfirstconsiderthecase,
thatthequantifierblockitselfconsistsofexistentialquantifiersandthatthequantifierblocktotherightconsistsofuniversalquantifiers.Letbetherightmostvariableinthe-thquantifierblock.Wedefinetobetheformulaleftright
left
right
left
left
right
right
Region
left
right
left
right
13
Transformingthisintoprenexnormalformwegetaquantifierprefixstartingwith
.Letusnowconsiderthecase,thatthe-leftrightleftrightthquantifierblockconsistsofuniversalquantifiersandthatthequantifierblockstotheleftandtotherightconsistofexistentialquantifiers.Letbe
totherightmostvariableinthe-thquantifierblock.Wedefineleftright
betheformula
left
right
left
left
right
right
Region
left
right
left
right
Transformingthisintoprenexnormalformwegetaquantifierprefixstartingwith
.leftrightleftright
Letbetherightmostvariableinthefirstquantifierblock.If
betheformulaquantifiedthenlet
isexistentially
left
right
Region
left
right
left
right
otherwiselet
be
left
right
Region
left
right
left
right
u
FromLemma5.1andLemma5.2wegetthefollowingleaflanguagecharacteriza-tionoftheclassesofthepolynomialtimehierarchy:Theorem5.3.LeafP
forall
.
Acloseinspectionoftheproofin[Fag74]showsthatthereisadirectcorre-spondencebetweencomputation-pathsandassignmentsoftheexistentiallyquantified
second-ordervariables.Thus,usingsecond-orderLindstr¨omquantifierswecande-scribetheconceptofleaflanguagedefinabilityintermsofmodel-theoreticnotions.Note,thatwedonotrequirethecomputationtreetobeafullbinarytree.
Proposition5.4.Letbealanguage,letbeanumbersuchthat,andletbeanondeterministicpolynomialtimemachineasdescribedinSect.2(i.e.withallpathsofthesamelength).ThenthereexistsaformulaandPath
suchthatasequenceofformulaeleafleaf
Leaf
Mod
Path
leaf
Path
leaf
14
Proof.Letbetheformula,whichisdescribedinPropo-Pathacceptsition2.2.Foreachcomputationpathofoninputthereexistsexactlyoneassign-mentsuchthat
Path
Forwemodifytheformulaacceptsuchthatitistrue,iffproducestheleafsymbol.Wedenotetheresultingformulabyleaf.Inthecorrespondingencodingoftheunarypredicateistrue,iffisproduced.Thus,wehave
Leaf
iff
Mod
Path
Forweconstructtheformulaeleaffromacceptaccord-leafingtotheencoding(seeSect.3):Forallletbeaformulathatistruefor,iffproducestheleaf-symbolonthepaththatcorrespondsto.Eachformulaleafnowconsistsofadisjunctionofallsuchthatthe-thbitinthebinaryrepresentationofisone.u
Corollary5.5.Let
beaclassoflanguages.
LeafP
Thesecond-orderLindstr¨omquantifierintheabovepropositionisappliedto-formulaeinordertoruleoutthoseassignmentsofthatdonotcorrespondtocompu-tationpathsof.Forlanguageclassesthatareclosedunderpadding(seeSect.4)wecangetridofthesecond-orderexistentialquantifier.Wemapthoseassignmentsofthatdonotcorrectlyrepresentacomputationpathoftothepaddingsymbol.
Lemma5.6.Let
beaclassoflanguagesthatisclosedunderpadding.Then
LeafP
LetbeanondeterministicTuringmachine,,and
beformulaeasdescribedinProposition5.4suchthatLeaf
Mod.WemodifythisformulasuchthattheLind-str¨omquantifierbounds,also.Asmentionedabove,wemapthoseassignmentsofthatdonotcorrectlyrepresentancomputationpathoftothepaddingsym-bol.AccordingtoSect.4,wehavetoextendthesequencebyanadditionalformula.Thenforallassignmentsthecorrespondingsymbol
isapaddingsymbol,iffistruefortheassign-in
Proof.():
ment.Theformulaistrue,iffforgivenassignmentsthePath
doesnotcorrectlyrepresentacomputationpathofwithrespecttoassignment
15
thenondeterministicchoicesrepresentedbyindicatethepaddingsymbol.Thuswehave
Leaf
.Wethereforeuse
Path
to
Mod
pad
Path
():Forprovingthisinclusionwedonotneedthefactthatisclosedunderpadding.
andwecanconstructapolynomial-timenon-Forgiven
deterministicTuringmachinewhichnondeterministicallyguessestheassignments
deterministically.Theofandafterwardsevaluatestheformulae
resultingbitstringisusedtodeterminethecorrectleafsymbolaccordingto.u
Combiningourleaflanguagecharacterizationsoftheclassesofthepolynomialtimehierarchy(Theorem5.3)withthejustgivenlemma,wenextexamineleaflan-guagesdefinedbyfirst-orderformulaestartingwithaLindstr¨omquantifier.Lemma5.7.Let
bealanguage.Thenwehaveforall
LeafP
:
pad
Proof.WecombineLemma5.1andLemma5.6toprovethislemma.
Letandbea-formula.AsintheproofofTheorem5.1wemaythinkofuniverseshavingcomputationpathsofaselements.Wetransformthefirst-orderformulaeintosecond-orderformulaeasintheproofof
intosecond-Theorem5.1.Inadditionwetransformthefreevariablesordervariables.ButasintheproofofLemma5.6,wehavetoconsiderthoseassignmentsforanythatdonotrepresentacomputationpathof.Tomapthoseassignmentstopaddingsymbolsweaddaformula
.Weget:Path
Leaf
Mod
pad
u
Lemma5.8.Let
bealanguage.Thenwehaveforall
:
LeafP
pad
Proof.ToprovethislemmawecombineLemma5.2andLemma5.6.andformulaForgiven
weconstructapolynomial-timeTuringmachine
suchthatpad
anda
-formula
16
Mod
Leaf
pad
.
guessesnondeterminis-SimilartotheproofofLemma5.6theTuringmachine
ticallyallassignmentsof.Thereisasubstringoftheresultingleafstringforeachassignmentof.Thesesubstringsstart(ontheleft)withandend(ontheright)with.Thefirst-orderLindstr¨omquantifierboundstwovariablesleftandright.Theassignmentsshouldpointtotheleftandrightboundaryofsomesubstring.WemapassignmentsthatdonotcorrectlyrepresentsuchboundariestopaddingsymbolsasintheproofofLemma5.6.Letbeaformulathatistrueiffthesymbolatpositionintheleafstringis.Wethenconstructtheformulaleftrightthatindicatesthepaddingsymbolasfollows:
left
right
left
right
left
right
WeconstructforeachformulaLemma5.1.simulatesmachinesinFig.2.
aTuringmachineasintheproofof
foreachassignmentofasshown
Figure2:Constructionofmachine
Wenowconstructforeachformulaafirstorderformula.AsintheproofofLemma5.1weconstructinductivelyasequenceofformulae
.Theconstructionofisidenticaltotheconstruc-tiongivenintheproofof5.1.Letbetherightmostvariableinthefirstquantifier
17
blockofandRegionbetheformulagivenintheproofofTheorem5.1thatistrue,ifftheassignmentofandpointtotheleftandrightboundaryofthesubstringthatcorrespondstosomeassignmentof.Bythedefinitionofwemayassumew.l.o.g.thatisexistentiallyquantified.Letleftrightbetheformula
left
right
left
left
right
right
Region
left
right
left
right
u
ThemaintheoremnowfollowsfromLemma5.7andLemma5.8.Theorem5.9.Lethaveforall:
beaclassoflanguagesthatisclosedunderpadding.Thenwe
LeafP
Wecannotgetasimilarresultfor-formulaesincetheformulaleftrightusedintheproofofLemma5.8isexistentiallyquantified.Howeverthefollowingcertainlyholds:
Corollary5.10.Lethaveforall:
beaclassoflanguagesthatisclosedunderpadding.Thenwe
LeafP
Finally,wewanttoaddressaninterestingspecialcase:theclassPSPACE.Bar-rington,Immerman,andStraubingshowedthatfirst-orderlogicwithgroupquantifiersdefinesexactlytheregularlanguages[BIS90].Hertrampfetal.[HLS93]whocharac-terizedPSPACEbyregularleaflanguagesshowedthatinfactforthischaracterizationalreadyonesingleregularlanguage,thewordproblemforthegroup,issufficient.Thus,thisleaflanguagecharacterizationyieldsthefollowing:
Corollary5.11.PSPACE
6Discussion
Aswehaveseen,Lindstr¨omquantifierswhichareawellstudiedlogicalconcepthaveacomplexitytheoreticcounterpart:thesocalledleaflanguagedefinability,whichhasbeenstudiedintensivelyintherecentpast.
18
Second-orderLindstr¨omquantifiersdefine(inamodeltheoreticsense)exactlythoselanguagescharacterizablebyleaflanguagesforpolynomialtimemachines.IfisaLindstr¨omquantifier,thenthelogicdefinesthecomplexityclassLeafP.Thusitmaybepossiblethatresultsaboutleaflanguagescontributetothestudyoftheexpressivepowerofsecond-orderLindstr¨omquantifiersonorderedfinitestructures,andviceversa.
Ofcourse,itwouldbenicetohavealeaflanguageanalogueforfirst-orderLind-str¨omquantifiers.Tobeabletodothisonewillhavetoconsider“leaflanguagesforFO”insteadofleaflanguagesforpolynomialtime.Tobemoreprecise,whatisanappropriaterestrictionofthecomputationmodelproducingleafwords?
Gottlobin[Got95]showedthatundersomeparticularassumptionsto,first-orderformulaewitharbitrarilynestedandexistentialanduniversalquantifiersyieldsuper-classesofL(thelogspacedecidablesets).Certainly,formulaewithnestedquan-tifiersshouldbeexaminedalongthelinesofthispaper,i.e.whenusedtodefineleaflanguages.
Furthermore,oneshouldconsiderleaflanguagesdefinedbysecond-orderformu-laetoinvestigatethestructureofcomplexityclassesaboveexponentialtime,e.g.theexponentialtimehierarchy.
Acknowledgment.WethankDavidBarringtonforsuggestingtheexaminationoflogicallydefinedleaflanguagesasaninterestingtopic.Thanksarealsoduetotheanonymousrefereesforhelpfulcomments.
References
[All96]
E.ALLENDER.Anoteonuniformcircuitlowerboundsforthecountinghierarchy.InProceedings2ndInternationalComputingandCombina-toricsConference(COCOON),volume1090ofSpringerLectureNotesinComputerScience,pages127–135,1996.
D.P.BOVET,P.CRESCENZI,ANDR.SILVESTRI.Auniformapproachtodefinecomplexityclasses.TheoreticalComputerScience,104:263–283,1992.
D.A.M.BARRINGTON,N.IMMERMAN,ANDH.STRAUBING.Onuni-formitywithinNC.JournalofComputerandSystemSciences,41:274–306,1990.
[BCS92]
[BIS90]
19
[BL96]
B.BORCHERTANDA.LOZANO.Succinctcircuitrepresentationsandleaflanguageclassesarebasicallythesameconcept.InformationPro-cessingLetters,58:211–215,2996.
H.J.BURTSCHICK.Berechnungs-undBeschreibungskomplexit¨atvonZ¨ahlfunktionenundLindstr¨omquantoren.PhDthesis,FachbereichInfor-matik,TU-Berlin,1996.
[Bur96]
´RIEN,ANDH.VOLLMER.Non-[CMTV96]H.CAUSSINUS,P.MCKENZIE,D.THE
[Ebb85]
[EF95][Fag74]
[Got95]
[Her95]
[HLS93][HVW95]
[HVW96]
deterministicNCcomputation.InProceedings11thComputationalComplexity,pages12–21,1996.ToappearinJournalofComputerandSystemSciences.
H.-D.EBBINGHAUS.Extendedlogics:Thegeneralframework.InJ.Bar-wiseandS.Feferman,editors,Model-TheoreticLogics,PerspectivesinMathematicalLogic,chapterII,pages25–76.SpringerVerlag,1985.H.D.EBBINGHAUSANDJ.FLUM.FiniteModelTheory.Springer,1995.R.FAGIN.Generalizedfirst-orderspectraandpolynomialtimerecogniz-ablesets.InR.Karp,editor,ComplexityofComputations,pages43–73,1974.
G.GOTTLOB.Relativizedlogspaceandgeneralizedquantifiersoverfi-nitestructures.TechnicalReportCD-TR-95/76,InstitutforInformationSystems,ViennaUniversityofTechnology,1995.Anextendedabstractappearedintheproceedingsofthe10thSymposiumonLogicinCom-puterScience,1995.
U.HERTRAMPF.Regularleaf-languagesand(non-)regulartreeshapes.TechnicalReportA-95-21,Institutf¨urMathematikundInformatik,Medi-zinischeUniversit¨atzuL¨ubeck,1995.
U.HERTRAMPF,C.LAUTEMANN,T.SCHWENTICK,H.VOLLMER,ANDK.W.WAGNER.Onthepowerofpolynomialtimebit-reductions.InProceedings8thStructureinComplexityTheory,pages200–207,1993.
U.HERTRAMPF,H.VOLLMER,ANDK.W.WAGNER.Onthepowerofnumber-theoreticoperationswithrespecttocounting.InProceedings10thStructureinComplexityTheory,pages299–314,1995.
U.HERTRAMPF,H.VOLLMER,ANDK.W.WAGNER.Onbal-ancedvs.unbalancedcomputationtrees.MathematicalSystemsTheory,29:411–421,1996.
20
[JMT94]
´RIEN.LogspaceandlogtimeB.JENNER,P.MCKENZIE,ANDD.THE
leaflanguages.InProceedings9thStructureinComplexityTheory,pages242–254,1994.
¨.Firstorderpredicatelogicwithgeneralizedquantifiers.P.LINDSTROM
Theoria,32:186–195,1966.
C.H.PAPADIMITRIOU.ComputationalComplexity.Addison-Wesley,1994.
L.STOCKMEYER.Thepolynomial-timehierarchy.TheoreticalComputerScience,3:1–22,1973.
H.STRAUBING.FiniteAutomata,FormalLogic,andCircuitComplexity.Birkh¨auser,1994.H.VEITH.Succinctrepresentation,leaflanguages,andprojectionreduc-tions.InProceedings10thStructureinComplexityTheory,pages118–126,1996.
N.K.VERESHCHAGIN.Relativizableandnon-relativizabletheoremsinthepolynomialtheoryofalgorithms.IzvestijaRossijskojAkademiiNauk,57:51–90,1993.InRussian.
[Lin66]
[Pap94]
[Sto73]
[Str94]
[Vei96]
[Ver93]
21
因篇幅问题不能全部显示，请点此查看更多更全内容