La lecture à portée de main
Découvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDécouvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDescription
Sujets
Informations
Publié par | mijec |
Nombre de lectures | 16 |
Langue | English |
Extrait
ASemanticMeasureoftheExecutionTimein
LinearLogic
D.deCarvalho
a
,
1
,M.Pagani
b
,
2
,L.TortoradeFalco
c
a
INRIALorraine–LORIA
b
LaboratoirePPS&Universite´Paris7
c
DipartimentodiFilosofia–Universita`RomaTre
Abstract
Wegiveasemanticaccountoftheexecutiontime(i.e.thenumberofcutelimination
stepsleadingtothenormalform)ofanuntyped
MELL
net.Wefirstprovethat:1)a
netishead-normalizable(i.e.normalizableatdepth0)ifandonlyifitsinterpretation
inthemultisetbasedrelationalsemanticsisnotemptyand2)anetisnormalizableif
andonlyifits
exhaustive
interpretation(asuitablerestrictionofitsinterpretation)
isnotempty.Wethengiveasemanticmeasureofexecutiontime:weprovethatwe
cancomputethenumberofcuteliminationstepsleadingtoacutfreenormalform
ofthenetobtainedbyconnectingtwocutfreenetsbymeansofacut-link,fromthe
interpretationsofthetwocutfreenets.Theseresultsareinspiredbysimilarones
obtainedbythefirstauthorfortheuntypedlambda-calculus.
Keywords:
LinearLogic,DenotationalSemantics,Computationalcomplexity
1Introduction
Rightfromthestart,LinearLogic(LL,[Gir87])appearedasapotentiallogical
tooltostudycomputationalcomplexity.Thelogicalstatusgivenbytheexpo-
nentials(thenewconnectivesofLL)totheoperationsoferasingandcopying
(correspondingtothestructuralrulesofintuitionisticandclassicallogic)shed
anewlightontheduplicationprocessresponsibleofthe“explosion”ofthe
sizeandtimeduringthecuteliminationprocedure.Thisiswitnessedbythe
Emailaddresses:
Daniel.decarvalho@loria.fr
(D.deCarvalho),
pagani@uniroma3.it
(M.Pagani),
tortora@uniroma3.it
(L.TortoradeFalco).
1
PartiallysupportedbyprojectNO-CoST(ANR,JC0543380)
2
SupportedbyapostdocfellowshipDip.toFilosofia,Universita`RomaTre
PreprintsubmittedtoElsevier
30December2008
contributiongivenbyLLtothewideresearchareacalledImplicitCompu-
tationalComplexity:atruebreakthroughwiththisrespectisGirard’sLight
LinearLogic(LLL,[Gir98]).AcarefulhandlingofLL’sexponentialsallows
theauthortokeepenoughcontrolontheduplicationprocess,andtoprove
thatafunction
f
isrepresentableinLLLifandonlyif
f
ispolytime.
Oneofthemainquestionsarisenfrom[Gir98]isthequestofadenotational
semanticssuitableforlightsystems(asemanticsofproofsinlogicalterms,or
moregenerallyamodel).Amongthemainattemptsinthisdirectionwecan
quoteontheonehand[MO00,Bai04],wherethestructures(games,coherent
spaces)associatedwithlogicalformulas
3
aremodifiedsothattheprinciples
validinLLbutnotinthechosenlightsystemdonotholdinthesemantics,
andontheotherhand[LTdF06]whichdealswithapropertyoftheelements
ofthestructures(theinterpretationsofproofs)characterizingthoseelements
which
can
interpretproofswithboundedcomplexity.
Adifferentapproachtothesemanticsofboundedtimecomplexityispossible:
thebasicideaistomeasurebysemanticmeanstheexecutionofanyprogram,
regardlesstoitscomputationalcomplexity.Theaimistocomparedifferent
computationalbehaviorsandtolearnafterwardssomethingontheveryna-
tureofboundedtimecomplexity.Followingthisapproach,in[dC07,dC08]one
oftheauthorsofthepresentpapercouldcomputetheexecutiontimeofan
untyped
λ
-termfromitsinterpretationintheKleislicategoryofthecomonad
associatedwiththefinitemultisetsfunctoronthecategory
Rel
ofsetsand
relations.Suchaninterpretationisthesameastheinterpretationofthenet
translatingthe
λ
-terminthemultisetbasedrelationalmodeloflinearlogic.
Theexecutiontimeismeasuredhereintermsofelementarystepsoftheso-
calledKrivinemachine.Also,[dC07,dC08]giveapreciserelationbetweenan
intersectiontypessystemintroducedby[CDCV80]andexperimentsinthe
multisetbasedrelationalmodel.ExperimentsareatoolintroducedbyGirard
in[Gir87]allowingtocomputetheinterpretationofproofspointwise.Anex-
perimentcorrespondstoatypederivationandtheresultofanexperiment
correspondstoatype.
4
WeapplyherethisapproachtoMultiplicativeandExponentialLinearLogic
(MELL),andweshowhowitispossibletocomputethenumberofstepsof
cuteliminationbysemanticmeans(noticethatourmeasurebeingthenumber
ofcuteliminationsteps,hereisafirstdifferencewith[dC07,dC08]where
Krivine’smachinewasusedtomeasureexecutiontime).LinearLogicoffers
3
Thebasicpatternofdenotationalsemanticsistoassociatewitheveryformula
anobjectofsomecategoryandwitheveryproofoftheformulaamorphismofthis
categorycalledtheinterpretationoftheproof.
4
Theintersectiontypessystemconsideredin[dC07,dC08]lacksidempotencyand
thisfactwascrucialinthatwork.Inthepresentpaper,thiscorrespondstothefact
thatweusemultisetsforinterpretingexponentialsandnotsetsasinthesetbased
coherentsemantics.Theuseofmultisetsisessentialinourworktoo.
2
averysharpwaytostudyGentzen’scuteliminationbyrepresentingproofs
asgraphswithboxes,called
proof-nets
[Gir87].Thepeculiarityofproof-nets
istoreducethenumberofcommutativecuteliminationsteps,whichinstead
aboundedinsequentcalculi.If
π
′
isaproof-netobtainedbyapplyingsome
stepsofcuteliminationto
π
,themainpropertyofanymodelisthatthe
interpretation
J
π
K
of
π
isthesameastheinterpretation
J
π
′
K
of
π
′
,sothat
from
J
π
K
itisclearlyimpossibletodeterminethenumberofstepsleading
from
π
to
π
′
.Nevertheless,ifweconsidertwocutfreeproof-nets
π
1
and
π
2
connectedbymeansofacut-link,wecanwonder:
(1)isitthecasethatthethusobtainednetcanbereducedtoacutfreeone?
(2)iftheanswertothepreviousquestionispositive,whatisthenumberof
cutreductionstepsleadingfromthenetwithcuttoacutfreeone?
Themainpointofthepaperistoshowthatitispossibletoanswerboththese
questionsbyonlyreferringto
J
π
1
K
and
J
π
2
K
5
.
Thefirstquestionmakessenseonlyinanuntypedframework(inthetyped
case,cuteliminationisstronglynormalizing,see[Gir87]),andindeedSubsec-
tion2.1isdevotedtodefineanuntypedversionofGirard’sproof-nets,based
onpreviousworks,mainly[Dan90,Reg92,LTdF06,PTdF09].Terui[Ter02]also
introducedacalculuscorrespondingtoanuntypedandintuitionisticversion
ofproof-netsofLightAffineLogicand[dC05]addressedtheproblemofchar-
acterizingthe(head-)normalizablenetsinthisrestrictedsetting.Weshifthere
fromtheintuitionistictotheclassicalframework.Letusmentionherethatto
improvereadabilitywechosetostateandproveourresultsforproof-nets(i.e.
logicallycorrectproof-structures),butcorrectness(inourframeworkDefini-
tion3)israrelyused(seealsotheconcludingremarks,Section6).Thecut
eliminationprocedurewedefineissimilarto
λ
-calculus
β
-reduction,inthe
sensethattheexponentialstep(thestep(!
/
?)ofDefinition6)ismoresimilar
toastepof
β
-reductionthanitusuallyis.Thisisessentialtoproveourresults
(seethediscussiononFig.5).
Weconsiderinthepapertworeductionstrategies:headreductionandstrat-
ifiedreduction.Thefirstoneconsistsinreducingthecutsatdepth0and
stop.Thesecondoneconsistsinreducingacutonlywhenthereexistsno
cutwith(strictly)smallerdepth.Thesereductionstrategiesextendthehead
(resp.leftmost)reductionof
λ
-calculus.
Wementiontherecentpapers[Lag06]and[LL08],wherethecomplexityoflin-
earlogiccuteliminationisanalysedbymeansofcontextandgamesemantics.
Itisverylikelythatourapproachandthoseof[Lag06],[LL08]arecloselyre-
5
Thequestions(andtheanswers)aremoregeneralthanitseems:everyproof-net
withcutsisthereductofsomeproof-netobtainedbycuttingtwocutfreeproof-nets
(Proposition34).
3
lated.Afineanalysisofthisrelationshouldhelptoclarifythecorrespondences
betweenrelationalandgamesemantics.
Section2isdevotedtodefineourversionofproof-net(Subsection2.1)and
themodelallowingtomeasurethenumberofcuteliminationsteps(Subsec-
tion2.2).InSection3,weshowhowexperimentsprovideacounterforhead
andstratifiedreductionsteps(Lemmas17,20).InSection4weanswerques-
tion(1),andinSection5weanswerquestion(2).
Letusconcludewithalittleremark.In[TdF03],thequestionofinjectivity
fortherelationalandcoherentsemanticsofLLisaddressed:isitthecase
thatfor
π
1
and
π
2
cutfree,from
J
π
1
K
=
J
π
2
K
onecandeduce
π
1
=
π
2
?Itis
conjecturedthatrelationalsemanticsisinjectiveforMELL,andthereisstill
noanswertothisquestion.Given
π
1
and
π
2
,wedon’tknowhowtocompute
thenormalformofthenetobtainedbyconnecting
π
1
and
π
2
bymeansofa
cut-linkfrom
J
π
1
K
and
J
π
2
K
.Thepresentpapershowsthatfrom
J
π
1
K
and
J
π
2
K
wecanatleastcomputethenumberofcuteliminationstepsleadingtothe
normalform.
2Preliminaries
Weintroducethesyntaxandthemodelforwhichweproveourresults:the
untypednetsandtheirinterpretationinthecategory
Rel
ofsetsandrelations.
2.1Untypednets
AftertheirintroductionbyGirardin[Gir87],proof-net