Partitioning predicates and substitution; diabolical and angelical nondeterminism

Partitioning predicates and substitution; diabolical and angelical nondeterminism.

Anyone involved with the formal semantics of if $B$ then so else ${S}_{1}$ Fi

has encountered the tautology

(0) $\left( {B ∧ {P}{0}}\right) \vee \left( {¬ B ∧ {P}{1}}\right) \equiv \left( {¬ {B}{v}{P}{0}}\right) ∧ \left( {{B}{v}{P}{1}}\right)$

This little note primarily deals with a generalisation of the latter formula.

Some nomenclature and notation

• We call X a "predicate" (or "boolean structure") on some space if it is a boolean expression in (or a boolean function applied to) the coordinates of (or the variables spanning) that space. (End of a.)
• Let $X$ be a predicate on some space; with $[X]$ we then denote $X$ universally quantified over (the coordinates of) that space. (End of $\bullet$ .) Functional application is denoted by an infix period, left-associative and with the highest binding power of all operators. (End of $\bullet$ .)
• With $B$ and $R$ boolean functions of some (under-stood) type, and $x$ a dummy of that type, the "numerical quantifier" $\underline{\mathbf{N}}$ is given by

$\left( {\underline{N}x;\underline{B}.x;\underline{R}.x}\right) =$ the number of distinct solutions

(End of $\bullet$ .)

The connection between existential and numerical quantification is

(1) $\left( {{\underline{\mathrm{E}}}{x} : {B}{.}x : {R}{.}x}\right) \equiv \left( {{\underline{\mathrm{N}}}{x} : {B}{.}x : {R}{.}x}\right) ≠ 0$ that between universal and numerical quantification is (Ax: B.x: R.x) = (Nx: B.x: ¬R.x) = 0 (End of Some nomenclature and notation.)

In the following "chosen" is the name of some type (e.g. integer, or the colours of the spectrum) independent of the space that will be introduced in the next sentence.

Let $B$ be a function that, applied to a chosen argument, yields as value a predicate on some space, and let $c$ be a chasen dummy.

Then

(N c: B. c: f r u e)

denotes a natural structure on that same space, and

(\underline {{N}} c: \mathbb {B}. c: t r u e) = 1

denotes a predicate on that space.

We now define "the B.c's are a set of partitioning predicates" to mean $\left\lbrack {\left( {{\mathrm{N}}_{\mathrm{C}} : \mathrm{B}.\mathrm{C} : \text{true}}\right) = {1}^{\prime }}\right\rbrack$ ,i.e. in each point of the space under consideration,precisely one of the B.c's holds.

with R a function of the same type as B and the B.c's being a set of partitioning predicates,

we have

[ (\underline {{E}} c: B. c: R. c) \equiv (\underline {{A}} c: B. c: R. c) ]

\begin{array}{l} \mathrm {P r o o f} [ (\mathrm {N c}: \mathrm {B . c : t r u e}) = 1 ] \ = {\mathrm {l a w o f t h e E x c l u d e d M i d d l e} } \ [ (N c: B. c: R. c \vee ¬ R. c) = 1 ] \ = {\mathrm {P r o p e r i e s} \mathrm {o f} \underline {{N}} } \ [ (\underline {{N c}}; B. c: R. c) + (\underline {{N c}}; B. c; ¬ R. c) = 1 ] \ ⇒ {(N \dots) y i e l d s a n a t u r a l v a l u e, h e n c e \ \mathrm {p r e c i s e l y} 1 \mathrm {o f t h e a d d e n a e q u a l s o f} \ [ (\underline {{N}} c: B. c: R. c) ≠ 0 \equiv (\underline {{N}} c: B. c: ¬ R. c) = 0 ] \ = {(1) a n d (2) } \ [ (\underline {{E}} c: B. c: R. c) \equiv (\underline {{A}} c: B. c: R. c) ] \ \end{array}

(End of Proof.)

Alternatively, the B.c's being a set of partitioning predicates, we could have associated with them a chosen structure C on the space in question, satisfying

(A: true: [B.C ≡ c=C])

Then, (4) can be established by observing

\begin{array}{l} [ (\underline {{E c}}; B. c: R. c) \equiv (\underline {{A c}}; B. c: R. c) ] \ = {(5) } \ [ (\underline {{E}} c: c = C: R. c) \equiv (\underline {{A}} c: c = C: R. c) ] \ = {\mathrm {o n e - p o i n t r u l e s} } \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s} \ \text {t r u e ,} \end{array} \right} \ \end{array}

and it is the latter argument that connects partitioning predicates to substitution.

Remark Note that, as a special consequence, with S a function from booleans to statements,

if $B$ then Strue else S=false

can (at least symbolically) be rendered by S.B. (End of Remark.)

The generalization From (0) to (4) corresponds to the transition from the alternative clause to the case statement that, with S a statement-valued function of a chosen argument could be rendered by - with "::" short for :: true:

(6) ${f}^{\rho }\left( {{\mathbb{I}}{c} : B,c \rightarrow S,c}\right) {f}{i}^{\rho }$

Remark. (6) is a generalization of the guarded-command notation in which our original conditional statement is written as

i f B \rightarrow S O [ ] i B \rightarrow S 1

(End of Remark.)

In terms of weakest preconditions, two definitions of the semantics of (6) now present themselves:

(7) [wp ("i $\rho \left( {\mathbb{I}c : B.c \rightarrow S.c{\rho }_{E}^{p},X}\right) \equiv \left( {Ec : B.c : w\rho \left( {S.c,X}\right) }\right) \rbrack$ (8) [wp ("iP([C:: B.c → S.c], X) ≡ (A. C:: B.C:: w p(S.c, X)))) , which, in view of (4), are equivalent for B.c's that form a partitioning set of predicates.

In the case statement, nondeterminism is introduced if its guards don't necessarily exclude each other, e.g. admitting a B that satisfies

(q) $\left\lbrack {\left( {\underline{N}c : B.c : f r u e}\right) ≥ 1}\right\rbrack$

In view of (1), (9) is equivalent to [(Ec: B.c. true)]; it excludes points in space where none of the guards holds. If $B^{\prime}$ satisfies (9) we have

(10) $\left\lbrack {\left( {{E}{C} : {B.C} : R.C}\right) \Leftarrow \left( {{A}{C} : {B.C} : R.C}\right) }\right\rbrack$

[Proof) [ (Nc: B.c: true) ≥ 1]

\begin{array}{l} = {\mathrm {E x c l u d e d M i d d l e a n d P r o p e r t i e s} \cap N } \ [ (N c: B. c: R. c) + (N c: B. c: 7 R. c) ≥ 1 ] \ ⇒ {\mathrm {a t m o s t o m e o f t h e a d d e n d a e q u a l s} 0 } \ [ (\mathrm {N c}: \mathrm {B . c . R . c}) ≠ 0 \Leftarrow (\mathrm {N c}: \mathrm {B . c .} ¬ \mathrm {R . c}) = 0 ] \ = {(1) a n d (2) } \ [ (\underline {{E}} c: B. c: R. c) \not \Leftarrow (\underline {{A}} c: B. c: R. c) ] \ \end{array}

(End of Proof.)

C.A.R. Hoare dubbed defini tions (7) and (8) "angelical" and "diabolical" nondeterminism. Definition (7) gives the precondition under which the case statement establishes X provided the nondeterminism is resolved by a most cooperative daemon; (8) gives that precondit iom, no matter how uncooperative the daemon. The latter implies the former.

Pasadena, 21 March 1986

pror. dr. Edsger W. Dgksta

Department of Computer Sciences

The University of Texas at Austin

Austin, TX. 78712 - 1188

United States of America.

PS. The above is mostly a synsthesis of EwD 834 and