At 14:18 +0200 1999/06/04, Mariano Suarez-Alvarez wrote:
>> >A ``category with + and ^ '' is called cartesian closed aditive
>> >category, cf MacLane, Category Theory for the Working Mathematician
>>
>> Is this a suggestion or a theorem?
>
>A definition.
I did not see the connection between the + and ^ of MacLane with those of
lambda calculus: One thing that is needed is that if A, B are in the
category then also A^B = Hom(B, A) is in the category, and that might work
with a Cartesian closed category, which expresses the ^ operator as the
existence of an adjoint.
But why is the existence of
M + N = lambda a b. M(a)(N(a)(b))
the same thing as that the category is additive? For example, the Church
numeral functionals can be added, but they do not take values in an abelian
group.
Exactly how is this connection between the lambda calculus and category
theory described? -- That is, one would expect to know that if one has a
category of some sort, it is equivalent to the lambda calculus, or
something like that.
Hans Aberg
* Email: Hans Aberg <mailto:[EMAIL PROTECTED]>
* Home Page: <http://www.matematik.su.se/~haberg/>
* AMS member listing: <http://www.ams.org/cml/>
