La lógica computacional ( CoL ) es un programa de investigación y un marco matemático para el rediseño de la lógica como 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 introducida y bautizada así por Giorgi Japaridze en 2003. [1]
En la lógica clásica, las fórmulas representan afirmaciones verdaderas o falsas . En la lógica de la ley, las fórmulas representan problemas computacionales . En la lógica clásica, la validez de una fórmula depende solo de su forma, no de su significado. En la lógica de la ley, validez significa ser siempre computable. En términos más generales, la lógica clásica nos dice cuándo la verdad de una afirmación dada siempre se sigue de la verdad de un conjunto dado de otras afirmaciones. De manera similar, la lógica de la ley nos dice cuándo la computabilidad de un problema dado A siempre se sigue de la computabilidad de otros problemas dados 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 .
La CoL formula problemas computacionales en su sentido más general ( el interactivo ). La 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 cada comportamiento posible del entorno. Tal máquina que juega al juego generaliza la tesis de Church-Turing al nivel interactivo. El concepto clásico de verdad resulta ser un caso especial de computabilidad de grado cero de interactividad. Esto hace que la lógica clásica sea un fragmento especial de la CoL. Por lo tanto, la 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 favorable a la independencia (IF) y ciertas extensiones adecuadas de la lógica lineal y la lógica intuicionista también resultan ser fragmentos naturales de la CoL. [2] [3] 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 la 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 para la planificación y la acción. De estas, hasta ahora solo se han explorado en profundidad las aplicaciones en teorías aplicadas constructivas: se han construido una serie de teorías de números basadas en CoL, denominadas "claritméticas", [4] [5] como alternativas significativas desde el punto de vista computacional y teórico de la complejidad a la aritmética de Peano de primer orden basada en la lógica clásica y sus variaciones, como los 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 hecho necesario desarrollar métodos de prueba alternativos, más generales y flexibles, como el cálculo circunferencial . [6] [7]
El lenguaje completo de CoL extiende 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 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 en repetidas ocasiones que el lenguaje de CoL es abierto y puede sufrir nuevas ampliaciones. Debido a la expresividad de este lenguaje, los avances en CoL, como la construcción de axiomatizaciones o la elaboración de teorías aplicadas basadas en CoL, generalmente se han limitado a uno u otro fragmento del lenguaje.
Los juegos que sustentan la semántica de CoL se denominan juegos estáticos . Estos juegos no tienen un orden de turnos; un jugador siempre puede mover mientras los otros jugadores están "pensando". Sin embargo, los juegos estáticos nunca castigan a un jugador por "pensar" demasiado tiempo (retrasando sus propios movimientos), por lo que estos juegos nunca se convierten en concursos de velocidad. Todos los juegos elementales son automáticamente estáticos, y por lo tanto se permite que los juegos sean interpretaciones de átomos generales.
En los juegos estáticos hay dos jugadores: la máquina y el entorno . La máquina solo puede seguir estrategias algorítmicas, mientras que no hay restricciones sobre el comportamiento del entorno. Cada partida (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. Para simplificar, suponemos 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 las victorias de la máquina en los del entorno, y viceversa. Por ejemplo, si el ajedrez es el juego de ajedrez (pero sin empates) 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 partidas de forma paralela. Una serie de A ∧ B o A ∨ B es una jugada simultánea en las dos conjunciones. La máquina gana A ∧ B si gana ambas. La máquina gana A ∨ B si gana al menos una de ellas. Por ejemplo, Ajedrez ∨¬ El ajedrez es un juego en dos tableros, uno jugado con blancas y otro con negras, y donde la tarea de la máquina es ganar en al menos un tablero. Un juego de este tipo se puede ganar fácilmente independientemente de quién sea el adversario, copiando sus movimientos de un tablero al otro.
El operador de implicación paralela → ("pimplificación") se define por A → B = ¬ A ∨ B . El significado intuitivo de esta operación es reducir B a A , es decir, resolver A siempre que el adversario resuelva B .
Los cuantificadores paralelos ∧ ("pall") y ∨ ("pexists") pueden definirse por ∧ xA ( x ) = A (0)∧ A (1)∧ A (2)∧... y ∨ xA ( x ) = A (0)∨ A (1)∨ A (2)∨.... Se trata, pues, de partidas simultáneas de A (0), A (1), A (2),..., cada una en un tablero distinto. La máquina gana ∧ xA ( x ) si gana todas estas partidas, y ∨ xA ( x ) si gana algunas.
Los cuantificadores ciegos ∀ ("blall") y ∃ ("blexists"), por otro lado, generan juegos de un solo tablero. Una serie de ∀ xA ( x ) o ∃ xA ( x ) es una serie única de A . La máquina gana ∀ xA ( x ) (respectivamente ∃ xA ( x )) si dicha serie es una serie ganada de A ( x ) para todos (respectivamente 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 esto que CoL usa los mismos símbolos para esos operadores que la lógica clásica. Sin embargo, cuando tales operadores se aplican a juegos no elementales, su comportamiento ya no es clásico. Así, 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 tercero excluido P ∨¬ P , sin embargo, sigue siendo válido. El mismo principio es invá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 termina como A a menos que la máquina haga un movimiento de "cambio", en cuyo caso A se abandona y el juego se reinicia y continúa como B . En la disyunción de alternancia ("tor") A ⩛ B , la máquina puede cambiar entre A y B cualquier número finito de veces. Cada operador de disyunción tiene su conjunción dual, obtenida intercambiando los roles de los dos jugadores. Los cuantificadores correspondientes pueden definirse además como conjunciones o disyunciones infinitas de la misma manera que en el caso de los cuantificadores paralelos. Cada tipo de disyunción también induce una operación de implicación correspondiente de la misma manera que este fue el caso con la implicación paralela →. Por ejemplo, la implicación de elección ("chimplicación") 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 recurrencia secuencial ("srecurrencia") y alternante ("trecurrencia") se pueden definir de manera similar.
Los operadores de correcurrencia se pueden definir como disyunciones infinitas. La recurrencia ramificada ("brecurrencia") ⫰ , que es el tipo más fuerte de recurrencia, no tiene una conjunción correspondiente. ⫰ A es un juego que comienza y continúa como A . Sin embargo, en cualquier momento, se permite al entorno hacer un movimiento "replicativo", que crea dos copias de la posición actual de A , dividiendo así el juego en dos hilos paralelos con un pasado común pero posiblemente desarrollos futuros diferentes. De la misma manera, el entorno puede replicar cualquiera de las posiciones de cualquier hilo, creando así más y más hilos de A . Esos hilos se juegan en paralelo, y la máquina necesita ganar A en todos los hilos para ser el ganador en ⫰ A . La correcurrencia ramificada ("cobrecurrencia") ⫯ se define simétricamente intercambiando "máquina" y "entorno".
Cada tipo de recurrencia induce además una versión débil correspondiente de la implicación y una versión débil de la negación. La primera se llama rimplicación y la segunda, refutación . La rimplicación ramificada ("brimplicación") A ⟜ B no es otra cosa que ⫰ A → B , y la refutación ramificada ("brefutación") de A es A ⟜ ⊥, donde ⊥ es el juego elemental que siempre se pierde. Lo mismo ocurre con todos los demás tipos de rimplicación y refutación.
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 presentan algunos ejemplos.
Sea f una función unaria . El problema de calcular f se escribirá como ⊓ x ⊔ y( y = f ( x )). Según 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 ser 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 gana la máquina 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 .
Sean p y q dos predicados unarios. Entonces ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) expresa el problema de reducción de Turing de q a p (en el sentido de que q es reducible por Turing 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 puede consultarse solo una vez. ⊓ x ⊔ y ( q ( x )↔ p ( y )) hace lo mismo para el problema de muchos-uno que reduce q a p . Con expresiones más complejas se pueden capturar todo tipo de relaciones y operaciones sin nombre pero potencialmente significativas en problemas computacionales, como, por ejemplo, "reducir mediante Turing el problema de semidecidir r al problema de muchos-uno que reduce q a p ". Al imponer restricciones de tiempo o espacio al trabajo de la máquina, se obtienen además contrapartes teóricas de la complejidad de tales relaciones y operaciones.
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 además por todas las teorías aplicadas basadas en esos sistemas. Por lo tanto, 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 especificación (meta) del programa. Entonces una prueba de G es –más precisamente, se traduce en– un programa que cumple con esa especificación. No hay necesidad de verificar que se cumpla la especificación, porque la prueba en sí es, de hecho, una verificación de ese tipo.
Ejemplos de teorías aplicadas basadas en CoL son las llamadas claritméticas . Estas son teorías de números basadas en CoL en el mismo sentido que la aritmética de Peano de primer orden PA se basa en la lógica clásica. Un sistema de este tipo suele ser una extensión conservadora de PA. Normalmente incluye todos los axiomas de Peano y les añade uno o dos axiomas extra-Peano como ⊓ x ⊔ y ( y = x' ) que expresa la computabilidad de la función sucesora. Normalmente también tiene una o dos reglas de inferencia no lógicas, como versiones constructivas de inducción o comprensión . A través de variaciones rutinarias en tales reglas se pueden obtener sistemas sólidos y completos que caracterizan una u otra clase de complejidad computacional interactiva 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, una teoría de este tipo se puede utilizar para encontrar no solo soluciones algorítmicas, sino también soluciones eficientes a pedido, 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 sólo sus postulados no lógicos varían según la clase de complejidad de destino. Su característica distintiva notable con respecto a otros enfoques con aspiraciones similares (como la aritmética acotada ) es que extienden la PA en lugar de debilitarla, preservando todo el poder deductivo y la conveniencia de esta última.