[Prev][Next][Index][Thread]
a question on type-free objs
A QUESTION ON TYPES AS OBJECTS OF CCC's
(and a little victory for proof-theorists !)
Given a category C and objects a, b we all know what a RETRACTION
of a into b is. Denote it by a<b.
Consider then the following notion:
In C a morphism p form c to d is PRINCIPAL if
for all f form c to d there exists g form c to c such that
f = pog .
(Warning: no unicity is required. E.g. goedel-numberings are principal
morphisms from numbers to partial recursive functions, in the
category of numbered sets, by the s-m-n theorem).
(Notation: In a CCC, write a arw b for the exponent).
FACT (easy): Let C be a CCC and t its terminal obj. Then
(1) (a arw a) < a IMPLIES
t<a AND there exists p principal from a to a arw a AND axa < a .
Can category theorists, who are so familiar with morphisms (principal and
not), retractions etc... answer, with their usual tools, the following:
QUESTION:
Does the reverse implication of (1) hold?
Eugenio Moggi and I have an answer to this (MFCS, Prague 1984, LNCS 176; we
are revising the paper for TCS) inspired by work of H.B. Curry,
surely a proof-theorist, in the 30's. It is entirely based on the
syntax of lambda calculus. A proof not based on syntax could bear some
information on the categorical meaning of "type-free functional
completeness", as principal morphisms characterize it .
(A category-theorist may look at our paper and try to mimick equations
>from proof theory by diagram chasing. But this would not work....)
Looking for an answer, we must aknowledge the priority of proof theory
in answering such a model theoretic question....
G.L.