Omskriving av graf - Graph rewriting

I datateknikk , graf transformasjon , eller graf omskriving vedrører teknikken for å lage en ny graf ut fra en opprinnelig graf av en algoritme. Den har mange applikasjoner, alt fra programvareteknikk ( programvarekonstruksjon og også programvareverifisering ) til layoutalgoritmer og generering av bilder.

Graftransformasjoner kan brukes som beregningsabstraksjon. Den grunnleggende ideen er at hvis tilstanden til en beregning kan representeres som en graf, kan ytterligere trinn i den beregningen deretter bli representert som transformasjonsregler på den grafen. Slike regler består av en original graf, som skal matches med en undergraf i fullstendig tilstand, og en erstatningsgraf som erstatter den matchede undergrafen.

Formelt består et omskrivingssystem for graf vanligvis av et sett med omskrivningsregler for skjemaet , med å bli kalt mønstergraf (eller venstre side) og kalles erstatningsgraf (eller høyre side av regelen). En regel for omskriving av graf blir brukt på vertsgrafen ved å søke etter en forekomst av mønstergrafen ( mønstermatching , og dermed løse problemet med subgrafisomorfisme ) og ved å erstatte den funnet forekomsten med en forekomst av erstatningsgrafen. Omskrivingsregler kan reguleres ytterligere når det gjelder merkede grafer , for eksempel i strengregulerte grafgrammatikker.

Noen ganger grafen grammatikk brukes som et synonym for graf omskriving system , spesielt i forbindelse med formelle språk ; de forskjellige ordlydene brukes til å understreke målet med konstruksjoner, som oppregning av alle grafer fra en startgraf, dvs. generering av et grafspråk - i stedet for bare å transformere en gitt tilstand (vertsgraf) til en ny tilstand.

Graf omskriving tilnærminger

Image
Topp: Eksempel på omskrivingsregel for graf ( optimalisering fra kompilatorkonstruksjon: multiplikasjon med 2 erstattet av tillegg). Nederst: Anvendelse av regelen for å optimalisere "y = x * 2" til "y = x + x".

Algebraisk tilnærming

Den algebraiske tilnærmingen til omskriving av graf er basert på kategoriteori . Den algebraiske tilnærmingen er videre delt inn i deltilnærminger, hvorav den vanligste er dobbel-pushout (DPO) -tilnærming og single-pushout (SPO) -tilnærming . Andre deltilnærminger inkluderer sesqui-pushout og pullback- tilnærmingen .

Fra perspektivet til DPO-tilnærmingen er en grafomskrivingsregel et par morfismer i kategorien grafer og grafer homomorfismer mellom dem :, også skrevet , hvor er injeksivt . Grafen K kalles invariant eller noen ganger limgrafen . En omskriving trinn eller anvendelse av en regel r til en vert graf G er definert ved to pushout diagrammer både med opprinnelse i det samme morphism , hvor D er en sammenheng graf (dette er der navnet dobbel -pushout kommer fra). En annen grafmorfisme modellerer en forekomst av L i G og kalles en kamp . Den praktiske forståelsen av dette er at det er et subgraf som er matchet fra (se problem med subgraph isomorfisme ), og etter at en match er funnet, erstattes med i vertsgrafen der det fungerer som et grensesnitt, som inneholder noder og kanter som er bevart når du bruker regel. Grafen er nødvendig for å feste mønsteret som blir matchet til konteksten: hvis det er tomt, kan samsvaret bare betegne en hel tilkoblet komponent i grafen .

I motsetning til en graf omskriving regel av SPO tilnærmingen er et enkelt morphism i kategorien av merkede multigraphs og delvis kartlegginger som bevarer multigraph struktur: . Dermed er et omskrivingstrinn definert av et enkelt pushout- diagram. Den praktiske forståelsen av dette er lik DPO-tilnærmingen. Forskjellen er at det ikke er noe grensesnitt mellom vertsgrafen G og grafen G 'som er resultatet av omskrivingstrinnet.

Fra det praktiske perspektivet er nøkkelskillet mellom DPO og SPO hvordan de håndterer sletting av noder med tilstøtende kanter, spesielt hvordan de unngår at slike slettinger kan etterlate "dinglende kanter". DPO-tilnærmingen sletter bare en node når regelen spesifiserer sletting av alle tilstøtende kanter også (denne dinglende tilstanden kan kontrolleres for en gitt kamp), mens SPO-tilnærmingen ganske enkelt disponerer de tilstøtende kantene, uten å kreve en eksplisitt spesifikasjon.

Det er også en annen algebraisk-lignende tilnærming til omskriving av grafer, hovedsakelig basert på boolsk algebra og en algebra av matriser, kalt matrisegrafgrammatikk .

Bestem omskriving av graf

Nok en annen tilnærming til omskriving av graf, kjent som bestemt grafomskriving, kom ut av logikk og databaseteori . I denne tilnærmingen blir grafer behandlet som databaseinstanser, og omskrivingsoperasjoner som en mekanisme for å definere spørsmål og visninger; derfor kreves all omskriving for å gi unike resultater ( opp til isomorfisme ), og dette oppnås ved å anvende en hvilken som helst omskrivningsregel samtidig gjennom hele grafen, uansett hvor den gjelder, på en slik måte at resultatet faktisk er unikt definert.

Omskriving av termgraf

En annen tilnærming til omskriving av graf er omskriving av begreper, som involverer prosessering eller transformasjon av begrepsgrafer (også kjent som abstrakte semantiske grafer ) ved hjelp av et sett med syntaktiske omskrivningsregler.

Begrepsgrafer er et fremtredende tema i programmeringsspråkforskning, siden regler for omskriving av begrepsgraf er i stand til å uttrykke en kompilators operative semantikk formelt . Begrepsgrafer brukes også som abstrakte maskiner som er i stand til å modellere kjemiske og biologiske beregninger, så vel som grafiske beregninger som samtidighetsmodeller. Begrepsdiagrammer kan utføre automatisert verifisering og logisk programmering siden de er velegnet til å representere kvantifiserte utsagn i førsteordenslogikk. Symbolsk programmeringsprogramvare er et annet program for begrepsgrafer, som er i stand til å representere og utføre beregning med abstrakte algebraiske strukturer som grupper, felt og ringer.

TERMGRAPH-konferansen fokuserer helt på forskning om omskriving av begrepsgraf og dens applikasjoner.

Klasser av grafgrammatikk og omskrivingssystem

Grafomskrivingssystemer grupperes naturlig i klasser i henhold til typen representasjon av grafer som brukes og hvordan omskrivningene uttrykkes. Begrepet grafgrammatikk, ellers tilsvarende grafomskrivingssystem eller grafutskiftningssystem, brukes oftest i klassifiseringer. Noen vanlige typer er:

Implementeringer og applikasjoner

Grafer er en uttrykksfull, visuell og matematisk presis formalisme for modellering av objekter (enheter) knyttet til relasjoner; objekter er representert av noder og forholdet mellom dem av kanter. Noder og kanter blir ofte skrevet og tilskrevet. Beregninger er beskrevet i denne modellen ved endringer i forholdet mellom enhetene eller ved attributtendringer av grafelementene. De er kodet i grafomskrivingsregler / graftransformasjonsregler og utført av grafomskrivingssystemer / graftransformasjonsverktøy.

Se også

Referanser

Sitater

Kilder