Di erential Linear Logic and Polarization

Lionel Vaux

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

Sujets

• Linear logic
• Polarization (waves)

Informations

• Publié par: mijec
• Nombre de lectures: 13
• Langue: English

Extrait

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:.loThi