2
$\begingroup$

Axioms For *

\begin{align} 1 + aa^* &\leq a^* \\ 1 + a^*a &\leq a^* \\ b + ax &\leq x \to a^*b \leq x \\ b + xa &\leq x \to ba^* \leq x \\ \end{align}

Elementary Results

\begin{align} a \leq b &\to a + c \leq b + c \\ a \leq b &\to ac \leq bc\, \wedge\, ca \leq cb \\ a \leq b &\to a^* \leq b^* \end{align}

Problem

Prove the following identity in a Kleene algebra using only the axioms and elementary results. $$(a + ab + b)^* = (a + b)^*$$

Solution: \begin{align} (a + b)^* &= (a + ab + b)^* \\ (a + b)^* &\leq (a + ab + b)^* \\ 1 + (a + b)(a + b)^* &\leq 1 + (a + ab + b)(a + ab + b)^* \\ (a + b)(a + b)^* &\leq (a + ab + b)(a + ab + b)^* \\ \end{align}

Quesiton

  1. So for them to be equal the sets should be contained in each other. At which point do I transition to an inequality?

  2. Is it right to say a $*$ cannot be removed since it has no inverse?

  3. Can I distribute into a $*$? Say $(a +b)(a + b)^*$ or do they need to have the same $*$ height?

Some hints to get further would be greatly appreciated.

$\endgroup$
2
$\begingroup$

I assume that in your definition $a \leq b$ iff $a + b = b$.

First, note that if $a \leq b$ and $b \leq a$, then $a = a + b = b + a = b$. Therefore, in order to show that $a = b$, it is sufficient to show that $a \leq b$ and $b \leq a$.

Now, you want to show that $(a + b)^\ast = (a + ab + b)^\ast$. As explained in the previous paragraph, it is sufficient to show that inequalities with $\leq$ in both directions hold ("[...] for them to be equal the sets should be contained in each other").


The inequality $(a + b)^\ast \leq (a + ab + b)^\ast$ is almost trivial:

$$(a + b) + ab = a + ab + b $$

therefore $(a + b) \leq (a + ab + b)$, and by monotonicity (your ER-3), it thus holds

$$(a + b)^\ast \leq (a + ab + b)^\ast.$$


The other direction is a bit trickier.

By monotonicity (ER-2), (def-$\leq$), (Ax-1):

$$a(a + b)^\ast \leq (a + b)(a + b)^\ast \leq 1 + (a + b)(a + b)^\ast \leq (a+b)^\ast$$

Analogously, $b(a + b)^\ast \leq (a+b)^\ast$.

From both previous statements, again using monotonicity (ER-2):

$$ab(a+b)^\ast \leq a(a+b)^\ast \leq (a+b)^\ast.$$

To summarize: so far, we know that $a$,$b$ and $ab$ are all $\leq (a+b)^\ast$.

Now, observe that from (ER-1), it follows that if $x \leq w$ and $y \leq w$, then $x + y \leq w + y \leq w + w = w$. Thus, from $a\leq (a + b)^\ast$, $ab \leq (a + b)^\ast$ and $b \leq (a + b)^\ast$, you obtain:

$$(a + ab + b)(a+b)^\ast = a(a+b)^\ast + ab(a+b)^\ast + b(a+b)^\ast \leq (a + b)^\ast.$$

Since additionally $1 \leq (a+b)^\ast$ (directly from Ax-1), you obtain:

$$1 + (a + ab + b)(a+b)^\ast \leq (a+b)^\ast.$$

With (Ax-3) it follows:

$$(a + ab + b)^\ast = 1\cdot(a + ab + b)^\ast \leq (a + b)^\ast$$


Thus, both inequalities hold, hence we get the equality.

You cannot simply "remove" $^\ast$, nothing is told about "inverse" in the definition of a Kleene algebra. I also don't know what you mean by "$\ast$-height".

$\endgroup$
  • $\begingroup$ So this expression $(a+b)+ab=a+ab+b$ you can use to deduce $(a+b)\leq(a+ab+b)$. I understand this but I just wonder if it is ok since we did not arrive there by manipulating the equation? This is why I was asking if is was possible to remove a $*$. For 3. I meant to say do the both need to have the same amount of stars so I can distribute say $(a+b)*(a+b)∗$ instead of $(a+b)(a+b)∗$? Thanks so much for your answer. $\endgroup$ – grant2088 Oct 7 '18 at 2:03
  • $\begingroup$ @grant2088 "$(a + b) + ab = a + ab + b$ hence $(a + b)\leq(a + ab + b)$" holds by definition of $\leq$, it's a zero-step "deduction". The "amount of stars" doesn't matter, because the closure operation is idemponent - either there is a star, or there isn't. But you can, of course, distribute $(a +b)c$ into $ac + bc$, again, by definition. As you can see, the list of properties in the Wiki is way longer than your 4 axioms. $\endgroup$ – Andrey Tyukin Oct 7 '18 at 11:34
  • $\begingroup$ Neither $+$ nor $\cdot$ distributes particularly well over the $\bullet^\ast$, e.g. $(a + b)^\ast c \neq a^\ast c + b ^\ast c$, or anything of that kind. $\endgroup$ – Andrey Tyukin Oct 7 '18 at 11:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.