Tutorial on the differential extensions of lambda-calculus ...

Tutorial on differential extensions Back to the origins Quantitative semantics Power series From Böhm trees to Taylor expansion Tutorial on the differential extensions of The syntax The Constructs lambda-calculus and linear logicThe Reductions Properties The Semantics (Non) determinism Finiteness spaces Taylor Expansion Concurrency Translation Bisimulation: the Issues February 16 2009Tutorial on differential Outline extensions Back to the Back to the origins origins Quantitative Quantitative semantics semantics Power series Power series From Böhm trees to Taylor From Böhm trees to Taylor expansion expansion The syntax The Constructs The syntax The Reductions Properties The Constructs The Semantics The Reductions (Non) determinism PropertiesFiniteness spaces Taylor Expansion Concurrency The Semantics Translation Bisimulation: the (Non) determinism Issues Finiteness spaces Taylor Expansion Concurrency Translation Bisimulation: the IssuesTutorial on differential Outline extensions Back to the Back to the origins origins Quantitative Quantitative semantics semantics Power series Power series From Böhm trees to Taylor From Böhm trees to Taylor expansion expansion The syntax The Constructs The syntax The Reductions Properties The Constructs The Semantics The Reductions (Non) determinism PropertiesFiniteness spaces Taylor Expansion Concurrency The Semantics Translation Bisimulation: the (Non) determinism Issues Finiteness spaces Taylor Expansion Concurrency Translation Bisimulation: the IssuesTutorial on differential At the beginning there was. . . extensions Girard’s quantitative semantics Back to the origins Quantitative semantics Power series Analysis Computer Science Proof theory From Böhm trees to Taylor expansion continuous functions λ-calculus NJ of→ ∞ ∞ ⇔ ⇔ The syntax The Constructs F( x )= F(x ) β-reduction cut-eliminationn n The Reductions Properties n=0 n=0 The Semantics (Non) determinism Finiteness spaces Taylor Expansion Concurrency Translation Bisimulation: the Issues Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic, Elsevier, 1988.Tutorial on differential At the beginning there was. . . extensions Girard’s quantitative semantics Back to the origins Quantitative semantics Power series Analysis Computer Science Proof Theory From Böhm trees to Taylor expansion power series λ-calculus LL of !⊸ ∞ ⇔ ⇔ The syntax n The Constructs a F β-reduction cut-eliminationn The Reductions Properties n=0 The Semantics linear functions: linear β-reduction: substructural(Non) determinism Finiteness spaces F(U+V)=F(U)+F(V) ⇔ using inputs ⇔ proofs: Taylor Expansion F(aU)=aF(U) exactly once ⊗, &,`,⊕ Concurrency Translation Bisimulation: the Issues Jean-Yves Girard. Linear Logic. Theoretical Computer Science, Elsevier, 1987.Tutorial on differential At the beginning there was. . . extensions Girard’s quantitative semantics Back to the origins Quantitative semantics Power series Analysis Computer Science Proof Theory From Böhm trees to Taylor expansion power series λ-calculus LL of !⊸ ∞ ⇔ ⇔ The syntax n The Constructs a F β-reduction cut-eliminationn The Reductions Properties n=0 The Semantics linear functions: linear β-reduction: substructural(Non) determinism Finiteness spaces F(U+V)=F(U)+F(V) ⇔ using inputs ⇔ proofs: Taylor Expansion F(aU)=aF(U) exactly once ⊗, &,`,⊕ Concurrency Translation Bisimulation: the Issues . . . though in linear logic the link with analysis is not convincing. . . differential linear logic wants to make this correspondence explicit Jean-Yves Girard. Linear Logic. Theoretical Computer Science, Elsevier, 1987.Tutorial on differential Why power series? (1) extensions What is the result of the application ML? Let us ask it to Böhm! Back to the origins Quantitative semantics ◮ compute finite approximations BT (ML)⊑ BT (ML)⊑ ...0 1 Power series From Böhm trees ◮ the result is the limit of these approximations: to Taylor expansion ∞The syntax The Constructs BT(ML) = BT (ML)dThe Reductions Properties d=0 The Semantics (Non) determinism Finiteness spaces Taylor Expansion Concurrency Translation Bisimulation: the Issues ◮ d expresses how "deep" BT (ML) is definedd ◮ the order⊑ between BT ’s is a definedness orderdTutorial on differential Why power series? (1) extensions What is the result of the application ML? Let us ask it to Böhm! Back to the origins Quantitative semantics ◮ compute finite approximations BT (ML)⊑ BT (ML)⊑ ...0 1 Power series From Böhm trees ◮ the result is the limit of these approximations: to Taylor expansion ∞The syntax The Constructs BT(ML) = BT (ML)dThe Reductions Properties d=0 The Semantics (Non) determinism Finiteness spaces Example (Y≡ λf.(λx.f(xx))(λx.f(xx))) Taylor Expansion Concurrency Translation BT (Yf) =⊥0 BT (Yf) = f(f(f⊥))3Bisimulation: the Issues BT (Yf) = f⊥1 ...BT (Yf) = f(f⊥)2 BT(Yf) = f(f(f ...)) ◮ d expresses how "deep" BT (ML) is definedd ◮ the order⊑ between BT ’s is a definedness orderdTutorial on differential Why power series? (1) extensions What is the result of the application ML? Let us ask it to Böhm! Back to the origins Quantitative semantics ◮ compute finite approximations BT (ML)⊑ BT (ML)⊑ ...0 1 Power series From Böhm trees ◮ the result is the limit of these approximations: to Taylor expansion ∞The syntax The Constructs BT(ML) = BT (ML)dThe Reductions Properties d=0 The Semantics (Non) determinism Finiteness spaces Example (Y≡ λf.(λx.f(xx))(λx.f(xx))) Taylor Expansion Concurrency Translation BT (Yf) =⊥0 BT (Yf) = f(f(f⊥))3Bisimulation: the Issues BT (Yf) = f⊥1 ...BT (Yf) = f(f⊥)2 BT(Yf) = f(f(f ...)) ◮ d expresses how "deep" BT (ML) is definedd ◮ the order⊑ between BT ’s is a definedness orderdTutorial on differential Why power series? (2) extensions Back to the origins Quantitative semantics Power series This approach yields wonderful accounts of qualitative properties From Böhm trees to Taylor of programs: expansion The syntax The Constructs Theorem (solvability) The Reductions Properties M solvable iff BT(M) =⊥ The Semantics (Non) determinism Finiteness spaces Theorem (normalizability)Taylor Expansion Concurrency M normalizable iff BT(M) finite and without⊥ Translation Bisimulation: the Issues Example BT(ΔΔ) =⊥ BT(Yf) = f(BT(Yf)) BT(2 2) = 4