[ Pobierz całość w formacie PDF ]
.4.Intuitionistic Linear Logiccorresponds to the linear »-calculus via a Curry-Howard isomorphism in thesame way as Intuitionistic Logic corresponds to the »-calculus.The formulaeof Intuitionistic Linear Logic correspond to types of the linear »-calculus inthe obvious way.We get the rules for assigning types to terms of the linear»-calculus if we decorate the proof-rules of Intuitionistic Linear Logic withterms in the appropriate way, and moreover, we can recover the proof-rules ifwe take the typing rules of the linear »-calculus and remove the terms.Theisomorphism on the level of proofs is essentially given by Proposition 2.4.2.As with the »-calculus, it is the case that all the ²-reductions of thelinear »-calculus appear as Curry-Howard interpretations of reduction rules ofIntuitionistic Linear Logic.For example, in the case of a (—"I, —"E) reduction31 Chapter 2.Linear Logicwe get· ·· ·x : A - x : A y : B - y : B· ··“ - u : A " - v : B··“, " - u —" v : A —" B ›, x : A, y : B - wC›, “, " -let u —" v be x —" y in w : C;· ·· ·· ·“ - u : A " - v : B···›, “, " - w[u, v/x, y] : CWe see that a ²-reduction has taken place on the term encoding the proofon which the reduction is performed.All ²-reductions actually do appear asCurry-Howard interpretations of reductions on the corresponding proofs.2.6 The Girard TranslationThe [Gir87] paper introduced the Girard Translation which embeds Intuition-istic Logic into Intuitionistic Linear Logic.We will state the Girard Transla-tion in terms of the Natural Deduction presentations of Intuitionistic Logicand Intuitionistic Linear Logic given in Appendix A.2 and Appendix A.4,respectively.The translation works at the level of formulae as well as at thelevel of proofs.At the level of formulae the Girard Translation is definedinductively as follows:1o = 1(A '" B)o = Ao&Bo(A Ò! B)o = !Ao Bo0o = 0(A (" B)o = !Ao•"!Bo32 2.6.The Girard TranslationAt the level of proofs the Girard Translation inductively translates a proofof a sequentA1,., An Binto a proof of the sequent!Ao,., !Ao - Bo.1 nIn what follows we consider each case except the symmetric ones.Specialcases of rules are used when appropriate.Recall that a double bar means anumber of applications of rules." A derivationA1,., An Apis translated into!Ao - !Aoq p!Ao - Aoq p= ============o!Ao,., !Ao - Ap1 n" A derivation“ 1is translated into!“o - 1" A derivation“ A “ B“ A '" Bis translated into!“o - Ao !“o - Bo!“o - Ao&Bo" A derivation“ A '" B“ Ais translated into!“o - Ao&Bo!“o - Ao33 Chapter 2.Linear Logic" A derivation“, A B“ A Ò!Bis translated into!“o, !Ao - Bo!“o - !Ao Bo" A derivation“ A Ò! B “ A“ Bis translated into!“o - Ao!“o - !Ao Bo !“o - !Ao!“o, !“o - Bo==========!“o - Bo" A derivation“ 0“ Cis translated into!“o - 0!“o - Co" A derivation“ A“ A (" Bis translated into!“o - Ao!“o - !Ao!“o - !Ao•"!Bo" A derivation“ A (" B “, A C “, B C“ C34 2.7.Concrete Modelsis translated into!“o - !Ao•"!Bo !“o, !Ao - Co !“o, !Bo - Co!“o, !“o - Co==========!“o - CoThe translation is sound with respect to provability in the sense that thesequent A1,., An B is provable (in Intuitionistic Logic) iff !Ao,., !Ao - Bo1 nis provable (in Intuitionistic Linear Logic).Moreover, it is shown in [Bie94]that the translation preserves ²-reductions.In [Gir87] it is shown that theGirard Translation is sound with respect to the standard coherence spaceinterpretation, that is, the interpretation of a proof in Intuitionistic Logicis essentially the same as the interpretation of its image under the GirardTranslation.A categorical version of this result can be found in [Bra96].2.7 Concrete ModelsAn example of a concrete model of Intuitionistic Linear Logic is the categoryof cpos and strict continuous functions.A cpo is a partial order with theproperty that each directed subset has a least upper bound.Note that thisentails that a cpo has a bottom element.A monotone function between cposis continuous if it preserves the least upper bound of any non-empty directedsubset, and it is strict if it preserves the bottom element.The symmetricmonoidal structure is given by the smash product, the internal-hom of twoobjects is given by the set of strict continuous functions with the pointwiseorder, and the comonad is given by the lift operation.It should be mentioned that the category of cpos and strict continuousfunctions is actually a model for intuitionistic relevant logic in the sense of[Jac94].Also the category of dI domains and linear stable functions is a modelof Intuitionistic Linear Logic.We will first define a dI domain.Let (D, )be a non-empty poset such that every finitely bounded subset X has a leastupper bound X where a subset X is finitely bounded iff every finite subsetof X has an upper bound.This entails that D has a bottom element, andmoreover, every non-empty subset X has a greatest lower bound which wewill denote by X.A prime element of D is an element d such thatd XÒ!"x"X.d x35 Chapter 2.Linear Logicfor any finitely bounded subset X.We will denote the set of prime elementsof D by Dp.The poset D is prime algebraic iff"d " D.d = {d " Dp | d d)}A finite element of D is an element d such thatd XÒ!"x"X.d xfor any non-empty directed subset X.We will denote the set of finite elementsof D by Do.The poset D is finitary iff"d " Do.|{d " D | d d}| [ Pobierz caÅ‚ość w formacie PDF ]
zanotowane.pl doc.pisz.pl pdf.pisz.pl przylepto3.keep.pl
.4.Intuitionistic Linear Logiccorresponds to the linear »-calculus via a Curry-Howard isomorphism in thesame way as Intuitionistic Logic corresponds to the »-calculus.The formulaeof Intuitionistic Linear Logic correspond to types of the linear »-calculus inthe obvious way.We get the rules for assigning types to terms of the linear»-calculus if we decorate the proof-rules of Intuitionistic Linear Logic withterms in the appropriate way, and moreover, we can recover the proof-rules ifwe take the typing rules of the linear »-calculus and remove the terms.Theisomorphism on the level of proofs is essentially given by Proposition 2.4.2.As with the »-calculus, it is the case that all the ²-reductions of thelinear »-calculus appear as Curry-Howard interpretations of reduction rules ofIntuitionistic Linear Logic.For example, in the case of a (—"I, —"E) reduction31 Chapter 2.Linear Logicwe get· ·· ·x : A - x : A y : B - y : B· ··“ - u : A " - v : B··“, " - u —" v : A —" B ›, x : A, y : B - wC›, “, " -let u —" v be x —" y in w : C;· ·· ·· ·“ - u : A " - v : B···›, “, " - w[u, v/x, y] : CWe see that a ²-reduction has taken place on the term encoding the proofon which the reduction is performed.All ²-reductions actually do appear asCurry-Howard interpretations of reductions on the corresponding proofs.2.6 The Girard TranslationThe [Gir87] paper introduced the Girard Translation which embeds Intuition-istic Logic into Intuitionistic Linear Logic.We will state the Girard Transla-tion in terms of the Natural Deduction presentations of Intuitionistic Logicand Intuitionistic Linear Logic given in Appendix A.2 and Appendix A.4,respectively.The translation works at the level of formulae as well as at thelevel of proofs.At the level of formulae the Girard Translation is definedinductively as follows:1o = 1(A '" B)o = Ao&Bo(A Ò! B)o = !Ao Bo0o = 0(A (" B)o = !Ao•"!Bo32 2.6.The Girard TranslationAt the level of proofs the Girard Translation inductively translates a proofof a sequentA1,., An Binto a proof of the sequent!Ao,., !Ao - Bo.1 nIn what follows we consider each case except the symmetric ones.Specialcases of rules are used when appropriate.Recall that a double bar means anumber of applications of rules." A derivationA1,., An Apis translated into!Ao - !Aoq p!Ao - Aoq p= ============o!Ao,., !Ao - Ap1 n" A derivation“ 1is translated into!“o - 1" A derivation“ A “ B“ A '" Bis translated into!“o - Ao !“o - Bo!“o - Ao&Bo" A derivation“ A '" B“ Ais translated into!“o - Ao&Bo!“o - Ao33 Chapter 2.Linear Logic" A derivation“, A B“ A Ò!Bis translated into!“o, !Ao - Bo!“o - !Ao Bo" A derivation“ A Ò! B “ A“ Bis translated into!“o - Ao!“o - !Ao Bo !“o - !Ao!“o, !“o - Bo==========!“o - Bo" A derivation“ 0“ Cis translated into!“o - 0!“o - Co" A derivation“ A“ A (" Bis translated into!“o - Ao!“o - !Ao!“o - !Ao•"!Bo" A derivation“ A (" B “, A C “, B C“ C34 2.7.Concrete Modelsis translated into!“o - !Ao•"!Bo !“o, !Ao - Co !“o, !Bo - Co!“o, !“o - Co==========!“o - CoThe translation is sound with respect to provability in the sense that thesequent A1,., An B is provable (in Intuitionistic Logic) iff !Ao,., !Ao - Bo1 nis provable (in Intuitionistic Linear Logic).Moreover, it is shown in [Bie94]that the translation preserves ²-reductions.In [Gir87] it is shown that theGirard Translation is sound with respect to the standard coherence spaceinterpretation, that is, the interpretation of a proof in Intuitionistic Logicis essentially the same as the interpretation of its image under the GirardTranslation.A categorical version of this result can be found in [Bra96].2.7 Concrete ModelsAn example of a concrete model of Intuitionistic Linear Logic is the categoryof cpos and strict continuous functions.A cpo is a partial order with theproperty that each directed subset has a least upper bound.Note that thisentails that a cpo has a bottom element.A monotone function between cposis continuous if it preserves the least upper bound of any non-empty directedsubset, and it is strict if it preserves the bottom element.The symmetricmonoidal structure is given by the smash product, the internal-hom of twoobjects is given by the set of strict continuous functions with the pointwiseorder, and the comonad is given by the lift operation.It should be mentioned that the category of cpos and strict continuousfunctions is actually a model for intuitionistic relevant logic in the sense of[Jac94].Also the category of dI domains and linear stable functions is a modelof Intuitionistic Linear Logic.We will first define a dI domain.Let (D, )be a non-empty poset such that every finitely bounded subset X has a leastupper bound X where a subset X is finitely bounded iff every finite subsetof X has an upper bound.This entails that D has a bottom element, andmoreover, every non-empty subset X has a greatest lower bound which wewill denote by X.A prime element of D is an element d such thatd XÒ!"x"X.d x35 Chapter 2.Linear Logicfor any finitely bounded subset X.We will denote the set of prime elementsof D by Dp.The poset D is prime algebraic iff"d " D.d = {d " Dp | d d)}A finite element of D is an element d such thatd XÒ!"x"X.d xfor any non-empty directed subset X.We will denote the set of finite elementsof D by Do.The poset D is finitary iff"d " Do.|{d " D | d d}| [ Pobierz caÅ‚ość w formacie PDF ]