Technische Samenvatting: De Complexiteit van Neerwaartse Sluitingen van Gekoppelde Talen

Probleemstelling

Het artikel behandelt de computationele complexiteit van het construeren van neerwaartse sluitingen voor gekoppelde talen (indexed languages). De neerwaartse sluiting van een taal $L$, aangeduid als $L^\downarrow$, is de verzameling van alle verspreide subwoorden van woorden in $L$. Volgens Higman's Lemma is $L^\downarrow$ altijd een reguliere taal, wat het een cruciale reguliere bovenbenadering maakt die wordt gebruikt bij de verificatie van systemen met oneindige toestanden (bijvoorbeeld modelcontrole van hogere-orde, asynchrone programma's en verliesgevoelige kanaalsystemen).

Hoewel de berekenbaarheid van neerwaartse sluitingen voor gekoppelde talen (equivalent aan pushdownautomata van orde-2 of 2-PDAs) in 2015 was vastgesteld via een algemeen algoritme gebaseerd op goed-quasi-ordeeringen, bleven de complexiteitsgrenzen voor deze constructie een open probleem. Specifiek was onbekend of een primitief-recurseve constructie bestond, en waren er geen boven- of ondergrenzen bekend voor de grootte van de resulterende automata. Voorafgaand aan dit werk was de beste bekende ondergrens voor de grootte van een niet-deterministische eindige automaat (NFA) voor de neerwaartse sluiting van een gekoppelde taal dubbel-exponentieel, en was de complexiteit van beslissingsproblemen zoals inclusie en equivalentie van neerwaartse sluitingen bekend als ten minste co-2-NEXP-hard.

Methodologie

De auteurs lossen dit open probleem op door strakke (asymptotisch overeenkomende) boven- en ondergrenzen te bieden. Hun aanpak berust op een nieuwe algebraïsche abstractie van stapelinhoud om gekoppelde grammatica's om te zetten in contextvrije grammatica's (CFG's) terwijl de neerwaartse sluiting behouden blijft.

1. Productiviteit en Annotatie

De constructie begint met het garanderen dat de ingevoerde gekoppelde grammatica productief is (elke zinsvorm kan een terminaal woord afleiden). De auteurs introduceren een geannoteerde versie van de grammatica waarbij stapelsymbolen worden gepaard met verzamelingen van niet-terminals die vanuit die stapelconfiguratie terminale woorden kunnen afleiden. Dit voorkomt de generatie van "dode" termen die niet kunnen bijdragen aan de taal, een eigenschap die essentieel is voor het behoud van de neerwaartse sluiting tijdens daaropvolgende transformaties.

2. De Stapelmonoid en Samenvattingen

De kern van de technische innovatie omvat theorie van eindige semigruppen. De auteurs definiëren een stapelmonoid $M$ (een eindige monoid van Boole-matrices) die het gedrag van stapeloperaties (duwen en poppen) codeert ten opzichte van de niet-terminals van de grammatica.

• Samenvattingen: Zij maken gebruik van recente vooruitgang in de semigruppentheorie (specifiek resultaten van Jecker en Gimbert et al.) om samenvattingen van willekeurig lange stapelwoorden te berekenen. Een samenvatting is een gecomprimeerde representatie van een stapelwoord die voldoende informatie behoudt om de uitkomst van duw- en pop-operaties ten opzichte van de monoid $M$ te bepalen.
• Pompen en Overslaan: De auteurs introduceren twee nieuwe afleidingsregels, pompen (pump) en overslaan (skip), die het uitbreiden en reduceren van stapelinfixen toestaan die naar hetzelfde idempotente element in de monoid afbeelden. Zij bewijzen dat deze regels de neerwaartse sluiting van de taal niet veranderen.
• Compressie: Door deze regels toe te passen, tonen zij aan dat elke stapelinhoud kan worden gecomprimeerd tot een samenvatting van beperkte grootte (exponentieel in de grootte van de grammatica). Deze compressie verliest effectief informatie over de exacte stapelinhoud, maar behoudt de neerwaartse sluiting.

3. Reductie tot Contextvrije Grammatica's

Met behulp van deze samenvattingen construeren de auteurs een contextvrije grammatica (CFG) $G_{CFG}$ die de oorspronkelijke gekoppelde grammatica $G$ simuleert. In $G_{CFG}$ worden de stapelinhouds van de gekoppelde grammatica vervangen door hun samenvattingen.

• De niet-terminals van $G_{CFG}$ zijn tripels $(A, X, \sigma)$, waarbij $A$ een niet-terminal is, $X$ een verzameling niet-terminals is, en $\sigma$ een haalbare samenvatting is.
• Duw- en pop-operaties in de oorspronkelijke grammatica worden gesimuleerd door operaties op samenvattingen (met behulp van de push en pop relaties gedefinieerd op de monoid).
• De auteurs bewijzen dat $L(G_{CFG})^\downarrow = L(G)^\downarrow$.

4. Complexiteitsanalyse

Aangezien de grootte van een samenvatting exponentieel begrensd is in de grootte van de grammatica, heeft de resulterende CFG $G_{CFG}$ een dubbel-exponentiële grootte. Bestaande algoritmen voor het berekenen van neerwaartse sluitingen van CFG's leveren een NFA op met een exponentiële grootte ten opzichte van de CFG. Bijgevolg levert de compositie een NFA voor $L(G)^\downarrow$ op met een drievoudig-exponentiële grootte.

Voor deterministische eindige automata (DFA) resulteert de standaard subsetconstructie toegepast op de drievoudig-exponentiële NFA in een viervoudig-exponentiële bovengrens.

Belangrijkste Bijdragen en Resultaten

Bovengrenzen

• NFA-grootte: Gegeven een gekoppelde grammatica van grootte $n$, kan een NFA voor diens neerwaartse sluiting worden berekend in drievoudig-exponentiële tijd en heeft een grootte van maximaal drievoudig-exponentieel ($O(\exp_3(n))$).
• DFA-grootte: Een DFA voor de neerwaartse sluiting kan worden geconstrueerd met een grootte van maximaal viervoudig-exponentieel ($O(\exp_4(n))$).
• Beslissingsproblemen: De problemen van inclusie van neerwaartse sluitingen ($L_1^\downarrow \subseteq L_2^\downarrow$) en equivalentie ($L_1^\downarrow = L_2^\downarrow$) voor gekoppelde talen zijn co-3-NEXP-compleet.

Ondergrenzen

De auteurs leveren overeenkomstige ondergrenzen, waarmee de strakheid van hun bovengrenzen wordt bewezen:

• NFA-ondergrens: Er bestaat een familie van gekoppelde grammatica's van polynoomiale grootte zodanig dat elke NFA voor hun neerwaartse sluiting ten minste drievoudig-exponentiële toestanden vereist. Dit wordt bereikt door een grammatica te construeren die de taal $\{a^{\exp_3(n)}\}$ genereert.
• DFA-ondergrens: Er bestaat een familie van gekoppelde grammatica's zodanig dat elke DFA voor hun neerwaartse sluiting ten minste viervoudig-exponentiële toestanden vereist.
• Pompendrempel: De resultaten impliceren dat de pompendrempel voor gekoppelde grammatica's (de maximale lengte van een woord in een eindige gekoppelde taal van grootte $n$) ten minste drievoudig-exponentieel groeit, waardoor een eerdere bewering van een dubbel-exponentiële grens in de literatuur wordt gecorrigeerd.

Betekenis

Het artikel beslecht een langdurig open probleem betreffende de complexiteit van neerwaartse sluitingen voor gekoppelde talen.

1. Strakke Grenzen: Het stelt vast dat de complexiteit strikt hoger is dan voor contextvrije talen (die dubbel-exponentieel zijn voor NFAs), maar lager dan de algemene toren van exponentiële functies die vaak geassocieerd wordt met systemen van hogere orde $k > 2$. De sprong van dubbel- naar drievoudig-exponentieel voor gekoppelde talen (orde-2) is onverwacht, gezien de lineaire groei van complexiteit voor andere problemen (zoals leegte) met betrekking tot de orde van de pushdownautomaton.
2. Algoritmische Haalbaarheid: Het bevestigt dat een primitief-recurseve constructie bestaat, waarmee de vraag wordt opgelost of het probleem merely berekenbaar is of effectief construeerbaar binnen een specifieke complexiteitsklasse.
3. Methodologische Vooruitgang: De techniek van het gebruik van op semigruppen gebaseerde samenvattingen om stapelinhoud te comprimeren terwijl de neerwaartse sluiting behouden blijft, biedt een nieuw hulpmiddel voor het analyseren van systemen van hogere orde, mogelijk toepasbaar op bredere klassen van systemen met oneindige toestanden.

De auteurs benadrukken dat hun resultaten zijn afgeleid uit een constructieve transformatie van gekoppelde grammatica's naar CFG's, waarbij gebruik wordt gemaakt van de algebraïsche eigenschappen van de stapelmonoid om de onbeperkte aard van de stapels op een manier te beheersen die de subwoordstructuur behoudt die essentieel is voor neerwaartse sluitingen.