La semantique relationnelle est injective pour la logique lineaire

pages

Français

Documents

2011

Écrit par
Daniel De Carvalho

Publié par
profil-urra-2012

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

Français

Ebook

2011

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

profil-urra-2012

Publié le

01 juin 2011

Nombre de lectures

Langue

Français

La semantique relationnelle est injective pour la logique lineaire Daniel de Carvalho LIPN - Universite Paris-Nord 30 juin 2011

morphisme de cogebres

lipn - universite paris-nord

canonicite des reseaux

travaux de danos

debut des annees

danos-regnier

Voir

Publié par

profil-urra-2012

Publié le

01 juin 2011

Nombre de lectures

Langue

Français

La s´emantique relationnelle est injective pour la
logique lin´eaire
Daniel de Carvalho
LIPN - Universit´e Paris-Nord
30 juin 2011Nouvelle syntaxe des r´eseaux
(Danos-Regnier) (1)
Dans la syntaxe originale (Girard, 1987), la contraction est
commutative:
RR
? = ?
...
...Nouvelle syntaxe des r´eseaux
(Danos-Regnier) (2)
Les travaux de Danos, Regnier et R´etor´e (ﬁn des ann´ees 80 - d´ebut
des ann´ees 90) consid`erent une contraction et un aﬀaiblissement
tels que
la contraction est associative:
RR
? ?
'
? ?
pour la contraction, l’aﬀaiblissement est neutre:
RR
w
'
?
...
...
...
...Nouvelle syntaxe des r´eseaux
(Danos-Regnier) (3)
la contraction est un morphisme de cog`ebres:
R R
?
'
! !?
l’aﬀaiblissement est un morphisme de cog`ebres:
R R
w w
'
! !
...
...
...
...Probl`emes :
Canonicit´e des r´eseaux?
Conﬂuence?
S´eparation?La s´emantique relationnelle
mˆeme interpr´etation que dans les mod`eles de coh´erence
non-uniforme (Ehrhard-Bucciarelli et Boudes);
espaces coh´erents d´eg´en´er´es (Girard);
espaces vectoriels d´eg´en´er´es (Ehrhard);
profoncteurs d´eg´en´er´es.
Le probl`eme de l’injectivit´e de la s´emantique est le suivant : a-t-on
0 0JRK = JR K) R ' R ?β
Le probl`eme de l’injectivit´e de la s´emantique relationnelle pour la
nouvelle syntaxe est ´equivalent au probl`eme de l’injectivit´e de
l’expansion de Taylor dans les r´eseaux diﬀ´erentiels
(Ehrhard-Regnier).Travaux connexes
Laurent-Tortora de Falco (2006) : caract´erisation des r´eseaux
en forme normale de SLL et ELL parmi les r´eseaux en forme
normale;
de Carvalho-Pagani-Tortora de Falco (2011) : nombre
d’´etapes d’´elimination des coupures via la s´emantique.R´esultats partiels
Tortora de Falco (2003) : fragment
X j?A℘AjA℘?AjA℘AjA
Aj!A
de Carvalho-Tortora de Falco (soumis) : MELL sans
aﬀablissement et sans?Exp´eriences (1)
On pose
D = A[(f+,gfg )0
D = D [(f+,g D D )[(f+,gM (D)).n+1 0 n n ﬁn
S
On pose D = D .nn2N
Une exp´erience de R est la donn´ee
d’une fonction de l’ensemble des ports de profondeur 0 de R
versM (D)ﬁn
et d’une fonction qui associe `a chaque boˆıte B de R un
multi-ensemble ﬁni de multi-ensembles ﬁnis d’exp´eriences de
B
qui v´eriﬁent les conditions suivantes:Exp´eriences (2)
[α] [β] [α] [β]