Omega språk

I formell språkteori inom teoretisk datavetenskap är ett oändligt ord en oändlig längdsekvens ( specifikt en ω-längdsekvens) av symboler , och ett ω-språk är en uppsättning oändliga ord. Här avser ω det första ordningstalet , mängden naturliga tal .

Formell definition

Låt Σ vara en uppsättning symboler (inte nödvändigtvis ändliga). Enligt standarddefinitionen från formell språkteori är Σ ^* mängden av alla finita ord över Σ. Varje finita ord har en längd, vilket är ett naturligt tal. Givet ett ord w med längden n , kan w ses som en funktion från mängden {0,1,..., n −1} → Σ, där värdet vid i ger symbolen vid position i . De oändliga orden, eller ω-orden, kan också ses som funktioner från $\mathbb {N}$ till Σ. Mängden av alla oändliga ord över Σ betecknas Σ ^ω . Mängden av alla finita och oändliga ord över Σ skrivs ibland Σ ^∞ eller Σ ^≤ω .

Således är ett ω-språk L över Σ en delmängd av Σ ^ω .

Operationer

Några vanliga operationer definierade på ω-språk är:

Skärning och förening: Givet ω-språken L och M , är både $L \cup M$ och $L \cap M$ ω-språk.
Vänster sammanlänkning: Låt L vara ett ω-språk och K vara ett språk med endast ändliga ord. Sedan K sammanfogas till vänster, och endast till vänster, till L för att ge det nya ω-språket KL .
Omega (oändlig iteration): Som notationen antyder är operationen $(\cdot )^{\omega }$ den oändliga versionen av Kleene-stjärnoperatorn på språk med ändlig längd. Givet ett formellt språk L är L ^{ω ω-språket för alla} oändliga ordsekvenser från L ; i funktionsvyn, av alla funktioner $\mathbb {N} \to L$ .
Prefix: Låt w vara ett ω-ord. Då innehåller det formella språket Pref( w ) varje finita prefix av w .
Limit: Givet ett ändligt långt språk L , är ett ω-ord w i gränsen för L om och endast om $Pref(w) \cap L$ är en oändlig mängd. Med andra ord, för ett godtyckligt stort naturligt tal n , är det alltid möjligt att välja något ord i L , vars längd är större än n , och som är ett prefix till w . Gränsoperationen på L kan skrivas L ^δ eller ${\vec {L}}$ .

Avstånd mellan ω-ord

Mängden Σ ^ω kan göras till ett metriskt utrymme genom definition av måttet $d:\Sigma ^{\omega }\times \Sigma ^{\omega }\rightarrow \mathbb {R}$ som:

d(w,v)=\inf\{2^{-|x|}\mid x\in \Sigma ^{* }\ {\text{och}}\ x\in {\text{Pref}}(w)\cap {\text{Pref}}(v)\}

där | x | tolkas som "längden på x " (antal symboler i x ), och inf är infimum över uppsättningar av reella tal . Om $w=v$ så finns det inget längsta prefix x och så $d(w,v)=0$ . Symmetri är tydlig. Transitivitet följer av det faktum att om w och v har ett maximalt delat prefix med längden $\min\{m,n\ }$ och v och u har ett maximalt delat prefix med längden n så är den första tecken i w och u måste vara samma så $d(w,u)\leq 2^{-\min\{m,n\}}\leq 2^{-m}+2^{-n}=d(w,v)+d(v ,u)$ . Därför d ett mått.

Viktiga underklasser

Den mest använda underklassen av ω-språken är uppsättningen ω-reguljära språk , som åtnjuter den användbara egenskapen att kännas igen av Büchi automata . Därför beslutsproblemet med ω-vanligt språkmedlemskap avgöras med hjälp av en Büchi-automat, och ganska enkelt att beräkna.

Om språket Σ är kraftmängden för en mängd (kallad "atomära propositioner") så är ω-språket en linjär tidsegenskap som studeras i modellkontroll .

Bibliografi

Perrin D. [ fr ] . och Pin, J.-E. " Infinite Words: Automata, Semigroups, Logic and Games ". Pure and Applied Mathematics Vol 141, Elsevier, 2004.
Staiger, L. " ω-Languages ". I G. Rozenberg och A. Salomaa , redaktörer, Handbook of Formal Languages , Volym 3, sidorna 339-387. Springer-Verlag, Berlin, 1997.
Thomas, W. "Automata på oändliga objekt". I Jan van Leeuwen , redaktör, Handbook of Theoretical Computer Science , Volym B: Formal Models and Semantics, sidorna 133-192. Elsevier Science Publishers, Amsterdam, 1990.