eta rule

• To: types@theory.lcs.mit.edu
• Subject: eta rule
• From: mcvax!margaux.inria.fr!huet@uunet.UU.NET (Gerard Huet)
• Date: Sat, 11 Jun 88 17:53:27 -0200

The eta rule in \-calculus is somewhat of a mystery to me, and I profit
of the current discussion to make two remarks.
1. From the syntactic point of view. There is a beautiful theory of
derivations in beta-\-calculus, due to J.J. Levy, and based on the
notion of residual. The parallel moves lemma may be expressed algebraically
by saying that the category of derivations (appropriately quotiented)
admits pushouts. This theory completely crumbles in the presence of the
eta-rule: beta and eta form (in term rewriting systems jargon) a CRITICAL
PAIR, and it is a syntactic miracle that (\x.(M x) N) conflues to (M N)
in 1 step by either rule. The notion of residual vanishes.
2. From the semantic point of view. One may wonder what is the categorical
interpretation of eta in the CCC models. The answer is IT DEPENDS.
If we model typed lambda-calculus, then eta translates directly as
the equation stating the unicity of Cur. Whereas if we model untyped
\-calculus, with a universal domain and a retract pair, then eta translates
to demanding that the retract is actually an isomorphism.
Gerard Huet

• Prev: Church-Rosser for typed systems
• Next: Reading seminar in logic -- meeting next week
• Index(es):
  • Main
  • Thread