Omega language

In formal language theory within theoretical computer science, an infinite word is an infinite-length sequence (specifically, an ωおめが-length sequence) of symbols, and an ωおめが-language is a set of infinite words. Here, ωおめが refers to the first infinite ordinal number, modeling a set of natural numbers.

Formal definition

Let Σしぐま be a set of symbols (not necessarily finite). Following the standard definition from formal language theory, Σしぐま^* is the set of all finite words over Σしぐま. Every finite word has a length, which is a natural number. Given a word w of length n, w can be viewed as a function from the set {0,1,...,n−1} → Σしぐま, with the value at i giving the symbol at position i. The infinite words, or ωおめが-words, can likewise be viewed as functions from $\mathbb {N}$ to Σしぐま. The set of all infinite words over Σしぐま is denoted Σしぐま^ωおめが. The set of all finite and infinite words over Σしぐま is sometimes written Σしぐま^∞ or Σしぐま^{≤ωおめが}.

Thus an ωおめが-language L over Σしぐま is a subset of Σしぐま^ωおめが.

Operations

Some common operations defined on ωおめが-languages are:

Intersection and union: Given ωおめが-languages L and M, both $L \cup M$ and $L \cap M$ are ωおめが-languages.
Left concatenation: Let L be an ωおめが-language, and K be a language of finite words only. Then K can be concatenated on the left, and only on the left, to L to yield the new ωおめが-language KL.
Omega (infinite iteration): As the notation hints, the operation $(\cdot )^{\omega }$ is the infinite version of the Kleene star operator on finite-length languages. Given a formal language L, L^ωおめが is the ωおめが-language of all infinite sequences of words from L; in the functional view, of all functions $\mathbb {N} \to L$ .
Prefixes: Let w be an ωおめが-word. Then the formal language Pref(w) contains every finite prefix of w.
Limit: Given a finite-length language L, an ωおめが-word w is in the limit of L if and only if $Pref(w) \cap L$ is an infinite set. In other words, for an arbitrarily large natural number n, it is always possible to choose some word in L, whose length is greater than n, and which is a prefix of w. The limit operation on L can be written L^δでるた or ${\vec {L}}$ .

Distance between ωおめが-words

The set Σしぐま^ωおめが can be made into a metric space by definition of the metric $d:\Sigma ^{\omega }\times \Sigma ^{\omega }\rightarrow \mathbb {R}$ as:

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

where |x| is interpreted as "the length of x" (number of symbols in x), and inf is the infimum over sets of real numbers. If $w=v$ then there is no longest prefix x and so $d(w,v)=0$ . Symmetry is clear. Transitivity follows from the fact that if w and v have a maximal shared prefix of length m and v and u have a maximal shared prefix of length n then the first $\min\{m,n\}$ characters of w and u must be the same so $d(w,u)\leq 2^{-\min\{m,n\}}\leq 2^{-m}+2^{-n}=d(w,v)+d(v,u)$ . Hence d is a metric.

Important subclasses

The most widely used subclass of the ωおめが-languages is the set of ωおめが-regular languages, which enjoy the useful property of being recognizable by Büchi automata. Thus the decision problem of ωおめが-regular language membership is decidable using a Büchi automaton, and fairly straightforward to compute.

If the language Σしぐま is the power set of a set (called the "atomic propositions") then the ωおめが-language is a linear time property, which are studied in model checking.

Bibliography

Perrin, D. and Pin, J.-E. "Infinite Words: Automata, Semigroups, Logic and Games". Pure and Applied Mathematics Vol 141, Elsevier, 2004.
Staiger, L. "ωおめが-Languages". In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, Volume 3, pages 339-387. Springer-Verlag, Berlin, 1997.
Thomas, W. "Automata on Infinite Objects". In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.