Di erential Linear Logic and Polarization

-

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

Description

Niveau: Supérieur, Doctorat, Bac+8
Di?erential Linear Logic and Polarization Lionel Vaux ? Laboratoire de Mathématiques de l'Université de Savoie, UMR 5127 CNRS 73376 Le Bourget-du-Lac Cedex, France Last modified: 2009-05-06 Abstract We extend EhrhardRegnier's di?erential linear logic along the lines of Laurent's polarization. We provide a denotational semantics of this new system in the well-known relational model of linear logic, extending canonically the semantics of both di?erential and polarized linear logics: this justifies our choice of cut elimination rules. Then we show this polarized di?erential linear logic refines the recently introduced convolution ?¯µ-calculus, the same as linear logic decomposes ?-calculus. 1 Introduction Di?erential Linear Logic. Di?erential interaction nets (DIN) were introduced by Ehrhard and Regnier in [1] to provide a notion of proof nets for the finitary fragment of their di?er- ential ?-calculus [2]. Both DIN and di?erential ?-calculus originate in the study of models of linear logic designed after Girard's quantitative semantics of ?-calculus [3], such as Ehrhard's finiteness spaces [4]. The distinctive attribute of these models is that intuitionistic proofs, hence typed ?-terms, are interpreted by power series in particular vector spaces; thus it makes sense to define di?erentiation on these.

  • linear logic

  • polarized di?erential

  • convolution ?¯µ-calculus

  • polarized

  • structural rules

  • compatibility between both

  • into linear


Subjects

Informations

Published by
Reads 13
Language English
Report a problem







D( xs )t
s s@ @ x t t t
@x @x
x s
s
0 0 0(fg) =f g +fg
: !A
!A( !A :1( !A

vacandenotationalnsemanaticsthoughofotknohisrules,nonce.ewisystisemccurrenceinthethemowwnell-knobwnisrelationalofmotdelolarization.ofolinearforlogic,lexttheendingccurrencescanonicallywhictheeseman73376ticsducedofrubtoothwithdierenoratoiretitsialtheandfunctionpitsolarizedthelinearanlogics:reducesthistjustilinesbourtlycinhoiceofusedcutofeliminationyrules.henceThenlwtoetshoduct:wFrancethisoie,pcanolarizeditdierentro-ttoialdereliclinearreelogiconrenesolutionthel'UnivrecenutlwhenytinsametroativducedsmoconbvofolutioneLionelapproolarizationa-calculus,etheesamet'sasanlinearlineslogicalondlecodierenmpaosessubstitutingPx-calculus.l1ofIn,trooductionanDierenhtialonceLineardLogic..Dierenetialhinateractionactuallynetsof(DIN)hwiserewinruletroderivducedab2009-05-06ysavoie.frEhrhardBourget-du-Lacand5127RSucetialgniereinlinear[1]oilstotheproofvidees,alogicnotionaofrule,proCostructuralofannetscforonentheconnitaryductfragmendetMath?matiquesofitstheirVdier-linearenusestialargumenandexactly-calculusThe[2].asBothderivDINeandadierenothtialcanLogice-calculustoriginateasinbthesstudylinearofximation,moderivdelstofvlinearoflabstractionogicWdesignedpafterLaurenGirard'stoquanabstractiotitativofehesemangticsgicofwhereLinearear-calculustial[EhrhardRegnier's3],obtsucinedhyasdEhrhard'senitenessacspaconeesinear[4].ccurrenceTheextendeiwherestineariccurrencenctivmeanseoattributewhicofistheseexactlymoindelsheaisreductionthatWinTheretuitionisticbpromanofs,suchenceotinypterm,edonetialconsiders-terms,sumarealinsucterpretedterms,bhysimilarptheoellwwnerforseriesheinativparticularofvproectorAbstractspaces;died:thLastuslionel.vaux@univ-itCedex,makLeesCNRSsUMRe.nshedierentoextensiondenebdierenreprotiationinonlogic:these.bThedodierentotialinDierenduction.costructuralblsdualprolinearestructuraltandoncovidtionorteddualydereliction.rencrulesANRctjectalge1raiondencestructurewithexpthetials,lainearvlogicproapproacmhSatoersit?resourcedesdeofandcomputation:unitaLabfunctionalauxprogramsdierenThe-calculusaemibofotiadiesithisinnotionSuppofbdierenFtiation,hipronCHoCoclosecorrespf : !A(B @ :A( !A
f@ : A( B f 0
?




coherencesucyhLLPthatlarthenofseries:itseriswview,ompyparetialsisativthe[linearconstructionspartbofpmorphisms[8]:,yi.e.Costructuraliotsyderivbativ[13]:eofatanpandoinmtythatto;romtogetherthewithFtheandconpvariablesolutionwproaduct,stahiofsofdeallynatesethestttialheandderivofativanderaction.atdananyalculiptrolledoinstructuralt.toTheofcutproeliminatiRegnieronppropcedureexpthenisreectscorrelationvwithalidsemanequationsofinisthesubformmotials).del.RegnierTheconstructionsystemcofLLPDINDiLLpresenexptedrules,inof[1a]Onisthenottoexactlyi.e.anstructureextensionformoftheliofnearardlogic:lineartheppro-tromotionhrulebisandmissing.terms:Itsystemiseenhoinwcaleviserconsiderpofossiblectocutreineredtroprogramsduceoutputs,it,ytogetherpwithTheseappropriateositionscut,eliminationtherules-calculusderivloednetsfromDanosthe10].semansemanticstiideancanonicallynitenessturesptialsaformces:vthisinstancedenes[7]dierenequiptial-monoidnetsvide(DN),ofwhicinhrulesdepartformfromfrtheonin(basicallyteractionexpnetorkparadigmt(see,latere.g.that[5]).theOneLafoncan[12]naturallydelinPtroInducetroasymmetrysequentialtwithcalculusproassotialciatedofswithgDN,putationalwhereativcutotherelimiendecompatuitionistictlogic,istructuralonyistendingguidedexpbpyThisthestudyreductionenofbnets:extensionscallryHodierenondencetialblinearAlogicw(DiLL)videdthisauthorsystem.aP-calculusolarization.aTheextensionnotionnoftialpnormolaritiesypindenabilitlinearhlogicawetasothmadeesprominenolvtnewbtyalthoughAndreoli'donesonewsystemorktheonoffo,cusingkprokindofsthis[6]coandyGirard'sofdeterministicwithsultipleystemconforbclassicaltermlogicreecting[7].olarizedTherules.latterenjoldecompedintoLLPthesimidenitiontooftranslationpcoolarizedinllinearineargiclogicof(LLP)studiedbyyandLauren[9,tF[8]:aiticalnointheofptheolarizedthatfragmenolarizationtextendsofstruc-linearoflogic,onenthetostructuralolarizedrulesulascanalsobalid.eorextendedGirard'stospacesallarenegativspaceseedformaulasstructureratherprothanaistics-formLLPulastheonlyterpretation.costructuralItonisolarizedwulasellbuiltknoownthatthattheirtheulastransitionvfromandanoneninWtuitionisticbsystemLaurentoanda[11]classicalshooneedcanthisbgeneralizes:e-monoidspaerformedtbategoryyformallomowingofdeductions.witholarizedmRules.ultiplshort,einconclusionduceformaulas.onSinceonennegativtees,formcostructuralulasandarevidesthedierentargetanalysislanguageproofthrGirard'sutranslationhofcom-implicativnotionederivformes.ulastheinhand,toextlinearndslolineargic,ositionwinelogicunderstandclassicalthatbLLPrelaxingcorresprules,ondsbtocanonicsucex-htheaofrelaxation.onenThetocomputationalolarizedcoulas.umotivntheterpartofofrelationscltertainedassyiothcaltheselogicofisCurwwecorrespllandestablished:analysiscylassicallogic.truthsrstresultyasproeinconthetrolinopduceserators.dierenItderelictioiswhicmoreoisvconserverepofossibleothto-calculusisdieren-calculus,yingextendenjotheconuenceCurryHostrongwalizationardtcorrespedondencethetoyasucclassicalalogicwitnessessetting,compatibilitwhilebretainingwthebinextensions,tuitiondoofnotprovofsewithymlogiultipleinconclusions.eFIndeed,orthisinstance,notPinarigot's13],delscan-calculustheandobtaineHerbaseliunionn'srulesmoDiLLtheseLLP-calculusthencanhecbthateycoofninsisystemdalreadyevredbas2c




x hx; (x)i
2
a()2 N
moofofthatare-calculusareinhoLLPthi.thenInandtheexplicitsprheolsenbtterpretpapperduwyeothratherinintialvMazzaestigatediertheexampleedectols,ofDiLLptheolarizaofttoier.ondierenonwDN:awlyereviewsconsidedierenrproptheinsystemareobtainedteractionb[17]yplusrelahxhing1,notvonlytranslationstructuralerulesortosimplenegativonetialform[14]ulasthebuterationalsotructuralcostructuralconrulesOrganizationtowpsystemositivtogethereiformthisulas.denotationalAgaintthelinearideasemanis.thPDN.athetPDN,pofolarizationkshoulddierenalso2extenddierentheofalgebraicmstructureasoflloexpellsonenDN,tialsxes.toconsideringplaxedolarizedandformesulas.givIntparticulatranslationr-calculus,-thisthepreservWeofssymtheensymmetrycutbvet-calculuswideas:eenelin'sstructuralinandjectcLLPostvructuralcounrulesmonoidindeltrocoducedwhenindenotationsDiLL.whicTheretoarethetsectionwinoemainpguidingnetslinestwhenrules.designingsectioncutveliminationsysteminvidingtticshiobsthesystem:osymmetryThisandthesemanoftics.andW4etializationconsidersectionatranslationmovdel-calculusofhinlineThearpaplogicawhiclimpsehtocanbacbthateolarizedextendedPtonetsbniteothnets,DiLLparticandortLLP:sucbbothfcorrelationLafonspaceThessimpleathosend.nibt,eDNnessyping,srpacyesiareelimination,renemenvtsrules.ofPDNtheinrelaationalp-moisdelcwhicthathosunderliesextendingGirard'sdierencoherenceofsthisew).mancalltics.setMoreym:eacinoltheisrariteinationlational.inonterpretationolutionofinlinearbasedlogicsimilarproinofs,Herbdual-calculusit-calculusytoboboilsofdothroughwn,toinreestigatevcomputationalersingterpartthetheorienoptationmooflingrelatioolarizednss.rules,Thisappliedallothewsoftotexts,deduce,hindualaterms.vofepapryInnatural2,weatroyc,thetheofsemanolarizedticstialof(PDN),pwitholarizedypingcreductionostThen,rucnt3,uralerulesalidatefromnewthatbofpropaolarizedsemanstructuralonrules:particularjustjecrevoferserelationalthedelcorrespfondinglogic.relations.canonicalTheextendsreexivrelationaleticsobbjectDNinLLPtroSectionducedbrieyinsequen[14]ofisLast,w5ellthesuitedofforconthisolutionstofudy:initasallotedws[15].toendintheterpreterbosesothquicDiLLgandatLLPwinbringatiationpurek(i.e.tounsetting.tPyDierenpNetsed)olarizedsetting,tialso(PDN)thatformalexpsumsonensimpletialwhicstructuralareandularcostructuralultipruleinsnets,arehexcstudiedhangedyb[16]yosymmetrywing,tand.pcolarizedofstructuralPDNrulesactuallyareofgivi.eenDINbpromotionyoaMainly-monoidPDNstructurefromonwhenthetobwhicject.isIteisbthenpeasyartozation,derivcutewhictheincomputationalolvbnewehaAnvsimpleiisourenofFigurepwitholarizedpurecostructuralyrulesing:frsothemofthisonsemanolutiontics.naturallyTheclsystemepresentermtedcalculusintialtheofcurrenattargetpapiser(seecanelobNets.eeseensignaturasaandLP:isscircuitbupwhereahnbbLofDiLLelgiv,an[15]y,rulestheelimauthortheinAtronetducedsignaturecontheaendbuiltresultfromofnitethisumcourseerofcthoughlst.3Ino o
!o o
o
⊗ o
`!!o oo!o !o
!o
c
a( ) + 1 cc c
c
0 a( ) 0cc ;:::;c c
c
[ ;:::; ]1 n

0 0 +
0
"
!
!
S
! ! (n) =
(0) (n) (n+1) (n) ! ! (n) = = [f ; g
00

@
! = 0
M;N ::= XjM Nj ?P
?P;Q ::= X jP
Qj !N
?? ? ? ?X = X (M N) = N
M
? ?(?P ) = !P

A)B = !A(B
? ?A;B ::= Xj ?A B ?A
? ? ? ?A ;B ::= X jA
!B !A
ositivprincipPDNalFigurepuortimplicativofequal).isc;onenthethepones,ossibleaothersymonesolsareocalle.deauxiliarynegationp,orts.wirInwhgeneral,ort,cellsortareydepictedDenitionbdRyontrtriangles,narywithsymbtheirlrespofectivyeledprincipalandpeortandputulasontthearetiphohfoptheithertriangle,symandpthebauxiliarysinceonesnotonetishe[1]:oppposcionteelictionedge.;TheandinterfacsignaturewofpalsimplearenetmislotheofsetwireofwiresiDet,stofreeeryptheortdecomps.(i.A-calculus)netyt,andisws:aimgivultisetofpresendysaacellalwisisoholwhicnet,eacortNoticePxesorts.tainofosimpleolsnetssimplesharingThetheortssamedepthinofterface,gnier'swhicyhwhosew,etioalsocconsideractto;bolseandtheelictioninnulterfaceakeningofowepThen.ofIfisitsisandyping.forformwriteultiareenetslinearwithenthefollosameyinnegativterface,ortswareeThedenote.additivloedanglinglyallotheirbmdualitultiset.unionbewherewnecell,isathat.RecallWlogiceinalsoofdenotenaturalbsimplyedisGirard'sthemanemptctedyinmonenultisetasofe:simple,nets,bwhatevaerositivthenetunderlyingAninmterfaceof-course:.loThisorshouldpnotabeeisconfusedbwithxthebewithmptayonsimplehnetHenceIf.,thattheoinmaterfaceconofsums,whicbhxisbemptareynecessarily.nets.W2.1esignaturwillareconsiderofcellsofofpathatspEhrhareciealDINkind:binarasymbbtensoro,xaricsacancellandwithosymontrbiolmhangeable.utercsymb,derwheredincisderarenetandnotlarytheolsweterfacewmatcchesakeningthe.ptheortseofalthePDNbioax-celopl.TAThebolarizedoulasxmareportsicativisexpdepictedtialaslogicagivrecbttheawingnutuallginductivlegrammars:con-e:taining(app,calwherewireswendsepdistinguishe:thesprincipaloppalsoortends,bwithywawithcircleddenedexclyamationMorganmark.y:LetWcellofbolesymaissignature.wires,Wctedendenecothecellsignatureevmatters:sots.bthatylinearinducformtuseditheonositiononminimaltheedepthdeductionofe.byoypxes:esointhroughptranslationconnexionyofnitelytbplacemenconneThethewire).tuitionistic,expwheretialdanglingorganizedafollo(ofnegativortare,whicandniolfsympy-not:eenepfre:iseacdened,simplewexamplee1:setcacordort,pwhose4inP Q M N P N N N P P
⊗ ` ∂
P⊗Q M`N ?P !N N N P P

o
o = o ) o
? ?o = !o(o = ?o o o i =o
!o ?i
o i !o ?i
0
I = p ;:::;p1 k
= ;:::;1 k
‘ p I i iPm
= jj=1
I ‘ j ‘I j I
!I =f0;:::;ng = N;N ;:::;N ‘ b 1 n I
b‘ 0 n !N;N ;:::;Nb ;:::;b 1 n
c d

i j i ji c j d c ;d c ;d


i jc ;d
i jc d
i jc d c d


i j0 c ;d
P Pn ni j 0 c ;d ! k 0k=1 k=1 k
0 i j c ;d c dk
0 ! k 0P Pn n0 0 0 = = ! i2f1;:::;ngi i 0 0i=0 i=0 i 0
0 0 ! =i 0 ii i
! n
0 0 0 0 0! ! ! n+1 0 n
e,2,denotewherseesotypresThenargiewirpinolarizetod,fo,rmulas.orIfolspurefallreayprtandtoswsvalloWh,ewhicfor,ols.isctingandeporthederferedex,d.interfaceversingedexofassignmentsimpletnetasequationit,e,i.e.negativa.listisof(theitsorfranyeieitselfpandorts,lsandaifredextheonstrtoypablejectndsubreduced,onttypconstangatesadditionalfreeanarefromortisortsaflisteofdepthtypnet,es,isthenewerwritesimplenedthenaione.bteifnettherconsideredecisof-course,aThistypinglows:ofonotranslatessuchethatetheInoutgoingfortypts)eoattprortrulasaformofisetialsuchonenof.ofWhecextendtypingtypinWghtoyalonl.PDN,hbytypingtheespfolFigurelowingesruleswhicfonlorsymsumse,and,bortoxes:neihatfortsexpreducedandtotuitionisticeinoffreetheariableevusareois2.3adennetductionwith.oraderthateddrinterfacacheeTheyis,ductthenislogic.oflineareinwriteas2.2sohetonwheras,aforthealdlwir-calculusb,formpurelsterpretfrinthentoinste;extendeifasmor(resp.easoveronlorder)nandiW[10]tirwherRegniepureandimple[9]s)Danosofyypbf,ofducedttrotexts),ineeredual,wnowesductionpAssumeydenetpPurenet,ulas.givenformeandifolarizedepbleofm,fthenPDNforsimpleaofbsucoxthatcaseselofthesymbrulesolisecialwire.spe,sucweahavbeThearesymbTheseaintsPDNcsimpleFofeacellstcredexthesomeofeypingrT,2:3Figurevuamnetwhcendsdy5theisbtheaprandomotiontheruleandofpLLP).indicesNoticeandthe,fourtptheolarizedptoypingtherulesnetforassignedstructuraltheandrecostructuralpcells.sFtheromi.e.thisppofolarizedandtminyping,theoneandstraighorientationtforwDenitionardlyWdeducesrstaneinetuitionisticat(resp.thepure)IftisypsimpleersystsuchewirmorienteforaPDN.eCutofelimination.andAmongtothetyppofortstheofeeacofhthecell,PDNsomeaaregivencalledFiguractive3,:wetypingheAsDenitioneypalcorrespcond,toeactiachvtheeisformsimpleulasobtaineinbytheemovingeeareobtainecantula:iandonelrule.y-not)Thewhonlyomactiv,epluggingpositivortad.ofisadnon-bsumsofolxpcelleisythesoprincipalasone;thebiyThiscon,trast,toall,the(resp.png,ortstof,aebachoaxsare,activ.e.ariableAfreecutand,ineatnetobtainisandaargumenwireebypet(thewueenconactivofeypptheorts.ofedistinctdenecells:eaatrdepth.e(itsdexisisd.theifdataisofsimpletosswinoterms),cifFiguryptells(the-terms.or,therdeptharandnetsindicesandofulas:activthaterpoortsandofassoisciatedddeduc(this! 0! !n+1
0 0! ! ! n0 n
m e m
r d
m e p
p
e2;3;4
0p
0m r p p p3
d1
d m1
@
!
X M (X) X
(!)
M (X) = ((i)) M (X) (i) = []i2!
i2 ! (D ) nn n2N
S(!)
D =; D =M (D ) D = D0 n+1 n nn2N
a2M (D) 2D a :: (0) = a
(i + 1) = (i) i2 ! (i) = []
i2 ! D =fg (a;)7! a ::1
M (D)D D = [] :: D
!

D
D i2! (?)(i) =(i) +