Logica lineare

La logica lineare è una logica substrutturale proposta da Jean-Yves Girard come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda^[1]. Sebbene questo sistema logico sia un oggetto di studio fine a sé stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la game semantics o la fisica dei quanti^[2] e la linguistica^[3], 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 regola di contrazione e di indebolimento (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 categorie cartesiane chiuse con categorie monoidali simmetriche, o dell'interpretazione della logica classica sostituendo le algebre booleane con le C*-algebre.

Sintassi

Il linguaggio della logica lineare classica (CLL) è definito induttivamente dalla seguente BNF:

$A$	::=	$p$ ∣ $p$ ^⊥
	∣	$A$ ⊗ $A$ ∣ $A$ ⊕ $A$
	∣	$A$ & $A$ ∣ $A$ ⅋ $A$
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	! $A$ ∣ ? $A$

dove $p$ e $p$ ^⊥ appartengono all'insieme delle proposizioni atomiche del linguaggio. Per motivi che saranno spiegati in seguito, i connettivi ⊗, ⅋, 1 e ⊥ sono detti moltiplicativi, mentre &, ⊕, ⊤ e 0 additivi, e i connettivi ! e ? sono chiamati esponenziali. In più, possiamo impiegare la seguente terminologia:

⊗ è detto "congiunzione moltiplicativa" o "per" (talvolta anche "tensore")
⊕ è detto "disgiunzione additiva" o "più"
& è detto "congiunzione additiva" o "con"
⅋ è detto "disgiunzione moltiplicativa" o "par"
! si legge "certamente" (o "bang")
? si legge "perché no"

Ogni proposizione $A$ in CLL ha un suo duale $A$ ^⊥, definito come segue:

$(p)$ ^⊥ $=p$ ^⊥			$(p$ ^⊥ $)$ ^⊥ $=p$
$(A$ ⊗ $B$ )^⊥ $=A$ ^⊥ ⅋ $B$ ^⊥			( $A$ ⅋ $B$ )^⊥ $=A$ ^⊥ ⊗ $B$ ^⊥
$A$ ⊕ $B$ )^⊥ $=A$ ^⊥ & $B$ ^⊥			$(A$ & $B$ )^⊥ $=A$ ^⊥ ⊕ $B$ ^⊥
$(1)$ ^⊥ $=$ ⊥			(⊥)^⊥ $=1$
$(0)$ ^⊥ $=$ ⊤			(⊤)^⊥ $=0$
$(!A)$ ^⊥ $=?(A$ ^⊥ $)$			$(?A)$ ^⊥ $=!(A$ ^⊥ $)$

Classificazione dei connettivi
	add	mul	exp
pos	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

Si osservi che $(-)$ ^⊥ è un'involuzione, ossia per qualsiasi proposizione $A$ ^⊥⊥ $=A$ . $A$ ^⊥ è anche detta negazione lineare di $A$ .

Le colonne della tabella suggeriscono un altro modo per classificare i connettivi della logica lineare, chiamato polarità: i connettivi negati nella colonna di sinistra (⊗, ⊕, 1, 0,!) sono chiamati positivi, mentre i loro duali a destra (⅋, &, ⊥, ⊤,?) sono chiamati negativi; cf. tabella a destra.

L'implicazione lineare non è inclusa nella grammatica dei connettivi, ma è definibile nella CLL usando la negazione lineare e la disigunzione moltiplicativa (par), da $A$ ⊸ $B:=A$ ^⊥⅋ $B$ . Il connettivo ⊸ è talvolta chiamato "lollipop" a causa della sua forma.

Note

^ Jean-Yves Girard, Linear logic (PDF), in Theoretical Computer Science, vol. 50, n. 1, 1987, pp. 1–102, DOI:10.1016/0304-3975(87)90045-4.
^ John Baez e Mike Stay, Physics, Topology, Logic and Computation: A Rosetta Stone (PDF), in Bob Coecke (a cura di), New Structures of Physics, 2008.
^ V. de Paiva, J. van Genabith e E. Ritter, Dagstuhl Seminar 99341 on Linear Logic and Applications (PDF), 1999.

Bibliografia

Girard, Jean-Yves. Linear logic, Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987.
Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. Proofs and Types. Cambridge Press, 1989.
Hoare, C. A. R., 1985. Communicating Sequential Processes. Prentice-Hall International. ISBN 0-13-153271-5
Lafont, Yves, 1993. Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, Brno, Czech Republic.
Troelstra, A.S. Lectures on Linear Logic. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.
A. S. Troelstra, H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
Di Cosmo, Roberto, and Danos, Vincent. The linear logic primer.
Introduction to Linear Logic (Postscript) by Patrick Lincoln
Introduction to Linear Logic by Torben Brauner
A taste of linear logic by Philip Wadler
Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
Overview of linear logic programming by Dale Miller. In Linear Logic in Computer Science, edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.
Linear Logic Wiki