Esponenziali in logica lineare

Logica matematica, teoria degli insiemi, algebre di Boole e di Heyting ...

Moderatore: Moderatori

Esponenziali in logica lineare

Messaggioda Nihilus il dom 19 lug 2015, 12:39

Due esercizietti sugli esponenziali:

1) Dimostrare che $!!A$ è linearmente equivalente a $!A$.

2) Dimostrare che a meno di equivalenza lineare ci sono soltanto sei modalità organizzate secondo il seguente reticolo:
$
\quad \, ?\\
\; \; \; ?!?\\
!? \quad \; ?!\\
\; \; \; !?!\\
\quad \, !\\
$
Cadi e non c'è nulla cui aggrapparti; cadi e la libertà è non trattenersi. Che perfezione...
Avatar utente
Nihilus
 
Messaggi: 102
Iscritto il: sab 22 set 2012, 14:05

Re: Esponenziali in logica lineare

Messaggioda killing_buddha il dom 19 lug 2015, 15:26

Cosa vogliono dire le varie cose? Ho il sospetto che $(-)!\colon \mathcal{C}\to \mathcal{C}$ sia un endofuntore di una categoria cartesiana chiusa, e che essere linearmente equivalenti significhi... qualcosa di correlato, ma io (e probabilmente anche altri utenti) non sono abbastanza addentro alle definizioni :mrgreen:
- Se incontri il Buddha uccidilo. Devi vivere libero da ogni dogma: se non riesci a uccidere Buddha, come ucciderai il tuo pregiudizio?
- "Peu d'abstraction on éloigne de la géometrie; beaucoup on y ramène"
Avatar utente
killing_buddha
 
Messaggi: 2739
Iscritto il: gio 17 lug 2008, 19:51

Re: Esponenziali in logica lineare

Messaggioda Nihilus il lun 20 lug 2015, 16:15

Sospetto errato!

In logica lineare le formule si possono interpretare come risorse che vengono consumate durante il processo deduttivo, questa peculiarità nasce da certe restrizioni su alcune regole deduttive (chiamate indebolimento e contrazione che consentono rispettivamente di duplicare e cancellare formule che non giocano alcun ruolo attivo in una deduzione).
Come conseguenza si ottengono due congiunzioni $\otimes$ ed $\&$, l'implicazione lineare $\multimap$, dei connettivi nullari $\bot$ (la "più grande" proposizione falsa), $\top$ (la "più grande" proposizione vera) e $1$ (la "più piccola" proposizione vera) ed infine la modalità !. Una formula $!A$ è persistente e le regole di duplicazione e cancellazione si applicano.

Il resto della logica si può definire a partire da questi ingredienti, ad esempio la negazione $A^{\bot} := A \multimap \bot$ o la seconda modalità $?A := (!A^{\bot})^{\bot}$.

Ecco un dizionario per i categoristi:

Definizione
Una categoria $*$-autonoma è una categoria monoidale chiusa simmetrica dotata di un oggetto distinto chiamato oggetto dualizzante $\bot$ tale che la mappa canonica $A \to $Hom$( $Hom$(A, \bot), \bot)$ sia un isomorfismo.
Si pensi l'hom interno come un'implicazione e la richiesta imposta come una legge di doppia negazione.


Definizione
Un modello della logica lineare è una categoria $*$-autonoma $\mathcal C$, che sia al contempo cartesiana e sia dotata di una comonade ! in modo che la sua categoria co-Kleisli sia cartesiana chiusa ed il funtore $\mathcal C_! \to \mathcal C$ sia un funtore monoidale (forte).


A questo punto la traduzione è presto fatta:
$\otimes$ logico corrisponde al prodotto monoidale $\otimes$.
$1$ corrisponde all'unità della struttura monoidale.
$\&$ corrisponde al prodotto in $\mathcal C$.
$\top$ corrisponde all'oggetto terminale.
$\bot$ corrisponde all'oggetto dualizzante della struttura $*$-autonoma.
$\multimap$ corrisponde all'hom interno.
La modalità ! corrisponde alla comonade.

Dimostrare sintatticamente una formula $A$ equivale a trovare un morfismo nel modello $1 \to A$.


Una chicca per le persone che a differenza di me riescono a capire il seguente teorema: la dualità di Verdier si può riscrivere in questo linguaggio.

Teorema (dualità di Verdier)
Sia $X$ uno schema di tipo finito su un campo $k$ e $D(X) := D_c^b(X , \bar{ \mathbb Q_l})$ la categoria derivata limitata dei fasci $l$-adici costruibili.
$D(X)$ è una categoria $*$-autonoma e l'oggetto dualizzante è il solito complesso dualizzante $K_X$.
Cadi e non c'è nulla cui aggrapparti; cadi e la libertà è non trattenersi. Che perfezione...
Avatar utente
Nihilus
 
Messaggi: 102
Iscritto il: sab 22 set 2012, 14:05

Re: Esponenziali in logica lineare

Messaggioda killing_buddha il dom 26 lug 2015, 0:04

Con i pochi elementi a mia disposizione per interpretarlo, non ci ero andato lontanissimo, anzi avevo detto proprio la stessa cosa: una comonade e' un particolare endofuntore, e la base $\cal C$ e' cartesiana chiusa. :P

Manca solo da precisare cosa vuol dire "linearmente equivalente"...
- Se incontri il Buddha uccidilo. Devi vivere libero da ogni dogma: se non riesci a uccidere Buddha, come ucciderai il tuo pregiudizio?
- "Peu d'abstraction on éloigne de la géometrie; beaucoup on y ramène"
Avatar utente
killing_buddha
 
Messaggi: 2739
Iscritto il: gio 17 lug 2008, 19:51

Re: Esponenziali in logica lineare

Messaggioda killing_buddha il dom 26 lug 2015, 14:42

Penso di avere un'idea usando come modello della logica lineare la bicategoria $\bf Prof$ dei profuntori (vedi qui, 5.5). Tu dimmi di piu' sulla equivalenza lineare. :bye:
- Se incontri il Buddha uccidilo. Devi vivere libero da ogni dogma: se non riesci a uccidere Buddha, come ucciderai il tuo pregiudizio?
- "Peu d'abstraction on éloigne de la géometrie; beaucoup on y ramène"
Avatar utente
killing_buddha
 
Messaggi: 2739
Iscritto il: gio 17 lug 2008, 19:51

Re: Esponenziali in logica lineare

Messaggioda Nihilus il lun 27 lug 2015, 14:51

Avevo dimenticato dell'equivalenza lineare che in effetti è una banalità. Due formule $A$ e $B$ sono linearmente equivalenti sse si può dimostrare $A \multimap B$ e $B \multimap A$ (in questo caso particolare non c'è differenza tra le due congiunzioni e si può scegliere a piacimento $(A \multimap B) \& (B \multimap A)$ o $(A \multimap B) \otimes (B \multimap A))$.

Nella pratica basta costruire due morfismi $1 \to \underline{Hom}(A,B)$ e $1 \to \underline{Hom}(B,A)$.

Attenzione però che non basta dimostrarlo per i profuntori, ma deve essere vero in tutti i modelli.

P.S.
$\mathcal C$ non è cartesiana chiusa in generale. La richiesta di chiusura cartesiana si fa sulla categoria coKleisli $\mathcal C_!$
Cadi e non c'è nulla cui aggrapparti; cadi e la libertà è non trattenersi. Che perfezione...
Avatar utente
Nihilus
 
Messaggi: 102
Iscritto il: sab 22 set 2012, 14:05

Re: Esponenziali in logica lineare

Messaggioda Feanor il sab 21 mag 2016, 14:59

Per chi volesse approcciarsi alla logica lineare, esiste questo bel testo introduttivo The linear logic primer, di V. Danos e R. Di Cosmo.
In particolare, gli esercizi dell'OP appaiono come esercizio 1.6.15.

Nihilus ha scritto:Attenzione però che non basta dimostrarlo per i profuntori, ma deve essere vero in tutti i modelli.

Ci sono risultati di soundness, per le categorie $*$-autonome come semantiche della logica lineare?
Feanor
 
Messaggi: 732
Iscritto il: lun 29 set 2008, 20:58

Re: Esponenziali in logica lineare

Messaggioda Nihilus il lun 6 giu 2016, 14:34

Sì, l'esercizio viene precisamente da quelle note!

Le categorie *-autonome corrispondono soltanto ad un frammento della logica lineare. C'è un teorema di correttezza e completezza per la logica lineare relativamente a quelli che ho chiamato 'modelli della logica lineare' nella mia prima riposta che sono categorie *-autonome con parecchia struttura extra.

Qui https://www.irif.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/biblio/categorical-semantics-of-linear-logic.pdf dovrebbe esserci la dimostrazione del teorema di correttezza e completezza.
Cadi e non c'è nulla cui aggrapparti; cadi e la libertà è non trattenersi. Che perfezione...
Avatar utente
Nihilus
 
Messaggi: 102
Iscritto il: sab 22 set 2012, 14:05


Torna a Logica

Chi c’è in linea

Visitano il forum: Nessuno e 1 ospite