A System of Interaction and Structure IV: The Exponentials and Decomposition
43
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
43
pages
English
Ebook
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
A System of Interaction and Structure IV: The Exponentials and Decomposition Lutz Straßburger INRIA Saclay–Ile-de-France and Ecole Polytechnique, France and Alessio Guglielmi University of Bath, UK and INRIA Nancy–Grand Est, France We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs. Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—proof theory General Terms: Deep Inference, Calculus of Structures, Linear Logic, Noncommutativity Additional Key Words and Phrases: Decomposition, Cut Elimination, !-?-Flow-Graphs 1. INTRODUCTION This is the fourth in a series of papers dedicated to the proof theory of a self-dual non-commutative operator, called seq, in the context of linear logic. The first paper “A System of Interaction and Structure” [Guglielmi 2007] intro- duced seq in the context of multiplicative linear logic.
- hilbert system
- ll ll
- linear logic
- decomposition ·
- commutative exponential
- rules become mutually
- r¯
- rules
- nel
ASystemofInteractionandStructureIV:
TheExponentialsandDecomposition
LutzStraßburger
INRIASaclay–ˆIle-de-FranceandE´colePolytechnique,France
dnaAlessioGuglielmi
UniversityofBath,UKandINRIANancy–GrandEst,France
Westudyasystem,calledNEL,whichisthemixedcommutative/non-commutativelinearlogic
BVaugmentedwithlinearlogic’sexponentials.Equivalently,NELisMELLaugmentedwith
thenon-commutativeself-dualconnectiveseq.Inthispaper,weshowabasiccompositionality
propertyofNEL,whichwecall
decomposition
.Thisresultleadstoacut-eliminationtheorem,
whichisprovedinthenextpaperofthisseries.Tocontroltheinductionmeasureforthetheorem,
werelyonanoveltechniquethatextractsfromNELproofsthestructureofexponentials,into
whatwecall!-?-Flow-Graphs.
CategoriesandSubjectDescriptors:F.4.1[
MathematicalLogicandFormalLanguages
]:
MathematicalLogic—
prooftheory
GeneralTerms:DeepInference,CalculusofStructures,LinearLogic,Noncommutativity
AdditionalKeyWordsandPhrases:Decomposition,CutElimination,!-?-Flow-Graphs
1.INTRODUCTION
Thisisthefourthinaseriesofpapersdedicatedtotheprooftheoryofaself-dual
non-commutativeoperator,called
seq
,inthecontextoflinearlogic.
Thefirstpaper
“ASystemofInteractionandStructure”
[Guglielmi2007]intro-
ducedseqinthecontextofmultiplicativelinearlogic.Theresultinglogiciscalled
BV
.Theproofsystemfor
BV
ispresentedintheformalismcalledthe
calculusof
structures
,whichisthesimplestformalisminthemethodologyof
deepinference
.
Infact,deepinferencewasbornpreciselyforgiving
BV
anormalizationtheory.
Inthesecondpaper
“ASystemofInteractionandStructureII:TheNeedfor
DeepInference”
[Tiu2006],AlwenTiushowsthatdeepinferenceisnecessaryto
obtainanalyticityfor
BV
.Inotherwords,traditionalGentzenprooftheoryisnot
sufficienttodealwithseq.
Thethirdpaper,currentlybeingelaborated,explorestheconnectionbetween
BV
andpomsetlogic[Retore´1997].
Thisfourthpaper,andthefifthpaper
“ASystemofInteractionandStructureV:
TheExponentialsandSplitting”
[GuglielmiandStraßburger2009]aredevotedto
theprooftheoryofsystem
BV
whenitisenrichedwithlinearlogic’sexponentials.
Wecall
NEL
(non-commutativeexponentiallinearlogic)theresultingsystem.We
canalsoconsider
NEL
as
MELL
(multiplicativeexponentiallinearlogic[Girard
1987])plusseq.
NEL
,whichwasfirstpresentedin[GuglielmiandStraßburger2002],
isconservativeover
BV
andover
MELL
augmentedbythemixandnullarymixrules
[FleuryandRetore´1994;Retore´1993;AbramskyandJagadeesan1994].Notethat,
ACMTransactionsonComputationalLogic,Vol.V,No.N,Month20YY,Pages1–43.
2
LutzStraßburgerandAlessioGuglielmi
like
BV
,
NEL
cannotbeanalyticallyexpressedoutsidedeepinference.System
NEL
canbeimmediatelyunderstoodbyanybodyacquaintedwiththesequentcalculus,
andisaimedatthesamerangeofapplicationsas
MELL
,butitoffers,ofcourse,
explicitsequentialcomposition.
NEL
isespeciallyinterestingbecauseitisTuring-complete[Straßburger2003c].
Thecomplexityof
MELL
iscurrentlyunknown,but
MELL
iswidelyconjectured
tobedecidable.Ifthatwasthecase,thenthelinetowardsTuring-completeness
wouldclearlybecrossedbyseq,which,infact,hasbeeninterpretedalreadyasan
effectivemechanismtostructureaTuringmachinetape.Thisissomethingthat
MELL
,whichisfullycommutative,apparentlycannotdo.
Thispaperisdevotedtothe
decompositiontheorem
.Togetherwiththe
splitting
theorem
in[GuglielmiandStraßburger2009]itimmediatelyyieldscut-elimination,
whichwillbeclaimedin[GuglielmiandStraßburger2009].
Decomposition(whichwasfirstpioneeredin[GuglielmiandStraßburger2001;
Straßburger2003b]for
BV
and
MELL
)isasfollows:wecantransformevery
NEL
derivationintoanequivalentone,composedofelevenderivationscarriedintoeleven
disjointsubsystemsof
NEL
.Thismeansthatwecanstudysmallsubsystemsof
NEL
inisolationandthencomposethemtogetherwithconsiderablemorefreedom
thaninthesequentcalculus,where,forexample,contractioncannotbeisolated
inaderivation.Decompositionismadeavailableinthecalculusofstructuresby
exploitingthetop-downsymmetryofderivationsthatistypicalofdeepinference.
Sucharesultisunthinkableinformalismslackinglocality,likeGentzensystems.
Thetechniquebywhichweprovetheresultisanevolutionandsimplification
ofatechniquethatwasfirstdevelopedin[Straßburger2003b]for
MELL
,butthat
wouldnotworkunmodifiedinthepresenceofseq.Infact,seqmakesmattersmore
complicated,duetosimilarphenomenatothoseunveiledbyTiu[Tiu2006],and
thatmakeseqintractableforGentzenmethods.
Someofthemainresultsofthispaperhavealreadybeenpresented,without
proof,in[GuglielmiandStraßburger2002].
2.THESYSTEM
Wedefinethelanguageforsystem
NEL
anditsvariants,asanextensionofthelan-
guagefor
BV
,definedin[Guglielmi2007].Intuitively,[
S
1
O
O
S
h
]corresponds
toasequent
⊢
S
1
,...,S
h
inlinearlogic,whoseformulaeareessentiallyconnected
bypars,subjecttocommutativity(andassociativity).Thestructure(
S
1
S
h
)
correspondstotheassociativeandcommutativetensorconnectionof
S
1
,...,
S
h
.
Thestructure
h
S
1
⊳
⊳
S
h
i
isassociativeand
non-commutative
:thiscorresponds
tothenewlogicalconnective,called
seq
,thatweaddtothoseof
MELL
.
1
Definition
2.1.
Therearecountablymany
positive
and
negativeatoms
.They,
positiveornegative,aredenotedby
a
,
b
,....
Structures
aredenotedby
S
,
P
,
Q
,
1
Pleasenotethatweslightlychangethesyntaxwithrespectto[Guglielmi2007;Tiu2006]:In
thesepaperscommaswhereusedintheplacesoftheconnectives
O
,
,and
⊳
.Althoughthereis
someredundancyinhavingtheconnectivesandthethreedifferenttypesofbrackets,wethink,it
iseasiertoparseforthereader.
ACMTransactionsonComputationalLogic,Vol.V,No.N,Month20YY.
ASystemofInteractionandStructureIV:TheExponentialsandDecomposition
3
AssociativitySingleton
[
R~
O
[
T~
]
O
U~
]=[
R~
O
T~
O
U~
][
R
]=(
R
)=
h
R
i
=
R
(
R~
(
T~
)
U~
)=(
R~
T~
U~
)Negation
h
R~
⊳
h
T~
i
⊳
U~
i
=
h
R~
⊳
T~
⊳
U~
i◦
=
◦
Commutativity[
R
1
O
O
R
h
]=(
R
¯
1
R
¯
h
)
[
R~
O
T~
]=[
T~
O
R~
](
R
1
R
h
)=[
R
¯
1
O
O
R
¯
h
]
(
R~
T~
)=(
T~
R~
)
h
R
1
⊳
⊳
R
h
i
=
h
R
¯
1
⊳
⊳
R
¯
h
i
Unit?
R
=!
R
¯
[
◦
O
R~
]=[
R~
]!
R
=?
R
¯
(
◦
R~
)=(
~R
)
R
¯
=
R
h◦
⊳
R~
i
=
h
R~
i
ContextualClosure
h
R~
⊳
◦i
=
h
R~
i
if
R
=
T
then
S
{
R
}
=
S
{
T
}
Fig.1.Basicequationsforthesyntacticequivalence=
R
,
T
,
U
,
V
,
W
,
X
and
Z
.Thestructuresofthe
language
NEL
aregeneratedby
S
::=
a
|◦|
[
|
S
O
{
z
O
S
}
]
|
(
|
S
{
z
S
}
)
|h
|
S
⊳
{
z
⊳
S
}
i|
?
S
|
!
S
|
S
¯,
>
0
>
0
>
0
where
◦
,the
unit
,isnotanatomand
S
¯isthe
negation
ofthestructure
S
.Structures
withaholethatdoesnotappearinthescopeofanegationaredenotedby
S
{}
.
Thestructure
R
isa
substructure
of
S
{
R
}
,and
S
{}
isits
context
.Wesimplify
theindicationofcontextincaseswherestructuralparenthesesfilltheholeexactly:
forexample,
S
[
R
O
T
]standsfor
S
{
[
R
O
T
]
}
.
Structurescomewithequationaltheoriesestablishingsomebasic,decidableal-
gebraiclawsbywhichstructuresareindistinguishable.Theseareanalogousto
thelawsofassociativity,commutativity,idempotency,andsoon,usuallyimposed
onsequents.Thedi
