World's most popular travel blog for travel bloggers.

# what is weak extensionality in $\lambda$-calculus?

, ,
Problem Detail:

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.

###### Answered By : Andrej Bauer

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.