Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda abstraction because there is nothing to do, kind of a pointless $\beta$-conversion.

So maybe $\eta$-conversion is something really deep and different from this, but, if it is, I don't get it, and I hope you can help me with it.

(Thank you and sorry, I know this is part of the very basics in lambda calculus)

share|improve this question
add comment

4 Answers

up vote 17 down vote accepted

Update [2011-09-20]: I expanded the paragraph about $\eta$-expansion and extensionality. Thanks to Anton Salikhmetov for pointing out a good reference.

$\eta$-conversion $(\lambda x . f x) = f$ is a special case of $\beta$- conversion only in the special case when $f$ is itself an abstraction, e.g., if $f = \lambda y . y y$ then $$(\lambda x . f x) = (\lambda x . (\lambda y . y y) x) =_\beta (\lambda x . x x) =_\alpha f.$$ But what if $f$ is a variable, or an application which does not reduce to an abstraction?

In a way $\eta$-rule is like a special kind of extensionality, but we have to be a bit careful about how that is stated. We can state extensionality as:

  1. for all $\lambda$-terms $M$ and $N$, if $M x = N x$ then $M = N$, or
  2. for all $f, g$ if $\forall x . f x = g x$ then $f = g$.

The first one is a meta-statement about the terms of the $\lambda$-calculus. In it $x$ appears as a formal variable, i.e., it is part of the $\lambda$-calculus. It can be proved from $\beta\eta$-rules, see for example Theorem 2.1.29 in "Lambda Calculus: its Syntax and Semantics" by Barendregt (1985). It can be understood as a statement about all the definable functions, i.e., those which are denotations of $\lambda$-terms.

The second statement is how mathematicians usually understand mathematical statements. The theory of $\lambda$-calculus describes a certain kind of structures, let us call them "$\lambda$-models". A $\lambda$-model might be uncountable, so there is no guarantee that every element of it corresponds to a $\lambda$-term (just like there are more real numbers than there are expressions describing reals). Extensionality then says: if we take any two things $f$ and $g$ in a $\lambda$-model, if $f x = g x$ for all $x$ in the model, then $f = g$. Now even if the model satisfies the $\eta$-rule, it need not satisfy extensionality in this sense. (Reference needed here, and I think we need to be careful how equality is interpreted.)

There are several ways in which we can motivate $\beta$- and $\eta$-conversions. I will randomly pick the category-theoretic one, disguised as $\lambda$-calculus, and someone else can explain other reasons.

Let us consider the typed $\lambda$-calculus (because it is less confusing, but more or less the same reasoning works for the untyped $\lambda$-calculus). One of the basic laws that should holds is the exponential law $$C^{A \times B} \cong (C^B)^A.$$ (I am using notations $A \to B$ and $B^A$ interchangably, picking whichever seems to look better.) What do the isomorphisms $i : C^{A \times B} \to (C^B)^A$ and $j : (C^B)^A \to C^{A \times B}$ look like, written in $\lambda$-calculus? Presumably they would be $$i = \lambda f : C^{A \times B} . \lambda a : A . \lambda b : B . f \langle a, b \rangle$$ and $$j = \lambda g : (C^B)^A . \lambda p : A \times B . g (\pi_1 p) (\pi_2 p).$$ A short calculation with a couple of $\beta$-reductions (including the $\beta$-reductions $\pi_1 \langle a, b \rangle = a$ and $\pi_2 \langle a, b \rangle = b$ for products) tells us that, for every $g : (C^B)^A$ we have $$i (j g) = \lambda a : A . \lambda b : B . g a b.$$ Since $i$ and $j$ are inverses of each other, we expect $i (j g) = g$, but to actually prove this we need to use $\eta$-reduction twice: $$i(j g) = (\lambda a : A . \lambda b : B . g a b) =_\eta (\lambda a : A . g a) =_\eta g.$$ So this is one reason for having $\eta$-reductions. Exercise: which $\eta$-rule is needed to show that $j (i f) = f$?

share|improve this answer
    
"Also, I have heard it said that η-rule is about extensionality of functions. This is false" If you augment the $\beta$-equality axioms and inference rules with the extensionality rule (see my answer), this set of inference rules captures exactly $\beta\eta$-equality, doesn't it? (i.e two terms are equal in this theory iff they are $\beta\eta$-equal) –  Marcin Kotowski Sep 19 '11 at 0:03
    
@Marcin: yes, extensionality implies $\eta$-rule, but not vice versa. How would you derive extensionality from $\beta$- and $\eta$-rules? –  Andrej Bauer Sep 19 '11 at 0:06
1  
let $=$ denote the smallest congruence that contains $=_{\beta}$ and satisfies extensionality (if $Mx=Nx$, then $M=N$). Then $M=N$ iff $M=_{\beta\eta}N$ (see e.g. first chapter of Urzyczyn, Sorensen "Lecture on Curry-Howard isomorphism) and in this sense $\eta$-rule captures the notion of extensionality. –  Marcin Kotowski Sep 19 '11 at 0:22
    
I see, you're thinking of extensionality as a schema, i.e., we prove that it holds for every particular pair of terms $M$ and $N$. I was thinking of extensionality as a statement. I think. Now I have to think about it. –  Andrej Bauer Sep 19 '11 at 4:57
1  
@AndrejBauer I agree that η-rule isn't full extensionality, but don't you think it is still a limited form of extensionality, i.e. it represents a class of obvious cases of extensionality. The original question is looking for motivations and concepts, and in this case I believe that thinking in terms of extensionality is useful (with some care taken of course not to go too far). –  Marc Hamann Sep 20 '11 at 13:06
show 2 more comments

In order to answer this question, we can provide the following quotation from the corresponding monograph “Lambda Calculus. Its Syntax and Semantics“ (Barendregt, 1981):

The point of introducing of $\beta\eta$-reduction is to provide an axiom for provable statements in extensional $\lambda$-calculus [the $\lambda + \text{ext}$ theory, where $\text{ext}$ stands for the rule $M x = N x \Rightarrow M = N$] such that it would have Church–Rosser property.

Proposition. $M =_{\beta\eta} N \Leftrightarrow \lambda\eta \vdash M = N \Leftrightarrow \lambda + \text{ext} \vdash M = N$.

[Its proof is based on the following theorem.]

Theorem (by Curry). The theories $\lambda + \text{ext}$ and $\lambda\eta$ are equivalent… [Its proof consists of two parts: $(\text{ext}) \Rightarrow (\eta)$ and vice versa.]

One of the reasons to consider the system $\lambda\eta$ is that it has a certain property of completeness… [Namely, in the sense of the following theorem.]

Theorem. Let $M$ and $N$ both have a normal form. Then, either $\lambda\eta \vdash M = N$, or $\lambda\eta + M = N$ is inconsistent…

HP-complete [after Hilbert–Post] theories correspond to maximum consistent theories in theory of models for the first-order logic.

share|improve this answer
add comment

$\eta$-reduction captures the notion of extensionality - two functions are considered equal iff they give the same outputs on the same inputs.

One way of formalizing this notion is the following: if we consider the relation $=_{\beta \eta}$, the transitive-reflexive closure of relation $\rightarrow_{\beta\eta}$, it is natural to characterize this relation in terms of inference rules of an equational theory (e.g.: rules of the form: if $M=N$, then $\lambda x.M = \lambda x.N$ and so on - characterizing $=_{\beta}$ requires about 7 rules of this kind).

Now, replacing $=_{\beta}$ with $=_{\beta\eta}$ amounts to introducing the axiom $\lambda x. Mx = M$, which is equivalent to the extensionality rule: if $Mx=Nx$, then $M=N$. This is exactly the notion that two functions equal on all input arguments should be considered identical.

share|improve this answer
    
It is false that extensionality follows from $\eta$-rule. –  Andrej Bauer Sep 19 '11 at 0:00
    
See Theorem 2.1.29 in the monograph by Barendregt (Lambda Calculus and its Semantics, 1985). –  user5456 Sep 19 '11 at 5:17
1  
@Anton: I suppose I am not too happy about the $\xi$-rule. –  Andrej Bauer Sep 19 '11 at 13:02
    
And I am in turn not too happy that happiness and “heard of”-like answers gain more attention than direct relevant quotes with the corresponding references. –  user5456 Sep 20 '11 at 11:34
    
@Anton: It's a popularity contest, didn't you know? ;-) Anyhow, what's with the $\xi$-rule that gets used in Barendregt. I don't recall anyone dragging the $\xi$-rule into discussion. We only have $\alpha$ and $\beta$. –  Andrej Bauer Sep 20 '11 at 14:24
show 3 more comments

Just to add to Andrej's very good answer: the theory of untyped $\lambda$-calculus with $\beta$ and $\eta$ reduction rules satisfies some very nice properties:

  • It is consistent in the sense that there are two terms, for example $\lambda x y.x$ and $\lambda x y.y$ that are not $\beta\eta$ equivalent. This is a consequence of the confluence theorem for $\beta\eta$ reduction.

  • It is a maximal consistent theory in the following sense: if $\iota$ is an
    equivalence relation on terms such that:

    1. It is closed by congruence: $u\ =_\iota\ v \Rightarrow t\ u\ =_\iota\ t\ v$ etc.

    2. It equates 2 non $\beta\eta$ equivalent terms that are normal forms: there exists $t$ and $u$ in normal form such that $t=_\iota u$ and $t\neq_{\beta\eta}u$. Then the theory is inconsistent: for every term $t$, $u$ in normal form, $t=_{\beta\eta\iota}u$.

    This is a consequence of Böhm's theorem.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.