Lógica não comutativa
A lógica não comutativa é uma extensão da lógica linear , que combina os conectivos comutativos da lógica linear com os conectivos multiplicativos não-comutativos do cálculo de Lambek. Seu cálculo de sequentes se baseia na estrutura de variedades de ordem (uma família de ordens cíclicas que pode ser vista como uma espécie de estrutura), e o critério para a correção de suas redes de prova é dado em termos de permutações parciais. Ela também tem uma semântica denotacional em que as fórmulas são interpretadas por módulos através de algumas Álgebras de Hopf específicas.
Não-comutatividade na lógica
[editar | editar código-fonte]Por extensão, o termo lógica não-comutativa também é usado por alguns autores para referir-se a uma família de lógicas subestruturais em que a regra de permutação é inadmissível. O restante deste artigo é dedicado a uma apresentação dessa acepção do termo.
A lógica não-comutativa mais antiga é o cálculo de Lambek, que deu origem à classe de lógicas conhecidas como gramáticas categóricas. Desde a publicação da lógica linear de Jean-Yves Girard houve várias lógicas não-comutativas propostas, isto é, a lógica linear cíclica de Davi Yetter, lógica pomset de Christian Retoré, e as lógicas não-comutativas BV e NEL estudadas no cálculo de estruturas.
A lógica não comutativa é às vezes chamada de lógica ordenada, uma vez que é possível com a maioria das lógicas não-comutativas propostas impor ordem total ou parcial nas fórmulas de sequentes. No entanto, isso não é completamente geral, já que algumas lógicas não-comutativas não suportam tal ordem, tal como a lógica linear cíclica de Yetter. Observe também que, enquanto a maioria das lógicas não-comutativas não permitem o enfraquecimento ou a contração juntamente com não-comutatividade, essa restrição não é necessária.
O cálculo de Lambek
[editar | editar código-fonte]Joachim Lambek propôs a primeira lógica não-comutativa em seu artigo científico (1958) 'Mathematics of Sentence Structure' para modelar as possibilidades combinatórias da sintaxe das línguas naturais.[1] O seu cálculo tornou-se, assim, um dos principais formalismos de linguística computacional.
Lógica linear cíclica
[editar | editar código-fonte]David N. Yetter propôs uma regra estrutural mais fraca no lugar da regra da permutação da lógica linear, produzindo lógica linear cíclica.[2] Os sequentes da lógica linear cíclica formam um anel, e por isso são invariantes sob rotação, onde regras de multipremissas associam os anéis às fórmulas descritas nas regras. O cálculo suporta três modalidades estruturais, uma modalidade auto-dual permitindo permutação, mas ainda linear, e os exponenciais de costume (? e !) da lógica linear, permitindo regras subestruturais não lineares para serem usadas em conjunto com a permutação.
Lógica pomset
[editar | editar código-fonte]A lógica pomset foi proposta por Christian Retoré em um formalismo semântico com dois operadores sequenciais existindo juntamente com os habituais operadores de "produto" e "par" da lógica linear, a primeira lógica proposta a dispor de ambos operadores comutativos e não-comutativos.[3] Um cálculo de sequente para a lógica foi dado, mas faltava-lhe um teorema da eliminação do corte; em vez disso, o sentido do cálculo foi estabelecido através de uma semântica denotacional.
BV e NEL
[editar | editar código-fonte]Alessio Guglielmi propôs uma variação do cálculo de Retoré, BV, em que os duas operações não-comutativas são recolhidas em um único operador auto-dual e propôs um novo cálculo de provas, o cálculo de estruturas para acomodar o cálculo. A principal novidade do cálculo de estruturas foi seu pervasivo uso de inferência profunda, que foi argumentado ser necessário para cálculos combinando operadores comutativos e não comutativos; esta explicação está de acordo com a dificuldade de conceber sistemas de sequentes para lógica pomset que tenha a eliminação do corte.
Lutz Strassburger desenvolveu um sistema relacionado, NEL, também para o cálculo de estruturas em que a lógica linear com a regra do "mix" aparecem como um subsistema.
Structads
[editar | editar código-fonte]Structads são uma abordagem às semânticas da lógica que são baseadas em generalizar a noção de sequente ao longo das linhas das "espécies combinatoriais" de Joyal, permitindo o tratamento de lógicas mais drasticamente fora do padrão do que as descritas acima, onde, por exemplo, ',' do cálculo sequente não é associativo.
Referências
[editar | editar código-fonte]- ↑ 65. ISSN 0002-9890. doi:10.2307/2310058
- ↑ 55. ISSN 0022-4812. doi:10.2307/2274953
- ↑ Col: Lecture Notes in Computer Science. [S.l.: s.n.] ISBN 978-3-540-62688-6. doi:10.1007/3-540-62688-3_43 Em falta ou vazio
|título=(ajuda)Falta o|titulo=(Ajuda)
Ligações externas
[editar | editar código-fonte]- Non-commutative logic I: the multiplicative fragment by V. Michele Abrusci and Paul Ruet, Annals of Pure and Applied Logic 101(1), 2000. Logical aspects of computational linguistics (PS) by Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré and Eric Villemonte de la Clergerie. Papers on Commutative/Non-commutative Linear Logic in the calculus of structures: a research homepage from which the papers proposing BV and NEL are available.