A Semantic Measure of the Execution Time in Linear Logic

-

English
35 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 16
Language English
Report a problem

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-netshavebeenextensively
studiedandusedasaproof-theoreticaltoolforseveralpurposes.Allthiswork
ledtomanyimprovementsoftheoriginalnotionintroducedbyGirard.
WeusehereanuntypedversionofGirard’sproof-nets.DanosandRegnier
[Dan90,Reg92]introducedandstudied“pureproof-nets”thatistheexact
notionofproof-netcorrespondingtopure
λ
-calculus.Therehasbeennoreal
needforadifferentnotionofuntypedproof-netuntilGirard’sworkonLight
LinearLogic[Gir98]:Terui[Ter02]introducesa“light”untyped
λ
-calculus
enjoyingstrongnormalizationinpolynomialtimeandencodingallpolytime
functions.Thiscalculusclearlycorrespondstoanuntypedandintuitionistic
versionofproof-nets.Inthesamespirit,anuntypednotionofproof-net(called
net
)isintroducedin[LTdF06]inordertoencodepolytimecomputations:the
noveltyhereistheshiftfromtheintuitionistictotheclassicalframework(see
also[PTdF09]).Thisyields
clashes
,thatiscutswhichcannotbereduced(see
Def.5andFig.2).

4

♭♭


!!


♭♭

♭♭


?
=
?

=



?
=
?

?
Fig.1.Someconventionstopictureanarbitrarynumberofnodes/edges

Byfollowing[Reg92,DR95],wechoosehereaversionofnetswhere?-linkshave
n

0premises(theselinksareoftenrepresentedbyatreeofcontractionsand
weakenings).Wealsohavea

-nodewhichisourwaytorepresentdereliction.
Thesechoicesallowastrictcorrespondencebetweenthenumberofstepsof
thecuteliminationofanetanditsinterpretationin
Rel
(seeTheorem38).
Wewillendthesubsectionwithabriefdiscussiononthesechoices.
Definition1(Ground-structure)
A
ground-structure
,or
g-structure
for
short,isafinite(possiblyempty)labelleddirectedacyclicgraphwhosenodes
(alsocalledlinks)aredefinedtogetherwithanarityandacoarity,i.e.agiven
numberofincidentedgescalledthe
premises
ofthenodeandagivennumber
ofemergentedgescalledthe
conclusions
ofthenode.Thevalidnodesare:
♭♭axcut

`
1

!

?


♭♭

Anedgecanhaveornota

label:anedgewithnolabel(resp.witha

label)
iscalled
logical
(resp.
structural
).The

-nodeshavealogicalpremiseanda
structuralconclusion,the
?
-nodeshave
k

0
structuralpremisesandone
logicalconclusion,the
!
-nodeshavenopremise,exactlyonelogicalconclusion,
alsocalled
main
conclusionofthenode,and
k

0
structuralconclusions,
called
auxiliary
conclusionsofthenode.Premisesandconclusionsofthenodes
ax
,
cut
,

,
`
,
1
,

arelogicaledges.Weallowedgeswithasourcebutno
target,theyarecalled
conclusions
oftheg-structure;weconsiderthatag-
structureisgivenwithanorder
(
c
1
,...,c
n
)
ofitsconclusions.
Wedenoteby
!(
α
)
thesetof
!
-linksofag-structure
α
.
Whendrawingag-structureweorderitsconclusionsfromlefttoright.Also
werepresentedgesorientedtop-downsothatwespeakofmovingupwardlyor
downwardlyinthegraph,andofnodesoredges“above”or“under”agiven
node/edge.Inthesequelwewillnotwriteexplicitlytheorientationofthe
edges.Inordertogivemoreconcisepictures,whennotmisleading,wemay
representanarbitrarynumberof

-edges(possiblyzero)asa

-edgewitha
diagonalstrokedrawnacross(seeFig1).Inthesamespirit,a?-linkwitha
diagonalstrokedrawnacrossitsconclusionrepresentsanarbitrarynumber
of?-links,possiblyzero(seeFig1).Givenanyset
X
,wedenoteby
X
the
setoffinitesequencesofelementsof
X
,andby
x
agenericelementof
X
.
Forexample,asequence(
c
1
,...,c
n
)ofconclusionsofag-structure
α
maybe
denotedsimplyby
c
.

5

Definition2(Untyped

-structure)
An
untyped

-structure
,orsimply

-
structure
,
π
ofdepth0
isag-structurewithout
!
-nodes;inthiscase,weset
ground(
π
)=
π
.An
untyped

-structure
π
ofdepth
d
+1
isag-structure
α
,denotedby
ground(
π
)
,withafunctionthatassignstoevery
!
-link
o
of
α
with
n
o
+1
conclusionsa

-structure
π
o
ofdepthatmost
d
,calledthe
boxof
o
,with
n
o
structuralconclusions,alsocalled
auxiliaryconclusions
of
π
o
,and
exactlyonelogicalconclusion,calledthe
mainconclusion
of
π
o
,andabijection
fromthesetofthe
n
o
structuralconclusionsofthelink
o
tothesetofthe
n
o
structuralconclusionsofthe

-structure
π
o
.Moreover
α
hasatleastone
!
-link
withaboxofdepth
d
.
Wesaythat
ground(
π
)
isthe
g-structureofdepth0of
π
;a
g-structureof
depth
d
+1in
π
isag-structureofdepth
d
oftheboxassociatedby
π
witha
!
-nodeof
ground(
π
)
.A
link
l
ofdepth
d
of
π
isalinkofag-structureofdepth
d
of
π
;wedenoteby
depth(
l
)
thedepth
d
of
l
.Werefermoregenerallytoa
link/g-structureof
π
meaningalink/g-structureofsomedepthof
π
.
Inordertomakevisualthecorrespondencebetweenaconclusionofa!-link
andtheassociatedconclusionoftheboxofthat!-link,werepresentthetwo
edgesbyasinglelinecrossingtheborderofthebox(forexampleseeFig.3).
Inthenextdefinitionweintroducetheuntypednetsbymeansofswitching
acyclicity.Thisisastandardnotionofcorrectnesswhichcharacterizesthe
structuressequentializableinacalculusextendedwiththemixrule[DR89].
Definition3(Untypednets)
A
switching
ofag-structure
α
isanundi-
rectedsubgraphof
α
obtainedbyforgettingtheorientationof
α
’sedges,by
deletingoneofthetwopremisesofeach
`
-node,andforevery
?
-node
l
with
n

1
premises,byerasingallbutonepremisesof
l
.
An
untyped

-net
,

-net
forshort,isa

-structure
π
s.t.everyswitchingof
everyg-structureof
π
isanacyclicgraph.An
untypednet
,
net
forshort,isa

-netwithnostructuralconclusion.
Noticethatwitheverystructuraledge
b
ofanetisassociatedexactlyone

-node(aboveit)andone?-node(belowit):wewillrefertothesenodesas
the

-node/
?
-nodeassociatedwith
b
.Observethatthe

-nodeandthe?-node
associatedwithagivenedgemighthaveadifferentdepth.
Concerningthepresenceofemptynets,noticethattheemptynetdoesexist
andithasnoconclusion.Itspresenceisrequiredbythecuteliminationpro-
cedure(Def.6):theeliminationofacutbetweena1-linkanda

-linkyields
theemptygraph,andsimilarlyforacutbetweena!-linkwithnoauxiliary
conclusionanda0-ary?-link.Ontheotherhand,noticealsothatwitha!-link
o
ofanet,itis
never
possibletoassociatetheemptynet:
o
hasatleastone
conclusionandthishasalsotobethecaseforthenetassociatedwith
o
.
Definition4(Sizeofnets)
The
size
s
(
α
)ofag-structure
α
isthenumber

6

oflogicaledgesof
α
.The
size
s
(
π
)ofa

-structure
π
isdefinedbyinduction
onthedepthof
π
,asfollows:
s
(
π
)=
s
(ground(
π
))+
o

!(ground(
π
))
s
(
π
o
)
.
PSinceweareinanuntypedframework,netsmay
⊥⊥⊥
!
contain“pathological”cuts(seeexamplesinFig.2)
cutcut
whicharenotreducible.Thesecutsarecalled
Fig.2.Twoclashes
clashes
andtheirpresenceisincontrastwithwhat
happensin
λ
-calculus,wherethesimplergrammar
oftermsavoidsclashesalsoinanuntypedframework.
Definition5(Clash)
Thetwoedgespremisesofacut-linkare
dual
when:

theyareconclusionsofresp.a

-nodeandofa
`
-node,or

theyareconclusionsofresp.a
1
-nodeandofa

-node,or

theyareconclusionsofresp.a
!
-nodeandofa
?
-node.
Acut-linkisa
clash
,whenthepremisesofthecut-nodearenotdualedges
andnoneofthetwoistheconclusionofan
ax
-link.
Definition6(Cutelimination)
Thecuteliminationisdefinedasin[DR95].
Toeliminateacut
t
inanet
π
meansingeneraltotransform
π
intoanet
6
t
(
π
)
bysubstitutingaspecificsubgraph
β
of
π
withasubgraph
β

havingthe
samependingedges(i.e.edgeswithnotargetornosource)as
β
.Thesub-
graphs
β
and
β

dependonthecut
t
andaredescribedinFig.3.
Wewillalsoreferto
t
(
π
)
asaonestepreductof
π
,andtothetransformations
associatedwiththedifferenttypesofcut-linkasthe
reductionsteps
.Wewrite
π

π

,when
π

istheresultofonereductionstep.
A
head-cut
isacutofdepth
0
in
π
;a
stratifiedcut
t
isacutsuchthatforev-
erycut(includingclashes)
t

of
π
wehavedepth
(
t
)

depth
(
t

)
.A
head
(resp.
stratified
)
reductionstep
isastepreducingahead-cut(resp.stratifiedcut);
wewrite
π

h
π

(resp.
π

s
π

),when
π

istheresultofonehead(resp.
stratified)reductionstep.
Wedenoteby


(resp.

h

and

s

)thereflexiveandtransitiveclosureof

(resp.

h
and

s
).Anet
π
is
head-normalizable
(resp.
normalizable
)if
thereexistsahead-cutfree(resp.cutfree)net
π
0
suchthat
π


π
0
.
A
reductionsequence
R
from
π
to
π

isasequence(possiblyemptyincase
π
=
π

)ofreductionsteps
π

π
1

...

π
n
=
π

.Theinteger
n
isthe
length
ofthereductionsequence.Areductionsequence
R
isa
headreduction
(resp.a
stratifiedreduction
)wheneverystepof
R
isahead(resp.astratified)
reductionstep.
Noticethatcuteliminationcannotbeappliedtoclashes,andthismeansthat
therearenetstowhichnocuteliminationstepcanbeapplied,evenifthey
arenotcutfree(considerforexamplethenetsofFig.2).
Noticealsothatcuteliminationisdefinedonnetsandnotongeneral

-nets.
6
Thefactthat
t
(
π
)isindeedanetshouldbechecked,see[Reg92].

7

(
ax
):
ataxc
btucf

gh
`
i
(

/
`
):
acut
bt⊥1(
1
/

):
acutb
t

ββk1cck1v
1
♭♭
v
k
♭♭♭♭!!♭♭(!
/
?):
o
!!
π♭♭♭



!
otb
1
?
b
k
α
acutbw
♭!♭♭!♭?

c
fcutghi
tuc
emptygraph

βkβ1π
o
c
1
π
o
c
k

cut

cut
♭♭!! ♭♭!!′α♭!♭♭


!
♭?

Fig.3.Cuteliminationfornets.Inthe(!
/
?)casewhathappensisthatthe!-link
o
dispatches
k
copiesof
π
o
(
k

0beingthearityofthe?-node
w
premiseofthecut)
insidethe!-boxes(ifany)containingthe

-nodesassociatedwiththepremisesof
w
;
noticealsothatthereductionduplicates
k
timesthepremisesof?-nodeswhichare
associatedwiththeauxiliaryconclusionsof
o
.

Thisisbecausewewant

toleaveunchangedthenumberofconclusionsof
anet:thisistrueonlyforthelogicalconclusions,thestructuralonesmaybe
changedbythe(!
/
?)-steps.Inthesequel,however,weneedtospeakof
the
cuteliminationofabox
π
o
(whichisa

-net)associatedwitha!-link
o
:in
thatcasewemeanthecuteliminationofthenetobtainedbyaddingto
π
o
the
?-linksof
π
associatedwiththestructuralconclusionsof
π
o
.
Definition7(Ancestor,residue)
Let
π

π

.Whenanedge
d
(resp.a
−←−←node
l
)of
π

comesfroma(unique)edge
d
(resp.node
l
)of
π
,wesaythat
−←−←d
(resp.
l
)isthe
ancestor
of
d
(resp.
l
)in
π
andthat
d
(resp.
l
)isa
residue
−←−←of
d
(resp.
l
)in
π

.Ifthisisnotthecase,then
d
(resp.
l
)hasnoancestor
in
π
,andwesayitisa
created
edge(resp.node).Weindicate,foreverytype
ofcuteliminationstepofFig.3,whichedges(resp.links)arecreatedin
π

(meaningthattheotheredges/nodesof
π

areresiduesofsome
π
’sedge/node).

8

2
n
+1

2times
z
n
t
}
i
|
mes
{
⊥⊥

⊥⊥⊥
1

1
{|}zπ
=
1
♭♭
1
♭♭
1

h

π

=
cut

cut
1

s

π
′′
=
1
♭♭♭♭!

!

!!!
t
n
?
♭t
n

1
t
1
?

cutcutcut

Fig.5.Exampleofthe“cost”ofcutelimination(
n

1).

WeusethenotationsofFig.3:

(
ax
)
:therearenocreatededges,norcreatednodesin
π

.Remarkthat
a,b
areerasedin
π

,sothatweconsider
c
in
π

astheresidueof
c
in
π
;

(

/
`
)
:therearenocreatededges,whilethetwonewcut-linksbetweenthe
twoleft(resp.right)premisesofthe
`
-and

-linksarecreatednodes;

(1
/

)
:therearenocreatededges,norcreatednodesin
π

;

(!
/
?)
:everyauxiliaryconclusionaddedtothe
!
-linkscontainingonecopyof
π
o
isacreatededge;everycutlinkbetween(acopyof)
π
o
’smainconclusion
and
c
i
isacreatednode.
7
Examples.
Itiswell-knownthattherearenon-
ax
normalizable
untyped
nets.Afamousexampleis
♭♭ax
thenetcorrespondingtotheuntyped
λ
-term
!

(
λx.xx
)(
λx.xx
)(see[Dan90],[Reg92]).Wegivein
♭♭♭
!
Fig.4aslightvariant(whichisnota
λ
-term),due

?
♭♭
toMitsuOkada.Thereadercancheckthatthisnet
!
cut♭
?
reducestoitselfbyone(!
/
?)stepandone(
ax
)step.
Fig.4.Exampleofa
Letusbrieflydiscusswithanexamplethereasonwe
non-normalizablenet.
choosethesyntaxof[Reg92,DR95],allowing?-links
ofarity
k

0.Considerthenet
π
inFig.5:different
headreductionsstartfrom
π
,dependingonwhich
cut
t
i
(for
i

n
)wechoosetoreduce.Buteverysuchreductioneventually
reachesthehead-cutfreenet
π

.Besides,allheadreductionsendingin
π

havethesamelength:theyconsistof
n
steps,oftype(!
/
?).Indeeditisa
generalpropertythattwohead(resp.stratified)reductionsofanetleading
toahead-cut(resp.cut)freenetalwayshavethesamelength,asprovenin
Corollary29.
Thispropertyisspecificofthesyntaxwehavechosen,whichgathersina
uniquestep(!
/
?)alltheexponentialstepsof
MELL
(see[DR95]).Inthe
7
Noticethatevery!-linkof
π

whichcontainsacopyof
π
o
isconsideredaresidue
ofthecorresponding!-linkof
π
,eventhoughithasdifferentauxiliaryconclusions.
Noticealsothattheedges/nodesineachcopyof
π
o
areconsideredresiduesofthe
correspondingedges/nodesin
π
o
.

9

originalsyntaxof[Gir87],the(!
/
?)stepsplitsin(!
/
?
d
),(!
/
?
w
),(!
/
?
c
)and
(!
/
!).Fromthepointofviewofthelengthofcutelimination,thischoicehas
someconsequences.Recallthe(!
/
?)stepasdepictedinFig.3,assumethatthe
cut-link
t
hasdepth0,andset
d
1
,...,d
k
asthedepthsofthe

-nodesassoci-
atedwiththe
k

0premisesofthe?-node
w
:thesingle(!
/
?)stepissimulated
inthesyntaxof[Gir87]byone(!
/
?
w
)stepif
k
=0,elseby
k

1stepsof
type(!
/
?
c
),
ik
=1
d
i
stepsoftype(!
/
!)and
k
stepsoftype(!
/
?
d
).Inparticular
Pthelengthofthissimulationisnotconstantbutitdependsonthearity
k
of
w
andonthedepthsofthe

-nodesabove
w
.Furthermore,thesefactorsmay
beaffectedbyother(!
/
?)reductionsteps,andthisyieldssimulations(bynets
of[Gir87])withdifferentlengthsofasamereductionsequence.Forexample,
thenet
π
ofFig.5canberewrittenintothehead-cutfree
π

(inthesense
ofourDefinition6)byreductionsof[Gir87]ofdifferentlengths.Oneofthe
shortestreductionisobtainedbyreducingthecuts
t
1
,...,t
n
inadecreasing
order(w.r.t.theindex):reduce
t
n
,thetwocreated(!
/
!)cutsandthenthetwo
created(!
/
?
d
)cuts,afterreduce
t
n

1
andthe(!
/
!),(!
/
?
d
)createdcuts,then
t
n

2
andsoforth.Thisreductionleadsto
π

after5
n
steps:
n
oftype(!
/
?
c
),2
n
oftype(!
/
!),and2
n
oftype(!
/
?
d
).Ontheotherhand,byreducing
t
1
,...,t
n
inanincreasingorder,onegetsoneofthelongestheadreductions:reduce
t
1
,
thetwocreated(!
/
!)cutsandthetwocreated(!
/
?
d
)cuts,afterfocuson
t
2
andnoticethatthereductionof
t
1
hascreatedtwonew?
c
nodesabove
t
2
andduplicatedtwo?
d
nodes,sothattosimulatethe(!
/
?)reductionof
t
2
we
needtoperform3(!
/
?
c
)steps,4(!
/
!)stepsand4(!
/
?
d
)steps,thenfor
t
3
we
need7(!
/
?
c
)steps,8(!
/
!)steps,andthesamenumberof(!
/
?
d
)steps,and
in
=1
((2
i

1)+2
×
2
i
)=3
×
2
n
+1

n

6,whichmaybemuchmorethanthe
s
P
oforth.Eventually,itturnsoutthatthelengthofthisreductionsequenceis
lengthofourreduction
π

h

π

.
ThisexamplealsoshowsthatitisnotobvioushowmanystepsofaTuring
machineareneededtoimplementourreduction.Wethinkapreciseanswer
tothisquestionshouldgeneralizeintheframeworkofnetsthecostmodel
developedbyDalLagoandMartiniforthecall-by-value
λ
-calculus[LM06].

Atlast,remarkthatevenifthelengthofhead-normalizationinoursyntax
maydifferconsiderablyfromthelengthofitssimulationinthesyntaxof
[Gir87],thesituationmightverywellbedifferentforstratifiednormalization.
IndeedintheexampleofFig.5,inordertoreachthecutfreenet
π
′′
fromthe
head-cutfreenet
π

oneneeds2
n
+1

2morestratifiedsteps(oftype(1
/

)),
sothatthetotallengthofthenormalization
8
π

s

π
′′
is
n
+2
n
+1

2,and,
asthereadercancheck,thetotallengthofitssimulationin[Gir87]mayvary
between5
n
+2
n
+1

2and4
×
2
n
+1

n

8:allthesefunctionsbelongtothe
samecomplexityclass(
EXP
).

8
Allstratifiedreductionsequencesleadingtoacutfreenormalformhavethesame
length(seeCorollary29).

01