4
$\begingroup$

I was reading the book lambda calculi , encountered an equality theory called "the rule of weak extensionality", which is shown as follows.

$\frac{M \, = \, N}{\lambda x.M \, = \, \lambda x.N}$

Yes, it is obviously true.

But why it is called the rule of weak extensionality? what is weak? what is extensionality here means?

I think the reason should be interesting.

$\endgroup$
6
$\begingroup$

There are different kinds of equality. Equality is said to be extensional when things are equal when their parts are equal, so to speak:

  1. Equality the elements of $A \times B$ is extensional if, for all $u, v : A \times B$, $u = v$ if and only if $\pi_1(u) = \pi_1(v)$ and $\pi_2(u) = \pi_2(v)$. Here $\pi_1$ and $\pi_2$ are canonical projections. That is, $u$ and $v$ are equal if they have the same components (parts).

  2. Equality of elements of $A \to B$ is extensional if, for all $f, g : A \to B$, $f = g$ if and only if $f(a) = g(a)$ for all $a : A$. That is, $f$ and $g$ are equal if they have the same values (parts).

  3. Equality of sets is equal if, for all sets $S$ and $T$, $S = T$ if and only if $x \in S \Leftrightarrow x \in T$ for all $x$. That is, $S$ and $T$ are equal if they have the same elements (parts).

Equality which is not extensional is called intensional. For instance, if by $A \to B$ we mean programs (pieces of code) which take inputs $A$ and produce outputs $B$ then equality of functions could simply mean equality of the code.

The rules of the $\lambda$-calculus do not specify whether equality is extensional or intensional. They allow for both possibilities. With this in mind we see that it is not entirely clear whether the $\xi$-rule (that's what it's called) $$\frac{M = N}{\lambda x . M = \lambda x . N} \tag{$\xi$}$$ should be part of $\lambda$-calculus. Normally it is, but we could envision a situation in which $\lambda x . M$ gets compiled differently from $\lambda x . N$ for some reason. So much about it being "obviously true".

Personally, I would not call the $\xi$-rule "weak extensionality" because that conveys the wrong idea. It is a congruence rule expressing the fact that $\lambda$-abstraction preserves equality. Another congruence rule is $$\frac{M_1 = M_2 \qquad N_1 = N_2}{M_1 N_1 = M_2 N_2}.$$

If we insist, we can think of the $\xi$-rule as weak form of extensionality in the sense that two $\lambda$-abstractions are equal if their bodies (parts) are equal.

$\endgroup$
  • $\begingroup$ Thank you for your answer. Could you point out some books or sources (ones which are easy to read, not too theoretical ) about this equality theory and lambda things explained in your answer? I really want to go through them. $\endgroup$ – alim Dec 3 '16 at 17:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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