オメガ言語

理論計算機科学における形式言語理論では、無限語は記号の無限長シーケンス（具体的には、ω長シーケンス）であり、ω言語は無限語の集合です。ここで、ωは最初の無限順序数を指し、自然数の集合をモデル化します。

Σ を記号の集合（必ずしも有限である必要はない）とする。形式言語理論の標準的な定義に従うと、 Σ ^{* はΣ 上のすべての}有限語の集合である。すべての有限語には長さがあり、これは自然数である。長さnの語wを考えると、w は集合 {0,1,..., n −1} → Σ からの関数と見なすことができ、 iの値は位置iの記号を与える。無限語、つまり ω 語も同様に、 からΣ への関数と見なすことができる。 Σ 上のすべての無限語の集合は Σ ^{ω と表記される。 Σ 上のすべての有限語}と無限語の集合は、 Σ ^∞または Σ ^≤ωと表記されることもある。 ${\displaystyle \mathbb {N} }$

したがって、 Σ 上のω 言語L はΣ ^ωの部分集合です。

ω 言語で定義されている一般的な演算には次のものがあります。

交差と結合

ω-言語LとM が与えられた場合、L ∪ MとL ∩ Mは両方ともω-言語です。

左連結

L をω 言語とし、Kを有限語のみの言語とします。すると、K をL の左側のみに連結して、新しい ω 言語KLが生成されます。

オメガ（無限反復）

表記が示唆するように、この演算は有限長言語上のクリーネスター演算子の無限バージョンです。形式言語Lが与えられた場合、L ^{ω は}Lのすべての無限単語列の ω 言語です。関数の観点から見ると、すべての関数のω 言語です。${\displaystyle (\cdot )^{\omega }}$${\displaystyle \mathbb {N} \to L}$

接頭辞

w をω-単語とする。すると、形式言語 Pref( w )にはwのすべての有限 接頭辞が含まれる。

制限

有限長言語Lが与えられたとき、 ω 語w がLの極限内にあるのは、Pref( w ) ∩ Lが無限集合である場合に限ります。言い換えると、任意の大きさの自然数nに対して、長さがnより大きく、wの接頭辞となるようなL内の語を常に選択することが可能です。 Lに対する極限演算はL ^δまたは と書くことができます。${\displaystyle {\vec {L}}}$

集合 Σ ^{ω は、次のように}計量を定義することによって計量空間にすることができます。 ${\displaystyle d:\Sigma ^{\omega }\times \Sigma ^{\omega }\rightarrow \mathbb {R} }$

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

ここで、| x | は「 xの長さ」（ x内の記号の数）として解釈され、inf は実数集合の最小値です。 の場合、最長プレフィックスxは存在しないので となります。 対称性は明らかです。 推移性は、wとv が長さmの最大共有プレフィックスを持ち、vとu が長さnの最大共有プレフィックスを持つ場合、 wとuの最初の文字は同じでなければならないという事実から得られます。 したがって、d はメトリックです。 ${\displaystyle w=v}$${\displaystyle d(w,v)=0}$${\displaystyle \min\{m,n\}}$${\displaystyle d(w,u)\leq 2^{-\min\{m,n\}}\leq 2^{-m}+2^{-n}=d(w,v)+d(v,u)}$

ω-言語の最も広く使われているサブクラスは、ω-正規言語の集合であり、これはBüchi オートマトンによって認識できるという便利な特性を持っています。したがって、 ω-正規言語のメンバーシップの決定問題は、 Büchi オートマトン を使用して決定可能であり、計算はかなり簡単です。

言語 Σ が集合のべき集合（「原子命題」と呼ばれる）である場合、ω 言語は線形時間特性であり、モデル検査で研究されます。

• Perrin, D.およびPin, J.-E.「無限語: オートマトン、半群、論理、ゲーム」。純粋および応用数学第 141 巻、Elsevier、2004 年。
• Staiger, L.「ω-言語」。G . RozenbergおよびA. Salomaa編著『形式言語ハンドブック』第 3 巻、339-387 ページ。Springer-Verlag、ベルリン、1997 年。
• Thomas, W. 「無限オブジェクト上のオートマトン」。Jan van Leeuwen編著『理論計算機科学ハンドブック』、第 B 巻: 形式モデルとセマンティクス、133-192 ページ。Elsevier Science Publishers、アムステルダム、1990 年。