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