Lógica monádica de segundo orden
En lógica matemática , la lógica monádica de segundo orden ( MSO ) es el fragmento de la lógica de segundo orden donde la cuantificación de segundo orden se limita a la cuantificación sobre conjuntos. [1] Es particularmente importante en la lógica de los gráficos , debido al teorema de Courcelle , que proporciona algoritmos para evaluar fórmulas monádicas de segundo orden sobre gráficos de ancho de árbol acotado . También es de fundamental importancia en la teoría de autómatas , donde el teorema de Büchi-Elgot-Trakhtenbrot da una caracterización lógica de los lenguajes regulares .
La lógica de segundo orden permite la cuantificación sobre predicados . Sin embargo, MSO es el fragmento en el que la cuantificación de segundo orden se limita a predicados monádicos (predicados que tienen un solo argumento). Esto se describe a menudo como cuantificación sobre "conjuntos" porque los predicados monádicos son equivalentes en poder expresivo a conjuntos (el conjunto de elementos para los cuales el predicado es verdadero).
La lógica monádica de segundo orden se presenta en dos variantes. En la variante considerada sobre estructuras como gráficos y en el teorema de Courcelle, la fórmula puede involucrar predicados no monádicos (en este caso, el predicado de borde binario ), pero la cuantificación está restringida a ser solo sobre predicados monádicos. En la variante considerada en la teoría de autómatas y el teorema de Büchi-Elgot-Trakhtenbrot, todos los predicados, incluidos los de la fórmula misma, deben ser monádicos.
La lógica monádica existencial de segundo orden (EMSO) es el fragmento de MSO en el que todos los cuantificadores sobre conjuntos deben ser cuantificadores existenciales , fuera de cualquier otra parte de la fórmula. Los cuantificadores de primer orden no están restringidos. Por analogía con el teorema de Fagin , según el cual la lógica existencial (no monádica) de segundo orden captura precisamente la complejidad descriptiva de la clase de complejidad NP , la clase de problemas que pueden expresarse en la lógica existencial monádica de segundo orden se ha denominado NP monádica. . La restricción a la lógica monádica hace posible probar separaciones en esta lógica que no han sido probadas para la lógica de segundo orden no monádica. Por ejemplo, en la lógica de los gráficos, probar si un gráfico está desconectado pertenece al NP monádico, ya que la prueba se puede representar mediante una fórmula que describe la existencia de un subconjunto adecuado de vértices sin aristas que los conecten con el resto del gráfico; sin embargo, el problema complementario, probar si un gráfico está conectado, no pertenece al NP monádico. [2] [3] La existencia de un par análogo de problemas complementarios, solo uno de los cuales tiene una fórmula existencial de segundo orden (sin la restricción a fórmulas monádicas) es equivalente a la desigualdad de NP y coNP , una cuestión abierta en computacional complejidad.
Por el contrario, cuando deseamos comprobar si una fórmula booleana MSO es satisfecha por un árbol finito de entrada , este problema puede resolverse en tiempo lineal en el árbol, traduciendo la fórmula booleana MSO a un árbol autómata [4] y evaluando el autómata en el árbol. Sin embargo, en cuanto a la consulta, la complejidad de este proceso generalmente no es elemental . [5] Gracias al teorema de Courcelle , también podemos evaluar una fórmula booleana MSO en tiempo lineal en un gráfico de entrada si el ancho del árbol del gráfico está acotado por una constante.
Para fórmulas MSO que tienen variables libres , cuando los datos de entrada son un árbol o tienen un ancho de árbol limitado, existen algoritmos de enumeración eficientes para producir el conjunto de todas las soluciones, [6] asegurando que los datos de entrada se preprocesan en tiempo lineal y que cada solución luego se produce en un retardo lineal en el tamaño de cada solución, es decir, retardo constante en el caso común donde todas las variables libres de la consulta son variables de primer orden (es decir, no representan conjuntos). También existen algoritmos eficientes para contar el número de soluciones de la fórmula MSO en ese caso. [7]