[Prev][Next][Index][Thread]
Embedding free CCC into SET
Date: Mon, 3 Aug 92 14:02:00 EDT
I would like to announce that a draft of a paper "On Free CCC" (by me)
is available from ftp triples.math.mcgill.ca. The paper contains a
proof of the following:
Theorem: Let C be a free cartesian closed category. Then there exists a
faithful structure preserving functor F:C->Set.
Isn't it just the H. Friedman's completeness result for the typed
lambda calculus? NO. One has also to show that in the free cartesian
closed category all the arrows into the terminal object are epi.
We prove the result using Mints' reductions (but with the repaired proof).
Along the way we conclude also that:
Mints reductions are weakly normalizing, the strategy being: first do
all eta-like expansions (with the restrictions) and
then beta-like reductions.
To get the file (if you can read ps files) do:
ftp triples.math.mcgill.ca
Name: anonymous
Password: "your e-mail address"
>cd pub/cubric
>binary
>get frccc.ps
>quit
If you can't read ps files there are also frccc.dvi and frccc.tex (which needs
Barr's diagram.tex macros and they are at the same ftp site except under
pub/texmacros). In case of any problems I'll gladly send you a copy by
regular mail. Any comments are welcome.
Djordje Cubric