logica lineare

La logica lineare è una proposta da come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda. Sebbene questo sistema logico sia un oggetto di studio fine a se stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la o la fisica dei quanti e la linguistica, in particolare per la sua enfasi sulle risorse limitate, la dualità e l'interazione. La logica lineare, di per sé, si presta a molteplici presentazioni e spiegazioni. Dal punto di vista della teoria della dimostrazione deriva da un'analisi del calcolo dei sequenti classico in cui gli usi della e di (regole strutturali) sono attentamente regolati. Al livello operativo questo significa che la deduzione logica non riguarda più solo l'espandere un insieme di "proposizioni vere", ma è anche un modo per manipolare risorse che non possono essere sempre duplicate o eliminate a piacere. In termini di semplici modelli denotazionali, la logica lineare può essere considerata come un raffinamento dell'interpretazione della logica intuizionistica sostituendo le con categorie monoidali simmetriche, o dell'interpretazione della logica classica sostituendo le algebre booleane con le .