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. 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, bem como a linguística, 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.