Lógica de computabilidad - Computability logic

No confundir con la lógica computacional .

La lógica de computabilidad ( CoL ) es un programa de investigación y un marco matemático para volver a desarrollar la lógica como una teoría formal sistemática de la computabilidad , en oposición a la lógica clásica, que es una teoría formal de la verdad. Fue introducido y nombrado así por Giorgi Japaridze en 2003.

En la lógica clásica, las fórmulas representan declaraciones verdaderas / falsas. En CoL, las fórmulas representan problemas de cálculo . En la lógica clásica, la validez de una fórmula depende solo de su forma, no de su significado. En CoL, la validez significa ser siempre computable. De manera más general, la lógica clásica nos dice cuándo la verdad de un enunciado dado siempre se sigue de la verdad de un conjunto dado de otros enunciados. De manera similar, CoL nos dice cuándo la computabilidad de un problema A dado siempre se sigue de la computabilidad de otros problemas B 1 , ..., B n . Además, proporciona una forma uniforme de construir realmente una solución ( algoritmo ) para tal A a partir de cualquier solución conocida de B 1 , ..., B n .

CoL formula problemas computacionales en su sentido más general: interactivo . CoL define un problema computacional como un juego jugado por una máquina contra su entorno. Tal problema es computable si hay una máquina que gana el juego contra todos los posibles comportamientos del entorno. Tal máquina de juego generaliza la tesis de Church-Turing al nivel interactivo. El concepto clásico de verdad resulta ser un caso especial de computabilidad con grado de interactividad cero. Esto hace que la lógica clásica sea un fragmento especial de CoL. Por tanto, CoL es una extensión conservadora de la lógica clásica. La lógica de computabilidad es más expresiva, constructiva y computacionalmente significativa que la lógica clásica. Además de la lógica clásica, la lógica amigable con la independencia (IF) y ciertas extensiones propias de la lógica lineal y la lógica intuicionista también resultan ser fragmentos naturales de CoL. Por lo tanto, los conceptos significativos de "verdad intuicionista", "verdad de lógica lineal" y "verdad de lógica IF" pueden derivarse de la semántica de CoL.

CoL responde sistemáticamente a la pregunta fundamental de qué se puede calcular y cómo; por lo tanto, CoL tiene muchas aplicaciones, como teorías aplicadas constructivas, sistemas de base de conocimiento, sistemas de planificación y acción. De estos, solo las aplicaciones en teorías aplicadas constructivas se han explorado extensamente hasta ahora: una serie de teorías numéricas basadas en CoL, denominadas "claritmética", se han construido como alternativas computacionalmente y teóricamente complejas significativas al Peano basado en la lógica clásica. aritmética y sus variaciones tales como sistemas de aritmética acotada .

Los sistemas de prueba tradicionales como la deducción natural y el cálculo secuencial son insuficientes para axiomatizar fragmentos no triviales de CoL. Esto ha requerido el desarrollo de métodos de prueba alternativos, más generales y flexibles, como el cálculo circular .

Idioma

Operadores de lógica de computabilidad: nombres, símbolos y lecturas

El lenguaje completo de CoL amplía el lenguaje de la lógica clásica de primer orden. Su vocabulario lógico tiene varios tipos de conjunciones, disyunciones, cuantificadores, implicaciones, negaciones y los llamados operadores de recurrencia. Esta colección incluye todos los conectivos y cuantificadores de la lógica clásica. El lenguaje también tiene dos tipos de átomos no lógicos: elementales y generales . Los átomos elementales, que no son más que los átomos de la lógica clásica, representan problemas elementales , es decir, juegos sin movimientos que la máquina gana automáticamente cuando es verdadero y se pierde cuando es falso. Los átomos generales, por otro lado, pueden interpretarse como cualquier juego, elemental o no elemental. Tanto semántica como sintácticamente, la lógica clásica no es más que el fragmento de CoL obtenido al prohibir los átomos generales en su lenguaje y prohibir todos los operadores que no sean ¬, ∧, ∨, →, ∀, ∃.

Japaridze ha señalado repetidamente que el lenguaje de CoL es abierto y puede sufrir más extensiones. Debido a la expresividad de este lenguaje, los avances en CoL, como la construcción de axiomatizaciones o la construcción de teorías aplicadas basadas en CoL, generalmente se han limitado a uno u otro fragmento propio del lenguaje.

Semántica

Los juegos subyacentes a la semántica de CoL se denominan juegos estáticos . Estos juegos no tienen orden de turno; un jugador siempre puede moverse mientras los otros jugadores están "pensando". Sin embargo, los juegos estáticos nunca castigan a un jugador por "pensar" demasiado (retrasando sus propios movimientos), por lo que estos juegos nunca se convierten en competencias de velocidad. Todos los juegos elementales son automáticamente estáticos, por lo que se permite que los juegos sean interpretaciones de átomos generales.

Hay dos jugadores en los juegos estáticos: la máquina y el medio ambiente . La máquina solo puede seguir estrategias algorítmicas, mientras que no existen restricciones sobre el comportamiento del entorno. Cada carrera (jugada) la gana uno de estos jugadores y la pierde el otro.

Los operadores lógicos de CoL se entienden como operaciones sobre juegos. Aquí examinamos informalmente algunas de esas operaciones. Por simplicidad asumimos que el dominio del discurso es siempre el conjunto de todos los números naturales: {0,1,2, ...}.

La operación ¬ de negación ("no") cambia los roles de los dos jugadores, convirtiendo los movimientos y victorias de la máquina en los del entorno, y viceversa. Por ejemplo, si el ajedrez es el juego de ajedrez (pero con los empates descartados) desde la perspectiva del jugador blanco, entonces ¬ El ajedrez es el mismo juego desde la perspectiva del jugador negro.

La conjunción paralela ∧ ("pand") y la disyunción paralela ∨ ("por") combinan juegos de forma paralela. Una carrera de A ∧ B o A ∨ B es un juego simultáneo en los dos conjuntos. La máquina gana A ∧ B si gana ambos. La máquina gana A ∨ B si gana al menos uno de ellos. Por ejemplo, Ajedrez ∨¬ El ajedrez es un juego de dos tableros, uno jugado en blanco y otro en negro, y donde la tarea de la máquina es ganar en al menos un tablero. Un juego así se puede ganar fácilmente, independientemente de quién sea el adversario, copiando sus movimientos de un tablero al otro.

La implicación paralelo operador → ( "pimplication") se define por A → B = ¬ A ∨ B . El significado intuitivo de esta operación se reduce B a A , es decir, la resolución de A siempre que el resuelve adversario B .

Los cuantificadores paralelos ∧ ("pall") y ∨ ("pexists") se pueden definir por ∧ xA ( x ) = A (0) ∧ A (1) ∧ A (2) ∧ ... y ∨ xA ( x ) = A (0) ∨ A (1) ∨ A (2) ∨ .... Por lo tanto, se trata de jugadas simultáneas de A (0), A (1), A (2), ..., cada una en un tablero separado . La máquina gana ∧ xA ( x ) si gana todos estos juegos, y ∨ xA ( x ) si gana algunos.

Los cuantificadores ciegos ∀ ("blall") y ∃ ("blexistas"), por otro lado, generan juegos de tablero único. Una carrera de ∀ xA ( x ) o ∃ xA ( x ) es una única ejecución de A . La máquina gana ∀ xA ( x ) (resp. ∃ xA ( x )) si tal corrida es una corrida ganada de A ( x ) para todos (resp. Al menos uno) valores posibles de x , y gana ∃ xA ( x ) si esto es cierto para al menos uno.

Todos los operadores caracterizados hasta ahora se comportan exactamente como sus contrapartes clásicas cuando se aplican a juegos elementales (sin movimiento) y validan los mismos principios. Es por eso que CoL usa los mismos símbolos para esos operadores que la lógica clásica. Sin embargo, cuando estos operadores se aplican a juegos no elementales, su comportamiento ya no es clásico. Entonces, por ejemplo, si p es un átomo elemental y P un átomo general, p → p ∧ p es válido mientras que P → P ∧ P no lo es. El principio del P ∨¬ P medio excluido , sin embargo, sigue siendo válido. El mismo principio no es válido con los otros tres tipos (elección, secuencial y alternancia) de disyunción.

La disyunción de elección ⊔ ("chor") de los juegos A y B , escrita A ⊔ B , es un juego en el que, para ganar, la máquina tiene que elegir uno de los dos disyuntos y luego ganar en el componente elegido. La disyunción secuencial ("sor") A ᐁ B comienza como A ; También extremos como A menos que la máquina hace un movimiento "interruptor", en cuyo caso A se abandona y se reinicia el juego y se mantiene como B . En la disyunción de alternancia ("tor") A ⩛ B , la máquina puede alternar entre A y B cualquier número finito de veces. Cada operador de disyunción tiene su doble conjunción, que se obtiene intercambiando los roles de los dos jugadores. Los cuantificadores correspondientes se pueden definir además como conjunciones o disyunciones infinitas de la misma manera que en el caso de los cuantificadores paralelos. Cada disyunción de género también induce una operación de implicación correspondiente de la misma manera que en el caso de la implicación paralela →. Por ejemplo, la implicación elección ( "chimplication") A ⊐ B se define como ¬ A ⊔ B .

La recurrencia paralela ("precurrencia") de A se puede definir como la conjunción paralela infinita A ∧A∧A∧ ... Los tipos de recurrencias secuenciales ("recurrencia") y alternancia ("trecurrencia") se pueden definir de manera similar.

Los operadores de corecurrencia se pueden definir como disyunciones infinitas. Recurrencia de ramificación ("brecurrencia") ⫰ , que es el tipo de recurrencia más fuerte, no tiene una conjunción correspondiente. ⫰ A es un juego que se inicia y se procede como A . En cualquier momento, sin embargo, se permite que el entorno haga un movimiento "replicativo", que crea dos copias de la posición actual de A , dividiendo así la obra en dos hilos paralelos con un pasado común pero posiblemente desarrollos futuros diferentes. De la misma manera, el medio ambiente puede replicar además cualquiera de las posiciones de cualquier hilo, creando así más y más hilos de A . Esos hilos se reproducen en paralelo, y la máquina necesita para ganar una en todas las discusiones que ser el ganador en ⫰ A . Corecurrence ramificado ("cobrecurrence") ⫯ se define simétricamente intercambiando "máquina" y "entorno".

Cada tipo de recurrencia induce además una correspondiente versión débil de implicación y una versión débil de negación. Se dice que la primera es una imitación y la segunda una refutación . La rimplicación ramificada ("brimplicación") A ⟜ B no es más que ⫰ A → B , y la refutación ramificada ("brefutación") de A es A ⟜ ⊥, donde ⊥ es el juego elemental siempre perdido. Lo mismo ocurre con todos los demás tipos de réplica y refutación.

Como herramienta de especificación de problemas

El lenguaje de CoL ofrece una forma sistemática de especificar una variedad infinita de problemas computacionales, con o sin nombres establecidos en la literatura. A continuación se muestran algunos ejemplos.

Sea f una función unaria. El problema de calcular f se escribirá como ⊓ x ⊔ y ( y = f ( x )). De acuerdo con la semántica de CoL, este es un juego donde el primer movimiento ("entrada") lo realiza el entorno, que debe elegir un valor m para x . Intuitivamente, esto equivale a pedirle a la máquina que diga el valor de f ( m ). El juego continúa como ⊔ y ( y = f ( m )). Ahora se espera que la máquina haga un movimiento ("salida"), que debería elegir un valor n para y . Esto equivale a decir que n es el valor de f (m). El juego ahora se reduce al elemental n = f ( m ), que la máquina gana si y solo si n es de hecho el valor de f ( m ).

Sea p un predicado unario. Entonces ⊓ x ( p ( x ) ⊔¬ p ( x )) expresa el problema de decidir p , ⊓ x ( p ( x ) & ᐁ ¬ p ( x )) expresa el problema de semidecidir p , y ⊓ x ( p ( x ) ⩛¬ p ( x )) el problema de aproximar recursivamente p .

Deje que p y q sean dos predicados unarios. Entonces ⊓ x ( p ( x ) ⊔¬ p ( x )) ⟜ ⊓ x ( q ( x ) ⊔¬ q ( x )) expresa el problema de Turing reductor de q a p (en el sentido de que q es Turing reducible a p si y solo si el problema interactivo ⊓ x ( p ( x ) ⊔¬ p ( x )) ⟜ ⊓ x ( q ( x ) ⊔¬ q ( x )) es computable). ⊓ x ( p ( x ) ⊔¬ p ( x )) → ⊓ x ( q ( x ) ⊔¬ q ( x )) hace lo mismo, pero para la versión más fuerte de la reducción de Turing, donde el oráculo para p se puede consultar solo una vez . ⊓ x ⊔ y ( q ( x ) ↔ p ( y )) hace lo mismo para el problema de muchos-uno la reducción de q a p . Con expresiones más complejas se puede capturar todo tipo de sin nombre, sin embargo, las relaciones potencialmente significativas y operaciones sobre los problemas computacionales, tales como, por ejemplo, "Turing reducir el problema de la semideciding r al problema de mucho-uno la reducción de q a p ". Al imponer restricciones de tiempo o espacio al trabajo de la máquina, se obtienen contrapartes teóricas de la complejidad de tales relaciones y operaciones.

Como herramienta de resolución de problemas

Los sistemas deductivos conocidos para varios fragmentos de CoL comparten la propiedad de que una solución (algoritmo) puede extraerse automáticamente de una prueba de un problema en el sistema. Esta propiedad es heredada por todas las teorías aplicadas basadas en esos sistemas. Entonces, para encontrar una solución para un problema dado, es suficiente expresarlo en el lenguaje de CoL y luego encontrar una prueba de esa expresión. Otra forma de ver este fenómeno es pensar en una fórmula G de CoL como una especificación de programa (objetivo). Entonces, una prueba de G es, más precisamente, se traduce en un programa que cumple con esa especificación. No es necesario verificar que se cumpla la especificación, porque la prueba en sí misma es, de hecho, una verificación de este tipo.

Ejemplos de teorías aplicadas basadas en CoL son las llamadas claritméticas . Estas son teorías numéricas basadas en CoL en el mismo sentido en que la aritmética de Peano PA se basa en la lógica clásica. Este sistema suele ser una extensión conservadora de la PA. Por lo general, incluye todos los axiomas de Peano y les agrega uno o dos axiomas extra de Peano como ⊓ x ⊔ y ( y = x ' ) que expresan la capacidad de cálculo de la función sucesora. Por lo general, también tiene una o dos reglas de inferencia no lógicas, como las versiones constructivas de inducción o comprensión. A través de variaciones rutinarias en dichas normas se puede obtener sistemas completos de sonido y la caracterización de una u otra interactivo computacional clase de complejidad C . Esto es en el sentido de que un problema pertenece a C si y solo si tiene una prueba en la teoría. Por lo tanto, dicha teoría puede usarse para encontrar no solo soluciones algorítmicas, sino también eficientes bajo demanda, como soluciones que se ejecutan en tiempo polinomial o espacio logarítmico. Cabe señalar que todas las teorías claritméticas comparten los mismos postulados lógicos, y solo sus postulados no lógicos varían según la clase de complejidad objetivo. Su característica distintiva notable de otros enfoques con aspiraciones similares (como la aritmética acotada ) es que amplían la PA en lugar de debilitarla, preservando todo el poder deductivo y la conveniencia de esta última.

Ver también

Referencias

enlaces externos