logica lineare
logica lineare
Proposta dal francese Jean-Yves Girard nel 1987, la logica lineare non si limita a considerare le proposizioni come oggetti dotati di valori di verità come nella logica standard, ma alla stregua di risorse impiegabili una volta sola ai fini del calcolo e quindi dotate di un costo. Anche se la logica lineare coincide con la logica standard nel caso di risorse illimitate, ciò impone una revisione del significato dei connettivi. Congiunzione e disgiunzione ricevono un’interpretazione moltiplicativa e una additiva, corrispondenti rispettivamente alla presenza simultanea o alternativa delle risorse. L’implicazione lineare (detta lollipop con riferimento al simbolo impiegato ‘–o’) indica un metodo per consumare la risorsa-antecedente in modo da ottenere la risorsa-conseguente, che può eliminare la risorsa-antecedente stessa. La negazione lineare (nil) descrive un rapporto di scambio azione/reazione, ma ha un comportamento analogo a quello della logica standard (nil nil A implica A) e garantisce, a differenza della logica intuizionista, la legge del terzo escluso in variante lineare. Due altri operatori sono (!) e (?), da leggere ‘ma certo’ (la risorsa è inesauribile e ha costo zero) e ‘perché no?’ (negazione di !). I rapporti con la logica intuizionista diventano trasparenti considerando che l’implicazione intuizionista A=>B si lascia rappresentare come !A–o B. Nella logica lineare vengono meno le leggi della logica standard come quella di contrazione (A, A, Γ⇒Δ|-A, Γ⇒Δ) e di indebolimento (Γ⇒Δ|-A, Γ⇒Δ). I sequenti lineari si prestano a interessanti rappresentazioni in termini di circuiti elettrici con prese, e sono numerose le applicazioni all’informatica (linguaggio PROLOG, gestione della memoria, studio degli algoritmi paralleli) e alla meccanizzazione del ragionamento. Le dimostrazioni in logica lineare perdono la natura sintattica e diventano oggetti geometrici detti reti di prova, che sono caratterizzate mediante pure proprietà geometriche (i ‘criteri di correttezza’), i quali consentono una trattazione astratta anche degli aspetti computazionali delle dimostrazioni. Dalla logica lineare è recentemente scaturita anche una nuova disciplina, la ludica, che studia le regole logiche in termini della nozione di gioco, puntando a superare la distinzione classica tra sintassi e semantica.