Partitioning predicates and punctual functions (see EWD955)

Partitioning predicates and punctual functions (see EWD955)

Let $f$ be a function from structures to structures, both on the same space. We then have Leibniz's Rule, i.e.

(A $X,Y\therefore \left\lbrack {X = Y}\right\rbrack \Rightarrow \left\lbrack {P,X = P,Y}\right\rbrack$ )

We may have the stronger

(1) $\left{ {\underline{A}{X,Y} : \left\lbrack {X = Y \Rightarrow {P}{1}X = {P}{1}Y}\right\rbrack }\right}$ ,

a state of affairs we characterize by saying " $F$ is a punctual function". In this note we present another characterization of punctual dependence, viz. distribution over partitioning.

In what follows

• green and yellow are some space-independent types (like boolean, real, integer, etc.) C is a green variable
• B is a function from a green argument to a boolean structure and it is partitioning, i.e.

$$ [ (\underset {-} {N} c: \underset {-} {B}. c: t r u e) = 1 ] $$

• $R$ is a function from a green argument to a yellow structure

We now consider the equation in the unknown yellow structure $z$

$\left( 2\right) \;z : \left\lbrack {\left( {{Q}{c} : {B}{c} : Z = R,c}\right) }\right\rbrack$

in which, $B$ being partitioning, it does not matter whether we read A or E for Q - see EWD 955-

In order to show that the solution of (2), if existing, is unique, we first prove Lemma 0 For partinioning B and boolean structure

$$ [ (\mathrm {Q c}: \mathrm {B . c}: X) ] \equiv [ X ] $$

[Qc: B.c: X)

$$ \begin{array}{l} = {E W D 9 5 5 } \ [ (E c: B. c: X) ] \ = {\mathrm {p r e d . c a l o} } \ [ (E c: B. c: t r u e) \wedge X ] \ = {\mathrm {r e l . b e t w e e n} \equiv \mathrm {a n d} \underline {{\mathbf {N}}} } \ [ (\mathrm {N c}; \mathrm {B . C : t r u e}) \geq 1 \land X ] \ = {B i s p a r t i l o n i n g } \ [ X ] \ \end{array} $$

(End of Proof.)

We now observe

$$ \begin{array}{l} [ (\mathrm {Q c}: \mathrm {B . c}: U = \mathrm {R . c}) ] \wedge [ (\mathrm {Q c}: \mathrm {B . c}: V = \mathrm {R . c}) ] \ = {E W D 9 5 5 } \ [ (A c: B. c: U = R. c) ] \wedge [ (A c: B. c: V = R. c) ] \ = {\overline {{p r e d . c a l c .}} } \ [ (A c: B. c: U = R. c \land V = R. c) ] \ \Rightarrow {\mathrm {p r e d . c a l c .} } \ [ (\dot {A} C; B. C: U = V) ] \ = {\mathrm {L e m m a} o } \ [ U = V ] \ \end{array} $$

from which the uniqueness follows.

But does the solution of (2) always exist? It does if "yellow" means "boolean"; then we can write it down in closed form, viz.

(3) (Qc: Bc: Rc)

$$ \begin{array}{l} \mathrm {P r o o f} [ (\underline {{Q}} c: \mathrm {B . c}: (\underline {{Q}} d: \mathrm {B . d}: \mathrm {R . d}) \Rightarrow \mathrm {R . c}) ] (x) \ = {E W D 9 5 5 } \ [ (A c: B. c: (Q d: B. d: R. d) \Rightarrow R. c) ] \ = {\mathrm {p r e d . c a l c} } \ [ (\underline {{Q}} d: B. d: R. d) \Rightarrow (A c: B. c: R. c) ] \ = {E W D 9 5 5 } \ [ (\underline {{Q}} c: B. c: (\underline {{Q}} d: B. d: R. d) \Leftarrow R. c) ] (x x) \ = {E W D 9 S S } \ [ (\underline {{E c}}; B. c: (\underline {{Q d}}; B. d; R. d) \not \Leftarrow R. c) ] \ = {\text {p r e d . c a l c} } \ [ (\underline {{Q}} d: B. d: R. d) \Leftarrow (A c: B. c: R. c) ] \ = {E W D 9 5 5 } \ \end{array} $$

From (x) and (xx) follows that (3) solves (2).

(End of Proof.)

For "yellow" another than boolean, we postulate that (2) has a solution. As Q stands traditionally for A or E , we invent a new notation; in view of the close connection with the case expression, we write the solution of (2) as

(4) (IIc: B.c: R.c)

Note For "yellow" meaning "real" or "integer", I could stand for MIN , MAX, S(um) , or Probuct). For these operations the analogue of the one-point rule holds. (End of Note.)

Now we can formulate

Theorem "function $f$ is punctual"三

$$ [ f. (I) c: B. c: R. c) = (I c: B. c: f. (R. c)) ] $$

$$ \mathrm {f o r a l l} R \mathrm {a n d p a r t i f i o n g} B $$

Proof

$$ L H S \Rightarrow R H S $$

$$ \mathrm {W i t h} [ Z = ([ c: B. c: R. c) ], \mathrm {w e d e r i v e f o r a n y} R \mathrm {a n d} B $$

$$ R H S $$

$$ = {\mathrm {d e f . o f} z } $$

$$ [ f, Z = ([ c: B. c: f. (R. c)) ] $$

$$ = {\mathrm {d e f . o p} [ 1, (2) \mathrm {w i t h} Z, R. c := P. Z, P. (R. c) ] $$

$$ [ (\underline {{Q}} c: B. c: \rho . Z = \rho . (R. c)) ] \quad ( * ) $$

$$ \Leftrightarrow {L H S, i. e. (1) \text {w i t h} X, Y := Z, R. c } $$

$$ [ (Q c; B. c; Z = R. c) ] $$

$$ = {\mathrm {d e f . o f} Z \mathrm {a n d} I, (2) } $$

RHS $\Rightarrow$ LHS

for arbitrary $X$ and $Y$ ,we have to show,using RHS,

$$ [ X = Y \Rightarrow P. X = P. Y ] $$

In view of (xxx) we shall derive this by proper instantia-tion of RHS, viz.

• c ranges over the two boolean structures $X = Y$ and $X \neq Y$
• B is the identity function; in view of $\left\lbrack {\left( {X = Y}\right) \neq \left( {X \neq Y}\right) }\right\rbrack$ , $\left\lbrack {R.\left( {X = Y}\right) = X}\right\rbrack$ and $\left\lbrack {R.\left( {X \neq Y}\right) = Y}\right\rbrack$

With $Z$ ,as above: $\left\lbrack {Z = \left( {\left\lbrack c : B.c : R.c}\right) }\right\rbrack ,Z\text{is with}}\right.$ This instantiation given as the unique solution of (see (2)),with $Q \mathrel{\text{:=}} E$ ,

$$ 2: [ (X = Y \land Z = X) \lor (X \neq Y \land Z = Y) ] $$

of which the -only!- solution $Z$ is given by

$$ [ Z = Y ] $$

After this groundwork we proceed

RHS

$$ \begin{array}{l} = {\mathrm {s e e} (x x x), \mathrm {a n d} Q := A } \ [ (\underset {\sim} {A C}: B. C: f. Z = f. (R. C)) ] \ \Rightarrow {\mathrm {w i t h t h e g i v e n i n s t a n t i a t i o n ,} c := (X = Y) } \ [ X = Y \Rightarrow f. Z = f. (R. (X = Y)) ] \ = {[ Z = Y ] a n d [ R, (X = Y) = X ] a n d (0) } \ [ X = Y \Rightarrow f. Y = f. X ] \ \end{array} $$

(End of Proof.)

Acknowledgement The above was written with A.J.M. van Gasteren looking over my shoulder.

Austin, 14 May 1986

pror. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austn, TX 78712. 1188

United States of America