[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.