Lógica linear

Lógica linear é um lógica subestrutural proposta por Jean-Yves Girard como um refinamento da lógica clássica e intuicionista, juntando as dualidades da primeira com muitas das propriedades construtivas da última.^[1] Embora a lógica também tenha sido estudada por si mesma, mais amplamente, as ideias da lógica linear têm influenciado em campos como linguagens de programação, jogos de semântica e física quântica,^[2] bem como a linguística,^[3] particularmente devido a sua ênfase na limitação de recursos, dualidade e interação.

A lógica linear presta-se a muitas apresentações, explicações e intuições diferentes. A prova-teoricamente, deriva de uma análise de cálculo sequencial clássico em que os usos das regras estruturais de contração e enfraquecimento são cuidadosamente controlados. Operacionalmente, isso significa que a dedução lógica já não se limita a uma coleção cada vez maior de "verdades" persistentes, mas é, também, uma maneira de manipular recursos que nem sempre podem ser duplicados ou descartados à vontade. Em termos de modelos denotacionais simples, a lógica linear pode ser vista como refinamento da interpretação da lógica intuicionista, substituindo as categorias fechadas cartesianas por categorias monoidais simétricas, ou da interpretação da lógica clássica, substituindo as álgebras booleanas por C *-álgebras.

Conectivos, dualidade e polaridade

Sintaxe

A linguagem da lógica linear clássica (LLC) é definida indutivamente pela notação BNF

A	::=	p ∣ p^⊥
	∣	A ⊗ A ∣ A ⊕ A
	∣	A & A ∣ A ⅋ A
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	!A ∣ ?A

Aqui p e p^⊥ variam sobre átomos lógicos. Por razões que serão explicadas abaixo, os conectivos ⊗, ⅋, 1, e ⊥ são chamados de multiplicativos; os conectivos &, ⊕, ⊤, e 0 são chamados de aditivos; e o conectivos ! e ? são chamados de exponenciais. Nós podemos empregar a seguinte terminologia:

• ⊗ é chamado de "conjunção multiplicativa" ou "vezes" (ou, às vezes, "tensor")
• ⊕ é chamado de "disjunção aditiva" ou "mais"
•  & é chamado de "conjunção aditiva" ou "com"
• ⅋ é chamado de "disjunção multiplicativa" ou "par"
• ! pronuncia-se "naturalmente" (ou, às vezes, "bang")
• ? é pronunciado "por que não"

Toda proposição A Aem LLC tem uma dual A┴, definida da seguinte forma:

(p)^⊥ = p^⊥			(p^⊥)^⊥ = p
(A ⊗ B)^⊥ = A^⊥ ⅋ B^⊥			(A ⅋ B)^⊥ = A^⊥ ⊗ B^⊥
(A ⊕ B)^⊥ = A^⊥ & B^⊥			(A & B)^⊥ = A^⊥ ⊕ B^⊥
(1)^⊥ = ⊥			(⊥)^⊥ = 1
(0)^⊥ = ⊤			(⊤)^⊥ = 0
(!A)^⊥ = ?(A^⊥)			(?A)^⊥ = !(A^⊥)

Classificação dos conectivos

adicionar	mul	exp
pos	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

Observe que (-)^⊥ é uma involução, isto é, A^⊥⊥ = A para todas as proposições. A^⊥ também é chamada de negação linear de A.

As colunas da tabela sugerem outra maneira de classificar os conectivos da lógica linear, denominada polaridade: os conectivos negados na coluna da esquerda (⊗, ⊕, 1, 0,!) são chamados de positivos, enquanto seus duais na coluna da direita (⅋, &, ⊥, ⊤,?) são chamados de negativos; cf. Tabela à direita.

A implicação linear não está incluída na gramática de conectivos, mas é definível em LLC usando a negação linear e a disjunção multiplicativa, por A ⊸ B := A┴ ⅋ B. O conectivo ⊸ às vezes é pronunciado "pirulito", devido à sua forma.

Apresentação do cálculo sequencial

Uma maneira de definir a lógica linear é como um cálculo sequente. Usamos as letras Γ e Δ para variar sobre a lista de proposições A1,..., An, também chamadas de contextos. Um sequente coloca um contexto à esquerda e à direita da catraca, escrito Γ Predefinição:Tee Δ. Intuitivamente, o sequente afirma que a conjunção de Γ implica a disjunção de Δ (embora queiramos dizer a conjunção e a disjunção "multiplicativas", como explicado abaixo). Girard descreve a lógica linear clássica usando apenas sequências unilaterais (onde o contexto esquerdo está vazio), e seguimos aqui essa apresentação mais econômica. Isso é possível porque qualquer local à esquerda de uma catraca pode sempre ser movido para o outro lado e duplamente.

Agora damos regras de inferência descrevendo como construir provas de sequências.^[4]

Primeiro, para formalizar o fato de que não nos importamos com a ordem das proposições dentro de um contexto, adicionamos a regra estrutural de troca:

${\displaystyle \vdash \Gamma }$ ${\displaystyle \vdash \Gamma }$

(Γ ' a permutation of Γ)

Note que nós não adicionamos regras estruturais de enfraquecimento e de contração, porque nos preocupamos com a ausência de proposições em uma sequência, e o número de cópias presentes.

Em seguida, adicionamos sequentes e cortes iniciais:

${\displaystyle \vdash A,A^{\perp }}$

${\displaystyle \vdash \Gamma ,A}$       ${\displaystyle \vdash A^{\perp },\Delta }$ ${\displaystyle \vdash \Gamma ,\Delta }$

A regra de corte pode ser vista como uma maneira de compor provas, e seqüências iniciais servem como as unidades de composição. Em certo sentido, essas regras são redundantes: à medida que introduzimos regras adicionais para a construção de provas abaixo, manteremos a propriedade de que seqüências iniciais arbitrárias podem ser derivadas de seqüências atômicas iniciais, e que sempre que um sequente é provável, pode ser dado um prova livre de cortes. Em última instância, esta propriedade de forma canônica (que pode ser dividida na completude das sequências iniciais atômicas e do teorema de eliminação de corte, induzindo uma noção de prova analítica) está por trás das aplicações da lógica linear na ciência da computação, pois permite que a lógica seja usada na pesquisa de prova e como um lambda-cálculo calculado com recurso.

Agora, explicamos os conectivos dando regras lógicas. Tipicamente, no cálculo sequente, é dada uma "regra-direita" e uma "regra-esquerda" para cada conectivo, descrevendo essencialmente dois modos de raciocínio sobre proposições envolvendo esse conectivo (por exemplo, verificação e falsificação). Em uma apresentação unilateral, uma vez que faz uso da negação: as regras certas para um conectivo (digamos ⅋) efetivamente desempenham o papel de regras-esquerda para o seu dual (⊗). Portanto, devemos esperar uma certa "harmonia" entre a(s) regra(s) para um conectivo e a(s) regra(s) para o seu dual.

Multiplicativos

As regras para a conjunção(⊗) e disjunção(⅋) multiplicativas:

${\displaystyle \vdash \Gamma ,A}$       ${\displaystyle \vdash \Delta ,B}$ ${\displaystyle \vdash \Gamma ,\Delta ,A\otimes B}$

${\displaystyle \vdash \Gamma ,A,B}$ ${\displaystyle \vdash \Gamma ,A}$ ⅋ ${\displaystyle B}$

e para as suas unidades:

${\displaystyle \vdash 1}$

${\displaystyle \vdash \Gamma }$ ${\displaystyle \vdash \Gamma ,\perp }$

Observe que as regras para conjunção e disjunção multiplicativa são admissíveis paraconjunção e disjunção simples sob uma interpretação clássica (isto é, são regras admissíveis no LK).

Aditivos

As regras para a conjunção(&) e disjunção(⊕) aditivas:

${\displaystyle \vdash \Gamma ,A}$       ${\displaystyle \vdash \Gamma ,B}$ ${\displaystyle \vdash \Gamma ,A\And B}$

${\displaystyle \vdash \Gamma ,A}$ ${\displaystyle \vdash \Gamma ,A\oplus B}$

${\displaystyle \vdash \Gamma ,B}$ ${\displaystyle \vdash \Gamma ,A\oplus B}$

e para as suas unidades:

${\displaystyle \vdash \Gamma ,}$⊤

(no rule for 0)

Observar que as regras para a conjunção e a disjunção aditivas são novamente admissíveis sob uma interpretação clássica. Mas agora podemos explicar a base para a distinção multiplicativa / aditiva nas regras para as duas versões diferentes da conjunção: para o conectivo multiplicativo (⊗), o contexto da conclusão (Γ, Δ) é dividido entre as premissas, enquanto que para o caso do conectivo aditivo (&), o contexto da conclusão (Γ) é transportado inteiro para ambas as premissas.

Exponenciais

Os exponenciais são usadas para dar acesso controlado ao enfraquecimento e contração. Especificamente, adicionamos regras estruturais de enfraquecimento e contração para proposições  ?'d:^[5]

${\displaystyle \vdash \Gamma }$ ${\displaystyle \vdash \Gamma ,?A}$

${\displaystyle \vdash \Gamma ,?A,?A}$ ${\displaystyle \vdash \Gamma ,?A}$

e use as seguintes regras lógicas:

${\displaystyle \vdash ?\Gamma ,A}$ ${\displaystyle \vdash ?\Gamma ,!A}$

${\displaystyle \vdash \Gamma ,A}$ ${\displaystyle \vdash \Gamma ,?A}$

Pode-se observar que as regras para os exponenciais seguem um padrão diferente das regras para os outros conectivos, e que não há mais uma simetria tão clara entre os duais ! e ?. Esta situação é corrigida em apresentações alternativas de LLC (por exemplo, a apresentação de LU).

Fórmulas Notáveis

Além das dualidades de De Morgan descritas acima, algumas equivalências importantes na lógica linear incluem:

Distributividade

${\displaystyle }$${\displaystyle A\otimes (B\oplus C)\equiv (A\otimes B)\oplus (A\otimes C)}$

Isomorfismo exponencial

${\displaystyle }$${\displaystyle \,!(A\&B)\equiv \,!A\otimes \,!B}$

(Aqui ${\displaystyle A\equiv B\quad =\quad (A\multimap B)\&(B\multimap A)}$.)

Suponha que ⅋ é qualquer um dos operadores binários: vezes, mais, com ou par (mas não a implicação linear). O que se segue não é, em geral, uma equivalência, apenas uma implicação:

Distribuições lineares

Um mapa que não é um isomorfismo ainda desempenha um papel crucial na lógica linear é:

(A ⊗ (B ⅋ C)) ⊸ ((A ⊗ B) ⅋ C)

As distribuições lineares são fundamentais na teoria de prova da lógica linear. A consequência desse mapa foi investigada pela primeira vez e denominada "distribuição fraca". Em um trabalho posterior, foi renomeado para "distribuição linear" para refletir a conexão fundamental à lógica linear.

Codificando lógica clássica/lógica intuicionística na lógica linear

Tanto a implicação intuicionística quanto a clássica podem ser recuperadas a partir da implicação linear inserindo exponenciais: a implicação intuicionística é codificada como !A ⊸ B, e a implicação clássica como !A ⊸ ?B.^[6] A ideia é que os exponenciais nos permitem usar uma fórmula tantas vezes quanto precisamos, o que é sempre possível na lógica clássica e na lógica intuicionística.

Formalmente, existe uma tradução de fórmulas da lógica intuicionística para fórmulas da lógica linear de uma forma que garante que a fórmula original é demonstrável na lógica intuicionística se, e somente se a fórmula traduzida é demonstrável na lógica linear. Usando a tradução negativa de Gödel–Gentzen, podemos, assim, inserir a lógica clássica de primeira ordem na lógica linear de primeira ordem.

A interpretação baseada em recursos

Lafont (1993) mostrou pela primeira vez como a lógica linear intuicionística pode ser explicada como uma lógica de recursos, proporcionando assim à linguagem lógica acesso a formalismos que podem ser utilizados para raciocinar sobre recursos dentro da própria lógica em vez de, como na lógica clássica, através de predicados e relações não-lógicos. O exemplo clássico de Antony Hoare (1985) da máquina de vending pode ser usado para ilustrar essa ideia.

Suponha que representamos ter uma barra de chocolate por uma proposição atômica de doces, e ter um dólar por $1. Para afirmar o fato de que com um dólar você vai comprar uma barra de chocolate, podemos escrever a implicação $1 ⇒ doces. Mas na lógica ordinária (clássica ou intuicionista), a partir de A e A ⇒ B pode-se concluir A ∧ B. Assim, a lógica comum nos leva a crer que podemos comprar a barra de chocolate e manter o nosso dólar!!! Evidentemente, podemos evitar esse problema usando codificações mais sofisticadas, ^{[esclarecimentos necessários]} embora, normalmente, tais codificações sofram com o problema de quadro. No entanto, a rejeição do enfraquecimento e da contração permite que a lógica linear evite esse tipo de raciocínio espúrio, mesmo com a regra "ingênua". Em vez de $1 ⇒ doces, que expressam a propriedade da máquina de venda automática como uma implicação linear $1 ⊸ doces. A partir de $1 e deste fato, pode-se concluir doces, mas não $1 ⊗ doces. Em geral, podemos usar a proposição de lógica linear A ⊸ B para expressar a validade de transformar o recurso A no recurso B.

Correndo com o exemplo da máquina de venda automática, vamos considerar as "interpretações de recursos" dos outros conectivos multiplicativos e aditivos. (Os exponenciais fornecem os meios para combinar essa interpretação de recursos com a noção usual de verdade lógica persistente.)

A conjunção multiplicativa (A ⊗ B) denota ocorrência simultânea de recursos, para ser usada como o consumidor direciona. Por exemplo, se você compra um pedaço de goma e uma garrafa de refrigerante, então você está solicitando goma ⊗ bebida. A constante 1 denota a ausência de qualquer recurso e, assim, funciona como a unidade de ⊗.

A conjunção aditiva (A & B) representa a ocorrência alternativa de recursos, cuja escolha é controlada pelo consumidor. Se na máquina de venda automática há um pacote de batatas fritas, uma barra de chocolate, e uma lata de refrigerante, cada um custando um dólar, então, devido ao preço, você pode comprar exatamente um desses produtos. Assim nós escrevemos $1 ⊸ (doces & batatas-fritas & bebida). Não escrevemos $1 ⊸ (doces ⊗ batatas-fritas ⊗ bebida), o que implicaria que um dólar é suficiente para comprar todos os três produtos juntos. No entanto, a partir de $1 ⊸ (doces & batatas-fritas & bebida), nós podemos deduzir corretamente $3 ⊸ (doces ⊗ batatas-fritas ⊗ bebidas), onde $3 := $1 ⊗ $1 ⊗ $1. A unidade ⊤ da conjunção aditiva pode ser vista como uma cesta de lixo para alternativas irrelevantes. Por exemplo, podemos escrever $3 ⊸ (doces & ⊤) para expressar que três dólares vão comprar uma barra de chocolate e outra coisa (não importa o quê).

A disjunção aditiva (A ⊕ B) representa  a ocorrência alternativa de recursos, cuja escolha é controlada pela máquina. Por exemplo, suponha que a máquina de venda automática permita o jogo: inserir um dólar e a máquina pode retornar uma barra de chocolate, um pacote de batatas fritas ou um refrigerante. Podemos expressar essa situação como $1 ⊸ (doces ⊕ batatas-fritas ⊕ bebida). A constante 0 representa um produto que não pode ser feito e, portanto, serve como a unidade de ⊕ (uma máquina que pode produzir A ou 0 é tão boa quando uma máquina que sempre produz A, porque nunca conseguirá produzir 0).

A disjunção multiplicativa (A ⅋ B) é mais difícil de ilustrar em termos da interpretação de recursos, embora possamos codificar de volta para a implicação linear, como A^⊥ ⊸ B ou B^⊥ ⊸ A.

Outros sistemas de prova

Redes de prova

Introduzido por Jean-Yves Girard, redes de prova foram criadas para evitar a burocracia, que é tudo o que faz duas derivações diferentes no ponto de vista lógico, mas não em um ponto de vista "moral".

Por exemplo, essas duas provas são "moralmente" idênticas:

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

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

O objetivo das redes de prova é torná-las idênticas, criando uma representação gráfica delas.

Semântica

Semântica algébrica

Decidabilidade/complexidade da vinculação

A relação de implicação na LLC total é indecidível.^[7] Fragmentos de LLC são frequentemente considerados, para os quais o problema de decisão é mais sutil:

• Lógica linear multiplicativa (LLM): apenas os conectivos multiplicativos. A ligação LLM é NP-completa.
• Lógica linear aditiva-multiplicativa (LLAM): apenas multiplicativos e aditivos(isto é, exponential-livre). A ligação LLMA é PSPACE-completa.
• Lógica linear exponencial-multiplicativa (LLEM): apenas multiplicativos e exponenciais. Após muitas tentativas, este fragmento mostrou-se decidível em 2015.^[8]
• A lógica linear afim (que é a lógica linear com enfraquecimento, uma extensão em vez de um fragmento) mostrou-se decidível, em 1995.^[9]

Variantes da lógica linear

Muitas variações da lógica linear surgem por meio de um retoque adicional às regras estruturais:

• Lógica afim, que proíbe a contração, mas permite o enfraquecimento global (uma extensão decidível).
• Lógica estrita ou lógica de relevância, que proíbe o enfraquecimento, mas permite a contração global.
• Lógica não-comutativa ou lógica ordenada, que elimina as regras de troca, além de impedir o enfraquecimento e a contração. Na lógica ordenada, a implicação linear divide-se na implicação da esquerda e na implicação da direita.

Diferentes variantes intuicionistas da lófica linear têm sido consideradas. Quando baseados em uma apresentação de cálculo de seqüência de conclusão única, como em LLI(Lógica Linear Intuicionista), os conectivos ⅋, ⊥, e ? estão ausentes, e a implicação linear é tratada como um conectivo primitivo. Em LLIC (Lógica Linear Intuicionista Completa) os conectivos ⅋, ⊥ e? estão presentes, a implicação linear é um conectivo primitivo e, da mesma forma que acontece na lógica intuicionista, todos os conectivos (exceto a negação linear) são independentes. Há também extensões de primeira e de ordem superior da lógica linear, cujo desenvolvimento formal é um tanto padrão (ver lógica de primeira ordem e lógica de ordem superior).

Ver também

• Tipo de sistema linear, um tipo subestrutural de sistema
• A lógica da unidade (LU)
• Redes de prova
• Geometria de interação
• Jogo de semântica
• A lógica intuicionista
• Lógica da computabilidade
• Ludics
• Espaços Chu
• Unicidade do tipo

Referências

1. Girard, Jean-Yves (1987). «Linear logic» (PDF). Theoretical Computer Science. 50 (1): 1-102. doi:10.1016/0304-3975(87)90045-4 
2. Baez, John; Mike Stay (2008). «Physics, Topology, Logic and Computation: A Rosetta Stone» (PDF). Bob Coecke. New Structures of Physics  A referência emprega parâmetros obsoletos |coautores= (ajuda)
3. de Paiva, V.; van Genabith, J.; Ritter, E. (1999). Dagstuhl Seminar 99341 on Linear Logic and Applications (PDF). [S.l.: s.n.] 
4. Girard (1987), p.22, Def.1.15
5. Girard (1987), p.25-26, Def.1.21
6. Di Cosmo, Roberto.The Linear Logic Primer. Course notes; chapter 2.
7. For this and the below complexity results, see: Lincoln, Patrick; Mitchell, John; Scedrov, Andre; Shankar, Natarajan (1992). «Decision Problems for Propositional Linear Logic». Annals of Pure and Applied Logic. 56: 239–311. doi:10.1016/0168-0072(92)90075-B 
8. Bimbó, Katalin. «The decidability of the intensional fragment of classical linear logic». Theoretical Computer Science. 597: 1-17. ISSN 0304-3975. doi:10.1016/j.tcs.2015.06.019 
9. Kopylov, A. P. (1 de junho de 1995). «Decidability of linear affine logic». , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. pp. 496–504. doi:10.1109/LICS.1995.523283 

Leitura adicional

• Girard, Jean-Yves. Linear logic, Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987.
• Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. Proofs and Types. Cambridge Press, 1989.
• Hoare, C. A. R., 1985. Communicating Sequential Processes. Prentice-Hall International. ISBN 0-13-153271-5
• Lafont, Yves, 1993. Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, Brno, Czech Republic.
• Troelstra, A.S. Lectures on Linear Logic. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.
• A. S. Troelstra, H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
• Di Cosmo, Roberto, and Danos, Vincent. The linear logic primer.
• Introduction to Linear Logic (Postscript) by Patrick Lincoln
• Introduction to Linear Logic by Torben Brauner
• A taste of linear logic by Philip Wadler
• Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
• Overview of linear logic programming by Dale Miller. In Linear Logic in Computer Science, edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.
• Linear Logic Wiki

Ligações externas

• A Linear Logic Prover (llprover), available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan