advertisement

Linear Type Theory Revisited (BACAT Feb 2014)

55 %
45 %
advertisement
Information about Linear Type Theory Revisited (BACAT Feb 2014)
Education

Published on February 22, 2014

Author: valeria.depaiva

Source: slideshare.net

Description

BACAT2: Valeria suggested that we discussed some old work on linear type theory to get up to date with newer work. Here are some slides for a background talk on linear type theory, based on Term Assignment for Intuitionistic Linear Logic. (Benton, Bierman, de Paiva and Hyland). Technical Report 262, University of Cambridge Computer Laboratory 1992.
advertisement

Linear Type Theory Revisited Valeria de Paiva Nuance Comms February 21, 2014

Introduction

Goals Discuss very old work (early 90’s) on linear type theories

Goals Discuss very old work (early 90’s) on linear type theories based on Term Assignment for Intuitionistic Linear Logic. (Benton, Bierman, de Paiva and Hyland). Technical Report 262, University of Cambridge Computer Laboratory 1992.

Goals Discuss very old work (early 90’s) on linear type theories based on Term Assignment for Intuitionistic Linear Logic. (Benton, Bierman, de Paiva and Hyland). Technical Report 262, University of Cambridge Computer Laboratory 1992. available from http://www.cs.bham.ac.uk/ vdp/publications/papers.html.

Goals Discuss very old work (early 90’s) on linear type theories based on Term Assignment for Intuitionistic Linear Logic. (Benton, Bierman, de Paiva and Hyland). Technical Report 262, University of Cambridge Computer Laboratory 1992. available from http://www.cs.bham.ac.uk/ vdp/publications/papers.html. then get to the state-of-the art...

Summary from Abstract Investigate the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic

Summary from Abstract Investigate the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic both sequent calculus and natural deduction proof systems

Summary from Abstract Investigate the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic both sequent calculus and natural deduction proof systems satisfying two important properties: the substitution property (the set of valid deductions is closed under substitution) and subject reduction (reduction on terms is well-typed)

Summary from Abstract Investigate the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic both sequent calculus and natural deduction proof systems satisfying two important properties: the substitution property (the set of valid deductions is closed under substitution) and subject reduction (reduction on terms is well-typed) a categorical model for Intuitionistic Linear Logic and how to use it to derive the term assignment

Summary from Abstract Investigate the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic both sequent calculus and natural deduction proof systems satisfying two important properties: the substitution property (the set of valid deductions is closed under substitution) and subject reduction (reduction on terms is well-typed) a categorical model for Intuitionistic Linear Logic and how to use it to derive the term assignment long (57 pages) but slow and easy...

Introduction the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic

Introduction the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic Previous approaches have simply annotated the sequent calculus with terms and have given little or no justification for their choice

Introduction the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic Previous approaches have simply annotated the sequent calculus with terms and have given little or no justification for their choice Phil Wadler: There’s no substitute for LL

Introduction the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic Previous approaches have simply annotated the sequent calculus with terms and have given little or no justification for their choice Phil Wadler: There’s no substitute for LL substitution lemma does not hold for the term assignment system in Abramsky’s ‘Computational Interpretations of Linear Logic’ (Cited by 546)

Digression: Other old work... Linear types can change the world Is there a use for linear logic? A taste of linear logic Operational interpretations of linear logic Reference counting as a computational interpretation of linear logic (Chirimar)

Introduction 2 solving the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic:

Introduction 2 solving the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic: Two ways By considering the sequent calculus formulation of the logic and using the underlying categorical constructions to suggest a term assignment system By considering a linear natural deduction system

Introduction 2 solving the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic: Two ways By considering the sequent calculus formulation of the logic and using the underlying categorical constructions to suggest a term assignment system By considering a linear natural deduction system two approaches produce equivalent term assignment systems

Introduction 2 solving the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic: Two ways By considering the sequent calculus formulation of the logic and using the underlying categorical constructions to suggest a term assignment system By considering a linear natural deduction system two approaches produce equivalent term assignment systems BUT for equality (via reduction of terms) matters are more subtle: natural equalities for category theory are stronger than those suggested by computational considerations

Outline of TR Girard’s Intuitionistic Linear Logic:

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus)

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction how our two systems of Intuitionistic Linear Logic are related

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction how our two systems of Intuitionistic Linear Logic are related the process of proof normalisation within the linear natural deduction system

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction how our two systems of Intuitionistic Linear Logic are related the process of proof normalisation within the linear natural deduction system model for Intuitionistic Linear Logic

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction how our two systems of Intuitionistic Linear Logic are related the process of proof normalisation within the linear natural deduction system model for Intuitionistic Linear Logic cut-elimination in the sequent calculus

Outline of TR Girard’s Intuitionistic Linear Logic: a simple categorical model of Intuitionistic Linear Logic (sequent calculus) a linear system of natural deduction how our two systems of Intuitionistic Linear Logic are related the process of proof normalisation within the linear natural deduction system model for Intuitionistic Linear Logic cut-elimination in the sequent calculus conclusions

Intuitionistic Linear Logic Recommended if sequent calculus/ND are not part of your vocab: Jean Gallier: Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. Theoretical Computer Science, 110(2), 249-239 (1993). from http://www.cis.upenn.edu/ jean/gbooks/logic.html multiplicative fragment of Intuitionistic Linear Logic (ILL)

Intuitionistic Linear Logic Recommended if sequent calculus/ND are not part of your vocab: Jean Gallier: Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. Theoretical Computer Science, 110(2), 249-239 (1993). from http://www.cis.upenn.edu/ jean/gbooks/logic.html multiplicative fragment of Intuitionistic Linear Logic (ILL) a refinement of intuitionistic logic (IL) where formulae must be used exactly once

Intuitionistic Linear Logic Recommended if sequent calculus/ND are not part of your vocab: Jean Gallier: Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. Theoretical Computer Science, 110(2), 249-239 (1993). from http://www.cis.upenn.edu/ jean/gbooks/logic.html multiplicative fragment of Intuitionistic Linear Logic (ILL) a refinement of intuitionistic logic (IL) where formulae must be used exactly once Weakening and Contraction rules are removed

Intuitionistic Linear Logic Recommended if sequent calculus/ND are not part of your vocab: Jean Gallier: Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. Theoretical Computer Science, 110(2), 249-239 (1993). from http://www.cis.upenn.edu/ jean/gbooks/logic.html multiplicative fragment of Intuitionistic Linear Logic (ILL) a refinement of intuitionistic logic (IL) where formulae must be used exactly once Weakening and Contraction rules are removed To regain the expressive power, rules returned in a controlled manner using operator “!”

Intuitionistic Linear Logic Recommended if sequent calculus/ND are not part of your vocab: Jean Gallier: Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. Theoretical Computer Science, 110(2), 249-239 (1993). from http://www.cis.upenn.edu/ jean/gbooks/logic.html multiplicative fragment of Intuitionistic Linear Logic (ILL) a refinement of intuitionistic logic (IL) where formulae must be used exactly once Weakening and Contraction rules are removed To regain the expressive power, rules returned in a controlled manner using operator “!” “!” similar to the modal necessity operator

Intuitionistic Linear Logic Rules

Generic Categorical considerations sequent calculus: providing not proofs themselves but a meta-theory concerning proofs fundamental idea of categorical treatment of proof theory propositions interpreted as objects of a category (or multicategory or polycategory)

Generic Categorical considerations sequent calculus: providing not proofs themselves but a meta-theory concerning proofs fundamental idea of categorical treatment of proof theory propositions interpreted as objects of a category (or multicategory or polycategory) proofs interpreted as maps of the category

Generic Categorical considerations sequent calculus: providing not proofs themselves but a meta-theory concerning proofs fundamental idea of categorical treatment of proof theory propositions interpreted as objects of a category (or multicategory or polycategory) proofs interpreted as maps of the category operations transforming proofs into proofs then correspond (if possible) to natural transformations between appropriate hom-functors

Categorical considerations dealing with sequents Γ multicategories A in principle we should deal with

Categorical considerations dealing with sequents Γ A in principle we should deal with multicategories simplifying assumption: multicategorical structure represented by a tensor product .

Categorical considerations dealing with sequents Γ A in principle we should deal with multicategories simplifying assumption: multicategorical structure represented by a tensor product . a sequent of form C1 , C2 , . . . , Cn A will be represented by C1 ⊗ C2 ⊗ . . . ⊗ Cn → A sometimes written as Γ → A

Categorical considerations dealing with sequents Γ A in principle we should deal with multicategories simplifying assumption: multicategorical structure represented by a tensor product . a sequent of form C1 , C2 , . . . , Cn A will be represented by C1 ⊗ C2 ⊗ . . . ⊗ Cn → A sometimes written as Γ → A (a coherence result is assumed)

Categorical considerations dealing with sequents Γ A in principle we should deal with multicategories simplifying assumption: multicategorical structure represented by a tensor product . a sequent of form C1 , C2 , . . . , Cn A will be represented by C1 ⊗ C2 ⊗ . . . ⊗ Cn → A sometimes written as Γ → A (a coherence result is assumed) We seek to enrich the sequent judgement to a term assignment judgement of the form x1 : C1 , x2 : C2 , . . . , xn : Cn e: A where the xi are distinct variables and e is a term.

Identity and Cut The sequent representing the Identity rule is interpreted as the canonical identity arrow idA : A → A

Identity and Cut The sequent representing the Identity rule is interpreted as the canonical identity arrow idA : A → A The corresponding rule of term formation is x : A x :A

Identity and Cut The sequent representing the Identity rule is interpreted as the canonical identity arrow idA : A → A The corresponding rule of term formation is x : A x :A The rule of Exchange we interpret by assuming that we have a symmetry for the tensor product

Identity and Cut The sequent representing the Identity rule is interpreted as the canonical identity arrow idA : A → A The corresponding rule of term formation is x : A x :A The rule of Exchange we interpret by assuming that we have a symmetry for the tensor product We suppress Exchange and the corresponding symmetry, considering multisets of formulae, so no term forming operations result from this rule (others do diff...)

Identity and Cut The sequent representing the Identity rule is interpreted as the canonical identity arrow idA : A → A The corresponding rule of term formation is x : A x :A The rule of Exchange we interpret by assuming that we have a symmetry for the tensor product We suppress Exchange and the corresponding symmetry, considering multisets of formulae, so no term forming operations result from this rule (others do diff...) The cut rule is interpreted as a generalized form of composition. if the maps f : Γ → A and g : A, ∆ → B are the interpretations of hypotheses of the rule, then the composite Γ ⊗ ∆ →f ⊗1∆ A ⊗ ∆ →g B is the interpretation of the conclusion

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule Composition corresponds to Cut: our operations commute where appropriate with Cut.

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule Composition corresponds to Cut: our operations commute where appropriate with Cut. Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution.

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule Composition corresponds to Cut: our operations commute where appropriate with Cut. Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. The rules for the constant I are parallel to the rules for the tensor product ⊗, which we describe next.

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule Composition corresponds to Cut: our operations commute where appropriate with Cut. Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. The rules for the constant I are parallel to the rules for the tensor product ⊗, which we describe next. The rules for (linear) implication are usual.

Substitution in Terms... Assumption: any logical rule corresponds to an operation on maps of the category which is natural in the interpretations of the components of the sequents which remain unchanged during the application of a rule Composition corresponds to Cut: our operations commute where appropriate with Cut. Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. The rules for the constant I are parallel to the rules for the tensor product ⊗, which we describe next. The rules for (linear) implication are usual. The rules for the modality ! are the hard ones. these slides will get us to page 12 of the report...

Text substitution Terms use this and BB to get equation (2)

Tensor Terms Abramsky introduced a let constructor for tensor products, a reasonable syntax to bind variables x and y in the term f .

Tensor Terms Abramsky introduced a let constructor for tensor products, a reasonable syntax to bind variables x and y in the term f . Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution.

Tensor Terms Abramsky introduced a let constructor for tensor products, a reasonable syntax to bind variables x and y in the term f . Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. Naturality in C gives rise to the equation equation explaining how lets interact with composition.

Tensor Terms Abramsky introduced a let constructor for tensor products, a reasonable syntax to bind variables x and y in the term f . Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. Naturality in C gives rise to the equation equation explaining how lets interact with composition. For the tensoring on the right, we simply multiply (or tensor) the terms.

Tensor Terms Abramsky introduced a let constructor for tensor products, a reasonable syntax to bind variables x and y in the term f . Composition is interpreted by textual substitution thus the free variables have to reflect the possibility for substitution. Naturality in C gives rise to the equation equation explaining how lets interact with composition. For the tensoring on the right, we simply multiply (or tensor) the terms. since the constant I is the unity for the tensor operation, its rules are similar.

Implication Terms Are just like usual implication (lambda) terms

Implication Terms Are just like usual implication (lambda) terms the difference is that the variable that your lambda binds has to be present in the context and only once

Implication Terms Are just like usual implication (lambda) terms the difference is that the variable that your lambda binds has to be present in the context and only once There is an explanation for why the Yoneda lemma is responsible for the simplification that one can do in the syntax (and why Peter Schroeder-Heister is really right about his formulation of Natural Deduction) but we don’t need to go there.

Modality ! Term Assignment The left rules are ok. The dereliction rules creates a binder, a bit like the tensor and the I rules.

Modality ! Term Assignment The left rules are ok. The dereliction rules creates a binder, a bit like the tensor and the I rules. The weakening and contraction rules discard and copy variables, and have naturality conditions as the tensor rule.

Modality ! Term Assignment The left rules are ok. The dereliction rules creates a binder, a bit like the tensor and the I rules. The weakening and contraction rules discard and copy variables, and have naturality conditions as the tensor rule. The problematic rule, ”promotion”

Multiplicative Term Assignment

Conclusions so Far... The categorical model can give you guidance for the shape of the type theory rules.

Conclusions so Far... The categorical model can give you guidance for the shape of the type theory rules. Categorical rules are about full beta and eta equivalence plus some naturality conditions (not very liked by FPers)

Conclusions so Far... The categorical model can give you guidance for the shape of the type theory rules. Categorical rules are about full beta and eta equivalence plus some naturality conditions (not very liked by FPers)

Conclusions so Far... Newer models plus new term calculi via DILL (Dual Intuitionistic Linear Logic) and monoidal adjunction models (Benton, Barber, Mellies, who else?...)

Conclusions so Far... Newer models plus new term calculi via DILL (Dual Intuitionistic Linear Logic) and monoidal adjunction models (Benton, Barber, Mellies, who else?...) Which one to read about?

Conclusions so Far... Newer models plus new term calculi via DILL (Dual Intuitionistic Linear Logic) and monoidal adjunction models (Benton, Barber, Mellies, who else?...) Which one to read about? Rewriting is a new ball game, which I would like to investigate too cf. Barney Hilken paper “Towards a proof theory of rewriting: the simply-typed 2-[lambda] calculus” Theor. Comp. Sci. Vol. 170, 1-2, pp 407-444. 1996.

Add a comment

Related presentations

Related pages

2014 - NASA Science

... 2014. Scientists using mission data from NASA’s Cassini spacecraft have identified 101 distinct geysers erupting on Saturn ... Feb. 26, 2014.
Read more

Nacirema - Wikipedia, the free encyclopedia

(March 2014) (Learn how and when ... "The Nacirema Revisited." Annals Of ... to undergraduate students the fundamentals of John Rawls's theory of justice ...
Read more

Institute of Technology, Allahabad - 211 004, India Centre ...

... 14 Feb 2014 On the complete Lie ... quadratic-linear Li´enard type equation x¨ +f(x)˙x2 + g(x)˙x+h(x) = 0 ... for ODEs can be obtained from his theory.
Read more

How To Solve Linear Programming Problem Using Simplex ...

... youtube .com/c/HappyLearning ... Published on Feb 23, 2014. ... In this video you will learn "How To Solve A Linear Programming Problem" of ...
Read more

Linear Algebra Done Wrong - Brown University Mathematics ...

Linear Algebra Done Wrong ... Chapter4is an introduction to spectral theory, and that is where the ... revisited.142 x6.
Read more

Nonlinear Analysis: Theory, Methods & Applications ...

Nonlinear Analysis: Theory, Methods & Applications Volume 141, In Progress Volume / Issue In ProgressA Volume/Issue that is "In Progress" contains final ...
Read more

string theory in nLab

type I string theory. ... Feb 2014, ESI Vienna ; Quantum anomalies. ... Superstring Perturbation Theory Revisited (arXiv:1209.5461)
Read more

The Criminologist

The Criminologist Page 1 ... it often implicates tipping points and non-linear systems, ... Click on Journals under the Browse by Product Type heading. 4.
Read more