Question: Is there any formulation in terms of category theory of pure untyped lambda calculus, only with alpha-equivalence and beta-reduction, but not with eta-reduction? Please provide links to the relevant sources, which have to contain proofs.
My impression (which could be wrong) is that the answer is NO. It becomes YES with eta-reduction, am I right?
Comment: This is again about pure untyped lambda calculus, only with alpha-equivalence and beta-reduction. compared with my graphic lambda calculus. So, in pure untyped lambda calculus there are only two moves: beta-reduction and (a collection of moves under the) alpha-equivalence. At first view, the graphic lambda calculus has much more moves. Let us neglect the emergent algebra moves, which are exterior to lambda calculus. Still, in graphic lambda calculus there are the fan-out moves and the pruning moves. Compare these moves with the long prose one has to write in order to really explain how alpha-equivalence works and how terms are written, with all rules and moves included so that a non-human computer might apply them.
UPDATE: The question, formulated as: “is lambda-beta representable?” is an open problem by Barendregt and others. See for the precise language the paper GRaph models of lambda-calculus at work, by C. Berline, Math Struct. for Comput. Sci. 16:1-37, 2006, link to ps.