Date: Tue, 5 Jul 1994 08:56:06 +0500 (GMT+4:00)
From: categories <cat-dist@mta.ca>
Subject: Categorical completeness results for the simply-typed lambda calculus.o

Date: Mon, 04 Jul 94 18:35:50 +0100
From: Alex Simpson <als@dcs.ed.ac.uk>


I would like to know if the results below are folklore. They don't
seem to be, as some recent papers have given lengthy proofs of special
cases. On the other hand, they do follow rather easily from an old result
due to Statman.

The results concern two categorical notions of completeness for
beta-eta conversion relative to the interpretation of the simply-typed
lambda-calculus in cartesian closed categories.


Let C be any CCC (not necessarily with finite limits).

Let I_X be the initial CCC generated by a nonempty set X of objects.

We say that beta-eta conversion has a COMPLETE INTERPRETATION IN C
if there is a faithful CC-functor from I_X to C.

We say that beta-eta conversion is COMPLETE FOR C if the class of all
CC-functors from I_X to C is collectively faithful.

(REMARK. These two definitions do not depend upon X as there is a
faithful CC-functor from C_X to C_1, where 1 is a singleton set.)


EXAMPLES. One category in which beta-eta conversion has a complete
interpretation is the category of sets. (This essentially follows from
Friedman's completeness theorem. The inclusion of product types makes
no significant difference. This latter remark also applies below, e.g.
to the quoted Statman theorem.) It is clear that if beta-eta
conversion has a complete interpretation in any C then it is also
complete for C. The converse does not hold: the category of finite
sets is complete but has no complete interpretation. (That it has no
complete interpretation was observed by Friedman. That it is complete
essentially follows from the Plotkin/Statman finite model theorem.)
Finally, for a trivial example of a C for which beta-eta conversion is
not complete, take C to be any cartesian closed preorder.


The results give necessary and sufficient conditions on C for the
two forms of completeness to hold.

THEOREM 1. Beta-eta conversion has a complete interpretation in C iff
C has an endomorphism all of whose iterates are distinct.

THEOREM 2. Beta-eta conversion is complete for C iff C is not a preorder.


Just some brief comments on the proofs. The stronger result is
Theorem 1. Theorem 2 can be derived from it by showing that if C is
not a preorder then C^omega (the countably infinite power of C) has a
"non-repeating" endomorphism as required by Theorem 1. Theorem 2 can
also be proved by mimicking the full type hierarchy over a finite set
within C, or alternatively by using Statman's characterization of
beta-eta conversion as a maximal congruence relation on closed terms
satisfying "typical ambiguity".

Theorem 1 is proved using a different Statman result. We use sigma to
range over types defined using exponentials and finite products from
one base type, 0. We use L,M,N to range over closed terms in the
simply-typed lambda-calculus with types as above.  We use =be for
beta-eta equality between terms.

Define the type T = (0 -> 0 -> 0) -> (0 ->0).

THEOREM (Statman [1]). For any sigma there is an L of type sigma -> T
such that, for all M, N of type sigma, M =be N iff L(M) =be L(N).

To prove Theorem 1, let a: A --> A be a non-repeating endomorphism
in C. One defines a CC-functor, F, from I_{0} to C by setting:

  F(0) = (A -> A) -> (A -> A).

One can show that F is faithful on the hom-set I_{0}(1,T) (by
encoding binary trees as Church numerals in F(0)). It follows
from Statman's theorem above that F is faithful.

[1] Statman, R.
    On the existence of closed terms in the typed lambda-calculus I.
    In Hindley, J. R. and Seldin, J. P. eds.
    To H. B. Curry Essays on Combinatory Logic, Lambda Calculus and
      Formalism.
    Academic Press.
    1980.

-----------------------------------------------------------------------------
Alex Simpson                       email: Alex.Simpson@dcs.ed.ac.uk
LFCS, Dept. of Computer Science,
University of Edinburgh,
Edinburgh EH9 3JZ, UK.             Tel:   +44 (0)31 650 5113

Date: Wed, 6 Jul 1994 21:50:43 +0500 (GMT+4:00)
From: categories <cat-dist@mta.ca>
Subject: Re: Categorical completeness results for the simply-typed lambda calculus.

Date: Wed, 6 Jul 94 14:25:55 EDT
From: Djordje Cubric <cubric@triples.math.mcgill.ca>

I would like to make ``a point of an empty set'' and say that Friedman's
completeness theorem for typed lambda calculus (with appropriate changes)
implies the completeness result for free cartesian closed categories (as
mentioned in a recent posting of Alex Simpson) provided that one proves
first that in a free ccc all objects have a global support. One way to do
that is to prove the confluence for the appropriate system of reductions.
Some of the recent papers were dealing with these reductions.
One can see that the completeness holds even when the free ccc has also free
arrows among freely generated types.


Djordje Cubric