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 modifica

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

  ::=   
    
  &    
1 ∣ 0 ∣ ⊤ ∣ ⊥
!  ∣ ? 

dove   e   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   in CLL ha un suo duale  , definito come segue:

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

Si osservi che   è un'involuzione, ossia per qualsiasi proposizione  ⊥⊥ .   è anche detta negazione lineare di  .

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    . Il connettivo ⊸ è talvolta chiamato "lollipop" a causa della sua forma.

Note modifica

  1. ^ 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.
  2. ^ 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.
  3. ^ V. de Paiva, J. van Genabith e E. Ritter, Dagstuhl Seminar 99341 on Linear Logic and Applications (PDF), 1999.

Ulteriori letture modifica

Altri progetti modifica

Collegamenti esterni modifica