En informática y teoría de lenguajes formales , los lenguajes ω-regulares son una clase de lenguajes ω que generalizan la definición de lenguajes regulares a palabras infinitas. Así como los lenguajes regulares aceptan cadenas finitas (como cadenas que comienzan en una a , o cadenas que alternan entre a y b ), los lenguajes ω-regulares aceptan palabras infinitas (como secuencias infinitas que comienzan en una a , o secuencias infinitas que alternan entre a y b ).
Definición formal
Sea A un lenguaje . Denotemos por A ω el conjunto cuyos elementos se obtienen concatenando palabras de A infinitas veces, es decir, el conjunto de funciones..
La clase de ω-lenguajes regulares se define inductivamente de la siguiente manera:
- Un ω , donde A es un lenguaje regular que no contiene la cadena vacía, es ω-regular;
- AB , la concatenación de un lenguaje regular A y un lenguaje ω-regular B (nótese que BA no está bien definido), es ω-regular;
- A ∪ B , donde A y B son lenguajes ω-regulares (esta regla solo se puede aplicar un número finito de veces), es ω-regular.
Tenga en cuenta que si A es regular, A ω no es necesariamente ω-regular, ya que A podría ser, por ejemplo, {ε}, el conjunto que contiene solo la cadena vacía , en cuyo caso A ω = A , que no es un lenguaje ω y, por lo tanto, no es un lenguaje ω-regular.
Es una consecuencia directa de la definición que los lenguajes ω-regulares son precisamente los lenguajes ω de la forma A 1 B 1 ω ∪ ... ∪ A n B n ω para algún n , donde los A i s y B i s son lenguajes regulares y los B i s no contienen la cadena vacía.
Equivalencia con el autómata de Büchi
Teorema : Un autómata de Büchi reconoce un lenguaje ω si y solo si es un lenguaje ω-regular.
Todo lenguaje ω-regular es reconocido por un autómata de Büchi no determinista; la traducción es constructiva. Utilizando las propiedades de cierre de los autómatas de Büchi y la inducción estructural sobre la definición de lenguaje ω-regular, se puede demostrar fácilmente que se puede construir un autómata de Büchi para cualquier lenguaje ω-regular dado.
Por el contrario, para un autómata de Büchi dado A = ( Q , Σ, δ, I , F ) , construimos un lenguaje ω-regular y luego mostraremos que este lenguaje es reconocido por A . Para una ω -palabra w = a 1 a 2 ... sea w ( i , j ) el segmento finito a i +1 ... a j − 1 a j de w . Para cada q , q' ∈ Q , definimos un lenguaje regular L q,q' que es aceptado por el autómata finito ( Q , Σ, δ , q , { q' }) .
Lema — Afirmamos que el autómata de Büchi A reconoce el lenguaje ⋃ q ∈ I , q ′ ∈ F L q,q' ( L q',q' − { ε } ) ω .
Supongamos que la palabra w ∈ L ( A ) y q 0 , q 1 , q 2 ,... es una secuencia de aceptación de A en w . Por lo tanto, q 0 está en I y debe haber un estado q' en F tal que q' ocurre infinitas veces en la secuencia de aceptación. Elijamos la secuencia infinita estrictamente creciente de índices i 0 , i 1 , i 2 ... tal que, para todo k ≥0, q i k es q' . Por lo tanto, w (0, i 0 )∈ L q 0 , q' y, para todo k ≥0, w ( i k , i k +1 )∈ L q',q' . Por lo tanto, w ∈ L q 0 ,q' ( L q',q' ) ω .
- Recíprocamente, supongamos que w ∈ L q,q' ( L q',q' − { ε } ) ω para algún q ∈ I y q '∈ F . Por lo tanto, existe una secuencia infinita y estrictamente creciente i 0 , i 1 , i 2 ... tal que w (0, i 0 ) ∈ L q,q' y, para todo k ≥0, w ( i k , i k +1 )∈ L q',q' . Por definición de L q,q' , existe una secuencia finita de A desde q hasta q' en la palabra w (0, i 0 ). Para todo k ≥0, existe una secuencia finita de A desde q' hasta q' en la palabra w ( i k , i k +1 ). Por esta construcción, existe una secuencia de A , que comienza desde q y en la que q' aparece infinitas veces. Por lo tanto, w ∈ L ( A ) .
Equivalencia con la lógica monádica de segundo orden
En 1962, Büchi demostró que los lenguajes ω-regulares son precisamente aquellos que se pueden definir en una lógica monádica de segundo orden particular llamada S1S.
Lecturas adicionales
- Wolfgang Thomas, «Autómatas sobre objetos infinitos». En Jan van Leeuwen , editor, Manual de Informática Teórica, volumen B: Modelos Formales y Semántica , páginas 133-192. Elsevier Science Publishers, Ámsterdam, 1990.
- Lenguajes formales
- Palabras infinitas