Lógica lineal

Lógica lineal ( Lógica lineal inglesa es una lógica subestructural, propuesta por Jean -Yves Girard como un refinamiento de la lógica clásica e intuicionista , combinando la dualidad de la primera con muchas propiedades constructivas de la segunda [1] , introducida y utilizada para el razonamiento lógico que tiene en cuenta el consumo de algún recurso [2 ] . Aunque la lógica también se ha estudiado por derecho propio, las ideas de la lógica lineal encuentran aplicaciones en una variedad de aplicaciones que requieren muchos recursos, incluida la verificación de protocolos de red , lenguajes de programación , teoría de juegos ( semántica de juegos ) [2] y física cuántica (porque la lógica lineal se puede considerar como la lógica de la teoría cuántica de la información ) [3] , la lingüística [4] .

Descripción

Sintaxis

El lenguaje de la lógica lineal clásica ( English classic linear logic, CLL ) se puede describir en la forma Backus-Naur :

UN ::= pags ∣ pags ⊥ | UN ⊗ UN ∣ UN ⊕ UN | UN & UN ∣ UN ⅋ UN | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | ! A∣ ? A

Dónde

p y p ⊥ son fórmulas atómicas ,

Conectivos lógicos y constantes:

Símbolo	Sentido
⊗	conjunción multiplicativa ("tensor", ing. "tensor" )
⊕	disyunción aditiva
&	conjunción aditiva
⅋	disyunción multiplicativa ("par", Inglés "par" )
!	modalidad " por supuesto "
?	modalidad " por qué no "
una	unidad para ⊗
0	cero para ⊕
⊤	nulo para &
⊥	unidad de ⅋

Los conectores binarios ⊗, ⊕, & y ⅋ son asociativos y conmutativos .

Todo enunciado A en lógica lineal clásica tiene un dual A ⊥ definido de la siguiente manera:

( pags ) ⊥ = pags ⊥			( pags ⊥ ) ⊥ = pags
( UN ⊗ segundo ) ⊥ = UN ⊥ ⅋ segundo ⊥			( UN ⅋ segundo ) ⊥ = UN ⊥ ⊗ segundo ⊥
( UN ⊕ segundo ) ⊥ = UN ⊥ y segundo ⊥			( UNA y segundo ) ⊥ = UNA ⊥ ⊕ segundo ⊥
(1) ⊥ = ⊥			(⊥) ⊥ = 1
(0) ⊥ = ⊤			(⊤) ⊥ = 0
(! UN ) ⊥ = ?( UN ⊥ )			(? UN ) ⊥ = !( UN ⊥ )

Interpretación significativa

En lógica lineal (a diferencia de la lógica clásica), las premisas a menudo se tratan como recursos prescindibles , por lo que la fórmula inicial o derivada puede estar limitada en el número de usos.

La conjunción multiplicativa ⊗ es similar a la operación de suma de conjuntos múltiples y puede expresar la unión de recursos.

Tenga en cuenta que (.) ⊥ es una involución , es decir, A ⊥⊥ = A para todas las declaraciones. A ⊥ también se llama la negación lineal de A .

La implicación lineal juega un papel importante en la lógica lineal, aunque no está incluida en la gramática conectiva. Se puede expresar en términos de negación lineal y disyunción multiplicativa

UN ⊸ segundo : = UN ⊥ ⅋ segundo .

El ligamento ⊸ a veces se llama "piruleta" ( ing. piruleta ) debido a su forma característica.

Una implicación lineal se puede utilizar en la salida cuando hay recursos en su lado izquierdo y el resultado son los recursos de la implicación lineal derecha. Esta transformación define una función lineal , lo que dio lugar al término "Lógica lineal" [5] .

La modalidad “por supuesto” (!) te permite designar un recurso como inagotable.

Ejemplo. Sea D un dólar y C una barra de chocolate. Entonces la compra de una barra de chocolate se puede denotar como D ⊸ C . La compra se puede expresar de la siguiente manera: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , es decir, que el dólar y la posibilidad de comprar una barra de chocolate con él conducen a una barra de chocolate, y la queda la oportunidad de comprar una barra de chocolate [5] .

A diferencia de la lógica clásica e intuicionista , la lógica lineal tiene dos tipos de conjunciones, lo que permite expresar la limitación de recursos. Agreguemos al ejemplo anterior la posibilidad de comprar una piruleta L. La posibilidad de comprar una barra de chocolate o una piruleta se puede expresar mediante una conjunción aditiva [6] :

D ⊸ L y C

Por supuesto, solo puedes elegir uno. Una conjunción multiplicativa denota la presencia de ambos recursos. Entonces, por dos dólares puedes comprar tanto una barra de chocolate como una piruleta:

re ⊗ re ⊸ L ⊗ C

La disyunción multiplicativa A ⅋ B puede entenderse como “si no A, entonces B”, y la implicación lineal A ⊸ B expresada a través de ella tiene el significado “¿se puede deducir B de A exactamente una vez?” [6]

La disyunción aditiva A ⊕ B denota la posibilidad tanto de A como de B, pero la elección no es tuya [6] . Por ejemplo, una lotería de ganar-ganar en la que puedes ganar una piruleta o una barra de chocolate se puede expresar mediante la disyunción aditiva:

RE ⊸ L ⊕ C

Fragmentos

Además de la lógica lineal completa, se utilizan sus fragmentos [7] :

LL: todos los enlaces están permitidos
MLL: solo multiplicativos (⊗, ⅋)
MALL: solo multiplicativos y aditivos (⊗, ⅋, ⊕, &)
MELL: solo multiplicativos y exponenciales (⊗, ⅋, !, ?)

Por supuesto, esta lista no agota todos los fragmentos posibles. Por ejemplo, hay varios fragmentos de Horn que usan implicación lineal (similar a las cláusulas de Horn ) en combinación con varios conectores. [ocho]

Los fragmentos de lógica son de interés para los investigadores en términos de la complejidad de su interpretación computacional. En particular, M.I. Kanovich demostró que un fragmento MLL completo es NP-completo , y un fragmento ⊕-Horn de una lógica lineal con una regla de debilitamiento( Regla de debilitamiento en inglés ) PSPACE-full . Esto puede interpretarse en el sentido de que administrar el uso de recursos es una tarea difícil, incluso en los casos más simples. [ocho]

Representación como cálculo secuencial

Una forma de definir la lógica lineal es el cálculo secuente . Las letras Γ y ∆ representan listas de oraciones y se denominan contextos . En una secuencia, el contexto se coloca a la izquierda y derecha de ⊢ ("debería"), por ejemplo: . A continuación se muestra el cálculo secuencial para MLL en formato bidireccional [7] . $A_{1},...,A_{n}$ ${\ estilo de visualización \ Gamma \ vdash \ Delta}$

Regla estructural - permutación. Las reglas de inferencia izquierda y derecha se dan, respectivamente:

${\cfrac {\Gamma ,A,B,\Gamma '\vdash \Delta }{\Gamma ,B,A,\Gamma '\vdash \Delta ))\;{\text{exL))\qquad {\cfrac {\Gamma \vdash \Delta ,A,B,\Delta '}{\Gamma \vdash \Delta ,B,A,\Delta '}}\;{\text{exR}}$

Identidad y sección :

${\cfrac {\cdot }{A\vdash A}}\;{\text{I}}\qquad {\cfrac {\Gamma \vdash \Sigma ,A,\Delta \qquad \Gamma ',A ,\Sigma '\vdash \Delta '}{\Gamma ,\Gamma ',\Sigma '\vdash \Sigma ,\Delta ,\Delta '))\;{\text{Cortar))$

Conjunción multiplicativa:

${\cfrac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\otimes B\vdash \Delta ))\;\otimes {\text{L))\qquad {\cfrac {\ Gamma \vdash A,\Delta \qquad \Gamma '\vdash B,\Delta '}{\Gamma ,\Gamma '\vdash A\otimes B,\Delta ,\Delta '))\;\otimes {\text{ R}}$

Disyunción multiplicativa:

${\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ',B\vdash \Delta '}{\Gamma ,\Gamma ',A{\text{⅋))B\vdash \Delta , \Delta '}}\;{\text{⅋L}}\qquad {\cfrac {\Gamma \vdash A,B,\Delta }{\Gamma \vdash A{\text{⅋}}B,\Delta } }\;{\texto{⅋R}}$

Negación:

${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,A^{\bot }\vdash \Delta }}\;\bot {\text{L}}\qquad {\cfrac {\ Gamma ,A\vdash \Delta }{\Gamma \vdash A^{\bot },\Delta }}\;\bot {\text{R}}$

Se pueden definir reglas similares para la lógica lineal completa, sus aditivos y exponenciales. Tenga en cuenta que las reglas estructurales de debilitamiento y reducción no se han agregado a la lógica lineal , ya que en el caso general las declaraciones (y sus copias) no pueden aparecer y desaparecer aleatoriamente en secuencias, como es habitual en la lógica clásica.

Notas

↑ Girard, Jean-Yves (1987). "Lógica lineal" (PDF) . Informática Teórica . 50 (1): 1-102. DOI : 10.1016/0304-3975(87)90045-4 . HDL : 10338.dmlcz/120513 . Archivado (PDF) desde el original el 2021-05-06 . Consultado el 24 de marzo de 2021 . Parámetro obsoleto utilizado |deadlink=( ayuda )
↑ 1 2 Preguntas algorítmicas de álgebra y lógica / TARJETA DE PROYECTO APOYADA POR LA FUNDACIÓN DE CIENCIAS DE RUSIA. Recuperado: 18/07/2021 . Consultado el 18 de julio de 2021. Archivado desde el original el 18 de julio de 2021. (indefinido)
↑ Báez, John ; Quédate, Mike (2008). Bob Coecke , editor. "Física, topología, lógica y computación: una piedra de Rosetta" (PDF) . Nuevas Estructuras de la Física . Archivado desde el original el 22 de marzo de 2021 . Consultado el 24 de marzo de 2021 . Parámetro obsoleto utilizado |deadlink=( ayuda )
↑ de Paiva, V. Dagstuhl Seminario 99341 sobre lógica lineal y aplicaciones / V. de Paiva, J. van Genabith, E. Ritter. - 1999. Archivado el 22 de noviembre de 2020 en Wayback Machine .
↑ 1 2 Lomazova, 2004 .
↑ 1 2 3 Lincoln, 1992 .
↑ 12 de Beffara , 2013 .
↑ 1 2 Max I. Kanovich. La complejidad de los fragmentos de Horn de Lógica Lineal. Anales de lógica pura y aplicada 69 (1994) 195-241

Literatura

Lomazova I. A. 6.5. Redes de Petri Anidadas y Lógica Lineal // Redes de Petri Anidadas: Modelado y Análisis de Sistemas Distribuidos con Estructura de Objetos. - M. : Mundo científico, 2004. - S. 175-185. — 208 págs. - ISBN 5-89176-247-1 .
Patricio Lincoln. Lógica lineal // ACM SIGACT Noticias. - 1992. - V. 23, N° 2 (mayo).
Emmanuel Befarara. Introducción a la lógica lineal (2013). (indefinido)

Enlaces

Lógica lineal , Enciclopedia de Filosofía de Stanford

Lógicas

Filosofía • Semántica • Sintaxis • Historia

Grupos lógicos

lógica clásica	lógica aristotélica Lógica proposicional Lógica de primer orden Lógica de segundo orden lógica de orden superior
lógica matemática	teoría de conjuntos Teoría del modelo teoría de la computabilidad Teoría de la prueba y matemáticas constructivas lógica lineal sistema formal conclusión natural cálculo de secuencias Álgebra de la lógica Lógica relevante lógica deóntica lógica intuicionista cálculo de Lambek
Lógica no clásica	intuicionismo lógica difusa Lógica subestructural lógica Descripción lógica Lógica multivaluada Síntesis lógica Lógica vinculante Lógica temporal Lógica modal ( Lógica híbrida ) lógica epistémica
lógica filosófica	Pensamiento crítico lógica informal razonamiento deductivo

Componentes

Lista de símbolos booleanos