The regularity calculus: a first trial

The regularity calculus: a first trial

We consider regular expressions built from a constant, letters from an alphabet and three constructors.

Axiom 0 Each letter is a regular expression

In the sequel, $a$ , $b$ ,and $c$ are variables of type "regular expression".

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

a ∥ b = b ∥ a

a ] a = a

(a ∥ b) ∥ c = a ∥ (b ∥ c)

Synthcic convention. In view of the associativity of $D$ we allow ourselves the omission of parentheses. Of our three constructors, $D$ is given the lowest binding power. (End of Synthcic convention.)

On regular expressions the relation $≤$ - pronounced

a ≤ b \equiv a ∥ b = b

Theorem 0 The relation $≤$ is

reflexive: $a ≤ a$

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

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

Note that reflexivity and anisymmetry can be com

$b$ ined into $a ≤ b ∧ b ≤ a = a = b . $

Proof Reflexivity follows from the idempotence of $\mathbb{P}$ 1, transitivity follows from the associativity of $\mathbb{P}$ , and antisymmetry follows from the symmetry of $\mathbb{P}$ (End of Proof.)

Theorem 1 The I is monotonic, i.e.

a ≤ b ⇒ a ∥ c ≤ b ∥ c

Proof $a ≤ b$

\begin{array}{l} = {d e f. o f ≤ } \ a ] b = b \ ⇒ {\mathrm {L e i b n i z} } \ a \llbracket b \rrbracket c = b \rrbracket c \ = {\mathrm {p r o p e r t i e s} } \ (a ∥ c) ∥ (b ∥ c) = (b ∥ c) \ = {\mathrm {d e f . o f} ≤ } \ a \Vdash c \le b \Vdash c \ \end{array}

(End of Proof.)

We introduce the constant 0 as special regular expression: it is the unit element of I :

The expression 0 is regular and satisfies

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

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

A v G _ {3 6} / E W D 8 8 2 - 2

(a b) c = a (b c)

Synthetic convention. In view of the associativity of concatenation we allow ourselves the omission of parentheses. Concatenation has a higher binding power than the I , i.e. ab IIc = (ab) II c . (End of Synthetic convention.)

Axiom 4 Concatenation distributes in both directions 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 2. Concatenation is monotonic in both its arguments, i.e.

a ≤ b ⇒ a c ≤ b c

b < c ⇒ a b < a c

\mathrm {C o r o l l a r y} 0. a ≤ b ∧ c ≤ d ⇒ a c ≤ b d

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

\begin{array}{l} b \le c \ = {\mathrm {d e f . o f} ≤ } \ b \Vdash c = c \ ⇒ {\text {L e i b n i z} } \ a (b ∥ c) = a c \ = {A x _ {1} \cos 4 } \ a b ∥ a c = a c \ = {\mathrm {d e f . o p} ≤ } \ a b ≤ a c \ \end{array}

(End of Proof of Theorem 2.)

Axiom 5 ${0a} = 0$ and ${a0} = 0$

For concatenation, a single unit element is introduced; we denote it by 1 , which will shortly be recognized as an abbreviation.

The $\mathit{exp}$ ression 1 is regular and $a = a$ and

(Expressions 0 and 1 differ from each other and from all the letters.)

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

\mathrm {A x i o m} 7 (a) b) ^ {} = (a ^ {} b ^ {}) ^ {}

\mathrm {F i x i o m} 8 (a b) ^ {} = 1 ∥ a (b a) ^ {} b

\mathrm {T h e o r e m 3} 0 ^ {*} = 1

\begin{array}{l} \begin{array}{l l} \mathrm {P r o o f} & \mathrm {t r u e} \end{array} \ = {A x. 8, w i t h b := 0 } \ (a 0) ^ {} = 1 ∥ a (0 a) ^ {} 0 \ = {A x. 5, l w i c e } \ 0 ^ {} = 1 \left[ \begin{array}{l l} 0 & \end{array} \right] \ = {A x. 2 } \ 0 ^ {} = 1 \ \end{array}

(End of Proof.)

Theorem 3 justifies our characterization of $\mathfrak{p}$ as "an abbreviation".

A v G 3 6 / E W D 8 8 2 - 4

Theorem 4 The $^ \text{喜} ^ { \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 {A x i o m 2 a n d T h e o r e m 3} } \ a ^ {} = (a ^ {} 1) ^ {} \ = {A x i o m 6 } \ a ^ {} = a ^ {} \qquad \mathrm {(E n d o f P r o o f .)} \ \end{array}

Theorem 4 justifies the name "closure".

Theorem 5 $1 = {1}^{ * }$

\begin{array}{l} \begin{array}{l l} \underline {{\mathrm {P r o o f}}} & \mathrm {t r u e} \end{array} \ = {\mathrm {T h e o r e m} 4 \mathrm {w i t h} a := 0 } \ 0 ^ {} = 0 ^ { } \ = {\mathrm {T h e r e m} 3 } \ 1 = 1 ^ {} (\mathrm {E n d o f P r o o f .}) \ \end{array}

Theorem 6 ${a}^{ * } = 1\ll a{a}^{ * } $ and ${b}^{ * } = 1∥ b * b \cdots$

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

Theorem 7 ${a}^{ * } = {a}^{ * }{a}^{ * }$

\begin{array}{l} \begin{array}{l l} \underline {{P r o o f}} & \text {t r u e} \end{array} \ = {\mathrm {t h e o r e m 6 w i t h} a := a ^ {} } \ a ^ { } = 1 ] a ^ {} a ^ {} \ = {\mathrm {T h e o r e m} 4 } \ a ^ {} = 1 ∥ a ^ {} a ^ {} \ = {A x i o m 6 } \ a ^ {} = 1 1 \left[ a ^ {} a ^ {} \right. \ \end{array}

A v g 36 / EWD882 -5

[\left{ {\text{Corollary }0and1 ≤ {a}^{ * }\text{ from Theorem }6}\right} ]

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

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

Proof True

[{a}^{ * } \mid a = {a}^{ * }]

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

Theorem 9 Closure is monotonic, i.e. $a ≤ b ⇒ {a}^{ * } ≤ {b}^{ * }$ .

Proof Under the assumption $a ≤ b$ ,i.e. $a| b = b$ ,

we have to prove ${a}^{ * } \mid {\left| {b}^{ * }\right| = {b}^{ * }}$ . Since ${b}^{ * } ≤ {a}^{ * }$ I ${b}^{ * }$

is obvious (from Axiom 1), it suffices on account

of Theorem 0, antisymmetry - to prove ${a}^{ * }$ I ${b}^{ * } ≤ {b}^{ * }$

under the assumption $a\left\lbrack b\right\rbrack = b$ . We observe

for any $c$

\begin{array}{l} c = a ^ {} \prod b ^ {} \ ⇒ {\mathrm {T h e o r e m} 8 } \ c ≤ (a ^ {} ] b ^ {}) ^ {} \ = {A x i o m 7, w i t h a := a ^ {} a n d b := b ^ {} } \ c ≤ (a ^ { } b ^ { }) ^ {} \ = {\mathrm {T h e o r e m} 4 } \ c ≤ (a ^ {} b ^ {}) ^ {} \ = {A x i o m 7 } \ c ≤ (a) b) ^ {} \ = {\mathrm {a s s u m p l i o n} a } b = b } \ \end{array}

A v G 36 / EWD 882-6

c ≤ b ^ {*} (\mathrm {E n d o f P r o o f .})

(The above proof is due to Rudolf H. Mak and Stefan Rönn.)

\mathrm {T h e o r e m 1 0} a ≤ b ^ {} \equiv a ^ {} ≤ b ^ {*}

\begin{array}{l} \mathrm {P r o o f .} a ≤ b ^ {} \ ⇒ {\mathrm {T h e o r e m} g } \ a ^ {x} ≤ b ^ {x x} \ = {\mathrm {T h e o r e m} 4 } \ a ^ {} ≤ b ^ {} \ a ^ {} ≤ b ^ {} \ ⇒ {\mathrm {T h e o r e m} 8 } \ a ≤ b ^ {} \ (E n d o f P r o o f.) \ \end{array}

The relation $c$ from $(a, b)$ between an expression $c$ and a pair of variables $(a, b)$ is defined as the strongest relation satisfying

0 f r o m (a, b)

a \underset {f r o m} {p r o m} (a, b) a n d b \underset {f r o m} {p r o m} (a, b)

\begin{array}{l} (c ] d) \underline {{f r o m}} (a, b) \equiv c \underline {{f r o m}} (a, b) \wedge d \underline {{f r o m}} (a, b) \ (c d) \underline {{\operatorname {P r o m}}} (a, b) \equiv c \operatorname {P r o m} (a, b) \wedge d \operatorname {P r o m} (a, b) \ c ^ {*} \underline {{f r o m}} (a, b) \equiv c \overline {{f r o m}} (a, b). \ \end{array}

If allows us to formulate

\mathrm {T h e o r e m 1 1} c \underset {\mathrm {f r u m}} {p} (a, b) ⇒ c ≤ (a \Vert b) ^ {*}

Proof. The proof is by induction over the syntax. We observe for the base - mainly on account of Theorem 8- $0 ≤ (a ∥ b)^{}, a ≤ (a \nparallel b)^{}, b ≤ (a \nparallel b)^{*}$ .

For the induction step, we prove under the hypothesis

A v G 3 6 / E W D 8 8 2 - 7

c ≤ (a ∥ b) ^ {} ∧ d ≤ (a ∥ b) ^ {}

(i) $c∥ d ≤ {\left( a∥ b\right) }^{ * }$ (Theorem 1 and Axiom 1, idempotence.) (ii) ${cd} ≤ {\left( a∥ b\right) }^{ * }$ (Corollary O and Theorem 7.) (iii) ${c}^{ * } ≤ {\left( a\right) }_{b}\left( \right.$ (Theorem 10.)

(End of Proof.)

Combining Theorems 10 and 11 we get

\begin{array}{r l} {\underline {{C o r o l l a r y , 1}}} & {= \underset {\mathrm {f r o m} (a, b)} {\rho} ⇒ c ^ {} ≤ (a) [ b) ^ {}} \end{array}

From Corollary 1, Theorem 9, and Theorem 0, antisymmetry, we conclude

Theorem 12 $a| b ≤ c ∧ c$ from $\left( {a,b}\right) ⇒ {c}^{ * } = {\left( a| b\right) }^{ * }.$

*

Intermezzo In the mean time we have discovered a few improvements of the above. We should add

Theorem $1/3$ $a ≤ a| b$

Proof true

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

Theorem 2/3 $a \mid b ≤ c \equiv a ≤ c ∧ b ≤ c$

Proof $a| b ≤ c$

= {\mathrm {T h e o r e m} 1 / 3 }

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

In connection with Axiom 2 it would have been appropriate to recall the general

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

\begin{array}{l} \mathrm {P r o o f} (\underline {{A}} a, b: U L \underline {{\Phi}} a = a \wedge b \underline {{\Phi}} U R = b) \ ⇒ {a := U R; b := U L } \ U L # U R = U R \wedge U L # U R = U L \ ⇒ {\mathrm {L e i b n i z} } \ U L = U R (\mathrm {E n d o f P r o o f .}) \ \end{array}

The theorem is of equal relevance for axiom 6.

We are tempted to replace ${Axiom} 5 $ by

The original Axiom 5 would then get the status of a corollary.

A v G 3 6 / E w D 8 8 2 - 9

In a similar vein we are tempted to strengthen Axiom 6 by adding to it

A x i o m 6 \frac {1}{2} 1 ≤ a b \equiv 1 ≤ a \wedge 1 ≤ b

\mathrm {T h e o r e m} 2 \frac {1}{2} 1 = a b \equiv 1 = a \wedge 1 = b

\mathrm {P r o o f} 1 = a ∧ 1 = b

\begin{array}{l} ⇒ {A x _ {i o m} G } \ 1 = a b \ \end{array}

\begin{array}{l} 1 = a b \ = {\mathrm {T h e o r e m} 0, \mathrm {r e f l e x i v i t y} } \ 1 ≤ a b ∧ 1 = a b \ = {A x i o m 6 1 / 2 } \ 1 \le a ∧ 1 \le b ∧ 1 = a b \ = {\mathrm {m o n o t o n i c i t y o f c o n c a t e n a t i o n a n d A x i o m 6} } \ 1 ≤ a ∧ 1 ≤ b ∧ 1 = a b ∧ b ≤ a b ∧ a ≤ a b \ ⇒ {\text {L e i b n i z} } \ 1 ≤ a ∧ 1 ≤ b ∧ b ≤ 1 ∧ a ≤ 1 \ = {\mathrm {T h e o r e m} 0, \mathrm {a n t i s y m m e t r y} } \ 1 = a \wedge 1 = b (\mathrm {E n d o f P r o o f .}) \ \end{array}

We probably need as well

A x i o m v _ {i} 1 ≤ a ∥ b \equiv 1 ≤ a \vee 1 ≤ b

A x i o m v i i a ≤ 1 \equiv a = 0 ≠ a = 1

(With $a \mathrel{\text{:=}} 1$ ,we derive from Axiom ${v}_{ii} 1 ≠ 0$ .)

(End of Intermezzo.)

Further addition:

\mathrm {T h e o r e m} 6

a a ^ {} = a ^ {} a

\begin{array}{l} \mathrm {P r o o f} z = a a ^ {} \ = {\mathrm {T h e o r e m} G \mathrm {w i t h} b := a } \ 2 = a (1) a ^ {} a) \ = {A x i o m s 4 a n d 6 } \ z = a ] a a ^ {} a \ = {A x i a m s 4 c m d 6 } \ z = (1 \Vert a a ^ {x}) a \ = {\mathrm {T h e o r e m} 6 } \ z = a ^ {} a (\mathrm {E n d o f P r o o f .}) \ \end{array}

We observe

\begin{array}{l} x = (a a) ^ {} ] a (a a) ^ {} \ ⇒ {\mathrm {L e i b n i z a n d A x i o m} 4 } \ 1 \ll a a (a a) ^ {} \rrbracket a (a a) ^ {} = 1 \rrbracket a x \ = {\mathrm {T h e o r e m} 6 } \ (a a) ^ {} \left[ \right] a (a a) ^ {} = 1 ] ] a x \ = {x) } \ x = 1 ] a x \ \end{array}

From the above we conclude that the equation $x : \left( {x = 1}\right) \mid a - x)$ (0)

is solved by $(aa)^ \Vdash a(aa)^$ ; on account of Theorem 6, it is also solved by $a^*$ . Our axioms so far - see Artio Salomaa "Theory of Automata", 1969 - do not suffice to conclude

A v G 3 6 / E W D 8 8 2 - 1 1

(a a) ^ {} ] a (a a) ^ {} = a ^ {*} . (1)

We could try to solve the problem by postulating that (0) has a unique solution, but that would be a mistake, as is shown by the following analysis.

\mathrm {T h e o r e m 1 3} 1 ≤ a \equiv a ^ {} = a a ^ {}

\begin{array}{l} \mathrm {P r o o f} a ^ {} = a a ^ {} \ = {\mathrm {T h e o r e m} 6 } \ 1 ] a a ^ {} = a a ^ {} \ = {\mathrm {d e f i n i t i o n} o f ≤ 3 \ 1 ≤ a a ^ {} \ = {A x i o m 6 ^ {1 / 2} } \ 1 ≤ a ∧ 1 ≤ a ^ {} \ = {1 ≤ a ^ {x} } \ 1 ≤ a \ \end{array}

(End of Proof.)

We now show that for $1 ≤ a$ equation (0) is solved by ${a}^{ * }$ I ${a}^{ * }c$ . To this end we observe

\begin{array}{l} z = 1 ∥ a (a ^ {} ∥ a ^ {} c) \ = {A x i o m 4 } \ z = 1 \left[ \begin{array}{l l} a & a ^ {} \end{array} \right] a a ^ {} c \ = {\mathrm {T h e o r e m} 6 } \ 2 = a ^ {} \prod a a ^ {} c \ = {1 ≤ a \mathrm {a n d} \mathrm {T h e o r e m 1 3} } \ z = a ^ {x} ] a ^ {x} c \ \end{array}

Note that in the above observation we have not made any assumption about $c$ . Since 151,

the above observation with $a \mathrel{\text{:=}} 1$ and ${1}^{ * } = 1 -$ The.

orem 5 - tells us that the postulate that (0)

has a unique solution leads to the conclusion

that 17c is unique , i.e. independent of C.

from the idempotence of 1 we would then

conclude 17c' = 1, i.e. $c ≤ 1 $ for any $c$ .

Axiom VII then tells us that for any $c \in$ we

have $c = 0 \vee c = 1\ldots$ Such a universe, however,

is too meagre to our taste: in view of our

earlier remark that 0 and 1 differ from all the

letters and - Axiom 0- that each letter is a regular

expression, we would be considering the not so inter-

testing situation of an empty alphabet.