Links花生壳免费域名
花生壳免费域名 时间:2021-01-02 阅读:()
TheStructureofFreeDomainSemiringsP.
Jipsen,G.
StruthChapmanUSheeldApril9,2008P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20081/1OutlineIntroductionDomainSemiringsFreedomainsemiringRepresentationbybyantichainsofsequencesRepresentationbybinaryrelationsConclusionP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20082/1IntroductionAsemiringisoftheform(A,+,0,·,1)suchthat(A,+,0)isacommutativemonoid(A,·,1)isamonoid·distributesoverallnitejoinsfromtheleftandrighti.
e.
x(y+z)=xy+xz,(x+y)z=xz+yzandx0=0x=0Asemiringisidempotentifx+x=xISisthevarietyofidempotentsemiringsLemmaAnidempotentsemiringisa(join-)semilatticewith0asbottomelement,withx≤ygivenbyx+y=y(since+isassoc,commuandidempotent)andx≤y=wxz≤wyz(sincew(x+y)z=wxz+wyz)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20083/1ExamplesExamplesofsemiringsare:Rings(N,+,0,·,1).
.
.
Examplesofidempotentsemiringsare:Reductsofrelationalgebras(A,+,0,;,1)ReductsofKleenealgebras(A,+,0,·,1)Reductsofresiduatedlattices(A,1)(R∪{∞},max,0)Boundeddistributivelattices(A,∨,0,∧,1).
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20084/1FreemonoidsandsemiringsLetXbeasetofvariables(orgenerators)ThefreemonoidoverXisX=n∈NXnwith1=emptysequenceand·asconcatenationBydistributivity,everytermtinthesignatureofsemiringscanbewrittenasanitejoinoftermsofthefreemonoidXExample:x(y+xz)(x+1)=xyx+xxzx+xy+xxzthefreeidempotentsemiringoverX,denotedbyFIS(X),isisomorphictothesetPn(X)ofallnitesubsetsofwordsoverXHereU+V=U∪VandU·V={uv:u∈U,v∈V}P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20085/1Decidabilitytheequationaltheoryofidempotentsemiringsisdecidable:Giventermss,t,usedistributivitytowritetermsinnormalformHowever,thequasiequationaltheory(=strictuniversalHorntheory)isundecidablebecause:Thewordproblemforsemigroupsisundecidable(Post)Everysemiringisasemigroupundertheoperation"·"EverysemigroupSisa"·"-subreductofitspowersetsemiringP(Se)(whereSethemonoidextensionofS)theclassof"·"-subreductsofsemiringsistheclassofallsemigroupsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20086/1DomainmonoidsAdomainmonoidisanalgebra(M,·,1,d)suchthat(M,·,1)isamonoidandd:M→Misafunctionthatsatises(D1)d(x)x=x(D2)d(xd(y))=d(xy)(D3)d(d(x)y)=d(x)d(y)(D4)d(x)d(y)=d(y)d(x)ThevarietiesofdomainmonoidsisdenotedbyDMLemmad(1)=1[takex=1in(D1)]d(d(x))=d(x)[takex=1in(D2)]d(x)d(x)=d(x)[takey=xin(D3)]d(M)={d(x):x∈M}isameetsemilatticewith1=topelementP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20087/1DomainsemiringsAdomainsemiringisanalgebra(A,+,0,·,1,d)suchthat(A,+,0,·,1)isasemiring(A,·,1,d)isadomainmonoidandthefollowingadditionalaxiomshold[Desharnais,Struth2008]d(x+y)=d(x)+d(y),d(0)=0andd(x)+1=1xd(x)+x=xx+x=xEverydomainsemiringisanidempotentsemiringThevarietiesofdomainsemiringsisdenotedbyDSP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20088/1ExamplesofdomainsemiringsExamplesofdomainsemiringsaree.
g.
reductsofrelationalgebraswithd(x)=(x;x)∧1,reductsofKleenealgebraswithdomainModelsofdomainsemiringsinCS:Idempotentsemiringsformedbysetsoftracesofaprogram(whicharealternatingsequencesofstateandactionsymbols)withdomaindenedbystartingstatesoftracesIdempotentsemiringsformedbysetsofpathsinagraphwithdomaindenedbysetsofstartingstatesApplicationsofdomainsemiringsandKleenealgebraswithdomainhavebeenstudiedintensivelyP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20089/1ApplicationsofdomainsemiringsThedomainoperationmodelsenablednessconditionsforactionsinprogramsandtransitionsystemsThedomainoperationcaneasilybeextendedintoamodaldiamondoperatorthatactsontheunderlyingalgebraofdomainelements[M¨oller,Struth2006]Linksthealgebraicapproachwithmoretraditionallogicsofprogramssuchasdynamic,temporalandHoarelogicsSomestandardsemanticsofprograms,includingtheweakestpreconditionandweakestliberalpreconditionsemantics,canbemodeledinthissettingApplicationscanbefoundinRelMiCSconferenceproceedingsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200810/1DomainsemiringsDomainsemiringswereoriginallyintroducedinatwo-sortedsettingThedomainoperationmapsarbitrarysemiringelementstoaspecialBooleansubalgebra[Desharnais,M¨oller,Struth2006]ArbitrarysemiringelementsmodelactionsofaprogramortransitionsystemTheelementsoftheBooleansubalgebramodelthestatesofthatsystemHereweusethesimplerandmoregeneralone-sortedapproachof[Desharnais,Struth2008]P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200811/1StudyingfreedomainsemiringsThefreedomainsemiringisinterestingforapplications:IdentiesexactlythosetermsofdomainsemiringsthathavethesamedenotationinalldomainsemiringsAllowsthedenitionofecientproofanddecisionproceduresThedomainaxiomsofdomainsemiringsarethesameasforrelationalgebrasandforKleenealgebraswithdomainBothrelationalgebrasandKleenealgebrashaverichandcomplex(quasi)equationaltheoriesRatherstudythesimplerequationaltheoryofdomainsemiringsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200812/1OutlineofresultsAim:giveanexplicitdescriptionoffreedomainsemiringsFDS(X)FirstdescribefreedomainmonoidFDM(X)ThenshowthattheseelementsarethejoinirreduciblesofFDS(X)FDS(X)isisomorphictothesetofniteantichainsintheposetofjoinirreduciblesShowFDS(X)isrepresentablebyaconcretealgebraofbinaryrelations,withrelationaldomainasoperationsDS=HSP{Relationaldomainsemirings}Finallyshowanydistributivelatticewithni-aryoperatorsoccursasdomainelementsofsomedomainsemiringwithni1-aryoperatorsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200813/1One-generateddomainterms(D1)d(x)x=x(D2)d(xd(y))=d(xy)(D3)d(d(x)y)=d(x)d(y)Asusual,wedenex0=1andxn+1=xnxLemmaInadomainmonoid,ifm≤nthend(xm)xn=xnandd(xm)d(xn)=d(xn)Proof.
Assumingm≤n,wewritexn=xmxnm,andusing(D1)wehaved(xm)xn=d(xm)xmxnm=xmxnm=xnNow(D3)impliesd(xm)d(xn)=d(d(xm)xn)=d(xn)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200814/1ExpandednormalformsOnelementsoftheformd(xj),theorderisinducedbythemeet-semilatticestructure:d(xj)≤d(xk)ij≥k,hencetheseelementsformachainForconcatenationsofbasicterms,rewritetheminexpandednormalform:d(xj0)xd(xj1)xd(xj2)x···xd(xjm)whereeachofthejk≥max{1+jk+1,2+jk+2,mk+jm}E.
g.
xd(x3)x2d(x2)=.
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200815/1DecreasingsequencesofnumbersForbrevitydenotesuchatermbythesequence(j0,j1,j2,jm)NotethatthisisalwaysastrictlydecreasingsequenceofnonnegativeintegersLetP=(P,≤)bethesetofallsuchsequences,orderedbyreversepointwiseorderThussequencesofdierentlengtharenotcomparable,andthemaximalelementsofthisposetare(0),(1,0),(2,1,0),.
.
.
correspondingtothetermsd(1)=1,d(x)xd(1)=x,d(x2)xd(x)xd(1)=x2,.
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200816/1Theposetofjoin-irreduciblesbelow1andxd(x5)d(x4)d(x3)d(x2)d(x1)1=d(x0)(5)(4)(3)(2)(1)(0).
.
.
xd(x2)xd(x3)xd(x4)xd(x5)xd(x6)x(1,0)(2,0)(3,0)(4,0)(5,0)(6,0).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
d(x6)xd(x)d(x6)xd(x2)d(x6)xd(x3)d(x6)xd(x4)xd(x5)(6,1)(6,2)(6,3)(6,4)(6,5)(5,4)=xd(x4)(4,3)=xd(x3)(3,2)=xd(x2)(2,1)=xd(x)(5,3)=d(x5)xd(x3)(4,2)=d(x4)xd(x2)(3,1)=d(x3)xd(x)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200817/1Theposetofjoin-irreduciblesbelowx2x2=(2,1,0)(3,1,0)(4,1,0)(5,1,0)(6,1,0).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
(6,2,0)(6,3,0)(6,4,0)(6,5,0).
.
.
.
.
.
.
.
.
.
.
.
(6,4,3)(5,3,2)(4,2,1)(3,2,1)(4,3,2)(5,4,3)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200818/1TheproductoftwodecreasingsequencesAmultiplicationisdenedonPbythefollowing"rippleproduct"(j0,j1,j2,jm)·(k0,k1,k2,kn)=(j′0,j′1,j′2,j′m,k1,k2,kn)wherej′m=max(jm,k0)andj′i=max(ji,j′i+1+1)fori=m1,2,1,0Forexample,(7,3,2)·(4,3,1)=(7,5,4,3,1),while(4,3,1)·(7,3,2)=(9,8,7,3,2)CanshowthatthisistheresultofmultiplyingthecorrespondingexpandednormalformsandrewritingresultinexpandednormalformItistediousbutnotdiculttocheckthatthisoperationisassociativeP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200819/1DomainandpartialorderThedomainofasequence(j0,j1,j2,jm)isthelength-onesequence(j0)Thiscorrespondstothedomaintermd(xj0)LetA(P)bethesetofniteantichainsofPApartialorderisdenedonA(P)bya≤bi↓a↓bThemultiplicationisextendedtoantichainsbyusingthecomplexproduct(i.
e.
U·V={uv:u∈U,v∈V})andbyremovingallnon-maximalelementsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200820/1RepresentationTheoremTherstresultshowsthattheone-generatedfreedomainsemiringcanberepresentedintermsofantichainsofdecreasingintegersequencesTheoremThejoinirreduciblesofFDS(x)formaposetthatisisomorphictoPandFDS(x)isisomorphictoA(P)Proof.
(outline)Bydistributivity,eachdomainsemiringtermt(x)canbewrittenasanitejoinofexpandednormalformtermsHenceanyjoinirreducibleelementofFDS(x)canberepresentedbyanexpandednormalformtermToshowthatPistheposetofthesejoinirreducible,itsucestoshowthatallexpandednormalformsarejoinirreducible,andthattwoexpandednormalformtermscanbedistinguishedinsomedomainmonoid(detailsinproceedings)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200821/1Exampletermandrelationforj=(4,3,1)j=(4,3,1)tj(x)=d(x4)xd(x3)xd(x)(s)(f)Xj={arrows}P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200822/1RepresentionofsemiringsbybinaryrelationsFirstnotethatforfreeidempotentsemiringsthisisalwayspossible[Bredihin,Schein1978]ForasetXofgenerators,aconcreteconstructioncanbeobtainedbyconsideringthecomplexalgebraofthefreegroupFGrp(X)Thisisalwaysarepresentablerelationalgebra,withtheelementsofthegroupasdisjointrelationsSincethefreemonoidXisasubsetofthefreegroup,theniteunionsoftherelationscorrespondingtosingletonwordsgivearelationalrepresentationofthefreeidempotentsemiringwithXassetofgeneratorsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200823/1RepresentionofsemiringsbybinaryrelationsHowever,notallidempotentsemiringscanberepresentedby∪,semiringsofrelations[Andreka1988,1991]showedthattheclassofalgebrasofrelations,closedunder∪,,thoughdenablebyquasiequations,isnotnitelyaxiomatisableHenceitisstrictlysmallerthanthenitelybasedvarietyofidempotentsemiringsSimilarlytheclassofalgebrasofrelationsclosedunderid,d,whered(R)=R;R∩id,isanon-nitelyaxiomatisablequasivariety,butnotavarietyP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200824/1RepresentionofsemiringsbybinaryrelationsTheoremTheone-generatedfreedomainsemiringcanberepresentedbyadomainsemiringofbinaryrelationsProof.
(outline)ToseethatFDS(x)canberepresentedbyacollectionofbinaryrelations,withoperationsofunion,compositionanddomain,itsucestoconstructarelationXonasetUsuchthats(X)=t(X)intherelationdomainsemiringP(U*U)foranydistinctpairofelementsofFDS(x)Thisisdonesimilarlytotheproofoftheprecedingtheorem,bytakingXtobetheunion(overdisjointbasesets)ofalltherelationsXjcorrespondingtothesequencesj∈PP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200825/1n-generatedcase(briey)Sofarouranalysishasconsideredtheone-generatedfreedomainsemiringThen-generatedcaseismorecomplex,buthasrecentlyalsobeenhandledAnormalformisgivenbyd(t0)y1d(t1)y2.
.
.
d(tn1)ynd(tn)wheretiarereducedtermsNormalformisgivenbyareducedtreeRelationalrepresentationsimilartotheone-generatedcaseFutureresearchisalsoaimingtodescribethestructureoffreedomainsemiringsinthepresenceofadditionalaxioms[Desharnais,Struth2008]showthatthedomainalgebrasd(S)inducedbythedomainaxiomscanbeturnedinto(co-)HeytingalgebrasorBooleanalgebrasbyimposingfurtherconstraintsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200826/1Anti-domainInparticular,addingthethreeaxiomsa(x)x=0,a(xy)≤a(xa(a(y)))anda(a(x))+a(x)=1foranantidomainfunctiona:S→Stothesemiringaxiomsanddeningdomainasd(x)=a(a(x))sucestoensured(S)isaBooleanalgebrarecoveralltheoremsoftheoriginaltwo-sortedaxiomatisationof[Desharnais,M¨oller,Struth2006]Basedontheseresults,inparticularthestructureofthefreeBooleandomainsemiringscertainlydeservefurtherinvestigationP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200827/1BooleandomainsemiringsgeneralizeJonsson-TarskiBAOs|xp=d(xp)isamodaloperatorond(A)Ingeneralfisanoperatoriffx+y,fx,fy,andf0,0BAO=BAwithoperatorsB=(B,+,0,·,1,,(fi)i∈I)BDSO=BooleanDSwithoperatorsA=(A,+,0,·,1,a,(gi)i∈I)Dened(A)=(a(a(A)),+,0,·,1,a,(|gi)i∈I)where|gi(p0,pn)=a(a(gi(p0,pn1)·pn))TheoremForanyBAOBthereexistsaBooleanDSOAsuchthatB=d(A)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200828/1DomainsemiringsgeneralizeGehrke-JonssonDLOsDLO=bnddistributivelatticeswithoperatorsB=(B,+,0,·,1,,(fi)i∈I)DSO=domainsemiringswithoperatorsA=(A,+,0,·,1,d,(gi)i∈I)Dened(A)=(d(A),+,0,·,1,d,(|gi)i∈I)where|gi(p0,pn)=d(gi(p0,pn1)·pn)TheoremForanyDLOBthereexistsaDSOAsuchthatB=d(A)Aisconstructedfromtherelationaldomainsemiringonthejoin-irreduciblesofthecanonicalextensionofBConclusion:DomainsemiringsgiveasimpleunisortedextensionofthestaticpropositionalframeworktothedynamicframeworkofsequencesP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200829/1References[H.
Andreka1989]Ontherepresentationproblemofdistributivesemilattice-orderedsemigroups,preprint(1988),AbstractsoftheAMS,Vol10,No2(March1989),p.
174.
[H.
Andreka1991]Representationsofdistributivelattice-orderedsemigroupswithbinaryrelations,AlgebraUniversalis28(1991),12–25.
[G.
Birkho1967]"LatticeTheory",3rded.
,Vol25ofAMSColloquiumPublications,AMS,1967,pp.
viii+420.
[D.
A.
Bredihin,B.
M.
Schein1978]Representationsoforderedsemigroupsandlatticesbybinaryrelations,Colloq.
Math.
39(1978),1–12.
[J.
Desharnais,B.
M¨oller,G.
Struth2006]Kleenealgebrawithdomain,ACMTransactionsonComputationalLogic,Vol7,No4,2006,798–833.
[J.
Desharnais,G.
Struth2008]ModalSemiringsRevisited,ResearchReportCS-08-01,DepartmentofComputerScience,TheUniversityofSheeld,2008.
[W.
McCune2007]Prover9,www.
prover9.
org[B.
M¨oller,G.
Struth2006]Algebrasofmodaloperatorsandpartialcorrectness,TheoreticalComputerScience,351,(2006),221–239.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200830/1
Jipsen,G.
StruthChapmanUSheeldApril9,2008P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20081/1OutlineIntroductionDomainSemiringsFreedomainsemiringRepresentationbybyantichainsofsequencesRepresentationbybinaryrelationsConclusionP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20082/1IntroductionAsemiringisoftheform(A,+,0,·,1)suchthat(A,+,0)isacommutativemonoid(A,·,1)isamonoid·distributesoverallnitejoinsfromtheleftandrighti.
e.
x(y+z)=xy+xz,(x+y)z=xz+yzandx0=0x=0Asemiringisidempotentifx+x=xISisthevarietyofidempotentsemiringsLemmaAnidempotentsemiringisa(join-)semilatticewith0asbottomelement,withx≤ygivenbyx+y=y(since+isassoc,commuandidempotent)andx≤y=wxz≤wyz(sincew(x+y)z=wxz+wyz)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20083/1ExamplesExamplesofsemiringsare:Rings(N,+,0,·,1).
.
.
Examplesofidempotentsemiringsare:Reductsofrelationalgebras(A,+,0,;,1)ReductsofKleenealgebras(A,+,0,·,1)Reductsofresiduatedlattices(A,1)(R∪{∞},max,0)Boundeddistributivelattices(A,∨,0,∧,1).
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20084/1FreemonoidsandsemiringsLetXbeasetofvariables(orgenerators)ThefreemonoidoverXisX=n∈NXnwith1=emptysequenceand·asconcatenationBydistributivity,everytermtinthesignatureofsemiringscanbewrittenasanitejoinoftermsofthefreemonoidXExample:x(y+xz)(x+1)=xyx+xxzx+xy+xxzthefreeidempotentsemiringoverX,denotedbyFIS(X),isisomorphictothesetPn(X)ofallnitesubsetsofwordsoverXHereU+V=U∪VandU·V={uv:u∈U,v∈V}P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20085/1Decidabilitytheequationaltheoryofidempotentsemiringsisdecidable:Giventermss,t,usedistributivitytowritetermsinnormalformHowever,thequasiequationaltheory(=strictuniversalHorntheory)isundecidablebecause:Thewordproblemforsemigroupsisundecidable(Post)Everysemiringisasemigroupundertheoperation"·"EverysemigroupSisa"·"-subreductofitspowersetsemiringP(Se)(whereSethemonoidextensionofS)theclassof"·"-subreductsofsemiringsistheclassofallsemigroupsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20086/1DomainmonoidsAdomainmonoidisanalgebra(M,·,1,d)suchthat(M,·,1)isamonoidandd:M→Misafunctionthatsatises(D1)d(x)x=x(D2)d(xd(y))=d(xy)(D3)d(d(x)y)=d(x)d(y)(D4)d(x)d(y)=d(y)d(x)ThevarietiesofdomainmonoidsisdenotedbyDMLemmad(1)=1[takex=1in(D1)]d(d(x))=d(x)[takex=1in(D2)]d(x)d(x)=d(x)[takey=xin(D3)]d(M)={d(x):x∈M}isameetsemilatticewith1=topelementP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20087/1DomainsemiringsAdomainsemiringisanalgebra(A,+,0,·,1,d)suchthat(A,+,0,·,1)isasemiring(A,·,1,d)isadomainmonoidandthefollowingadditionalaxiomshold[Desharnais,Struth2008]d(x+y)=d(x)+d(y),d(0)=0andd(x)+1=1xd(x)+x=xx+x=xEverydomainsemiringisanidempotentsemiringThevarietiesofdomainsemiringsisdenotedbyDSP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20088/1ExamplesofdomainsemiringsExamplesofdomainsemiringsaree.
g.
reductsofrelationalgebraswithd(x)=(x;x)∧1,reductsofKleenealgebraswithdomainModelsofdomainsemiringsinCS:Idempotentsemiringsformedbysetsoftracesofaprogram(whicharealternatingsequencesofstateandactionsymbols)withdomaindenedbystartingstatesoftracesIdempotentsemiringsformedbysetsofpathsinagraphwithdomaindenedbysetsofstartingstatesApplicationsofdomainsemiringsandKleenealgebraswithdomainhavebeenstudiedintensivelyP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,20089/1ApplicationsofdomainsemiringsThedomainoperationmodelsenablednessconditionsforactionsinprogramsandtransitionsystemsThedomainoperationcaneasilybeextendedintoamodaldiamondoperatorthatactsontheunderlyingalgebraofdomainelements[M¨oller,Struth2006]Linksthealgebraicapproachwithmoretraditionallogicsofprogramssuchasdynamic,temporalandHoarelogicsSomestandardsemanticsofprograms,includingtheweakestpreconditionandweakestliberalpreconditionsemantics,canbemodeledinthissettingApplicationscanbefoundinRelMiCSconferenceproceedingsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200810/1DomainsemiringsDomainsemiringswereoriginallyintroducedinatwo-sortedsettingThedomainoperationmapsarbitrarysemiringelementstoaspecialBooleansubalgebra[Desharnais,M¨oller,Struth2006]ArbitrarysemiringelementsmodelactionsofaprogramortransitionsystemTheelementsoftheBooleansubalgebramodelthestatesofthatsystemHereweusethesimplerandmoregeneralone-sortedapproachof[Desharnais,Struth2008]P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200811/1StudyingfreedomainsemiringsThefreedomainsemiringisinterestingforapplications:IdentiesexactlythosetermsofdomainsemiringsthathavethesamedenotationinalldomainsemiringsAllowsthedenitionofecientproofanddecisionproceduresThedomainaxiomsofdomainsemiringsarethesameasforrelationalgebrasandforKleenealgebraswithdomainBothrelationalgebrasandKleenealgebrashaverichandcomplex(quasi)equationaltheoriesRatherstudythesimplerequationaltheoryofdomainsemiringsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200812/1OutlineofresultsAim:giveanexplicitdescriptionoffreedomainsemiringsFDS(X)FirstdescribefreedomainmonoidFDM(X)ThenshowthattheseelementsarethejoinirreduciblesofFDS(X)FDS(X)isisomorphictothesetofniteantichainsintheposetofjoinirreduciblesShowFDS(X)isrepresentablebyaconcretealgebraofbinaryrelations,withrelationaldomainasoperationsDS=HSP{Relationaldomainsemirings}Finallyshowanydistributivelatticewithni-aryoperatorsoccursasdomainelementsofsomedomainsemiringwithni1-aryoperatorsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200813/1One-generateddomainterms(D1)d(x)x=x(D2)d(xd(y))=d(xy)(D3)d(d(x)y)=d(x)d(y)Asusual,wedenex0=1andxn+1=xnxLemmaInadomainmonoid,ifm≤nthend(xm)xn=xnandd(xm)d(xn)=d(xn)Proof.
Assumingm≤n,wewritexn=xmxnm,andusing(D1)wehaved(xm)xn=d(xm)xmxnm=xmxnm=xnNow(D3)impliesd(xm)d(xn)=d(d(xm)xn)=d(xn)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200814/1ExpandednormalformsOnelementsoftheformd(xj),theorderisinducedbythemeet-semilatticestructure:d(xj)≤d(xk)ij≥k,hencetheseelementsformachainForconcatenationsofbasicterms,rewritetheminexpandednormalform:d(xj0)xd(xj1)xd(xj2)x···xd(xjm)whereeachofthejk≥max{1+jk+1,2+jk+2,mk+jm}E.
g.
xd(x3)x2d(x2)=.
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200815/1DecreasingsequencesofnumbersForbrevitydenotesuchatermbythesequence(j0,j1,j2,jm)NotethatthisisalwaysastrictlydecreasingsequenceofnonnegativeintegersLetP=(P,≤)bethesetofallsuchsequences,orderedbyreversepointwiseorderThussequencesofdierentlengtharenotcomparable,andthemaximalelementsofthisposetare(0),(1,0),(2,1,0),.
.
.
correspondingtothetermsd(1)=1,d(x)xd(1)=x,d(x2)xd(x)xd(1)=x2,.
.
.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200816/1Theposetofjoin-irreduciblesbelow1andxd(x5)d(x4)d(x3)d(x2)d(x1)1=d(x0)(5)(4)(3)(2)(1)(0).
.
.
xd(x2)xd(x3)xd(x4)xd(x5)xd(x6)x(1,0)(2,0)(3,0)(4,0)(5,0)(6,0).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
d(x6)xd(x)d(x6)xd(x2)d(x6)xd(x3)d(x6)xd(x4)xd(x5)(6,1)(6,2)(6,3)(6,4)(6,5)(5,4)=xd(x4)(4,3)=xd(x3)(3,2)=xd(x2)(2,1)=xd(x)(5,3)=d(x5)xd(x3)(4,2)=d(x4)xd(x2)(3,1)=d(x3)xd(x)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200817/1Theposetofjoin-irreduciblesbelowx2x2=(2,1,0)(3,1,0)(4,1,0)(5,1,0)(6,1,0).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
(6,2,0)(6,3,0)(6,4,0)(6,5,0).
.
.
.
.
.
.
.
.
.
.
.
(6,4,3)(5,3,2)(4,2,1)(3,2,1)(4,3,2)(5,4,3)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200818/1TheproductoftwodecreasingsequencesAmultiplicationisdenedonPbythefollowing"rippleproduct"(j0,j1,j2,jm)·(k0,k1,k2,kn)=(j′0,j′1,j′2,j′m,k1,k2,kn)wherej′m=max(jm,k0)andj′i=max(ji,j′i+1+1)fori=m1,2,1,0Forexample,(7,3,2)·(4,3,1)=(7,5,4,3,1),while(4,3,1)·(7,3,2)=(9,8,7,3,2)CanshowthatthisistheresultofmultiplyingthecorrespondingexpandednormalformsandrewritingresultinexpandednormalformItistediousbutnotdiculttocheckthatthisoperationisassociativeP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200819/1DomainandpartialorderThedomainofasequence(j0,j1,j2,jm)isthelength-onesequence(j0)Thiscorrespondstothedomaintermd(xj0)LetA(P)bethesetofniteantichainsofPApartialorderisdenedonA(P)bya≤bi↓a↓bThemultiplicationisextendedtoantichainsbyusingthecomplexproduct(i.
e.
U·V={uv:u∈U,v∈V})andbyremovingallnon-maximalelementsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200820/1RepresentationTheoremTherstresultshowsthattheone-generatedfreedomainsemiringcanberepresentedintermsofantichainsofdecreasingintegersequencesTheoremThejoinirreduciblesofFDS(x)formaposetthatisisomorphictoPandFDS(x)isisomorphictoA(P)Proof.
(outline)Bydistributivity,eachdomainsemiringtermt(x)canbewrittenasanitejoinofexpandednormalformtermsHenceanyjoinirreducibleelementofFDS(x)canberepresentedbyanexpandednormalformtermToshowthatPistheposetofthesejoinirreducible,itsucestoshowthatallexpandednormalformsarejoinirreducible,andthattwoexpandednormalformtermscanbedistinguishedinsomedomainmonoid(detailsinproceedings)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200821/1Exampletermandrelationforj=(4,3,1)j=(4,3,1)tj(x)=d(x4)xd(x3)xd(x)(s)(f)Xj={arrows}P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200822/1RepresentionofsemiringsbybinaryrelationsFirstnotethatforfreeidempotentsemiringsthisisalwayspossible[Bredihin,Schein1978]ForasetXofgenerators,aconcreteconstructioncanbeobtainedbyconsideringthecomplexalgebraofthefreegroupFGrp(X)Thisisalwaysarepresentablerelationalgebra,withtheelementsofthegroupasdisjointrelationsSincethefreemonoidXisasubsetofthefreegroup,theniteunionsoftherelationscorrespondingtosingletonwordsgivearelationalrepresentationofthefreeidempotentsemiringwithXassetofgeneratorsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200823/1RepresentionofsemiringsbybinaryrelationsHowever,notallidempotentsemiringscanberepresentedby∪,semiringsofrelations[Andreka1988,1991]showedthattheclassofalgebrasofrelations,closedunder∪,,thoughdenablebyquasiequations,isnotnitelyaxiomatisableHenceitisstrictlysmallerthanthenitelybasedvarietyofidempotentsemiringsSimilarlytheclassofalgebrasofrelationsclosedunderid,d,whered(R)=R;R∩id,isanon-nitelyaxiomatisablequasivariety,butnotavarietyP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200824/1RepresentionofsemiringsbybinaryrelationsTheoremTheone-generatedfreedomainsemiringcanberepresentedbyadomainsemiringofbinaryrelationsProof.
(outline)ToseethatFDS(x)canberepresentedbyacollectionofbinaryrelations,withoperationsofunion,compositionanddomain,itsucestoconstructarelationXonasetUsuchthats(X)=t(X)intherelationdomainsemiringP(U*U)foranydistinctpairofelementsofFDS(x)Thisisdonesimilarlytotheproofoftheprecedingtheorem,bytakingXtobetheunion(overdisjointbasesets)ofalltherelationsXjcorrespondingtothesequencesj∈PP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200825/1n-generatedcase(briey)Sofarouranalysishasconsideredtheone-generatedfreedomainsemiringThen-generatedcaseismorecomplex,buthasrecentlyalsobeenhandledAnormalformisgivenbyd(t0)y1d(t1)y2.
.
.
d(tn1)ynd(tn)wheretiarereducedtermsNormalformisgivenbyareducedtreeRelationalrepresentationsimilartotheone-generatedcaseFutureresearchisalsoaimingtodescribethestructureoffreedomainsemiringsinthepresenceofadditionalaxioms[Desharnais,Struth2008]showthatthedomainalgebrasd(S)inducedbythedomainaxiomscanbeturnedinto(co-)HeytingalgebrasorBooleanalgebrasbyimposingfurtherconstraintsP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200826/1Anti-domainInparticular,addingthethreeaxiomsa(x)x=0,a(xy)≤a(xa(a(y)))anda(a(x))+a(x)=1foranantidomainfunctiona:S→Stothesemiringaxiomsanddeningdomainasd(x)=a(a(x))sucestoensured(S)isaBooleanalgebrarecoveralltheoremsoftheoriginaltwo-sortedaxiomatisationof[Desharnais,M¨oller,Struth2006]Basedontheseresults,inparticularthestructureofthefreeBooleandomainsemiringscertainlydeservefurtherinvestigationP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200827/1BooleandomainsemiringsgeneralizeJonsson-TarskiBAOs|xp=d(xp)isamodaloperatorond(A)Ingeneralfisanoperatoriffx+y,fx,fy,andf0,0BAO=BAwithoperatorsB=(B,+,0,·,1,,(fi)i∈I)BDSO=BooleanDSwithoperatorsA=(A,+,0,·,1,a,(gi)i∈I)Dened(A)=(a(a(A)),+,0,·,1,a,(|gi)i∈I)where|gi(p0,pn)=a(a(gi(p0,pn1)·pn))TheoremForanyBAOBthereexistsaBooleanDSOAsuchthatB=d(A)P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200828/1DomainsemiringsgeneralizeGehrke-JonssonDLOsDLO=bnddistributivelatticeswithoperatorsB=(B,+,0,·,1,,(fi)i∈I)DSO=domainsemiringswithoperatorsA=(A,+,0,·,1,d,(gi)i∈I)Dened(A)=(d(A),+,0,·,1,d,(|gi)i∈I)where|gi(p0,pn)=d(gi(p0,pn1)·pn)TheoremForanyDLOBthereexistsaDSOAsuchthatB=d(A)Aisconstructedfromtherelationaldomainsemiringonthejoin-irreduciblesofthecanonicalextensionofBConclusion:DomainsemiringsgiveasimpleunisortedextensionofthestaticpropositionalframeworktothedynamicframeworkofsequencesP.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200829/1References[H.
Andreka1989]Ontherepresentationproblemofdistributivesemilattice-orderedsemigroups,preprint(1988),AbstractsoftheAMS,Vol10,No2(March1989),p.
174.
[H.
Andreka1991]Representationsofdistributivelattice-orderedsemigroupswithbinaryrelations,AlgebraUniversalis28(1991),12–25.
[G.
Birkho1967]"LatticeTheory",3rded.
,Vol25ofAMSColloquiumPublications,AMS,1967,pp.
viii+420.
[D.
A.
Bredihin,B.
M.
Schein1978]Representationsoforderedsemigroupsandlatticesbybinaryrelations,Colloq.
Math.
39(1978),1–12.
[J.
Desharnais,B.
M¨oller,G.
Struth2006]Kleenealgebrawithdomain,ACMTransactionsonComputationalLogic,Vol7,No4,2006,798–833.
[J.
Desharnais,G.
Struth2008]ModalSemiringsRevisited,ResearchReportCS-08-01,DepartmentofComputerScience,TheUniversityofSheeld,2008.
[W.
McCune2007]Prover9,www.
prover9.
org[B.
M¨oller,G.
Struth2006]Algebrasofmodaloperatorsandpartialcorrectness,TheoreticalComputerScience,351,(2006),221–239.
P.
Jipsen,G.
Struth(ChapmanUSheeld)FreeDomainSemiringsApril9,200830/1
- Links花生壳免费域名相关文档
- 设置花生壳免费域名
- 投标人花生壳免费域名
- 地址花生壳免费域名
- 花生壳免费域名--花生壳绑定tomcat 花生壳路由器的设置
- 花生壳花生壳动态域名使用方法详解(免费动态域名)
- 花生壳通过花生壳服务申请免费域名
标准互联（450元）襄阳电信100G防御服务器 10M独立带宽
目前在标准互联这边有两台香港云服务器产品，这不看到有通知到期提醒才关注到。平时我还是很少去登录这个服务商的，这个服务商最近一年的促销信息比较少，这个和他们的运营策略有关系。已经从开始的倾向低价和个人用户云服务器市场，开始转型到中高端个人和企业用户的独立服务器。在这篇文章中，有看到标准互联有推出襄阳电信高防服务器100GB防御。有三款促销方案我们有需要可以看看。我们看看几款方案配置。型号内存硬盘IP...
盘点AoYoZhuJi傲游主机商8个数据中心常见方案及八折优惠
傲游主机商我们可能很多人并不陌生，实际上这个商家早年也就是个人主机商，传说是有几个个人投资创办的，不过能坚持到现在也算不错，毕竟有早年的用户积累正常情况上还是能延续的。如果是新服务商这几年确实不是特别容易，问到几个老牌的个人服务商很多都是早年的用户积累客户群。傲游主机目前有提供XEN和KVM架构的云服务器，不少还是亚洲CN2优化节点，目前数据中心包括中国香港、韩国、德国、荷兰和美国等多个地区的CN...
3C云1核1G 9.9元 4核4G 16元 美国Cera 2核4G 24元
3C云互联怎么样？3C云互联专注免备案香港美国日本韩国台湾云主机vps服务器,美国高防CN2GIA,香港CN2GIA,顶级线路优化,高端品质售后无忧！致力于对互联网云计算科技深入研发与运营的极客共同搭建而成,将云计算与网络核心技术转化为最稳定,安全,高速以及极具性价比的云服务器等产品提供给用户！专注为个人开发者用户,中小型,大型企业用户提供一站式核心网络云端服务部署,促使用户云端部署化简为零,轻松...
花生壳免费域名为你推荐
-
域名查询怎么查域名的注册商租服务器我想租服务器，请问会提供哪些服务？虚拟主机推荐虚拟主机哪个好免费虚拟主机申请免费域名和免费虚拟主机申请以及绑定求详解查询ip怎么查询IP地址网站域名空间网站域名和空间成都虚拟空间成都市规划信息技术中心如何？虚拟空间免费试用那位给我介绍个可以试用三天的虚拟空间。深圳网站空间怎么样建立网站虚拟主机系统虚拟主机采用什么操作系统?