Soy un programador con control sobre los autómatas, pero no sobre la lógica.
Leí en periódicos que los dos están estrechamente relacionados. Los autómatas finitos deterministas (DFA), los autómatas de árbol y los autómatas visiblemente pushdown están todos relacionados con la lógica monádica de segundo orden (MSO). Aunque entiendo que los autómatas y las personas (en documentos) han tratado de explicarme la relación con MSO, siempre asumen una sólida formación en lógica y una comprensión de MSO.
Cuando miro libros y cursos sobre lógica, en su mayoría solo manejan lógica de primer orden, lo que parece bastante simple y que consta de solo unos pocos conceptos: variables, o, y no, implica, para todos, existe, etc.
¿Puede alguien explicarme o señalarme un recurso que pueda explicar:
- ¿Qué es la lógica de segundo orden en contraste con la lógica de primer orden?
- ¿Qué es la lógica monádica vs no monádica?
- ¿Por qué es importante que una lógica de segundo orden sea monádica para ser decidible O por qué esta es la pregunta incorrecta?
- ¿Por qué es decidible la lógica monádica de segundo orden?
- ¿La relación con al menos DFA?
Si es un recurso, sería bueno si supone que soy un programador y no un lógico. Esto significa que me gustaría entender cómo lo implementaría como código, porque hasta entonces las matemáticas me parecen mágicas;)
Gracias por cualquier ayuda que me puedan dar. Yo realmente lo apreciaría.
fuente
Respuestas:
La lógica monádica de segundo orden es la lógica de primer orden más la cuantificación sobre conjuntos. Entonces, además de poder decir que existe un elemento de dominio con alguna propiedad ( ), también puede decir que existe un conjunto de elementos de dominio con alguna propiedad. Entonces, por ejemplo, podemos definir la capacidad de 3 colores de los gráficos diciendo∃x…
En palabras, hay colores rojo, verde y azul que
La lógica general de segundo orden permite no solo la cuantificación sobre conjuntos sino también sobre relaciones arbitrarias sobre el dominio. Recuerde que una relación es un conjunto de -tuplas sobre el dominio, para algunos . Los conjuntos son solo relaciones unarias: y una tupla es solo un elemento del dominio.k k k=1 1
Honestamente, no recuerdo los problemas de capacidad de decisión. Un punto clave es que la lógica completa de segundo orden le permite cuantificar en existencia un orden lineal del dominio
Es decir, existe una relación binaria que es total, antisimétrica y transitiva, es decir, es un orden lineal en el dominio . Eso le da implícitamente un orden lineal en para cualquier , y puede usar relaciones en para suficientemente grande como para simular una cinta de máquina de Turing. Pero, con SO monádico, no puedes hacer ninguna de estas cosas.D Dn n Dn n
(Supongo que, si su dominio es infinito, probablemente deba especificar además que el orden lineal es discreto y tiene un elemento mínimo; entonces sabe que tiene un segmento inicial que es isomorfo a los números naturales, y eso debería ser suficiente.)
En entradas finitas, el fragmento existencial de SO - fórmulas de la forma , donde son símbolos de relación y es de primer orden - define exactamente NP . La lógica completa de segundo orden define exactamente la jerarquía polinómica. Esto se debe exactamente a la capacidad de codificar máquinas de Turing y al hecho de que cuantificar una colección fija de relaciones te da una cantidad polinómica de cosas con las que jugar.∃R1…∃Rkφ Ri φ
Podemos representar cadenas sobre algún alfabeto finito por estructuras relacionales. El vocabulario tiene un símbolo de relación binaria que se interpretará como un orden lineal, y un símbolo de relación poco para cada carácter . Cada elemento del dominio es un carácter en la cadena, el orden lineal le indica en qué orden aparecen los caracteres y las relaciones indican qué carácter aparece en cada posición.Σ ≤ Ra a∈Σ Ra
Ahora, supongamos que tenemos un DFA con estados y supongamos que estamos tratando con cadenas finitas, por ahora. Podemos escribir una fórmula que sea ampliamente similar a la fórmula de tres colores que dice que nuestro DFA acepta la cadena codificada por su entrada. Dice que hay conjuntos (de elementos de dominio, es decir, posiciones en la cadena) , de modo que será el conjunto de posiciones en la cadena en la que el autómata se encuentra en el estado . Entonces afirma que:k Q1,…,Qk Qi i
Si esta fórmula es verdadera, el autómata debe aceptar la cadena; si es falso, el autómata debe rechazarlo. Para los NFA, solo decimos que cada posición está en al menos un estado y el estado final está en al menos un estado de aceptación. Para entradas infinitas, podemos codificar, por ejemplo, la condición de Büchi diciendo "para todas las posiciones en la entrada, si está en un estado de aceptación, hay algo de tal que también está en un estado de aceptación.j j ′ > j j ′j j j′>j j′
En este momento, no recuerdo la prueba de lo contrario (que todo lo definible en MSO puede ser reconocido por un autómata apropiado). Si tengo tiempo, lo buscaré y publicaré un boceto.
Por el contrario , podemos representar el significado de las fórmulas MSO por autómatas de estado finito inductivamente, siguiendo la construcción de los autómatas. Para ello aumentamos el alfabeto del autómata, mediante la adición de componentes que indican el valor de las variables de posición libres y establecer las variables . Si leemos una cadena a lo largo del autómata, encontramos exactamente un para indicar una cierta posición , y las posiciones en un conjunto se marcan de la misma manera.X 1 i Xi X 1 i X
Las fórmulas básicas son para "posición tiene el símbolo ", para " es un elemento de " e para "posición está antes de la posición ". Estas fórmulas se pueden representar mediante los siguientes autómatas simples de estado finito (sobre el alfabeto aumentado adecuado para la fórmula):i a i ∈ X i X i < j i jRa(i) i a i∈X i X i<j i j
Fórmulas más complicadas se construyen utilizando las conectivas booleanas y los cuantificadores existenciales . El significado pretendido de estos operadores se traduce fácilmente a los idiomas como los operadores de lenguaje union , complemento y proyección , que es la operación que elimina el componente correspondiente del alfabeto aumentado. Para la unión, debemos prestar atención a los alfabetos aumentados en caso de que las dos partes de la fórmula no estén de acuerdo con el conjunto de variables libres. La proyección es simple, pero cambiará un autómata determinista a uno no determinista.∃ i , ∃ X ∪∨,¬ ∃i,∃X ∪ c
fuente