The regularity calculus: a second trial

The regularly calculates: a second trial

(This is a successor to the incompleted AvG36/ EWD882: "The regularity calculus: a first trial" and consequently owes a lot to A.J.M. van Gasteren. The absence of her initials on top of this text is explained by the sad circumstance that I have to carry out my second trial without her guidance.)

We consider regular expressions built from the two constants 0 and 1 , the letters from some alphabet, and three constructors.

Axiom 0 The constants O and 1 , and the letters of the alphabet are all different regular expressions.

Unless mentioned otherwise, a , b , c , and d are in the formulae in the sequel variables of type "regular expression".

Axiom 1 The expression $a$ is regular. The infix operator (constructor) - pronounced "bar" is symmetric, idempotent, and associative, i.e.

[{a}^{\prime }\left\lbrack {{b}^{\prime } = {b}^{\prime }}\right\rbrack a\text{,}] [{a}^{2} + {2a} = 8{b}^{2}] $(a| b)| c = a| (b| c)$

Synctic convention. In view of the associativity of $\mathbb{I}$ , we allow ourselves the omission of parentheses. Of the three constructors, $\mathbb{I}$ is given the lowest binding power. (End of Syntactic convention.)

On regular expressions, the relation $≤$ -pro- nounced "at most" - is defined by

a ≤ b \equiv a \bigr ] b = b

Theorem 0 The relation

reflexive: $a ≤ a$

transitive: $a ≤ b ∧ b ≤ c ⇒ a ≤ c$

antisymmetric: $a ≤ b ∧ b ≤ a ⇒ a = b$ .

Note that reflexivity and antisymmetry can be combined into $a ≤ b ∧ b ≤ a \equiv a = b $ .

Proof Reflexivity follows from the idempotence of $\mathbb{I}$

Comment The last line of above proof reveals that "antisymmetry" is an unfortunate name for the property it denotes. (End of Comment.)

Theorem 1 $a ≤ a| b$

Proof true.

\begin{array}{l} = {A x i o m 1 } \ a ∥ a ∥ b = a ∥ b \ = {\mathrm {d e f i n i t i o n} o f ≤ 3 \ a ≤ a ∥ b (\mathrm {E n d o f P r o o f .}) \ \end{array}

Remark Note how our syntactic convention has shortened the proof by one step. Without it, we would have been forced to write

true

\begin{array}{l} = {A x i o m 1, i d e m p o t e n c e } \ (a ∥ a) ∥ b = a ∥ b \ = {\mathrm {A x i o m 1 , a s s o c i a t i v i t y} } \ a \Vdash (a \Vdash b) = a \Vdash b \ = {\mathrm {d e f i n i t i o n} o f ≤ 3 \ a ≤ a ] b \ \end{array}

(End of Remark.)

Theorem 2 $a \Vdash b ≤ c \equiv a ≤ c ∧ b ≤ c$

Proof

\begin{array}{l} a ] b ≤ c \ = {\mathrm {T h e o r e m} 1 } \ a ≤ a ∥ b \wedge b ≤ a ∥ b \wedge a ∥ b ≤ c \ ⇒ {\mathrm {T h e o r e m} 0, \mathrm {t r a n s i t i v i t y} \mathrm {t w i c e} } \ a ≤ c ∧ b ≤ c \ = {\mathrm {d e f i n i t i o n} o f ≤ 3 \ a ∥ c = c \wedge b ∥ c = c \ ⇒ {\text {L e i b n i z} } \ a \Vdash (b \Vdash c) = c \ = {\mathrm {d e f i n i t i o n} o p ≤ 3 \ a ] b ≤ c (\mathrm {E n d o f P r o o f}). \ \end{array}

Theorem 3 The $\mathbb{I}$ is monotonic, i.e.

a ≤ b ⇒ a ] c ≤ b ] c

Proof

\begin{array}{l} a ≤ b \ = {\mathrm {d e f i n i t i o n} o p ≤ 3 \ a ∥ b = b \ ⇒ {\mathrm {L e i b o n i z} } \ a \bigr ] b \bigr ] c = b \bigr ] c \ \end{array}

EWD902-3

\begin{array}{l} = {A x i o m 1 } \ (a ∥ c) ∥ (b ∥ c) = b ∥ c \ = {\mathrm {d e f i n i t i o n} o f ≤ 3 \ a \ll c ≤ b ] c (\mathrm {E n d o f P r o o f .}) \ \end{array}

Remark As we have only used that $\mathbb{I}$ is symmetric, idempotent, and associative, the above is a special instance of a rather general state of affairs. (End of Remark.)

Our second constructor, called "concatenation", indicated by juxtaposition, and not pronounced, is introduced by

Axiom 2 The expression ab is regular. The (invisible) infix operator of concatenation is associative, i.e.

(a b) c = a (b c)

Synactic convention In view of the associativity of concatenation, we allow ourselves the omission of parentheses. Concatenation has a higher binding power than the $\mathbb{I}$ , i.e. $ab \ll c = (ab) \gg c$ . (End of Syntactic convention.)

Concatenation and I are connected by

Axiom 3 Concatenation distributes in both direc. tions over the I , i.e.

\begin{array}{l} (a ∥ b) c = a c ∥ b c \ a (b ] c) = a b ] a c \ \end{array}

Theorem 4. Concatenation is monotonic in both its arguments, i.e.

a ≤ b ⇒ a c ≤ b c

b ≤ c ⇒ a b ≤ a c

Corollary $a ≤ b ∧ c ≤ d ⇒ {ac} ≤ {bd}$

Proof of Theorem 4

\begin{array}{l} a < b \ = {\mathrm {d e f .} \varphi ≤ 3 \ a ∥ b = b \ ⇒ {\mathrm {L e i b n i z} } \ (a ∥ b) c = b c \ = {A x i o m 3 } \ a c ∥ b c = b c \ = {d e p. o f ≤ 3 a c ≤ b c \ \end{array}

\begin{array}{l} b ≤ c \ = {\mathrm {d e f .} o f ≤ } \ b \vert c = c \ ⇒ {\text {L e i b n i z} } \ a (b) [ c) = a c \ = {A x i o m 3 } \ a b ] a c = a c \ = {\mathrm {d e f .} o p ≤ 3 \ a b ≤ a c \ \end{array}

(End of Proof of Theorem 4.)

Before introducing unit elements for the two above constructors, we recall the general

Theorem For a binary operator with a left and a right unit element, the unit element is unique.

Proof Denoting the unit elements by $L$ and $R$ respectively and the operator by juxtaposition we observe

\begin{array}{l} (\underline {{A}} x, y: L x = x \wedge y R = y) \ ⇒ {x := \overline {{R}}; y := L } \ L R = R ∧ L R = L \ \end{array}

⇒ {L e i b n i z }

L = R

(E n d o f P r o o f.)

For the symmetric I , the theorem is only of mild interest.

Axiom 4 Constant $0$ is the unit element of $\mathbb{I}$

i.e.

a ∥ 0 = a, 0 ∥ a = a, o r 0 ≤ a

Axiom 5 Constant 1 is the unit element of concate- nation, i.e.

1 a = a \mathrm {a n d} a 1 = a.

\mathrm {A x i o m} 6 a b = 0 \equiv a = 0 \vee b = 0

\mathrm {C o r o l l a r y} 1 a 0 = 0 \mathrm {a n d} 0 b = 0

Our last constructor, called "closure", indicated by a postfix * with the highest binding power and pronounced "star", satisfies

\mathrm {A x i o m} \mathbb {Z} (a \Vdash b) ^ {} = (a ^ {} b ^ {}) ^ {}

f x i o m 8 (a b) ^ {} = 1 ∥ a (b a) ^ {} b

\mathrm {T h e o r e m 5} a ^ {} = 1 \mathrm {I I} a a ^ {} \mathrm {a n d} b ^ {} = 1 \mathrm {I I} b ^ {} b

Proof. From Axiom 8 with $b := 1$ and $a := 1$ respectively, and Axiom 5. (End of Proof.)

Our next theorem connects the two constants:

Theorem 6 ${0}^{ * } = 1$

Proof true.

\begin{array}{l} = {\mathrm {T h e o r e m} 5 \mathrm {w i t h} a := 0 } \ 0 ^ {} = 1 ] 0 0 ^ {} \ = {\mathrm {C o r o l a r y} 1 \mathrm {w i t h} b := 0 ^ {} } \ 0 ^ {} = 1 ∥ 0 \ = {A x i o m 4 w i t h a := 1 } \ 0 ^ {x} = 1 \qquad (\mathrm {E n d o f P r o o f .}) \ \end{array}

Taking Axiom 7 into account as well, we can now justify the name "closure":

Theorem 7 The $^ \text{喜}$ is idempotent, i.e. $a^{\star} = a^{\star \star}$

Proof true.

\begin{array}{l} = {A x i o m 7 w i t h b := 0 } \ (a) 0 ^ {} = (a ^ {} 0 ^ {}) ^ {} \ = {\mathrm {T h e o r e m} 6 } \ (a \Vert 0) ^ {} = (a ^ {} 1) ^ {} \ = {A x i o m s 4 8 5 } \ a ^ {} = a ^ {} a ^ {} \ \end{array}

Theorem 8 $a ≤ {a}^{ * }$

Proof true.

$a ≤ {a}^{ * }$ (End of Proof.)

\begin{array}{l} = {\mathrm {T h e o r e m} 5, \mathrm {u n f o l d i n g o n c e} } \ a ^ {} = 1 ∥ a (1 ∥ a a ^ {}) \ = {A x i o m s 3 8 5 } \ a ^ {} = 1 ] a ] a a a ^ {} \ ⇒ {\mathrm {T h e o r e m} 1 } \ \end{array}