Three very little problems from Eindhoven

Three very little problems from Eindhoven

In my correspondence with Wim Feigen, he mentioned in the last months three little prob- lems, which are nice enough not to be for- gotten. Hence this note, which is purely for the record, and possibly for the instruction of my students. All in this note has been thought of by others before.

An "endofunction" is, by definition, a function whose value and whose argument are of the same type. Let $f$ be an endo-function that is idempotent and surjective, i.e.

(0) $f\left( {f \cdot x}\right) = f \cdot x\;$ for all $x\;\therefore$ and (1) $\left\langle {\exists y : f.y = x}\right\rangle$ for all $x$ . show that $f$ is the identity function, i.e. (2) $f \cdot x = x\;$ for all $x$ .

To prove this, we observe for any $x$

$$ f \cdot x = x $$

$$ \begin{array}{l} = {(1), i. e. \mathrm {l e t} y \mathrm {s a t i s f y} f \cdot y = x } \ f _ {\cdot} (f \cdot y) = f \cdot y \ = \left{ \begin{array}{l l} (0) & \mathrm {w i t h} x := y \ \mathrm {t r u e} \end{array} \right} \ \end{array} $$

The proof is not difficult to design.

given (0), like demonstrandum (2), e quates two expressions that only differ by 1 in their number of f-applications, (1) is the only given that equates something to the right-hand side of (2).

Finally, note that we did not build the proof on the terms "idempotent", "surjective" and "identity function", but on the formal definitions of these concepts.

Let $N$ be a natural number such that $N \geq 1$ , and let $f$ be an endofunction such that $f^N$ has exactly 1 fixpoint; show, that $f$ has exactly 1 fixpoint.

In the problem statement, two "new" elements entered the picture: the notation "fN" and the notion "fixpoint"; we deal with the first one first.

For endofunction $f$ and natural $n$ ,

(3) ${f}^{0}x = x$ for all $x$ ${f}^{n + 1} \cdot x = {f}^{n} \cdot \left( {f \cdot x}\right)$ for all $x,n$

The function $f^n$ is sometimes called a "functional iteration" of $f$ . About functional iteration we shall need the following lemma

$$ (5) \qquad f ^ {n}. (f. x) = f. (f ^ {n}. x) \qquad \mathrm {f o r a l l} x, n. $$

Proof of (5). The recursive definition (3), (4) of $f^n$ and the fact that (5) is a proof obligation "for all $n$ ", make a proof by mathematical induction all but mandatory. Here we go.

For the base we have to demonstrate (5) with $n = 0$ :

$$ \begin{array}{l} p ^ {0} (f. x) = f _ {.} (f ^ {0}. x) \ = {3, \mathrm {t w i c e} } \ (f, x) = f. (x) \ = {\mathrm {r e d u n d a n c y o f p a r e n t h e s e s} } \ \end{array} $$

For the step, we have to imply (5) with $n := N + 1$ by (5) with $n \leq N$ . It is customary not to introduce the extra identifier $N$ and to use $n$ instead, and to label the appeals to (5) with $n \leq N$ by the magic clause "ex hypothes". We shall follow the custom,

and observe for any $x,n$

$$ \begin{array}{l} f ^ {n + 1}. (f \cdot x) \ = {(4) \mathrm {w i t h} x := (f. x) } \ f ^ {n} \cdot (f \cdot (f \cdot x)) \ = {e x h y p o t h e s e, i. e. (5) w i t h x := (f. x) } \ f. (f ^ {n}. (f ^ {y} \cdot x)) \ = {4 } \ f: (f ^ {n + 1}, x) \ \end{array} $$

(End of Proof of (5).)

Note. The proof of (5) has been included for purely educational reasons: it is one of a class of thousands and thousands, and, "if you have seen one of them, you have seen them all". The structure of the above proof is traditionally captured by the expression "mathematical induction over $n$ ". (End of note.)

Aside With functional composition $\theta$ de-

fined by

$$ (f \circ g) \cdot x = f \cdot (g \cdot x), $$

(5) can be formulated as

$$ f ^ {n} \circ f = f _ {0} f ^ {n} $$

Above, the step has been proved with two different instantiations for $x$ in (4). For-ulate (4) and the proof of the step in terms of the functional composition

operator $0$ , and you will discover to need that the latter is associative, i.e.

$$ (f \circ g) ^ {\circ} h = f ^ {\circ} (g ^ {\circ} h) \quad \mathrm {f o r a l l} f, g, h. $$

(End of A)

Let us now deal with the notion of a "fixpoint": " $x$ is a fixpoint of $f$ " means $f.x = x$ . A very simple lemma connects fixpoints and functional iteration: any fixpoint of $f$ is also a fixpoint of any functional iteration of $f$ :

(6) ${f}^{n}q = q \Rightarrow {p}^{n} \cdot q = q\;$ for all $f,q,n$ .

The proof is by mathematical induction over $n$ , and -after the above elaboration about mathematical induction- is left, in confidence, to the reader.

After these preliminaries we return to our theorem to be proved. We capture the situation that ${f}^{N}$ has exactly 1 fixpoint by naming it, $p$ say:

(7) ${f}^{N} \cdot p = p$ (8) ${f}^{N}q = q \Rightarrow q = p\;$ for all $q$

Here (7) expresses that $p$ is a fixpoint of ${f}^{N}$ ,and(8)that it is the only one.

On account of (6), the only acceptable candidate for the only fixpoint of $f$ is $p$ , i.e. we propose to demonstrate " $f$ has exactly 1 fixpoint" by showing

(9) $f \cdot p = p$ (10) $f \cdot q = q \Rightarrow q = p$ for all $q$ .

To show (9), we observe

$$ \begin{array}{l} \iff \quad f \cdot p = p \quad \left{ \begin{array}{l} (8) \ 0 \end{array} \right. \mathrm {w i t h} \quad q := f \cdot p \rbrace \ p ^ {N} (f, p) = f \cdot p \ = {(\overline {{5}}) \mathrm {w i t h} n, x := N, p } \ f \cdot (f ^ {N} \cdot p) = f \cdot p \ \Leftrightarrow \quad {\mathrm {L e i b n i z} ^ {\prime} s ^ {\prime} \mathrm {P r i n c i p l e} } \ P ^ {N} \cdot P = P \ = {7 } \ \end{array} $$

true

To show (10) we observe for any $q$

$$ \begin{array}{l} q = p \ \Leftrightarrow {(\delta) } \ p ^ {N}. q = q \ \Leftrightarrow \quad {(6) \mathrm {w i t h} n := N } \ f \cdot q = q \ \end{array} $$

QuoD erat demonstrandum.

This problem was communicated (and per-

haps designed $)\;by\;M.L.\;Hau t u s.$

We consider a set on which is defined a relation which is a "partial order", i.e. is

(11) reflexive: $x \leq x$ (12) antisymmetric: $x \leq y \land y \leq x \Rightarrow x = y$ (13) transitive: $x \leq y \land y \leq z \Rightarrow x \leq z$

All three properties will be used below. Furthermore, our set is postulated to be such that for any two elements $x,y$ the "infimum", denoted by $x\downarrow y$ , exists; it has the defining property that for all $w$

$$ (1 4) \quad w \leq x \downarrow y \equiv w \leq x \wedge w \leq y $$

Instantiating (14) with $w \mathrel{\text{:=}} x \downarrow y$ and using (11), viz. that $\leq$ is reflexive,we directly derive

$$ (1 5) \quad x \downarrow y \leq x \quad \wedge \quad x \downarrow y \leq y $$

a property that will be used below.

Endofunction $f$ is "monotonic" means that for all $x,y$

$$ (1 6) \quad x \leq y \Rightarrow f. x \leq f. y $$

and " $p$ is a least prefixpoint of $p$ " means

(17) ${f}_{1}p \leq p$ (18) $f \cdot x \leq x \Rightarrow p \leq x$ for all $x$

Remark Let $p$ and $q$ each be a least prefixpoint of $f$ . Instantiating (18) with $x := q$ and using $f.g \leq q$ , we derive $p \leq q$ ; similarly we derive $q \leq p$ and on account of (12), viz. that is anti-symmetric, we conclude that $p = q$ . In other words, a function has at most 1 least prefixpoint (it could have none at all). (End of Remark.)

For a partial order with infimum and a monotonic endofunction $f$ with least prefixpoint p -i.e. under validity of (11) through (18) - we are requested to show that $f^2$ has a least prefixpoint, i.e. we have to show the existence of a q such that (19) $f.\left( {p,q}\right) \leq q$ and (20) $f.\left( {f \cdot x}\right) \leq x \Rightarrow q \leq x$ for all $x$ .

It is sweetly reasonable to expect a constructive existence proof , i.e. a speciCific choice for q so that we can prove

(19) and (20). Let us first look at our obligation to prove (19), since that is the simplest of the two.

Since we have not yet used that $\leq$ is transitive,we can decide to conclude (19) for suitably chosen $z$ from

$$ f. (f. q) \leq z \land z \leq q $$

Remark Because is reflexive, we never need to regret that decision: the choices $z := f$ (f.g.) and $z := q$ con. vert the above back into the original (19). (End of Remark.)

Because the structural novelty of (19) is 2 f-applications more to the left of than to its right, we choose, to bridge that gap, $z := f$ .r, with r to be suitably chosen later. We now observe for any $q, r$

$f. \left( {f,q}\right) \leq q$ ${ < \text{ is transient } \mid \end{array}$ $f.\left( {f,q}\right) \leq f.r \land f.r \leq q$ $\Leftrightarrow \left{ \begin{array}{l} f.\text{ is monotonic: (16) with }x,y = \left( {p,q}\right) ,r} \ f,q \leq r \land f,r \leq q \end{array}\right. ,$

a proof-obligation that we can halve

by choosing r and q equal to each other. With $r \mathrel{\text{:=}} g$ we are left with the obligation to demonstrate $f \cdot q \leq q$ for suitably chosen . There are now two reasons for chosing $q \mathrel{\text{:=}} p$ :

(i) given (17) then completes the proof (ii) the consequent of (20) -still to be proved- then becomes the same as the consequent of given (18).

Having established

$\left( {19}^{\prime }\right) \;f.\left( {f.p}\right) \leq p$

our final proof obligation is

$\left( {2{0}^{\prime }}\right) \;f.\left( {p,x}\right) \leq x \Rightarrow p \leq x\;\text{for all}x.$

$\left( {20}^{\prime }\right)$ would be established by a

calculus of the form

$$ p \le x $$

$$ \begin{array}{l} \Leftrightarrow \quad {(1 8) } \ p \cdot x \leq x \ \Leftrightarrow \quad {\texttt {? ? ?} } \ f (f. x) \leq x \ \end{array} $$

but there is no way in which the hint $\left{ {???}\right}$ can justify the last step. (There exist counter examples.) This is the

moment to exploit a very special structural property of (18): while its consequent is strengthened when x is replaced by a "smaller" y (i.e. satisfying y < x), its antecedent is not necessarily strengthened by that replacement (and might become provable).

Remark The phenomenon usually occurs when a quantity -like $p$ in this example has been given as the extreme solution of an equation. We encounter the same situation when an induction hypothesis is strengthened in order to make the induction step provable. This third problem is included because it presents such a nice example of the phenomenon. (End of Remark.)

We use the existence of the infimum, in particular (15) to construct an expression that is "smaller" than $x$ . After the introduction of $\downarrow$ , it has to be eliminated again; to the right of $\leq$ we do this via (14) - what else? and to the left of $\leq$ via (15) - what else?

We observe for any $x$

$$ \begin{array}{l} \Leftarrow \quad P \leq x \quad {1 5) \mathrm {w i t h} y := f \cdot x; \mathrm {t r a n s i t i v i t y o f} p \leq 3 \ p \leq x \downarrow f \cdot x \ \Leftrightarrow \quad {(1 8) \mathrm {w i t h} x := x \downarrow f \cdot x } \ f. (x \downarrow f. x) \leq x \downarrow f. x \ = f (1 4) \mathrm {w i t h} w, y := f (x \downarrow f. x), f. x \ = \left{ \begin{array}{l l} (1 4) \mathrm {w i t h} & w, y := f _ {\cdot} (x \downarrow f _ {\cdot} x), f _ {\cdot} \ f _ {\cdot} (x \downarrow f _ {\cdot} x) \leq x & \wedge f _ {\cdot} (x \downarrow f _ {\cdot} x) \leq f _ {\cdot} x \end{array} \right. \ \Leftrightarrow {(\mathrm {1 5}) \mathrm {w i t h} y := f. x - \mathrm {b o t h c o n j u n c t s}! -, \mathrm {m o n o t o n i c i t y} o p, \mathrm {f}, \mathrm {t r a n s i t i v i t y} o p \leq 3 \ f. (p. x) \leq x \quad f. x \leq p. x \ = {\leq s r e f l e x i v e } \ f. (f. x) \ \end{array} $$

QuoD erat demonstrandum.

Remark The choice $y = f.x$ for (15) in the first step is not surprising. The purpose of appealing to (18) is to eliminate $p$ from the intermediate result, so we should not instantiate with an expression containing $p$ ; $p.x$ is the simplest combination of the two identifiers left. (End of Remark.)

In the above proof development I essentially followed Wim H.J. Feyn, the problem was communicated (and possibly designed) by Henk Doorn bos and Jaap C.S.P. van der Woude; the

latter also constructed a counterexample demonstrating that no {\???} could exist.

I thank the students that attend my current undergraduate course for the incentive to write this down (and Mont Blanc, USA, which repaired my pen and made it again a pleasure to handle.)

Austin, 4 February 1996

proo. ds. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA