La lógica lineal es una lógica subestructural propuesta por el lógico francés Jean-Yves Girard como un refinamiento de la lógica clásica e intuicionista , uniendo las dualidades de la primera con muchas de las propiedades constructivas de la segunda. [1] Aunque la lógica también se ha estudiado por sí misma, de manera más amplia, las ideas de la lógica lineal han sido influyentes en campos como los lenguajes de programación , la semántica de juegos y la física cuántica (porque la lógica lineal puede verse como la lógica de la teoría de la información cuántica ), [2] así como la lingüística , [3] particularmente debido a su énfasis en la limitación de recursos, la dualidad y la interacción.
La lógica lineal se presta a muchas presentaciones, explicaciones e intuiciones diferentes. En teoría de la demostración , se deriva de un análisis del cálculo secuencial clásico en el que se controlan cuidadosamente los usos de (las reglas estructurales ) contracción y debilitamiento . Operativamente, esto significa que la deducción lógica ya no se trata simplemente de una colección en constante expansión de "verdades" persistentes, sino también de una forma de manipular recursos que no siempre se pueden duplicar o desechar a voluntad. En términos de modelos denotacionales simples , la lógica lineal puede verse como un refinamiento de la interpretación de la lógica intuicionista al reemplazar las categorías cartesianas (cerradas) por categorías monoidales simétricas (cerradas) , o la interpretación de la lógica clásica al reemplazar las álgebras de Boole por las C*-álgebras . [ cita requerida ]
El lenguaje de la lógica lineal clásica (LLC) se define inductivamente mediante la notación BNF
Aquí p y p ⊥ abarcan átomos lógicos . Por razones que se explicarán a continuación, los conectivos ⊗, ⅋, 1 y ⊥ se denominan multiplicativos , los conectivos &, ⊕, ⊤ y 0 se denominan aditivos y los conectivos ! y ? se denominan exponenciales . Podemos emplear además la siguiente terminología:
Los conectivos binarios ⊗, ⊕, & y ⅋ son asociativos y conmutativos; 1 es la unidad para ⊗, 0 es la unidad para ⊕, ⊥ es la unidad para ⅋ y ⊤ es la unidad para &.
Toda proposición A en CLL tiene un dual A ⊥ , definido de la siguiente manera:
Obsérvese que (-) ⊥ es una involución , es decir, A ⊥⊥ = A para todas las proposiciones. A ⊥ también se denomina negación lineal de A .
Las columnas de la tabla sugieren otra forma de clasificar los conectivos de la lógica lineal, denominadapolaridad : los conectivos negados en la columna de la izquierda (⊗, ⊕, 1, 0, !) se llamanpositivos, mientras que sus duales en la derecha (⅋, &, ⊥, ⊤, ?) se llamannegativos; cf. tabla de la derecha.
La implicación lineal no está incluida en la gramática de los conectivos, pero se puede definir en CLL usando negación lineal y disyunción multiplicativa, por A ⊸ B := A ⊥ ⅋ B . El conectivo ⊸ a veces se pronuncia "lollipop", debido a su forma.
Una forma de definir la lógica lineal es como un cálculo secuencial . Usamos las letras Γ y Δ para abarcar listas de proposiciones A 1 , ..., A n , también llamadas contextos . Un secuencial coloca un contexto a la izquierda y a la derecha del torniquete , escrito Γ Δ . Intuitivamente, el secuencial afirma que la conjunción de Γ implica la disyunción de Δ (aunque nos referimos a la conjunción y disyunción "multiplicativas", como se explica a continuación). Girard describe la lógica lineal clásica usando solo secuenciales unilaterales (donde el contexto de la izquierda está vacío), y aquí seguimos esa presentación más económica. Esto es posible porque cualquier premisa a la izquierda de un torniquete siempre se puede mover al otro lado y dualizar.
Ahora damos reglas de inferencia que describen cómo construir pruebas de secuencias. [4]
En primer lugar, para formalizar el hecho de que no nos importa el orden de las proposiciones dentro de un contexto, agregamos la regla estructural del intercambio :
Nótese que no agregamos las reglas estructurales de debilitamiento y contracción, porque nos preocupamos por la ausencia de proposiciones en un consecuente y el número de copias presentes.
A continuación añadimos los secuenciadores iniciales y los cortes :
La regla de corte puede verse como una forma de componer demostraciones, y los consecuentes iniciales sirven como unidades para la composición. En cierto sentido, estas reglas son redundantes: a medida que introducimos reglas adicionales para construir demostraciones más adelante, mantendremos la propiedad de que se pueden derivar consecuentes iniciales arbitrarios a partir de consecuentes iniciales atómicos, y que siempre que un consecuente sea demostrable, se le puede dar una demostración sin cortes. En última instancia, esta propiedad de forma canónica (que se puede dividir en la completitud de los consecuentes iniciales atómicos y el teorema de eliminación de cortes , lo que induce una noción de demostración analítica ) se encuentra detrás de las aplicaciones de la lógica lineal en la ciencia informática, ya que permite que la lógica se use en la búsqueda de demostraciones y como un cálculo lambda consciente de los recursos .
Ahora, explicamos los conectivos dando reglas lógicas . Por lo general, en el cálculo consecuente se dan tanto "reglas de derecha" como "reglas de izquierda" para cada conectivo, describiendo esencialmente dos modos de razonamiento sobre proposiciones que involucran ese conectivo (por ejemplo, verificación y falsación). En una presentación unilateral, en cambio, se hace uso de la negación: las reglas de derecha para un conectivo (por ejemplo, ⅋) desempeñan efectivamente el papel de reglas de izquierda para su dual (⊗). Por lo tanto, deberíamos esperar una cierta "armonía" entre la(s) regla(s) para un conectivo y la(s) regla(s) para su dual.
Las reglas para la conjunción multiplicativa (⊗) y la disyunción (⅋):
y para sus unidades:
Obsérvese que las reglas para la conjunción y disyunción multiplicativas son admisibles para la conjunción y disyunción simples bajo una interpretación clásica (es decir, son reglas admisibles en LK ).
Las reglas para la conjunción aditiva (&) y la disyunción (⊕):
y para sus unidades:
Obsérvese que las reglas para la conjunción y disyunción aditivas son nuevamente admisibles bajo una interpretación clásica. Pero ahora podemos explicar la base para la distinción multiplicativa/aditiva en las reglas para las dos versiones diferentes de la conjunción: para el conectivo multiplicativo (⊗), el contexto de la conclusión ( Γ , Δ ) se divide entre las premisas, mientras que para el conectivo de caso aditivo (&) el contexto de la conclusión ( Γ ) se lleva íntegro a ambas premisas.
Las exponenciales se utilizan para dar acceso controlado al debilitamiento y la contracción. En concreto, añadimos reglas estructurales de debilitamiento y contracción para las proposiciones ? 'd: [5]
y utilizar las siguientes reglas lógicas, en las que ?Γ representa una lista de proposiciones, cada una prefijada con ? :
Se podría observar que las reglas para los exponenciales siguen un patrón diferente de las reglas para los otros conectivos, similar a las reglas de inferencia que gobiernan las modalidades en las formalizaciones de cálculo secuencial de la lógica modal normal S4 , y que ya no hay una simetría tan clara entre los duales ! y ? . Esta situación se remedia en presentaciones alternativas de CLL (por ejemplo, la presentación LU).
Además de las dualidades de De Morgan descritas anteriormente, algunas equivalencias importantes en lógica lineal incluyen:
Por definición de A ⊸ B como A ⊥ ⅋ B , las dos últimas leyes de distributividad también dan:
(Aquí A ≣ B es ( A ⊸ B ) y ( B ⊸ A ) .)
Un mapa que no es un isomorfismo pero que juega un papel crucial en la lógica lineal es:
Las distribuciones lineales son fundamentales en la teoría de la demostración de la lógica lineal. Las consecuencias de esta función se investigaron por primera vez en [6] y se la denominó "distribución débil". En trabajos posteriores se la rebautizó como "distribución lineal" para reflejar la conexión fundamental con la lógica lineal.
Las siguientes fórmulas de distributividad no son en general una equivalencia, solo una implicación:
Tanto la implicación intuicionista como la clásica se pueden recuperar a partir de la implicación lineal insertando exponenciales: la implicación intuicionista se codifica como ! A ⊸ B , mientras que la implicación clásica se puede codificar como !? A ⊸ ? B o ! A ⊸ ?! B (o una variedad de posibles traducciones alternativas). [7] La idea es que los exponenciales nos permiten usar una fórmula tantas veces como necesitemos, lo que siempre es posible en la lógica clásica e intuicionista.
Formalmente, existe una traducción de fórmulas de lógica intuicionista a fórmulas de lógica lineal de manera que se garantice que la fórmula original sea demostrable en lógica intuicionista si y solo si la fórmula traducida es demostrable en lógica lineal. Utilizando la traducción negativa de Gödel–Gentzen , podemos así integrar la lógica clásica de primer orden en la lógica lineal de primer orden.
Lafont (1993) fue el primero en demostrar que la lógica lineal intuicionista puede explicarse como una lógica de recursos, lo que permite que el lenguaje lógico tenga acceso a formalismos que pueden utilizarse para razonar sobre los recursos dentro de la propia lógica, en lugar de, como en la lógica clásica, por medio de predicados y relaciones no lógicas. El ejemplo clásico de la máquina expendedora de Tony Hoare (1985) puede utilizarse para ilustrar esta idea.
Supongamos que representamos tener una barra de chocolate por la proposición atómica candy , y tener un dólar por $1 . Para indicar el hecho de que un dólar le comprará una barra de chocolate, podríamos escribir la implicación $1 ⇒ candy . Pero en la lógica ordinaria (clásica o intuicionista), de A y A ⇒ B se puede concluir A ∧ B . ¡Entonces, la lógica ordinaria nos lleva a creer que podemos comprar la barra de chocolate y quedarnos con nuestro dólar! Por supuesto, podemos evitar este problema utilizando codificaciones más sofisticadas, [ aclaración necesaria ] aunque típicamente tales codificaciones sufren el problema del marco . Sin embargo, el rechazo del debilitamiento y la contracción permite que la lógica lineal evite este tipo de razonamiento espurio incluso con la regla "ingenua". En lugar de $1 ⇒ candy , expresamos la propiedad de la máquina expendedora como una implicación lineal $1 ⊸ candy . De $1 y este hecho, podemos concluir candy , pero no $1 ⊗ candy . En general, podemos utilizar la proposición de lógica lineal A ⊸ B para expresar la validez de transformar el recurso A en el recurso B.
Siguiendo con el ejemplo de la máquina expendedora, consideremos las "interpretaciones de recursos" de los otros conectores multiplicativos y aditivos. (Los exponenciales proporcionan los medios para combinar esta interpretación de recursos con la noción habitual de verdad lógica persistente ).
La conjunción multiplicativa ( A ⊗ B ) denota la ocurrencia simultánea de recursos, que se utilizarán como indique el consumidor. Por ejemplo, si compra un chicle y una botella de refresco, entonces está solicitando chicle ⊗ refresco . La constante 1 denota la ausencia de cualquier recurso y, por lo tanto, funciona como la unidad de ⊗.
La conjunción aditiva ( A & B ) representa la ocurrencia alternativa de recursos, cuya elección controla el consumidor. Si en la máquina expendedora hay un paquete de papas fritas, una barra de chocolate y una lata de refresco, cada uno cuesta un dólar, entonces por ese precio puedes comprar exactamente uno de estos productos. Por lo tanto, escribimos $1 ⊸ ( caramelos & papas fritas & bebida ) . No escribimos $ 1 ⊸ ( caramelos ⊗ papas fritas ⊗ bebida ) , lo que implicaría que un dólar es suficiente para comprar los tres productos juntos. Sin embargo, de $1 ⊸ ( caramelos & papas fritas & bebida ) , podemos deducir correctamente $3 ⊸ ( caramelos ⊗ papas fritas ⊗ bebida ) , donde $3 := $1 ⊗ $1 ⊗ $1 . La unidad ⊤ de la conjunción aditiva puede verse como una papelera para recursos innecesarios. Por ejemplo, podemos escribir $3 ⊸ ( candy ⊗ ⊤) para expresar que con tres dólares puedes obtener una barra de chocolate y algunas otras cosas, sin ser más específicos (por ejemplo, papas fritas y una bebida, o $2, o $1 y papas fritas, etc.).
La disyunción aditiva ( A ⊕ B ) representa la ocurrencia alternativa de recursos, cuya elección controla la máquina. Por ejemplo, supongamos que la máquina expendedora permite juegos de azar: inserte un dólar y la máquina puede dispensar una barra de chocolate, un paquete de papas fritas o un refresco. Podemos expresar esta situación como $1 ⊸ ( caramelo ⊕ papas fritas ⊕ bebida ) . La constante 0 representa un producto que no se puede fabricar y, por lo tanto, sirve como unidad de ⊕ (una máquina que podría producir A o 0 es tan buena como una máquina que siempre produce A porque nunca tendrá éxito en producir un 0). Entonces, a diferencia de lo anterior, no podemos deducir $3 ⊸ ( caramelo ⊗ papas fritas ⊗ bebida ) de esto.
Introducidas por Jean-Yves Girard , las redes de prueba fueron creadas para evitar la burocracia , es decir todas las cosas que hacen que dos derivaciones sean diferentes desde el punto de vista lógico, pero no desde el punto de vista "moral".
Por ejemplo, estas dos pruebas son "moralmente" idénticas:
El objetivo de las redes de prueba es hacerlas idénticas creando una representación gráfica de ellas.
La relación de implicación en CLL completa es indecidible . [8] Al considerar fragmentos de CLL, el problema de decisión tiene una complejidad variable:
Al modificar aún más las reglas estructurales, surgen muchas variaciones de la lógica lineal:
Se han considerado diferentes variantes intuicionistas de la lógica lineal. Cuando se basa en una presentación de cálculo secuencial de conclusión única, como en ILL (Intuitionistic Linear Logic), los conectivos ⅋, ⊥ y ? están ausentes, y la implicación lineal se trata como un conectivo primitivo. En FILL (Full Intuitionistic Linear Logic) los conectivos ⅋, ⊥ y ? están presentes, la implicación lineal es un conectivo primitivo y, de manera similar a lo que ocurre en la lógica intuicionista, todos los conectivos (excepto la negación lineal) son independientes. También existen extensiones de primer y de orden superior de la lógica lineal, cuyo desarrollo formal es más o menos estándar (véase lógica de primer orden y lógica de orden superior ).
Medios relacionados con Lógica lineal en Wikimedia Commons
