Hi, In lambda-calculus one can define the product of types A and B by: forall C, (A->B->C)->C. with pairing and projections defined as: pair ≡ λx.λy.λz.z x y fst ≡ λp.p (λx.λy.x) snd ≡ λp.p (λx.λy.y) What would be the equivalent in a closed monoidal category? Would we get a product for free? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Remark: as far as I remember, one need to be cautios calling this a product, because ordinary product equations do not hold with this definition and standard equality of lambda-calculus. Best wishes Sergei Soloviev
Hi,
In lambda-calculus one can define the product of types A and B by:
forall C, (A->B->C)->C.
with pairing and projections defined as:
pair ≡ λx.λy.λz.z x y fst ≡ λp.p (λx.λy.x) snd ≡ λp.p (λx.λy.y)
What would be the equivalent in a closed monoidal category? Would we get a product for free?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
More to the point, it is a "weak product" (lacking the uniqueness condition one usually has) - I think this is discussed in Lambek Scott, but am away from my library to verify this ... -= rags =- On Wed, 18 Aug 2010, soloviev@irit.fr wrote:
Remark:
as far as I remember, one need to be cautios calling this a product, because ordinary product equations do not hold with this definition and standard equality of lambda-calculus.
Best wishes
Sergei Soloviev
Hi,
In lambda-calculus one can define the product of types A and B by:
forall C, (A->B->C)->C.
with pairing and projections defined as:
pair ÿÿ ÿÿx.ÿÿy.ÿÿz.z x y fst ÿÿ ÿÿp.p (ÿÿx.ÿÿy.x) snd ÿÿ ÿÿp.p (ÿÿx.ÿÿy.y)
What would be the equivalent in a closed monoidal category? Would we get a product for free?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear David, If you consider not only a closed monoidal category, but a full model of dual intuitionistic linear logic (DILL) with parametric polymorphism, the answer is yes. A model of DILL means among other things that the tensor is symmetric, and that there is a comonad, usually denoted ! . Writing --o for the closed structure and --> for the Girard encoding A --> B = !A --o B, then one can first encode coproducts as A + B = forall C . (A --o C) --> (B --o C) --> C and then products as A x B = forall C . ((A --o C) + (B --o C)) --o C Further details on these encodings can be found in Linear Abadi and Plotkin Logic, by Birkedal, Møgelberg and Petersen, Logical methods in Computer Science, 2(5). Rasmus On 17 August 2010 15:27, David Leduc <david.leduc6@googlemail.com> wrote:
Hi,
In lambda-calculus one can define the product of types A and B by:
forall C, (A->B->C)->C.
with pairing and projections defined as:
pair ≡ λx.λy.λz.z x y fst ≡ λp.p (λx.λy.x) snd ≡ λp.p (λx.λy.y)
What would be the equivalent in a closed monoidal category? Would we get a product for free?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
David, this is a lazy reply - I did not check anything out. One would be working with a second-order linear lambda calculus, presumably, so only the definition below of "pair" works. If one made a suitable "cut-down" version of Rasmus et al's paper, with parametricity, I would expect that, with your definition, one gets a tensor product adjoint to the function space. I don't have an immediate guess as to what one gets without parametricity. Gordon On Tue, Aug 17, 2010 at 2:27 PM, David Leduc <david.leduc6@googlemail.com>wrote:
Hi,
In lambda-calculus one can define the product of types A and B by:
forall C, (A->B->C)->C.
with pairing and projections defined as:
pair ≡ λx.λy.λz.z x y fst ≡ λp.p (λx.λy.x) snd ≡ λp.p (λx.λy.y)
What would be the equivalent in a closed monoidal category? Would we get a product for free?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (5)
-
David Leduc -
Gordon Plotkin -
Rasmus Møgelberg -
Robert Seely -
soloviev＠irit.fr