product for free

product for free

[David Leduc]

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/ ]

Re: product for free

[soloviev]

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/ ]

Re: product for free

[Rasmus Møgelberg]

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/ ]

Re: product for free

[Gordon Plotkin]

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/ ]

Re: product for free

[Robert Seely]

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/ ]