Counting characters

Counting characters

In [0], "factors" are introduced in relation algebra in the usual fashion. I quote the definition of the binary operator $\backslash$ (pronounced "under"):

(7) $\mathrm{{RE}} \smallsetminus \mathrm{T} \equiv \mathrm{{SORE}}$

Instancitating (7) with $R \mathrel{\text{:=}} S \backslash T$ gives -since is reflexive- the "rule of cancelation"

(9) $\operatorname{SOSAT} = \mathrm{T}$

(In [0], other identifiers are used; I have followed its convention of giving $\lambda$ a higher binding power than 0 .)

Four pages later, the operator \\ is used to prove - about the reflexive transitive closure - $R\circ R^{} = R^{}\circ R$ . The ping-pong argument starts with

$$ \begin{array}{r l} & {\mathcal {R} \circ \mathcal {R} ^ {} \subseteq \mathcal {R} ^ {} \circ \mathcal {R}} \ {\equiv} & {{\mathrm {f a c t o r s :} (7) }} \ & {\mathcal {R} ^ {} \subseteq \mathcal {R} \setminus (\mathcal {R} ^ {} \circ \mathcal {R})} \end{array} $$

$$ \begin{array}{r l} {\Leftarrow} & \ & {\quad \mathrm {T h e p r o o f c o n t a i n s a s e c o n d r e f e r e n c e}} \ {\mathrm {t o (7) a n d 2 r e f e r e n c e s t o (9) .}} & \ & {\quad * * * *} \end{array} $$

Instead of constructing the expression

$R \backslash \left( {{R}^{ * } \circ R}\right)$ ,we could have named it, say $K$ ,defining $K$ would have required

(7) $X \in K \equiv R \circ X \in {R}^{ * } \circ R$ ,

and instantiaing this with $x\coloneqq k$ gives the tailored rule of cancelation

$\left( {9}^{\prime }\right) \;R \circ K \subseteq {R}^{ * } \circ R$

The ping-pong argument would then start

$$ R \circ R ^ {} \in R ^ {} \circ R $$

$$ \begin{array}{l} \equiv \left{ \begin{array}{l l} (7 ^ {\prime}) \mathrm {w i t h} X := R ^ {} \end{array} \right} \ \mathbb {R} ^ {} \subseteq K \ \end{array} $$

The introduction of a new identifier $K$ and the 20 characters needed to form ${17}^{\prime }$ and(9')are an investment,but worth the price,because each time we replace $R \backslash \left( {{R}^{ * } \circ R}\right)$ by $K$ ,we save 7 characters,and the complete proof in [0] presents that opportunity 13 times, and after all ${13} \cdot 7 - {20} = {71}$ . It is significant:

I $\cup R \cup R \backslash \left( {{R}^{ * } \circ R}\right) \circ R \backslash \left( {{R}^{ * } \circ R}\right) \subseteq R \backslash \left( {{R}^{ * } \circ R}\right)$

is much less pleasant to deal with than I u R u KoK E K

Excluding the hints, the formulae of the proof offering the 13 opportunities consist of 195 characters. (And after all, 195-91=104)

Why do I spend an evening writing a technical note whose mathematical content is absolutely nil? I think because I wholeheartedly agree with the authors of [O] when they write on pg 1:

"Second, it is not sufficiently recognised that formal methods must combine precision with conciseness.

Amen.

[0] R.C. Backhouse and H. Doornbos "Mathematical Induction Made Calculation". Computing Science Notes 94/16, Department of Mathematics and Computing Science, Eindhoven University of Technology

Petit Jean State Park, AR Saturday 21 May 1994

p r o f. d r. Eds g e r W. D y k s t r a D e p a r t m e n t o f C o m p u t e r S c i e n c e s The University of Texas at Austin Austin, TX 78712-1188 USA