A Semantic Measure of the Execution Time in Linear Logic

Daniel De Carvalho

Description

Niveau: Supérieur, Doctorat, Bac+8
A Semantic Measure of the Execution Time in Linear Logic D. de Carvalho a,1, M. Pagani b,2, L. Tortora de Falco c aINRIA Lorraine – LORIA bLaboratoire PPS & Universite Paris 7 cDipartimento di Filosofia – Universita Roma Tre Abstract We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped MELL net. We first prove that: 1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus. Key words: Linear Logic, Denotational Semantics, Computational complexity 1 Introduction Right from the start, Linear Logic (LL, [Gir87]) appeared as a potential logical tool to study computational complexity.

• girard's light


• linear logic


• girard's proof


• cut elimination


• steps leading


• main question


• denotational semantics

Sujets

• Pagani
• Linear logic
• Cut-elimination theorem
• Denotational semantics

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:
[e-mail]
(D.deCarvalho),
[e-mail]
(M.Pagani),
[e-mail]
(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