Tutorial on the differential extensions of lambda-calculus ...
112 Pages
English

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

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

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

Subjects

Informations

Published by
Reads 118
Language English
Document size 1 MB

Exrait

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