Transcription
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsTutorial on the differential extensions oflambda-calculus and linear logicPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesFebruary 16 2009
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionOutlineBack to the originsQuantitative semanticsPower seriesFrom Böhm trees to Taylor expansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesThe syntaxThe ConstructsThe ReductionsPropertiesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: the Issues
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionOutlineBack to the originsQuantitative semanticsPower seriesFrom Böhm trees to Taylor expansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesThe syntaxThe ConstructsThe ReductionsPropertiesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: the Issues
Tutorial ondifferentialextensionsBack to theoriginsAt the beginning there was. . .Girard’s quantitative semanticsQuantitativesemanticsAnalysisPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiescontinuousfunctions GGF(xn ) F (xn )n 0Computer Science λ-calculusβ-reductionProof theoryNJ of cut-eliminationn 0The Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesJean-Yves Girard.Normal functors, power series and λ-calculus.Annals of Pure and Applied Logic, Elsevier, 1988.
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionAt the beginning there was. . .Girard’s quantitative semanticsAnalysispowerseries Xan F nComputer Science λ-calculusProof Theory β-reductionLL of ! cut-eliminationn 0linear functions:F(U V) F(U) F(V)F(aU) aF(U) linear β-reduction:using inputsexactly once ConcurrencyTranslationBisimulation: theIssuesJean-Yves Girard.Linear Logic.Theoretical Computer Science, Elsevier, 1987.substructuralproofs: , &, ,
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionAt the beginning there was. . .Girard’s quantitative semanticsAnalysispowerseries Xan F nComputer Science λ-calculusProof Theory β-reductionLL of ! cut-eliminationn 0linear functions:F(U V) F(U) F(V)F(aU) aF(U) linear β-reduction:using inputsexactly once substructuralproofs: , &, , ConcurrencyTranslationBisimulation: theIssues. . . though in linear logic the link with analysis is not convincing. . .differential linear logic wants to make this correspondence explicitJean-Yves Girard.Linear Logic.Theoretical Computer Science, Elsevier, 1987.
Tutorial ondifferentialextensionsWhy power series? (1)What is the result of the application ML? Let us ask it to Böhm!Back to theoriginsQuantitativesemantics compute finite approximations BT0 (ML) BT1 (ML) . . . the result is the limit of these approximations:Power seriesFrom Böhm treesto TaylorexpansionThe syntaxBT(ML) The ConstructsThe Reductions GBTd (ML)d 0PropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssues d expresses how "deep" BTd (ML) is definedthe order between BTd ’s is a definedness order
Tutorial ondifferentialextensionsWhy power series? (1)What is the result of the application ML? Let us ask it to Böhm!Back to theoriginsQuantitativesemantics compute finite approximations BT0 (ML) BT1 (ML) . . . the result is the limit of these approximations:Power seriesFrom Böhm treesto TaylorexpansionThe syntaxBT(ML) The ConstructsThe Reductions GBTd (ML)d 0PropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionExample (Y λf .(λx.f (xx))(λx.f (xx)))ConcurrencyBT0 (Yf ) BT1 (Yf ) f TranslationBisimulation: theIssuesBT2 (Yf ) f (f ) BT3 (Yf ) f (f (f )).BT(Yf ) f (f (f . . . ))d expresses how "deep" BTd (ML) is definedthe order between BTd ’s is a definedness order
Tutorial ondifferentialextensionsWhy power series? (1)What is the result of the application ML? Let us ask it to Böhm!Back to theoriginsQuantitativesemantics compute finite approximations BT0 (ML) BT1 (ML) . . . the result is the limit of these approximations:Power seriesFrom Böhm treesto TaylorexpansionThe syntaxBT(ML) The ConstructsThe Reductions GBTd (ML)d 0PropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionExample (Y λf .(λx.f (xx))(λx.f (xx)))ConcurrencyBT0 (Yf ) BT1 (Yf ) f TranslationBisimulation: theIssuesBT2 (Yf ) f (f ) BT3 (Yf ) f (f (f )).BT(Yf ) f (f (f . . . ))d expresses how "deep" BTd (ML) is definedthe order between BTd ’s is a definedness order
Tutorial ondifferentialextensionsWhy power series? (2)Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThis approach yields wonderful accounts of qualitative propertiesof programs:The syntaxThe ConstructsThe ReductionsPropertiesTheorem (solvability)M solvable iff BT(M) 6 The Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationTheorem (normalizability)M normalizable iff BT(M) finite and without Bisimulation: theIssuesExampleBT( ) BT(Yf ) f (BT(Yf ))BT(2 2) 4
Tutorial ondifferentialextensionsWhy power series? (2)Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThis approach yields wonderful accounts of qualitative propertiesof programs:The syntaxThe ConstructsThe ReductionsPropertiesTheorem (solvability)M solvable iff BT(M) 6 The Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationTheorem (normalizability)M normalizable iff BT(M) finite and without Bisimulation: theIssuesExampleBT( ) BT(Yf ) f (BT(Yf ))BT(2 2) 4
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is used
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is used
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is used
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is used
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is used
Tutorial ondifferentialextensionsFrom Böhm trees to Taylor expansionBack to theoriginsQuantitativesemanticsScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe SemanticsBT(ML) (Non) determinismFiniteness spaces Gd 0Taylor ExpansionBTd (ML)τ (ML) X 1hτ (M)i τ (L)nn!ConcurrencyTranslationBisimulation: theIssues. . . but be careful! d and n have a very different nature: d is qualitative — how deep normalization is gone?n is quantitative — how many calls normalization has done?
Tutorial ondifferentialextensionsFrom Böhm trees to Taylor expansionBack to theoriginsQuantitativesemanticsScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe SemanticsBT(ML) (Non) determinismFiniteness spaces Gd 0Taylor ExpansionBTd (ML)τ (ML) X 1hτ (M)i τ (L)nn!ConcurrencyTranslationBisimulation: theIssues. . . but be careful! d and n have a very different nature: d is qualitative — how deep normalization is gone?n is quantitative — how many calls normalization has done?
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFrom Böhm trees to Taylor expansionScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionBT(ML) GBTd (ML)d 0ConcurrencyTranslationBisimulation: theIssuesBT0 (2) BT1 (2) λfx .f BT2 (2) λfx .f (f )BT3 (2) λfx .f (fx )τ (ML) X 1hτ (M)i τ (L)nn!
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFrom Böhm trees to Taylor expansionScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionBT(ML) GBTd (ML)d 0ConcurrencyTranslationBisimulation: theIssuesBT0 (2) BT1 (2) λfx .f BT2 (2) λfx .f (f )BT3 (2) λfx .f (fx )τ 0 (2) 0τ (ML) X 1hτ (M)i τ (L)nn!
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFrom Böhm trees to Taylor expansionScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionBT(ML) GBTd (ML)τ (ML) d 0ConcurrencyTranslationBisimulation: theIssuesBT0 (2) BT1 (2) λfx .f BT2 (2) λfx .f (f )BT3 (2) λfx .f (fx )τ 0 (2) 0τ 1 (2) λfx .hf i1X 1hτ (M)i τ (L)nn!
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFrom Böhm trees to Taylor expansionScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionBT(ML) GBTd (ML)d 0τ (ML) X 1hτ (M)i τ (L)nn!ConcurrencyTranslationBisimulation: theIssuesBT0 (2) BT1 (2) λfx .f BT2 (2) λfx .f (f )BT3 (2) λfx .f (fx )τ 0 (2) 0τ 1 (2) λfx .hf i1X 1λfx .hf i(hf i1)nτ 2 (2) n!n
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFrom Böhm trees to Taylor expansionScott cpo(D, )vector spacesRhX ifinite Böhm treeλx .x (f )term with resourcesλx .hx i(hf i1)3Power seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionBT(ML) GBTd (ML)τ (ML) d 0X 1hτ (M)i τ (L)nn!ConcurrencyTranslationBisimulation: theIssuesBT0 (2) BT1 (2) λfx .f BT2 (2) λfx .f (f )BT3 (2) λfx .f (fx )τ 0 (2) 0τ 1 (2) λfx .hf i1X 1λfx .hf i(hf i1)nτ 2 (2) n!nX λfx .hf i(hf ix m1 · · · hf ix mn )τ 3 (2) n!m1 ! . . . mn !m ,.,m1n
Tutorial ondifferentialextensionsWhy power series? (3). . . but what about quantitative properties?Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe Constructs how many times L is called for computing BTd (ML)? how many steps do we need to compute BTd (ML)?Scott’s order does not answer these questions. One needs The ReductionsProperties The Semanticscoefficients able to count the calls to Lan addition able to sum different calls(Non) determinismFiniteness spacesTaylor Expansionpower series is a way to have a semantical accountof quantitative properties of programsConcurrencyTranslationBisimulation: theIssuesML X1hMi(L)nn!n 0hMi(L)n is a term with resources: n meaning how many times L is useda complete example
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionAt the beginning there was. . .Girard’s quantitative semanticsAnalysispowerseries Xan F nComputer Science λ-calculusProof Theory β-reductionLL of ! cut-eliminationn 0linear functions:F(U V) F(U) F(V)F(aU) aF(U) linear β-reduction:using inputsexactly once substructuralproofs: , &, , ConcurrencyTranslationBisimulation: theIssues. . . though in linear logic the link with analysis is not convincing. . .differential linear logic wants to make this correspondence explicitJean-Yves Girard.Linear Logic.Theoretical Computer Science, Elsevier, 1987.
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionOutlineBack to the originsQuantitative semanticsPower seriesFrom Böhm trees to Taylor expansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesThe syntaxThe ConstructsThe ReductionsPropertiesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: the Issues
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionOutlineBack to the originsQuantitative semanticsPower seriesFrom Böhm trees to Taylor expansionThe syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesThe syntaxThe ConstructsThe ReductionsPropertiesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesThe Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: the Issues
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFamily picture / The netsABA B 1 Power seriesFrom Böhm treesto TaylorexpansionA BA BTensorPar1 OneBottomThe syntaxThe ConstructsπThe ReductionsPropertiesThe Semantics(Non) determinism?Finiteness spacesA?A?A?ATaylor mulation: !A!!AWeakening?B1 ?Bk?B1 ?Bk!AExponential πiiSumAk
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFamily picture / The netsABA B 1 Power seriesFrom Böhm treesto TaylorexpansionA BA BTensorPar1 OneBottomThe syntaxThe ConstructsπThe ReductionsPropertiesThe Semantics(Non) determinism?Finiteness spacesA?A?A?ATaylor mulation: !A!!AWeakening?B1 ?Bk?B1 ?Bk!AExponential πiiSumAk
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsFamily picture / The netsABA B 1 Power seriesFrom Böhm treesto TaylorexpansionA BA BTensorPar1 OneBottomThe syntaxThe ConstructsπThe ReductionsPropertiesThe Semantics(Non) determinism?Finiteness spacesA?A?A?ATaylor mulation: !A!!AWeakening?B1 ?Bk?B1 ?Bk!AExponential πiiSumAk
Tutorial ondifferentialextensionsFamily picture / The calculusBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntax The ConstructsThe Reductions:: termsProperties Vvariablesh i ! λV. abstractionapplicationThe Semantics(Non) determinismN h iFiniteness spacesTaylor Expansion:: polytermsConcurrency0 zero sumTranslationBisimulation: theIssues !bags:: 1empty ! !union linear arg. exp(N h i)exponential arg.
Tutorial ondifferentialextensionsFamily picture / The calculusBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntax The ConstructsThe Reductions:: termsProperties Vvariablesh i ! λV. abstractionapplicationThe Semantics(Non) determinismN h iFiniteness spacesTaylor Expansion:: polytermsConcurrency0 zero sumTranslationBisimulation: theIssues !bags:: 1empty ! !union linear arg. exp(N h i)exponential arg.
Tutorial ondifferentialextensionsDeveloping the trinityBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe syntaxLet us develop the idea at the level of syntaxThe ConstructsThe ReductionsPropertiesThe Semanticsf :A Blinear functionsAg:A Banalytic functions!AfB(Non) determinismFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssueshgiB
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe usual suspects / Contraction andweakeningContractionweakeningsharing of a variabledeclaration of constant functions.The syntaxf (x1 , x2 )The Constructsf (x , x )The ReductionsProperties!AThe Semantics(Non) determinismFiniteness spacesTaylor Expansion!Ax1x2Concurrencyhf iB!Af (y )Translationyhf iBBhf ig(x , y ) : f (y )Bisimulation: theIssues!C?xxy!A?hf iB!CIn programs: duplication (joining queries) and erasing (dummyvariables, empty query).
Tutorial ondifferentialextensionsThe usual suspects / DerelictionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionNew interpretation: f linear, dereliction amounts to just seeing it asa series.The syntaxThe ConstructsThe Reductionsf ·xProperties0 f ·x X0(x n )n 2The Semantics(Non) determinismFiniteness spacesTaylor tion: theIssuesIn programs, it is the query of a single use of an input:occurrences of variables!
Tutorial ondifferentialextensionsThe usual suspects / PromotionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionThe exponential box allows to compose.The syntaxThe Constructsg(x ), f (y )The ReductionsPropertiesf (g(x ))The Semantics(Non) determinismFiniteness spacesTaylor ExpansionConcurrency!AhgiB!Bhf iC!AhgiB!!Bhf iCTranslationBisimulation: theIssuesWe will say more in the section on the Taylor expansion.In programs: reusable package, the exponential argument exp(t).
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsThe unusual suspects / SumFunctions A B have a commutative monoidal structure. . . Insimpler words,Power seriesFrom Böhm treesto Taylorexpansionf (x ), g(x )The syntax(f g)(x ) : f (x ) g(x )The ConstructsThe ReductionsPropertiesAThe Semantics(Non) determinismAFiniteness spacesTaylor ExpansionConcurrencyfB,AgBBisimulation: theIssuesB ATranslationfgB There is also the function/net/process 0, of any type. We call sums of nets polynets.As we already hinted, sums model non determinism (or anindependent parallelism) of programs.
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsSums and promotionSums and 0 do not exit boxes: the evaluation function f , x 7 f (x )is linear in f but not in x (unless f itself is linear).Power seriesFrom Böhm treesto Taylorexpansiong(x ), h(x ), f (y )The syntaxThe Constructsf ((g h)(x ))f (y )f (0)C!AThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spaces!ATaylor on: theIssues!AhhiB!Ahf i hhi0!!Bhf iC!!Bhf iC
Tutorial ondifferentialextensionsThe unusual supspects / CocontractionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionCocontraction allows to subsitute a sum for the argument of ananalytic function.f (z)f (x y )The syntaxThe Constructs!AThe ReductionsPropertiesThe Semantics(Non) determinismzhf iByxIn fact!Ahf i!B!AFiniteness spacesTaylor Expansion?ConcurrencyTranslationBisimulation: theIssues?! !?In programs: joining resources, the bag ST given by bags S and T .
Tutorial ondifferentialextensionsThe unusual supspects / CoweakeningBack to theoriginsQuantitativesemanticsPower seriesSimilarily, coweakening is evaluation in 0.From Böhm treesto TaylorexpansionThe syntaxf (z)The Constructsf (0)The ReductionsProperties!AThe Semantics(Non) determinismxhf iB!hf iFiniteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesAgain 0 !(we will introduce the above as a reduciton)In programs: the empty resource, 1.!B
Tutorial ondifferentialextensionsThe unusual suspects / CoderelictionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionCodereliction is derivation at 0 along a linear variable.The syntaxThe ConstructsThe Reductionsf (x )PropertiesThe Semantics f (x ) x·zx 0(Non) determinismFiniteness spacesTaylor ExpansionConcurrency!Axhf iBzA!!Ahf iBTranslationBisimulation: theIssuesIn programs: introduction of a single use resource, the lineararguments inside the bags.
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsComposite constructs / General partialderivationTo obtain the syntax ofalready sawn, as f x x v· u we can use the constructsPower seriesFrom Böhm treesto Taylorexpansion f (x ) xThe syntax·u x v f (x v ) x·ux 0The ConstructsThe ReductionsPropertiesIn particular f xcan be regarded as itself evaluated in x . . . SoThe Semantics(Non) determinismFiniteness spacesTaylor Expansionf (x )ConcurrencyTranslation f (x )·z xBisimulation: theIssues!Axhf iB!Ax!zAIn programs: linear substitution t x!· u.hf iB
Tutorial ondifferentialextensionsBack to theoriginsSums and reductions Reductions and equivalences are defined by context closure.QuantitativesemanticsPower seriesFrom Böhm treesto TaylorexpansionµThe syntaxThe Constructs µ′The ReductionsPropertiesω[ ]The Semanticsω[ ](Non) determinismFiniteness spacesTaylor ExpansionConcurrency TranslationBisimulation: theIssues Sums spread to the box containing the redex (or the wholenet).Two flavours: µµ′ π if µ µ′ , µ simple;P π P ′′i µi i µi if µi µi , at least one strictly.Confluence and nondeterminism? Confluence ensures thatnondetermism does not depend on what part of the programwe reduce.
Tutorial ondifferentialextensionsBack to theoriginsThe known reductionsThe known onesQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion?π!?π π? !?The syntaxThe ConstructsThe ReductionsProperties?π!?π!The Semanticsπ(Non) determinismFiniteness spaces!? Taylor ExpansionConcurrencyTranslationBisimulation: theIssuesπσ!!π σ!!
Tutorial ondifferentialextensionsBack to theoriginsThe known reductionsThe known onesQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion?π!?π π? !?The syntaxThe ConstructsThe ReductionsPropertiesThe Semantics(Non) determinismFiniteness spacesA single-use query to a reusable resource?i.e.the extractiona packageπ from!? π!π!Taylor ExpansionConcurrencyTranslationBisimulation: theIssuesComposition with an analytical function?which is linearπσ!!π σ!!
Tutorial ondifferentialextensionsBack to theoriginsThe known reductionsThe known onesQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion?π!?π π? !?The syntaxThe ConstructsThe ReductionsProperties?π!?π!The Semantics(Non) determinismFiniteness spacesπ!? Taylor ExpansionConcurrencyTranslationBisimulation: theIssuesTwo queries from a reusable resourcei.e.ππ!the duplication of a packageσ!σ!Composition on a shared variable!
Tutorial ondifferentialextensionsBack to theoriginsThe known reductionsThe known onesQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion?π!?π π? !?The syntaxThe ConstructsThe ReductionsPropertiesThe Semanticsπ(Non) determinismFiniteness spacesEmpty query from a reusable resourceπ!? i.e.garbage collection!? Taylor ExpansionComposition withfunctionπ!? a constantConcurrencyTranslationBisimulation: theIssuesπσ!!π σ!!
Tutorial ondifferentialextensionsBack to theoriginsThe known reductionsThe known onesQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion?π!?π π? !?The syntaxThe ConstructsThe Reductionsπ?Properties!The Semantics(Non) determinismFiniteness spacesπ!resource? A reusablequerying another oneTaylor Expansionπ?Associativity of compositionConcurrencyTranslation!Bisimulation: theIssuesπσ!!π σ!!
Tutorial ondifferentialextensionsCodereliction vs derelictionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion!? In analysis:The syntaxThe ConstructsThe Reductions (g · x ) x 0 · z g · z xPropertiesThe Semantics(Non) determinismFiniteness spacesTaylor Expansionz!?xg zgConcurrencyTranslationBisimulation: theIssuesIn programs: a single-use query encounters a single-use resourceand is resolved. x· u u. x
Tutorial ondifferentialextensionsCocontranction and coweakening vs derelictionBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion!? ?!The syntaxThe ConstructsThe Reductions? !?!? 0analysis: it is linearity!PropertiesThe Semantics(Non) determinismg · (x y ) g · x g · y ,g · 0 0.Finiteness spacesTaylor ExpansionConcurrencyTranslationBisimulation: theIssuesprograms: a single-use query vs two resources,nondeterministic choice. Or vs an empty one, anondeterministic dead end.hλx .x i uv u v , hλx .x i 1 0.
Tutorial ondifferentialextensionsCodereliction vs contraction and coweakeningCompletely simmetric!Back to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion! ? ?!!!!?!? 0analysis: they come from the laws of derivation!The syntaxThe ConstructsThe ReductionsProperties f (x,x)·u xx 0 (x,x) x·The Semantics f (y ,z) f (y ,z) ·u y , zy ,z x 0 (Non) determinismFiniteness spaces f (y ,0) yy 0 f (0,z) zz 0Taylor ExpansionConcurrencyTranslationBisimulation: theIssuesand k x 0.programs: two queries meet a single-use resourcesnondeterministic choice. Or, an empty query meetsa single use resource, coming to an error (it is notaffine). hsi T x·u t x s x· u T hsi· u 0 if x 6 t. T x ·u .
Tutorial ondifferentialextensionsRouting: (co)contractions and (co)weakeningsBack to theoriginsQuantitativesemanticsPower seriesFrom Böhm treesto Taylorexpansion!?The syntaxThe Constructs?!?! The ReductionsProperties!The Semantics(Non) determinismConcurrencyTranslationBisimulation: theIssues !!!Finiteness spacesTaylor Expansion? ?analysis: f (x , y )f (x , x )f (u v , u v ) is the sameas f (x , y )f (u1 v1 , u2 v2 )f (u v , u v ). f (0, 0) is the same if sharing does not happen,if f (x ) is constant in x , then f (y z) is so in yand z.programs: routing of queries and resources.
Tutorial ondifferentialextensionsBack to theoriginsQuantitativesemanticsCocontraction and coweakening vs boxRecall that cocontractions and coweakenings are, in a way, boxes.Power seriesFrom Bö
lambda-calculus and linear logic February 16 2009. Tutorial on differential extensions Back to the origins Quantitative semantics Power series From Böhm trees to Taylor expansion The syntax The Constructs The Reductions Pro
