Composition, lambda-calculus, and some more

Composition, $\lambda$ - calculus, and some more

The other day I saw - courtesy Tony Hoare- for the associativity of functional composition a proof of the following structure.

For functions $f,g,h$ we have to show

(0) ${f}{0}\left( {g \circ h}\right) = \left( {{f}{0}g}\right) \circ h$

where $0$ is defined by: for functions $p, q$

(1) ${p}^{ \circ }q = \left( {{\lambda }_{2} : p.\left( {q \cdot z}\right) }\right)$

from the $\lambda$ -calculus we use

(2) ${\left( \lambda x : E\right) }_{\cdot }y =$ "E with $y$ substituted for $x$ "

We observe for any $f,g,h$

$$ f _ {0} (g o h) $$

$= \left{ {\left( 1\right) \text{ with }p,q = f,\left( {g \circ h}\right) }\right}$

$$ (\lambda z: f. ((g o h). z)) $$

$= \left{ {\left( i\right) \text{ with }p,q,z = g,h,x}\right}$

$$ (\lambda z: f. ((\lambda x: g. (h. x)). z)) $$

$= \left{ {\left( 2\right) \text{ with }E,y \mathrel{\text{:=}} g\left( {h.x}\right) ,z}\right}$

$$ (\lambda z: f. (g. (h. z))) $$

$= \left{ \left( 2\right) \text{ with }E,y \mathrel{\text{:=}} f.\left( {g \cdot x}\right) ,h \cdot z}$

$$ (\lambda z: (\lambda x: f. (g. x)) ^ {\cdot}, (h. z)) $$

$= \left{ \begin{array}{l} { 1} \text{ with }p,q,z \end{array}\right. = p,q,x$

$$ (\lambda z: (f \circ g). (h. z)) $$

$= { \left( 1\right)$ with $p,q \mathrel{\text{:=}} \left( {{p}_{0}g}\right) ,h}$

$$ (f o g) \circ h $$

thus having proved (0). The use of the $\lambda$ -calculus enabled us to carry out this proof in terms of equality of functions.

Let us now pursue what happens when we circumvent the λ-calculus and carry the argu-ment out in equality of function applications. Our demonstrandum becomes

(4) $\left( {{f}{0}\left( {g,h}\right) }\right) .z = \left( {\left( {{f}{0}g}\right) \cdot h}\right) .z\quad$ for all $z$ and the definition of functional composition (5) $\left( {p \circ q}\right) \cdot z = p \cdot \left( {q \cdot z}\right) \;$ for all $z\;\therefore$

We observe for any $z$

$$ (p \circ (g o h)). z $$

$$ \begin{array}{l} = \left{ \begin{array}{l l} {(5) w i t h p, q := f, (g o h)} \ {f. ((g o h). z)} \end{array} \right} \ \begin{array}{r l} {p, q} & {:= g, h }} \ {p. (g. (h. z))} & \end{array} \ = {f (5) \mathrm {w i t h} p, q, z := f, g, h. z } \ = \begin{array}{l} {{(5) w i t h p, q := (p o g), h }} \ {((f o g) o h). 2} \end{array} \ \end{array} $$

thus having proved (5). As the instantiations of $p,q$ show, these are in a sense different renderings of the "same" proof, but in another sense the proofs are very different!

In the proof of (0) -as the reader may verify-, the first two steps may be interchanged, and so may the last two; in the proof of (5) -as the reader may verify- the order of the steps is fixed. (The latter proof is, in fact, a genuine instance of "There is only one thing you can do.). Since there is no virtue in spurious freedom this is a reason for prefering the latter.

More important is that the two middle steps of the former proof have completely disappeared in the latter one. We can view them as an artefact of the notation; from a technical point we can observe that, whereas (1) has only two free variables, (5) has three: the additional one enables us to subsume the identification of the subexpression h.z in its instantiation. The more free variables a rewrite rule has, the more powerful it seems! In spite of all we hear in favour of "lifting", the transition from (5) to (1) does not seem an improvement here.

Another striking difference is in the depth of parenthesis nesting. In the latter proof it is homogeneously 2, in the former it begins and ends at 1, but reaches 4 in between (which seems excessive). The observation is made because

the difference is striking, but I hesitate to attach a moral to it. Symbol counts for the results in the former proof yield 7,16,23,16,23,16,7, (sum 108), for the latter 11,11,11,11,11 (sum 55); sum and maximum differ both by a factor of 2.

with thanks to Tony Hoare for exposing me to this example of the $\lambda$ -calculus in action.

Post Scriptum In a hand-out of Tony's on Category Theory I saw a familiar ugliness that we can now recognize as a manifestation of the same phenomenon. In an example he introduces the (would-be) set Russell in the usual way

$$ \mathrm {R u s s e l} = {x \mid x \notin x } $$

and then needs -again in the usual way- an argument by case analysis of a whole para-graph to show that the acceptance of the above definition leads to a contradiction. Had he defined Russel, instead of by (6), by

$$ (7) \quad x \in \mathrm {R u s s e l} \equiv x \notin x \quad \mathrm {f o r a l l} x $$

the instantiation $x \mathrel{\text{:=}}$ Russel would have sufficed to produce the desired contradiction:

$$ R u s s e l \in R u s s e l \equiv R u s s e l \notin R u s s e l $$

It is exactly the same phenomenon: in $\lambda$ -

notation, (6) could be rendered by defining the membership function eRusel by

$$ \epsilon \mathrm {R u s s e l} = (\lambda x: x \notin x) $$

in (7) , this function is applied to a dummy, ready for instantiation.

I knew that the set notation as used in (6) is a notational mistake. (The first $x$ plays a double role: it identifies the dummy and repre-sents the general element.) I also knew from experience that it is almost always more conven-ient to name the membership predicate than to name the set. And now we know the simple reason why.

Austin, 16 September 1989

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA