¿Cuál es la extensión mínima de FO que captura la clase de idiomas regulares?

Contexto: relaciones entre lógica y autómatas

El teorema de Büchi establece que la lógica de segundo orden monádico sobre cadenas (MSO) captura la clase de lenguajes regulares. La prueba muestra que en realidad existencial MSO ( o EMSO ) sobre cadenas es suficiente para capturar los lenguajes regulares. Esto puede ser un poco sorprendente, ya que, sobre las estructuras generales, MSO es estrictamente más expresivo que . $\exists\text{MSO}$ $\exists\text{MSO}$

Mi pregunta (original): ¿una lógica mínima para los idiomas normales?

¿Existe una lógica que, sobre las estructuras generales, es estrictamente menos expresiva que , pero que aún captura la clase de lenguajes regulares cuando se considera sobre cadenas? $\exists\text{MSO}$

En particular, me gustaría saber qué fragmento de los idiomas regulares es capturado por FO sobre cadenas cuando se extiende con un operador de punto menos fijo (FO + LFP). Parece un candidato natural para lo que estoy buscando (si no es ). $\exists\text{MSO}$

Una primera respuesta

Según la respuesta de @ makoto-kanazawa , tanto FO (LFP) como FO (TC) capturan más que los lenguajes regulares, donde TC es un operador de cierre transitivo de relaciones binarias. Queda por ver si TC puede ser reemplazado por otro operador o conjunto de operadores de tal manera que la extensión capture exactamente la clase de lenguajes regulares y no otros.

La lógica de primer orden por sí sola, como sabemos, no es suficiente, ya que captura idiomas libres de estrellas, una subclase adecuada de los idiomas regulares. Como ejemplo clásico, el lenguaje Paridad no puede expresarse usando una oración FO. $\;\;=(aa)^*$

Pregunta actualizada

Aquí hay una nueva redacción de mi pregunta, que permanece sin respuesta.

¿Cuál es la extensión mínima de la lógica de primer orden de manera que FO + esta extensión, cuando se toma sobre cadenas, captura exactamente la clase de lenguajes regulares?

Aquí, una extensión es mínima si es la menos expresiva (cuando se toma sobre estructuras generales) entre todas las extensiones que capturan la clase de lenguajes regulares (cuando se toman sobre cadenas).

reference-request lo.logic regular-language finite-model-theory Janoma
fuente

μ

$\mu$

μ

$\mu$

Parece estar probado en dx.doi.org/10.1109/LICS.1988.5137 para el árbol infinito, y en dx.doi.org/10.1007/3-540-61604-7_60 para la equivalencia con el fragmento de MSO invariante de bisimulación sobre estructuras arbitrarias.

Sylvain

Echo un vistazo al segundo artículo, aunque me temo que muchos conceptos son nuevos para mí. En particular, no sabía acerca de los sistemas de transición invariantes con bisimulación. Parece ser que los DFA son casos particulares de un sistema de transición, pero no sé si son invariantes a la bisimulación. Si lo son, eso respondería parte de mi pregunta (podría haber otra lógica menos expresiva para los idiomas normales); si no lo son, creo que no se puede decir nada, ya que todavía podría haber una equivalencia al considerar solo las cadenas.

Janoma

a_{1} \dots a_{n}

$a_1\cdots a_n$

Σ^{*}

$\Sigma^\ast$

Σ = 2^{P r o p}

$\Sigma=2^{\mathit{Prop}}$

⟨ {1, \dots, n}, 1, {(i, i + 1) ∣ i < n}, {i ∣ p \in a_{i}}_{p \in P r o p} ⟩

$\langle\{1,\dots,n\},1,\{(i,i+1)\mid i<n\},\{i\mid p\in a_i\}_{p\in\mathit{Prop}}\rangle$

FO (LFP) captura PTIME en estructuras ordenadas, y las cadenas son estructuras ordenadas. Por lo tanto, los idiomas definibles por FO (LFP) incluyen todos los idiomas normales y mucho más. http://dx.doi.org/10.1016/S0019-9958(86)80029-8

$\{ a^n b^n \mid n \geq 1 \}$

Makoto Kanazawa
fuente

Excelente. No sé a qué te refieres con TC ^ 1 y TC ^ 2, ¿es eso un error tipográfico? Hasta donde yo sé, en el libro mencionas que la notación utilizada es FO (TC) para la extensión de FO con cierre transitivo y FO (DTC) para la extensión de FO con cierre transitivo determinista , que se define de manera diferente. Sin embargo, no he encontrado el ejercicio que mencionas. Queda por ver si hay un operador menos expresivo que TC que todavía permita capturar idiomas regulares. Actualizaré mi pregunta en consecuencia.