La semantique relationnelle est injective pour la logique lineaire

profil-urra-2012 - Daniel De Carvalho

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

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

48 pages

Français

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

A propos
Informations
Extrait

Description

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

Informations

Publié par	profil-urra-2012
Publié le	01 juin 2011
Nombre de lectures	47
Langue	Français

Extrait

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)
[α] [β] [α] [β]