Nested Besede

Vzdržuje Rajeev Alur

aka vidno potisni jeziki

Kaj so ugnezdene besede?

 

What are nested words?

Vgnezdene besede so model za predstavitev podatkov tako z linearnim naročanjem kot s hierarhično ugnezdenim ujemanjem elementov. Primeri podatkov s takšno dvojno linearno-hierarhično strukturo vključujejo izvrševanje strukturiranih programov, jezikovnih podatkov, označenih z jezikom, in HTML / XML dokumentov. Vgnezdena beseda je sestavljena iz zaporedja linearno urejenih pozicij, povečanih z gnezdilnimi robovi, ki povezujejo klice z vračili (ali odprte oznake za bližnje oznake). Robovi ne prečkajo ustvarjanja pravilno ugnezdene hierarhične strukture in dovoljujemo, da se nekateri robovi čakajo na čakanje. To gnezdilno strukturo lahko edinstveno predstavlja zaporedje, ki določa vrste položajev (klici, vračila in notranji podatki). Vgnezdene besede posplošujejo obe besedi in urejena drevesa ter omogočata operacije besed in dreves.

Avtomatizacija ugnezdanih besed — akceptorji končnih držav za ugnezdene besede, določite razred rednih jezikov ugnezdenih besed. Ta razred ima vse privlačne teoretične lastnosti, ki jih uživajo klasični navadni besedni jeziki: deterministični gnezdeni avtomatski izrazi so izraziti kot njihovi nedeterministični nasprotniki; razred je zaprt pod sindikatom, presečišče, komplementiranje, združevanje, Kleene- *, predpone in jezikovni homomorfizmi; članstvo, praznina, jezikovna vključenost in jezikovna enakovrednost so vse odločne; definicija v monadni logiki drugega reda natančno ustreza prepoznavnosti končnega stanja. Ti rezultati se posplošujejo tudi v neskončne ugnezdene besede.

Kako se nanašajo na kontekstne jezike besed?

Glede na jezik L ugnezdenih besed nad abecedo, linearno kodiranje ugnezdenih besed daje jezik L ‘nad označeno abecedo, sestavljeno iz simbolov, označenih s tipom položaja. Če je L pravilen jezik ugnezdenih besed, potem je L ‘brez konteksta. Dejansko avtomat za potiskanje, ki sprejema L ‘, ima posebno strukturo: pri branju klica mora avtomat pritisniti en simbol, medtem ko odčita simbol za vračanje, mora popiti en simbol (če je snop prazen) in med branjem notranji simbol, lahko samo posodobi svoje stanje nadzora. To avtomatsko imenujemo vidno potisni avtomat in razred besednih jezikov, ki jih sprejemajo vidno potisni jeziki (VPL). Ker so lahko naši avtomati določeni, VPL ustrezajo podrazredi determinističnih kontekstnih jezikov (DCFL). VPLs generalizirajo jezike za jezike, jezike z zaklepanjem in uravnotežene jezike, in imajo boljše lastnosti zapiranja kot CFL, DCFL ali parantezni jeziki.

Trdimo, da je za algoritemsko preverjanje strukturiranih programov, namesto da bi program gledali kot na jezik brez konteksta nad besedami, bi ga morali gledati kot reden jezik ugnezdenih besed (ali enakovredno vidno potisni jezik), kar bi omogočilo model preverjanje številnih lastnosti (kot so pregled stackov, pred-post pogoji), ki niso izrecni v obstoječi logiki specifikacij.

Na splošno avtomat za potiskanje služi za dva različna namena: odkrivanje hierarhičnega ujemanja in obdelava / poizvedovanje ujemanja. V aplikacijah, pri katerih je pomemben le drugi namen (kot pri programski analizi), lahko nadomestite avtomatizacijo z avtomatizacijo s pomočjo NWA s številnimi koristmi.

Kako se nanašajo na naročena drevesa?

Podatki z dvojno linearno-hierarhično strukturo se tradicionalno oblikujejo z binarno in bolj splošno z uporabo urejenih neoviranih dreves in z uporabo avtomatov dreves. Pri naročenih drevesih so vozlišča z istim staršem linearno urejena, klasični prehodi dreves, kot je infix (ali globina-levo-desno), se lahko uporabijo za določitev implicitnega naročanja vseh vozlišč. Izkazalo se je, da so ograje, kjer je varovanje zaporedje urejenih dreves, poseben razred ugnezdenih besed, in sicer tisti, ki ustrezajo besedam Dyck, in redni jeziki hedge ustrezajo uravnoteženim jezikom.

Za obdelavo dokumentov imajo vgnezdene besede veliko več prednosti glede na naročena drevesa. Predstavitev na podlagi drevesa implicitno predvideva, da se lahko vhodni linearni podatki razčlenijo v drevo, zato ne moremo predstaviti in obdelati podatkov, ki se morda ne razčlenijo pravilno. Operacije z besedami, kot so predpone, pripone in združitve, medtem ko so naravni za obdelavo dokumentov, nimajo podobnih drevesnih operacij. Drugič, avtomati dreves lahko naravno izrazijo omejitve glede zaporedja oznak vzdolž hierarhične poti in tudi po levi-desni brati in sestri, vendar imajo težave pri zajemanju omejitev, ki se nanašajo na svetovni linearni vrstni red. Na primer, poizvedba, da se vzorci p1, … pk pojavijo v dokumentu v tem vrstnem redu, se prevedejo v deterministični besedni avtomat (in s tem deterministični NWA) linearne velikosti, vendar mora standardno deterministično avtomat za drevo navzgor za to poizvedbo velikostni eksponent v k. NWA je mogoče obravnavati kot nekakšen drevesni avtomat, tako da sta avtomatska drevesa od spodaj navzgor in avtomatska drevesa od zgoraj navzdol posebni primeri. Ti rezultati kažejo, da je poizvedba lahko bolj jedrnato kodirana v pogledu ugnezdenih besed s prednostmi kompleksnosti. Avtentičnost v besedi ustvari besedo od leve proti desni, obdeluje robove za gnezdenje, ko in ko pridejo. To se ujema z SAX API za XML, zato ima naravno uporabo v pretočnih algoritmih.

Reference

Model ugnezdenih besed je potekal skozi nekaj iteracij: Glej vidno potisne jezike; Alur in Madhusudan; STOC 2004; in dodajanje gnezdilne strukture besedam; Alur in Madhusudan; DLT 2006. Priporočamo, da preberete to enotno polno različico (Journal of ACM, 2009). Povabljeni pogovor na CSR 2007 je tudi dobro izhodišče.

Namen te strani je spremljati obsežne nadaljnje raziskave o tej temi. Pošljite mi e-pošto s komentarji in / ali predlaganimi dodatki.

Orodja

Dodatne težave pri odločanju o VPA / NWA

  • Vidno potisne igre; Loding, Madhusudan in Serre; FSTTCS 2004.
  • Vidno potisni avtomati: od jezikovne ekvivalence do simulacije in bisimulacije; Srba; CSL 2006.
  • Težave z zakonitostjo za vidno potisne jezike; Barany, Loding in Serre; STACS 2006.
  • O problemu članstva za vidno potisne jezike; La Torre, Napoli in Parente; ATVA 2006.
  • Simbolno vidno potisni avtomat; D’Antoni in Alur; CAV 2014.

Sestavine in minimiziranje

  • Dogodki za vidno potisne jezike; Alur, Kumar, Madhusudan in Viswanathan; ICALP 2005.
  • Minimiziranje, učenje in preverjanje skladnosti za Boolove programe; Kumar, Madhusudan in Viswanathan; CONCUR 2006.
  • Minimiziranje variant vidno avtomatov potiskanja; Chervet in Walukiewicz; MFCS 2007.
  • Minimizacija vidno avtomatov za pišanje z delnim maksimalnim SAT-om; Heizmann, Schilling in Tischner; TACAS 2017.

Logika časovne in fiksne točke; Izrazitost

  • Temeljna logika ugnezdenih klicev in vračil; Alur, Etessami in Madhusudan; TACAS 2004.
  • Redni jeziki ugnezdenih besed: fiksne točke, avtomatizacija in sinhronizacija; Arenas, Barcelo in Libkin; ICALP 2007.
  • Logika prvega reda in časovne logike za ugnezdene besede, Alur, Arenas, Barcelo, Etessami, Immerman in Libkin; LICS 2007.
  • Nadomestni avtomati in časovni pritrditveni izračun za vidne jezike; Bozzelli; CONCUR 2007.
  • Slovnična predstavitev vidno potisnih jezikov; Baran in Barringer; WoLLIC 2007.
  • Utežene logike za ugnezdene besede in algebraične formalne serije moči; Matissen; ICALP 2008.
  • Vidno racionalni izrazi; Bozzelli in Sanchez; FSTTCS 2012.
  • Vidno linearna časovna logika; Bozzelli in Sanchez; IJCAR 2014.

Specifikacije za analizo programa

  • Vidiki na podlagi VPA: boljša podpora za protokole AOP; Nguyen in Sudholt; SEFM 2006.
  • Programi za instrumentiranje C z vgrajenimi besednimi monitorji; Chaudhuri in Alur; SPIN 2007.
  • Sintetiziranje monitorjev za varnostne lastnosti – tokrat s klici in vračili; Rosu, Chen in Ball; RV 2008.
  • Časovna razlaga postopkovnih programov; Alur in Chaudhuri; VMCAI 2010.
  • Vgnezdeni interpolanti; Heizmann, Hoenicke in Podelski; POPL 2010.
  • Preverjanje združljivosti proizvajalca in potrošnika; Drscoll, Burton in Reps; FSE 2011.
  • Varno programiranje z vidno varnostnimi igrami; Harris, Jha in Reps; CAV 2012.

Obdelava XML in Avtomatizacija dreves

  • Vidno utišanje izraznih učinkov za obdelavo toka XML; Vrč; PLAN-X 2005.
  • Vidno potisni jeziki za pretakanje XML; Kumar, Madhusudan in Viswanathan; WWW 2007.
  • Srečanje z besedami in drevesi; Alur; PODS 2007.
  • Prepisovanje vidno potiskanih jezikov za integracijo podatkov XML; Thomo in Venkatesh; CIKM 2008.
  • Avtomatski tokovi dreves; Gauwin, Niehren in Roos; Pisma za obdelavo informacij 2009.
  • Najstarejša poizvedba, ki se odziva na deterministične avtomatizirane besede v besedilu; Gauwin, Niehren in Tison; FCT 2009.
  • Avtomat za poizvedbo za ugnezdene besede; Madhusudan in Viswanathan; MFCS 2009.
  • Od navadnih izrazov do ugnezdenih besed: Unifying languages ​​in izvrševanje poizvedb za relacijske in XML sekvence; Mozafari, Zeng, Zaniolo; VLDB 2010.
  • Visoko zmogljiva kompleksna obdelava dogodkov prek tokov XML; Mozafari, Zeng, Zaniolo; SIGMOD 2012.
  • Pretočni fragmenti naprej XPath; Gauwin in Niehren; CIAA 2012.
  • Zgodnje izbiranje vozlišča XPath na tokovih XML; Debarbieux, Gauwin, Niehren, Sebastian in Zergaoui; 2012.

Pretvorniki

  • Vidno potisni pretvorniki za približno validacijo pretakanja XML; Thomo, Venkatesh in Ye; FoIKS 2008.
  • Vidno pretočni pretvorniki; Raskin in Servais; ICALP 2008.
  • Enakovrednost determinističnih gnezdenih besed v Wordove pretvornike; Staworko, Laurence, Lemay, Niehren; FCT 2009.
  • Lastnosti Visible Pushdown pretvornikov; E. Filiot, J.-F. Raskin, P.-A. Reynier, F. Servais in J.-M. Talbot; MFCS 2010.
  • XEvolve: okvir za razvoj sheme XML; F. Picalausa, F. Servais in E. Zimànyi; SACSVT 2011.
  • Pretočnost prenosnih besednih transdukcij; E. Filiot, O. Gauwin, P.-A. Reynier, F. Servais. FSTTCS 2011.
  • Pretočni drevesni pretvorniki; R. Alur in L. D’Antoni; ICALP 2012.
  • Visible Pushdown pretvorniki z Look-Ahead. E. Filiot in F. Servais. SOFSEM 2012.

Ugnezdena drevesa

  • Izračun točke za lokalni in globalni programski tok; Alur, Chaudhuri in Madhusudan; POPL 2006.
  • Jeziki vgrajenih dreves; Alur, Chaudhuri in Madhusudan; CAV 2006.
  • Vidno potisni jeziki in prepis terminov; Chabin in Rety; FroCos 2007.
  • Vidno avtomatov dreves s pomnilnikom in omejitvami; Comon-Lundh, Jacquemard, Perrin; Logične metode v računalništvu 2008.

Besede z več gnezdami

  • Beležka o ugnezdenih besedah; Blass in Gurevich; Microsoft Research TR; 2006.
  • Robusten razred kontekstno občutljivih jezikov; La Torre, Madhusudan in Parlato; LICS 2007.
    2-vidno potisni avtomat; Carotenuto, Murano in Peron; DLT 2007.
  • Uresničljivost sočasnih rekurzivnih programov; Bollig, Grindei in Habermehl; FoSSaCS 2009.

Novi rezultati z vidljivostjo klicev / povračil

  • Idealiziran Algol tretjega reda z ponovitvijo je odločen; Murawski in Walukiewicz; FoSSaCS 2005.
  • Sinhronizacija avtomatov za potiskanje; Božič; DLT 2006.
  • Procesna dinamična logika z rekurzivnimi programi; Loding in Serre; FoSSaCS 2006.
  • Višinsko-deterministični avtomat za utripanje; Nowotka in Srba; MFCS 2007.
  • Neskončna avtomatska karakterizacija dvojnega eksponentnega časa; La Torre, Madhusudan in Parlato; CSL 2008.

Izzivalna odprta težava (zdaj rešena!)

Razmislite o naslednjem problemu odločanja: če sta oba dva redna jezika L1 in L2 ugnezdenih besed, ali obstaja pravilen jezik R besed preko označene abecede, tako da je presečišče (R, L1) enako L2? To ni znano, da je odločilno, tudi v posebnem primeru, da je L1 niz vseh dobro ujemajočih besed. Motivacija je naslednja: na splošno je za preverjanje, ali vhod spada v L2, procesorju potrebuje sklad. Predpostavimo pa, da imamo že kakšno dodatno znanje o vložku, da spada v niz L1 (na primer, morda vemo, da je vnos dobro ujemanje), ali se lahko to znanje uporabi za konstrukcijo DFA A, tako da za vhodne podatke v L1, A je sposoben odločati o članstvu v L2. To težavo navdihuje dokument “Potrjevanje pretočnih XML dokumentov” Segoufin in Vianu, PODS 2002, ki predstavlja tudi delno rešitev.

Nedavno je Eryk Kopczynski dokazal neodločljivost te težave: glej nevidne jezike, LICS 2016.

Vir: https://www.cis.upenn.edu/~alur/nw.html