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

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 ${\displaystyle \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 Σ^ω.

Some common operations defined on ω-languages are:

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

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 ${\displaystyle w=v}$ then there is no longest prefix x and so ${\displaystyle 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 ${\displaystyle \min\{m,n\}}$ characters of w and u must be the same so ${\displaystyle d(w,u)\leq 2^{-\min\{m,n\}}\leq 2^{-m}+2^{-n}=d(w,v)+d(v,u)}$. Hence d is a metric.

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.