Lógica linear - Linear logic

A lógica linear é uma 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 segunda. Embora a lógica também tenha sido estudada por si mesma, de forma mais ampla, as ideias da lógica linear têm sido influentes em campos como linguagens de programação , semântica de jogos e física quântica (porque a lógica linear pode ser vista como a lógica da teoria da informação quântica ) , bem como linguística , particularmente por causa de sua ênfase na limitação de recursos, dualidade e interação.

A lógica linear se presta a muitas apresentações, explicações e intuições diferentes. Prova-teoricamente , ele deriva de uma análise do cálculo sequencial clássico no qual os usos (das regras estruturais ) de contração e enfraquecimento são cuidadosamente controlados. Operacionalmente, isso significa que a dedução lógica não é mais apenas sobre uma coleção cada vez maior de "verdades" persistentes, mas também uma forma de manipular recursos que nem sempre podem ser duplicados ou jogados fora à vontade. Em termos de modelos denotacionais simples , a lógica linear pode ser vista como um refinamento da interpretação da lógica intuicionista, substituindo as categorias cartesianas (fechadas) por categorias monoidais simétricas (fechadas) , ou a 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 (CLL) é definida indutivamente pela notação BNF

$UMA$	:: =	$p ∣ p ⊥$
	$∣$	$A \otimes A ∣ A \oplus A$
	$∣$	$A & A ∣ A ⅋ A$
	$∣$	$1 ∣ 0 ∣ ⊤ ∣ ⊥$
	$∣$	$! A ∣? UMA$

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


Símbolo	Nome
⊗	conjunção multiplicativa	vezes	tensor
⊕	disjunção aditiva	mais
E	conjunção aditiva	com
⅋	disjunção multiplicativa	par
!	é claro	estrondo
?	Por que não

Os conectivos binários ⊗, ⊕, & e ⅋ são associativos e comutativos; 1 é a unidade de ⊗, 0 é a unidade de ⊕, ⊥ é a unidade de ⅋ e ⊤ é a unidade de &.

Cada proposição $A$ em CLL tem um dual $A ⊥$ , definido como segue:

$(p) ⊥ = p ⊥$			$(p ⊥) ⊥ = p$
$(A \otimes B) ⊥ = A ⊥ ⅋ B ⊥$			$(A ⅋ B) ⊥ = A ⊥ \otimes B ⊥$
$(A \oplus B) ⊥ = A ⊥ & B ⊥$			$(A e B) ⊥ = A ⊥ \oplus B ⊥$
$(1) ⊥ = ⊥$			$(⊥) ⊥ = 1$
$(0) ⊥ = ⊤$			$(⊤) ⊥ = 0$
$(! A) ⊥ =? (A ⊥)$			$(? A) ⊥ =! (A ⊥)$

Classificação de conectivos
	adicionar	mul	exp
pos	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

Observe que $(-) ⊥$ é uma involução , ou seja, $A ⊥⊥ = A$ para todas as proposições. $A ⊥$ também é chamado de negação linear de $A$ .

As colunas da tabela sugerem outra forma 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 à direita (⅋, &, ⊥, ⊤,?) São chamados de negativos ; cf. mesa à direita.

Implicação linear não está incluído na gramática de conectivos, mas é definível em CLL usando negação linear e disjunção multiplicativo, por $um ⊸ B : = Um ⊥ ⅋ B$ . O conectivo ⊸ às vezes é pronunciado " pirulito ", devido à sua forma.

Apresentação de cálculo sequencial

Uma maneira de definir a lógica linear é como um cálculo sequencial . Usamos as letras $Γ$ e $Δ$ para percorrer a lista de proposições $A 1, ..., A n$ , também chamadas de contextos . Um sequente coloca um contexto à esquerda e à direita da catraca , escrito ${\ displaystyle \ vdash}$ . Intuitivamente, o sequente afirma que a conjunção de $Γ$ acarreta a disjunção de $Δ$ (embora estejamos nos referindo à conjunção e disjunção "multiplicativas", como explicado abaixo). Girard descreve a lógica linear clássica usando apenas sequentes unilaterais (onde o contexto do lado 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 dualizado.

Agora fornecemos regras de inferência que descrevem como construir provas de sequentes.

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}

{\ displaystyle \ vdash}

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

Em seguida, adicionamos sequentes e cortes iniciais :

{\ displaystyle \ vdash}

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

${\ displaystyle \ vdash}$

A regra de corte pode ser vista como uma forma de compor provas, e os sequentes iniciais servem como unidades de composição. Em certo sentido, essas regras são redundantes: à medida que introduzimos regras adicionais para a construção de provas abaixo, vamos manter a propriedade de que sequentes iniciais arbitrários podem ser derivados de sequentes iniciais atômicos, e que sempre que um sequente for provável, ele pode receber um corte prova gratuita. Em última análise, esta propriedade da forma canônica (que pode ser dividida em completude dos sequentes iniciais atômicos e o teorema de eliminação do 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, uma vez que permite que a lógica seja usado na pesquisa de prova e como um cálculo lambda com reconhecimento de recursos .

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

Multiplicativos

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

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

${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

e para suas unidades:



${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

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

Aditivos

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

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

${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

e para suas unidades:



${\ displaystyle \ vdash}$

(nenhuma regra para

0

)

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

Exponenciais

Os exponenciais são usados para dar acesso controlado ao enfraquecimento e contração. Especificamente, adicionamos regras estruturais de enfraquecimento e contração para as proposições? 'D:

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

e use as seguintes regras lógicas:

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

Pode-se observar que as regras para as exponenciais seguem um padrão diferente das regras para os outros conectivos, assemelhando-se às regras de inferência que regem as modalidades em formalizações de cálculo sequencial da lógica modal normal S4, e que não há mais uma simetria clara entre os duais! e ?. Esta situação é corrigida em apresentações alternativas de CLL (por exemplo, a apresentação LU ).

Fórmulas notáveis

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

Distributividade

A \otimes (B \oplus C) ≣ (A \otimes B) \oplus (A \otimes C)

(A \oplus B) \otimes C ≣ (A \otimes C) \oplus (B \otimes C)

A ⅋ (B & C) ≣ (A ⅋ B) e (A ⅋ C)

(A e B) ⅋ C ≣ (A ⅋ C) e (B ⅋ C)

Por definição de $A ⊸ B$ como $A ⊥ ⅋ B$ , as duas últimas leis de distributividade também fornecem:

A ⊸ (B & C) ≣ (A ⊸ B) e (A ⊸ C)

(A \oplus B) ⊸ C ≣ (A ⊸ C) e (B ⊸ C)

(Aqui $A ≣ B$ é $(A ⊸ B) & (B ⊸ A)$ .)

Isomorfismo exponencial

! (A e B) ≣! A \otimes! B

? (A \oplus B) ≣? A ⅋? B

Distribuições lineares

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

(A \otimes (B ⅋ C)) ⊸ ((A \otimes B) ⅋ C)

As distribuições lineares são fundamentais na teoria da prova da lógica linear. As consequências deste mapa foram investigadas e chamadas de "distribuição fraca". Em trabalhos subsequentes, ela foi renomeada para "distribuição linear" para refletir a conexão fundamental com a lógica linear.

Outras implicações

As seguintes fórmulas de distributividade não são em geral uma equivalência, apenas uma implicação:

! A \otimes! B ⊸! (A \otimes B)

! A \oplus! B ⊸! (A \oplus B)

? (A ⅋ B) ⊸? A ⅋? B

? (A e B) ⊸? A &? B

(A e B) \otimes C ⊸ (A \otimes C) e (B \otimes C)

(A e B) \oplus C ⊸ (A \oplus C) e (B \oplus C)

(A ⅋ C) \oplus (B ⅋ C) ⊸ (A \oplus B) ⅋ C

(A & C) \oplus (B & C) ⊸ (A \oplus B) & C

Codificando lógica clássica / intuicionista em lógica linear

Tanto a implicação intuicionista quanto a clássica podem ser recuperadas da implicação linear inserindo exponenciais: a implicação intuicionista é codificada como $! A ⊸ B$ , enquanto a implicação clássica pode ser codificada como $!? A ⊸? B$ ou $! A ⊸?! B$ (ou uma variedade de traduções alternativas possíveis). A ideia é que os exponenciais nos permitem usar uma fórmula quantas vezes precisarmos, o que sempre é possível na lógica clássica e intuicionista.

Formalmente, existe uma tradução de fórmulas de lógica intuicionista em fórmulas de lógica linear de uma forma que garante que a fórmula original pode ser demonstrada em lógica intuicionista se e somente se a fórmula traduzida for demonstrável em lógica linear. Usando a tradução negativa de Gödel – Gentzen , podemos incorporar a lógica clássica de primeira ordem na lógica linear de primeira ordem.

A interpretação do recurso

Lafont (1993) primeiro mostrou como a lógica linear intuicionista pode ser explicada como uma lógica de recursos, fornecendo assim à linguagem lógica acesso a formalismos que podem ser usados para raciocinar sobre recursos dentro da própria lógica, em vez de, como na lógica clássica, por meios de predicados e relações não lógicas. O exemplo clássico da máquina de venda automática de Tony Hoare (1985) pode ser usado para ilustrar essa ideia.

Suponha que representam ter uma barra de chocolate pela proposição atômica $doces$ , e ter um dólar por $$ 1$ . Para afirmar o fato de que um dólar comprará uma barra de chocolate para você, poderíamos escrever a implicação $$ 1 \Rightarrow doce$ . Mas na lógica comum (clássica ou intuitionistic), de $A$ e $A \Rightarrow B$ pode-se concluir $A \land B$ . Portanto, a lógica comum nos leva a acreditar que podemos comprar a barra de chocolate e ficar com o nosso dólar! É claro que podemos evitar esse problema usando codificações mais sofisticadas, embora normalmente tais codificações sofram do 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 \Rightarrow doce$ , expressamos a propriedade da máquina de venda automática como uma implicação linear de $$ 1 ⊸ doce$ . A partir de $$ 1$ e desse fato, podemos concluir $doces$ , mas não $doces de$ $$ 1 \otimes$ . Em geral, podemos usar a proposição lógica linear $A ⊸ B$ para expressar a validade de transformar recursos $A$ em recurso $B$ .

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

A conjunção multiplicativa $(A \otimes B)$ denota a ocorrência simultânea de recursos, a serem usados conforme orientação do consumidor. Por exemplo, se você comprar um chiclete e uma garrafa de refrigerante, então você está solicitando $goma \otimes bebida$ . A constante 1 denota a ausência de qualquer recurso e, portanto, funciona como a unidade de ⊗.

A conjunção aditiva $(A e B)$ representa a ocorrência alternativa de recursos, cuja escolha o consumidor controla. Se na máquina de venda automática houver um pacote de salgadinhos, uma barra de chocolate e uma lata de refrigerante, cada um custando um dólar, então por esse preço você pode comprar exatamente um desses produtos. Assim, escrevemos $$ 1 ⊸ (doces e batatas fritas e bebidas)$ . Nós não escrever $$ 1 ⊸ (doces \otimes fichas \otimes bebida)$ , o que implicaria isso basta um dólar para a compra de todos os três produtos juntos. No entanto, de $$ 1 ⊸ (doces e batatas fritas e bebidas)$ , podemos deduzir corretamente $$ 3 ⊸ (doces \otimes batatas fritas \otimes bebida)$ , onde $$ 3 : = $ 1 \otimes $ 1 \otimes $ 1$ . A unidade ⊤ de conjunção aditiva pode ser vista como um cesto de lixo para recursos desnecessários. Por exemplo, podemos escrever $$ 3 ⊸ (doce \otimes ⊤)$ para expressar que com três dólares você pode obter uma barra de chocolate e outras coisas, sem ser mais específico (por exemplo, batatas fritas e uma bebida, ou $ 2, ou $ 1 e batatas fritas , etc.).

A disjunção aditiva $(A \oplus B)$ representa a ocorrência alternativa de recursos, cuja escolha a máquina controla. Por exemplo, suponha que a máquina de venda automática permita jogos de azar: insira um dólar e a máquina poderá dispensar uma barra de chocolate, um pacote de batatas fritas ou um refrigerante. Podemos expressar essa situação como $$ 1 ⊸ (doce \oplus batata frita \oplus 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 quanto uma máquina que sempre produz $A$ porque nunca terá sucesso em produzir um 0). Portanto, ao contrário do que foi $dito$ acima, não podemos deduzir $$ 3 ⊸ (doce \otimes chips \otimes bebida)$ disso.

Disjunção multiplicativa $(Um ⅋ B)$ é mais difícil de brilho, em termos de recurso a interpretação, embora nós pode codificar para trás em implicação linear, quer como $um ⊥ ⊸ B$ ou $B ⊥ ⊸ Uma$ .

Outros sistemas de prova

Redes de prova

Introduzidas por Jean-Yves Girard , as redes de provas foram criadas para evitar a burocracia , ou seja, todas as coisas que diferenciam duas derivações do ponto de vista lógico, mas não do ponto de vista "moral".

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

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

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

Semântica

Semântica algébrica

Decidibilidade / complexidade de vinculação

A relação de implicação em CLL completo é indecidível . Ao considerar fragmentos de CLL, o problema de decisão tem complexidade variável:

Lógica linear multiplicativa (MLL): apenas os conectivos multiplicativos. A vinculação de MLL é NP-completa , mesmo se restringindo a cláusulas de Horn no fragmento puramente implicativo ou a fórmulas livres de átomos.
Lógica linear multiplicativa-aditiva (MALL): apenas multiplicativos e aditivos (ou seja, sem exponencial). A vinculação de MALL é PSPACE completa .
Lógica linear multiplicativa-exponencial (MELL): apenas multiplicativos e exponenciais. Por redução do problema de alcançabilidade para redes de Petri , a vinculação de MELL deve ser pelo menos EXPSPACE-hard , embora a própria decidibilidade tenha tido o status de um problema aberto de longa data. Em 2015, uma prova de decidibilidade foi publicada na revista TCS , mas posteriormente se revelou errônea.
A lógica linear afim (ou seja, a lógica linear com enfraquecimento, uma extensão em vez de um fragmento) mostrou-se decidível, em 1995.

Variantes

Muitas variações da lógica linear surgem por meio de ajustes adicionais nas 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 relevante , que proíbe o enfraquecimento, mas permite a contração global.
Lógica não comutativa ou lógica ordenada, que retira a regra de troca, além de impedir o enfraquecimento e a contração. Na lógica ordenada, a implicação linear se divide ainda em implicação à esquerda e implicação à direita.

Diferentes variantes intuicionistas da lógica linear foram consideradas. Quando baseado em uma apresentação de cálculo sequencial de conclusão única, como em ILL (Intuitionistic Linear Logic), os conectivos ⅋, ⊥ e? estão ausentes e a implicação linear é tratada como um conectivo primitivo. Em FILL (Full Intuitionistic Linear Logic) os conectivos ⅋, ⊥ e? estão presentes, a implicação linear é um conectivo primitivo e, à semelhança do que acontece na lógica intuicionista, todos os conectivos (exceto a negação linear) são independentes. Existem também extensões de primeira ordem 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 ).

Veja também

Referências

Leitura adicional

Girard, Jean-Yves. Linear logic , Theoretical Computer Science, Vol 50, no 1, pp. 1-102, 1987.
Girard, Jean-Yves, Lafont, Yves e Taylor, Paul. Provas e tipos . Cambridge Press, 1989.
Hoare, CAR, 1985. Communicating Sequential Processes . Prentice-Hall International. ISBN 0-13-153271-5
Lafont, Yves, 1993. Introdução à lógica linear . Notas de aula da Escola de Verão TEMPUS sobre Métodos Algébricos e Categóricos em Ciência da Computação , Brno, República Tcheca.
Troelstra, AS Lectures on Linear Logic . CSLI (Centro para o Estudo da Linguagem e Informação) Notas de Aula No. 29. Stanford, 1992.
AS Troelstra , H. Schwichtenberg (1996). Teoria da Prova Básica . Na série Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, ISBN 0-521-77911-1 .
Di Cosmo, Roberto e Danos, Vincent. O primer da lógica linear .
Introdução à lógica linear (postscript) por Patrick Lincoln
Introdução à lógica linear por Torben Brauner
Uma amostra da lógica linear de Philip Wadler
Lógica linear de Roberto Di Cosmo e Dale Miller . The Stanford Encyclopedia of Philosophy (edição do outono de 2006), Edward N. Zalta (ed.).
Visão geral da programação de lógica linear por Dale Miller . Em Linear Logic in Computer Science , editado por Ehrhard, Girard, Ruet e Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.
Wiki de lógica linear

links externos

Mídia relacionada à lógica linear no Wikimedia Commons
A Linear Logic Prover (llprover) , disponível para uso online, em: Naoyuki Tamura / Dept of CS / Kobe University / Japan

Languages

In other projects