Lógica lineal

lógica lineal es una lógica subestructural propuesta por 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. Aunque la lógica también se ha estudiado por sí misma, en términos más generales, 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)., así como la lingüística, 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. Teóricamente, se deriva de un análisis del cálculo secuencial clásico en el que los usos de la contracción y el debilitamiento (las reglas estructurales) se controlan cuidadosamente. Operacionalmente, 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, se puede considerar que la lógica lineal refina la interpretación de la lógica intuicionista reemplazando categorías cartesianas (cerradas) por categorías monoidales simétricas (cerradas), o la interpretación de la lógica clásica reemplazando álgebras booleanas por álgebras C*.

Conectivas, dualidad y polaridad

Sintaxis

El lenguaje de la lógica lineal clásica (CLL) se define inductivamente mediante la notación BNF.

Aquí p y p^⊥< /span> rango sobre átomos lógicos. Por razones que se explicarán a continuación, las conectivas ⊗, ⅋, 1 y ⊥ se denominan multiplicativas, las conectivas &, ⊕, ⊤ y 0 se denominan aditivas, y los conectivos! y ? se llaman exponenciales. Además podemos emplear la siguiente terminología:

Conectivos binarios ⊗, ⊕ y & y ⅋ son asociativos y conmutativos; 1 es la unidad de ⊗, 0 es la unidad de ⊕, ⊥ es la unidad de ⅋ y ⊤ es la unidad de &.

Cada proposición A en CLL tiene una dual A< /var>^⊥, definido de la siguiente manera:

Observe que (-)^⊥ es una involución, es decir, A ^⊥⊥ = A para todas las proposiciones. A^⊥ también se llama negación lineal de A.

Las columnas de la tabla sugieren otra forma de clasificar las conectivas de la lógica lineal, denominada polaridad: los conectivos negados en la columna de la izquierda (⊗, ⊕, 1, 0, !) se llaman positivos, mientras que sus duales de la derecha (⅋, &, ⊥, ⊤, ?) se denominan negativos; cf. mesa de la derecha.

Implicación lineal no está incluido en la gramática de los conectivos, pero se puede definir en CLL mediante negación lineal y disyunción multiplicativa, mediante A ⊸ B:= < var>A^⊥ ⅋ B. El conectivo ⊸ a veces se pronuncia "piruleta" debido a su forma.

Presentación de cálculo secuencial

Una manera de definir la lógica lineal es como un cálculo secuencial. Usamos las letras . y Δ para abarcar la lista de propuestas A₁,... A_n, también llamado contexts. A sequent coloca un contexto a la izquierda y a la derecha del torntil, escrito . ${displaystyle vdash }$ Δ. Intuitivamente, el secuente afirma que la conjunción de . implica la disyunción de Δ (aunque nos referimos a la conjunción y disyunción "multiplicativa", como se explica a continuación). Girard describe la lógica lineal clásica usando sólo un lado secuenciadores (donde el contexto izquierdo está vacío), y seguimos aquí esa presentación más económica. Esto es posible porque cualquier local a la izquierda de un torntil siempre puede ser trasladado al otro lado y dualizado.

Ahora damos reglas de inferencia que describen cómo construir pruebas de secuentes.

Primero, para formalizar el hecho de que no nos importa el orden de las proposiciones dentro de un contexto, agregamos la regla estructural de intercambio:

${displaystyle vdash }$ A1, A2, Δ

${displaystyle vdash }$ A2, A1, Δ

Tenga en cuenta que no agregamos las reglas estructurales de debilitamiento y contracción, porque sí nos importa la ausencia de proposiciones en una secuencia y el número de copias presentes.

A continuación añadimos secuencias iniciales y cortes:

${displaystyle vdash }$ A, A⊥

${displaystyle vdash }$. A ${displaystyle vdash }$ A⊥, Δ ${displaystyle vdash }$ Δ

La regla de corte puede verse como una forma de componer pruebas, y las secuencias iniciales sirven como unidades para la composición. En cierto sentido, estas reglas son redundantes: a medida que introducimos reglas adicionales para construir pruebas a continuación, mantendremos la propiedad de que se pueden derivar secuencias iniciales arbitrarias a partir de secuencias iniciales atómicas, y que siempre que una secuencia sea demostrable se le puede dar un corte. prueba gratuita. En última instancia, esta propiedad de la forma canónica (que puede dividirse en la integridad de las secuencias iniciales atómicas y el teorema de eliminación de cortes, lo que induce una noción de prueba analítica) se encuentra detrás de las aplicaciones de la lógica lineal en la informática, ya que permite que la lógica sea utilizado en la búsqueda de pruebas y como cálculo lambda con reconocimiento de recursos.

Ahora, explicamos las conectivas dando reglas lógicas. Normalmente, en el cálculo secuencial se dan ambas "reglas correctas" y "gobiernos de izquierda" para cada conectivo, que esencialmente describe dos modos de razonamiento sobre proposiciones que involucran ese conectivo (por ejemplo, verificación y falsificación). En una presentación unilateral, se hace uso de la negación: las reglas de la derecha para una conectiva (digamos ⅋) desempeñan efectivamente el papel de las reglas de la izquierda para su dual (⊗). Por tanto, deberíamos esperar una cierta "armonía" entre la(s) regla(s) de un conectivo y la(s) regla(s) de su dual.

Multiplicativos

Las reglas para la conjunción multiplicativa (⊗) y la disyunción (⅋):

${displaystyle vdash }$. A ${displaystyle vdash }$ Δ, B ${displaystyle vdash }$ Δ, A ⊗ B

${displaystyle vdash }$. A, B ${displaystyle vdash }$. A ⅋ B

y para sus unidades:

${displaystyle vdash }$ 1

${displaystyle vdash }$. ${displaystyle vdash }$, ⊥

Observe que las reglas para la conjunción y la disyunción multiplicativas son admisibles para la conjunción y la disyunción simples bajo una interpretación clásica. (es decir, son reglas admisibles en LK).

Aditivos

Las reglas para la conjunción aditiva (&) y la disyunción (⊕):

${displaystyle vdash }$. A ${displaystyle vdash }$. B ${displaystyle vdash }$. A " B

${displaystyle vdash }$. A ${displaystyle vdash }$. A ⊕ B

${displaystyle vdash }$. B ${displaystyle vdash }$. A ⊕ B

y para sus unidades:

${displaystyle vdash }$, ⊤

(sin regla para 0)

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 de la distinción multiplicativo/aditivo en las reglas para las dos versiones diferentes de conjunción: para el conectivo multiplicativo (⊗), el contexto de la conclusión (Γ, Δ< /span>) se divide entre las premisas, mientras que para el caso aditivo conectivo (&) el contexto de la conclusión (Γ) se lleva completo a ambas premisas.

Exponenciales

Los exponenciales se utilizan para dar acceso controlado al debilitamiento y la contracción. Específicamente, agregamos reglas estructurales de debilitamiento y contracción para las proposiciones ?'d:

${displaystyle vdash }$. ${displaystyle vdash }$ ¿Qué?A

${displaystyle vdash }$ ¿Qué?A, ?A ${displaystyle vdash }$ ¿Qué?A

y utilice las siguientes reglas lógicas:

${displaystyle vdash }$ ? A ${displaystyle vdash }$ ¡Gilipollas!A

${displaystyle vdash }$. A ${displaystyle vdash }$ ¿Qué?A

Se podría observar que las reglas para las exponenciales siguen un patrón diferente de las reglas para las otras conectivas, asemejándose a las reglas de inferencia que gobiernan las modalidades en formalizaciones de cálculo sucesivas de la lógica modal normal S4, y que ya no existe una solución tan clara. ¡Simetría entre los duales! y ?. Esta situación se soluciona con presentaciones alternativas de CLL (p. ej., la presentación LU).

Fórmulas notables

Además de las dualidades de De Morgan descritas anteriormente, algunas equivalencias importantes en lógica lineal incluyen:

Distribución

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).)

El isomorfismo exponencial

Distribución lineal

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 prueba de la lógica lineal. Las consecuencias de este mapa se investigaron por primera vez y se denominaron "distribución débil". En trabajos posteriores se le cambió el nombre a "distribución lineal" para reflejar la conexión fundamental con la lógica lineal.

Otras consecuencias

Las siguientes fórmulas de distributividad no son en general una equivalencia, sólo una implicación:

Codificación de la lógica clásica/intuicionista en lógica lineal

Tanto la implicación intuicionista como la clásica se pueden recuperar de la implicación lineal insertando exponenciales: la implicación intuicionista se codifica como !A ⊸ B< /span>, mientras que la implicación clásica se puede codificar como !?A ⊸ ?B o !A ⊸ ?!B (o una variedad de posibles traducciones alternativas). La idea es que los exponenciales nos permitan usar una fórmula tantas veces como necesitemos, lo cual 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 una manera que garantiza que la fórmula original es demostrable en lógica intuicionista si y sólo si la fórmula traducida es demostrable en lógica lineal. Utilizando la traducción negativa de Gödel-Gentzen, podemos incorporar la lógica clásica de primer orden en la lógica lineal de primer orden.

La interpretación del recurso

Lafont (1993) mostró por primera vez cómo la lógica lineal intuicionista puede explicarse como una lógica de recursos, proporcionando así al lenguaje lógico acceso a formalismos que pueden usarse para razonar sobre recursos dentro de la lógica misma, en lugar de, como en la lógica clásica, lógica, por medio de predicados y relaciones no lógicas. El clásico ejemplo de la máquina expendedora de Tony Hoare (1985) puede utilizarse para ilustrar esta idea.

Supongamos que representamos tener una barra de chocolate mediante la proposición atómica caramelo y tener un dólar mediante $1. Para expresar el hecho de que con un dólar se puede comprar una barra de chocolate, podríamos escribir la implicación $1 ⇒ dulce. Pero en lógica ordinaria (clásica o intuicionista), de A y A ⇒ < var>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, aunque normalmente dichas 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 los "ingenuos" regla. En lugar de $1 ⇒ candy, expresamos la propiedad de la máquina expendedora como una lineal implicación $1 ⊸ dulces. De $1 y este hecho, podemos concluir dulces, pero no $1 ⊗ dulces. En general, podemos utilizar la proposición de lógica lineal A ⊸ B para expresar la validez del recurso transformante A en el recurso B.

Siguiendo el ejemplo de la máquina expendedora, considere las "interpretaciones de recursos" de los demás conectivos 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).

Conjunción multiplicativa (A ⊗ B) denota la aparición simultánea de recursos, que se utilizarán según las indicaciones del consumidor. Por ejemplo, si compras un chicle y una botella de refresco, entonces estás solicitando chicle ⊗ bebida. La constante 1 denota la ausencia de cualquier recurso y, por lo tanto, funciona como la unidad de ⊗.

Conjunción aditiva (A & B) representa una ocurrencia alternativa de recursos, cuya elección controla el consumidor. Si en la máquina expendedora hay un paquete de patatas fritas, una barra de chocolate y una lata de refresco, cada uno de los cuales cuesta un dólar, entonces por ese precio puedes comprar exactamente uno de estos productos. Así escribimos $1 ⊸ (dulces & chips & bebida) . No escribimos $1 ⊸ (dulces ⊗ chips ⊗ bebida), lo que implicaría que un dólar sería suficiente para comprar los tres productos juntos. Sin embargo, de $1 ⊸ (dulces & chips & bebida) , podemos deducir correctamente $3 ⊸ (dulces ⊗ chips ⊗ bebida< /var>), donde $3:= $1 ⊗ $1 ⊗ $1 . La unidad ⊤ de 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 conseguir un caramelo barra y algunas cosas más, sin ser más específico (por ejemplo, patatas fritas y bebida, o 2$, o 1$ y patatas fritas, etc.).

La disyunción aditiva (A ⊕ B) representa una 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 podrá dispensar una barra de chocolate, un paquete de patatas fritas o un refresco. Podemos expresar esta situación como $1 ⊸ (caramelo ⊕ chips ⊕ 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 bueno como una máquina que siempre produce A porque nunca logrará producir un 0). Entonces, a diferencia de lo anterior, no podemos deducir $3 ⊸ (dulces ⊗ chips ⊗ bebida) de esto.

Otros sistemas de prueba

Redes a prueba

Introducidas por Jean-Yves Girard, las redes de prueba han sido creadas para evitar la burocracia, es decir todas las cosas que diferencian dos derivaciones en el punto de vista lógico, pero no en un &# 34;moral" Punto de vista.

Por ejemplo, estas dos pruebas son "moralmente" idéntico:

${displaystyle vdash }$ A, B, C, D ${displaystyle vdash }$ A ⅋ B, C, D ${displaystyle vdash }$ A ⅋ B, C ⅋ D

${displaystyle vdash }$ A, B, C, D ${displaystyle vdash }$ A, B, C ⅋ D ${displaystyle vdash }$ A ⅋ B, C ⅋ D

El objetivo de las redes de prueba es hacerlas idénticas mediante la creación de una representación gráfica de ellas.

Semántica

Semántica algebraica

Decidabilidad/complejidad de la vinculación

La relación de vinculación en CLL completa es indecidible. Al considerar fragmentos de CLL, el problema de decisión tiene una complejidad variable:

• Lógica lineal multiplicativa (MLL): sólo los conectores multiplicativos. La implicación MLL es completa con NP, incluso restringiendo a las cláusulas Horn en el fragmento puramente implicativo, o a fórmulas libres de átomos.
• Lógica lineal multiplicativa-additiva (MALL): sólo multiplicativas y aditivos (es decir, libre exponencial). La implicación MALL es completa con PSPACE.
• Lógica lineal multiplicativa-exponencial (MELL): sólo multiplicativos y exponenciales. Mediante la reducción del problema de alcance de las redes Petri, la implicación MELL debe ser al menos resistente a EXPSPACE, aunque la decidibilidad ha tenido el estado de un problema abierto de larga data. En 2015, se publicó una prueba de decidibilidad en la revista TCS, pero más tarde se mostró erróneo.
• La lógica lineal fina (es decir, la lógica lineal con debilitamiento, una extensión más que un fragmento) se mostró decidable, en 1995.

Variantes

Muchas variaciones de la lógica lineal surgen al modificar aún más las reglas estructurales:

• Affine la lógica, que prohíbe la contracción pero permite el debilitamiento global (una extensión decidable).
• Lógica estricta o lógica relevante, que prohíbe debilitar pero permite la contracción global.
• Lógica no conmutativa o lógica ordenada, que elimina la regla del intercambio, además de la prohibición del debilitamiento y la contracción. En la lógica ordenada, la implicación lineal se divide aún más en la impresión izquierda y la impresión derecha.

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 (Lógica Lineal Intuicionista), los conectivos ⅋, ⊥ y ? están ausentes y la implicación lineal se trata como un conectivo primitivo. En FILL (lógica lineal intuicionista completa), los conectivos ⅋, ⊥ y ? están presentes, la implicación lineal es un conectivo primitivo y, de manera similar a lo que sucede en la lógica intuicionista, todos los conectivos (excepto la negación lineal) son independientes. También existen extensiones de la lógica lineal de primer orden y superior, cuyo desarrollo formal es algo estándar (ver lógica de primer orden y lógica de orden superior).