A question and a comment about untyped lambda calculus

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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s