Lemma of Arden

The lemma of Arden makes a statement about sets of character strings, which in the context of formal languages ​​are the subject of theoretical computer science , more specifically of automaton theory .

formulation

Let it be any alphabet ; stand for the Kleene star , for the positive transitive envelope , for the concatenation of two sets of strings and for their ordinary union (in this priority - brackets are accordingly neglected). Then the following equivalence applies: ${\displaystyle \Sigma }$ ${\displaystyle *}$ ${\displaystyle +}$ ${\displaystyle \cdot }$ ${\displaystyle \cup }$

${\displaystyle \left(\forall Y\subseteq \Sigma ^{+}\right)\left(\forall Z\subseteq \Sigma ^{*}\right)\left(\left(X=Y\cdot X\cup Z\right)\leftrightarrow \left(X=Y^{*}\cdot Z\right)\right)}$

or the following equation:

${\displaystyle \left(\forall Y\subseteq \Sigma ^{+}\right)\left(\forall Z\subseteq \Sigma ^{*}\right)\left(\left\{X\subseteq \Sigma ^{*}\mid X=Y\cdot X\cup Z\right\}=\left\{Y^{*}\cdot Z\right\}\right)}$

In words: For an arbitrary set of strings and a set of strings that does not contain the empty word , the equation has only one solution . ${\displaystyle Z}$ ${\displaystyle Y}$ ${\displaystyle \epsilon }$ ${\displaystyle X=Y\cdot X\cup Z}$ ${\displaystyle X=Y^{*}\cdot Z}$

proof

For the sake of readability, quantization is omitted in both parts of the proof, which is not a problem with universal quantification as long as no specifications are made for the variables in question. Corresponding positions are dealt with specially.

execution

Let there be a solution for in the equation . ${\displaystyle S}$ ${\displaystyle X}$ ${\displaystyle X=Y\cdot X\cup Z}$

Superset

First, the definition of the Kleene star is applied and the distributivity of the concatenation across associations is used:

${\displaystyle S\supseteq \left(Y^{*}\cdot Z=\left(\bigcup _{n\geq 0}Y^{n}\right)\cdot Z=\bigcup _{n\geq 0}Y^{n}\cdot Z\right)}$

Now it can be shown by complete induction over that it holds for all : ${\displaystyle n}$ ${\displaystyle S\supseteq Y^{n}\cdot Z}$ ${\displaystyle n\geq 0}$

• Induction hypothesis

${\displaystyle S\supseteq Y^{n}\cdot Z}$

• Induction start

${\displaystyle \left(S\supseteq Z\right)\rightarrow \left(S\supseteq \left\{\varepsilon \right\}\cdot Z\right)\rightarrow \left(S\supseteq Y^{0}\cdot Z\right)}$

• Induction step

${\displaystyle \left(S\supseteq Y\cdot S\cup Z\right)\rightarrow \left(S\supseteq Y\cdot S\right)\rightarrow \left(S\supseteq Y\cdot Y^{n}\cdot Z\right)\rightarrow \left(S\supseteq Y^{n+1}\cdot Z\right)}$

Since for different n all are pairwise disjoint, the original superset relationship follows from this . ${\displaystyle Y^{n}}$ ${\displaystyle \left(\forall n\geq 0\right)\left(S\supseteq Y^{n}\right)}$ ${\displaystyle S\supseteq Y^{*}\cdot Z}$

Subset

Here the proof is indirect: It is thought not apply, making it at least a word with has to give. Because is, must also be an element of , or put another way . In the first case is made up of two sub- words and , so . Since there cannot be the empty word (which demands quantification ), it follows . If one considers the smallest of those assumed as existing , then it would also have to apply, but this contradicts the assumption . In the other case, that is , the contradiction also arises . Since both cases end in contradictions, it must have been wrong to assume that it does not hold. ${\displaystyle S\subseteq Y^{*}\cdot Z}$ ${\displaystyle w}$ ${\displaystyle \left(w\in S\right)\wedge \left(w\notin Y^{*}Z\right)}$ ${\displaystyle S=Y\cdot S\cup Z}$ ${\displaystyle w}$ ${\displaystyle Y\cdot S\cup Z}$ ${\displaystyle \left(w\in Y\cdot S\right)\vee \left(w\in Z\right)}$ ${\displaystyle w}$ ${\displaystyle y\in Y}$ ${\displaystyle s\in S}$ ${\displaystyle w=ys}$ ${\displaystyle y}$ ${\displaystyle Y\subseteq \Sigma ^{+}}$ ${\displaystyle \left|s\right|<\left|w\right|}$ ${\displaystyle w}$ ${\displaystyle s\in Y^{*}Z}$ ${\displaystyle w\notin Y^{*}Z}$ ${\displaystyle w\in Z}$ ${\displaystyle w\in Y^{*}Z}$ ${\displaystyle S\subseteq Y^{n}\cdot Z}$

Reverse direction

This line of proof is trivial, since it suffices to show that the equation solves at all: ${\displaystyle Y^{*}Z}$ ${\displaystyle X=Y\cdot X\cup Z}$

${\displaystyle \left(X=Y^{*}\cdot Z\right)\rightarrow \left(X=\left(Y^{+}\cup \left\{\varepsilon \right\}\right)\cdot Z\right)\rightarrow \left(X=\left(Y\cdot Y^{*}\cup \left\{\varepsilon \right\}\right)\cdot Z\right)\rightarrow \left(X=Y\cdot Y^{*}\cdot Z\cup \left\{\varepsilon \right\}\cdot Z\right)\rightarrow \left(X=Y\cdot X\cup Z\right)}$

application

The central meaning of the Arden lemma is its application in automaton theory. It makes it easier to determine the technical description of the language accepted by a non-deterministic finite automaton (NEA) :

A NEA is considered , the states of which are to be designated with the natural numbers from to (i.e. ). In addition, the following definitions are used: ${\displaystyle {\mathcal {A}}=\left(Q,\Sigma ,\Delta ,i,F\right)}$ ${\displaystyle 1}$ ${\displaystyle n}$ ${\displaystyle Q=\left\{1,2,\ldots ,n\right\}}$

${\displaystyle A_{q,r}=\left\{\sigma \in \Sigma \mid \left(q,\sigma ,r\right)\in \Delta \right\}}$

${\displaystyle B_{q}={\begin{cases}\left\{\varepsilon \right\}&q\in F\\\left\{\right\}&q\notin F\end{cases}}}$

With the help of these sets the sublanguage of each state can be specified: ${\displaystyle q\in Q}$

${\displaystyle L_{q}=\left(\bigcup _{r\in Q}A_{q,r}\cdot L_{r}\right)\cup B_{q}}$

The definition of gives a system of equations with equations: ${\displaystyle L_{q}}$ ${\displaystyle n}$

${\displaystyle {\begin{array}{c}L_{1}=A_{1,1}\cdot L_{1}\cup A_{1,2}\cdot L_{2}\cup \ldots \cup A_{1,n}\cdot L_{n}\cup B_{1}\\L_{2}=A_{2,1}\cdot L_{1}\cup A_{2,2}\cdot L_{2}\cup \ldots \cup A_{2,n}\cdot L_{n}\cup B_{2}\\\vdots \\L_{n}=A_{n,1}\cdot L_{1}\cup A_{n,2}\cdot L_{2}\cup \ldots \cup A_{n,n}\cdot L_{n}\cup B_{n}\end{array}}}$

Now one brings a partial language into a suitable form, which enables the application of the lemma:

${\displaystyle L_{q}=A_{q,q}\cdot L_{q}\cup \left(\left(\bigcup _{r\in Q\setminus \left\{q\right\}}A_{q,r}\cdot L_{r}\right)\cup B_{q}\right)}$

According to Arden's lemma, this statement is equivalent to the following:

${\displaystyle L_{q}=A_{q,q}^{*}\cdot \left(\left(\bigcup _{r\in Q\setminus \left\{q\right\}}A_{q,r}\cdot L_{r}\right)\cup B_{q}\right)}$

This solution is clear. If you now insert into all other equations, you get an equation system with one less variable and in this way you can simplify further and further down to the trivial case in which only one equation is left, which is independent of all other sub-languages can solve. By inserting it backwards, you then also get the other sub-languages ​​in order to finally determine the unambiguous solution of the entire system of equations and to identify the language accepted by the automaton . ${\displaystyle L_{q}}$ ${\displaystyle L_{i}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle L({\mathcal {A}})}$

Algebraic consideration

From the perspective of abstract algebra , the structure of a dioid represents what means that both and form a monoid and is distributive over . The neutral element regarding the union is the empty set and the neutral element regarding the concatenation is . Due to the lack of invertibility, it is generally not possible to solve equations using this structure. The lemma of Arden makes it possible at least to determine the solutions of some special equations and that even clearly. ${\displaystyle \left({\mathcal {P}}\left(\Sigma ^{*}\right),\cup ,\cdot \right)}$ ${\displaystyle \left({\mathcal {P}}\left(\Sigma ^{*}\right),\cup \right)}$ ${\displaystyle \left({\mathcal {P}}\left(\Sigma ^{*}\right),\cdot \right)}$ ${\displaystyle \cdot }$ ${\displaystyle \cup }$ ${\displaystyle \left\{\varepsilon \right\}}$

Examples

Simple examples

${\displaystyle \left(X=\left\{a\right\}\cdot X\cup \left\{b\right\}\right)\quad \leftrightarrow \quad \left(X=\left\{a\right\}^{*}\cdot \left\{b\right\}=\left\{a^{n}b\mid n\geq 0\right\}=\left\{b,ab,aab,aaab\ldots \right\}\right)}$

${\displaystyle \left(X=\left\{0,1\right\}\cdot X\cup \left\{u,v\right\}\right)\quad \leftrightarrow \quad \left(X=\left\{0,1\right\}^{*}\cdot \left\{u,v\right\}=\left\{u,v,0u,0v,1u,1v,00u,00v,01u,01v,10u,10v,\ldots \right\}\right)}$

Complex example

${\displaystyle {\mathcal {A}}=\left(\left\{S_{0},S_{1},S_{2},S_{3},S_{4}\right\},\left\{0,1\right\},\Delta ,S_{0},\left\{S_{1},S_{3}\right\}\right)}$

${\displaystyle \Delta =\left\{(S_{0},\varepsilon ,S_{1}),(S_{0},\varepsilon ,S_{3}),(S_{1},0,S_{2}),(S_{1},1,S_{1}),(S_{2},0,S_{1}),(S_{2},1,S_{2}),(S_{3},0,S_{3}),(S_{3},1,S_{4}),(S_{4},0,S_{4}),(S_{4},1,S_{3})\right\}}$

This gives the following system of equations:

${\displaystyle {\begin{array}{lclcl}L_{S_{0}}&=&\{\,\}\cdot L_{S_{0}}\cup \left\{\varepsilon \right\}\cdot L_{S_{1}}\cup \{\,\}\cdot L_{S_{2}}\cup \left\{\varepsilon \right\}\cdot L_{S_{3}}\cup \{\,\}\cdot L_{S_{4}}&=&L_{S_{1}}\cup L_{S_{3}}\\L_{S_{1}}&=&\{\,\}\cdot L_{S_{0}}\cup \left\{1\right\}\cdot L_{S_{1}}\cup \left\{0\right\}\cdot L_{S_{2}}\cup \{\,\}\cdot L_{S_{3}}\cup \{\,\}\cdot L_{S_{4}}\cup \left\{\varepsilon \right\}&=&\left\{1\right\}\cdot L_{S_{1}}\cup \left\{0\right\}\cdot L_{S_{2}}\cup \left\{\varepsilon \right\}\\L_{S_{2}}&=&\{\,\}\cdot L_{S_{0}}\cup \left\{0\right\}\cdot L_{S_{1}}\cup \left\{1\right\}\cdot L_{S_{2}}\cup \{\,\}\cdot L_{S_{3}}\cup \{\,\}\cdot L_{S_{4}}&=&\left\{0\right\}\cdot L_{S_{1}}\cup \left\{1\right\}\cdot L_{S_{2}}\\L_{S_{3}}&=&\{\,\}\cdot L_{S_{0}}\cup \{\,\}\cdot L_{S_{1}}\cup \{\,\}\cdot L_{S_{2}}\cup \left\{0\right\}\cdot L_{S_{3}}\cup \left\{1\right\}\cdot L_{S_{4}}\cup \left\{\varepsilon \right\}&=&\left\{0\right\}\cdot L_{S_{3}}\cup \left\{1\right\}\cdot L_{S_{4}}\cup \left\{\varepsilon \right\}\\L_{S_{4}}&=&\{\,\}\cdot L_{S_{0}}\cup \{\,\}\cdot L_{S_{1}}\cup \{\,\}\cdot L_{S_{2}}\cup \left\{1\right\}\cdot L_{S_{3}}\cup \left\{0\right\}\cdot L_{S_{4}}&=&\left\{1\right\}\cdot L_{S_{3}}\cup \left\{0\right\}\cdot L_{S_{4}}\end{array}}}$

By applying the lemma one gets the solution step by step:

${\displaystyle L_{S_{2}}=\left\{0\right\}\cdot L_{S_{1}}\cup \left\{1\right\}\cdot L_{S_{2}}}$

${\displaystyle \rightarrow \quad L_{S_{2}}=\left\{1\right\}^{*}\cdot \left\{0\right\}\cdot L_{S_{1}}}$

${\displaystyle L_{S_{1}}=\left\{1\right\}\cdot L_{S_{1}}\cup \left\{0\right\}\cdot L_{S_{2}}\cup \left\{\varepsilon \right\}=\left\{1\right\}\cdot L_{S_{1}}\cup \left\{0\right\}\cdot \left\{1\right\}^{*}\cdot \left\{0\right\}\cdot L_{S_{1}}\cup \left\{\varepsilon \right\}=\left(\left\{1\right\}\cup \left\{0\right\}\cdot \left\{1\right\}^{*}\cdot \left\{0\right\}\right)\cdot L_{S_{1}}\cup \left\{\varepsilon \right\}}$

${\displaystyle \rightarrow \quad L_{S_{1}}=\left(\left\{1\right\}\cup \left\{0\right\}\cdot \left\{1\right\}^{*}\cdot \left\{0\right\}\right)^{*}}$

${\displaystyle L_{S_{4}}=\left\{1\right\}\cdot L_{S_{3}}\cup \left\{0\right\}\cdot L_{S_{4}}}$

${\displaystyle \rightarrow \quad L_{S_{4}}=\left\{0\right\}^{*}\cdot \left\{1\right\}\cdot L_{S_{3}}}$

${\displaystyle L_{S_{3}}=\left\{0\right\}\cdot L_{S_{3}}\cup \left\{1\right\}\cdot L_{S_{4}}\cup \left\{\varepsilon \right\}=\left\{0\right\}\cdot L_{S_{3}}\cup \left\{1\right\}\cdot \left\{0\right\}^{*}\cdot \left\{1\right\}\cdot L_{S_{3}}\cup \left\{\varepsilon \right\}=\left(\left\{0\right\}\cup \left\{1\right\}\cdot \left\{0\right\}^{*}\cdot \left\{1\right\}\right)\cdot L_{S_{3}}\cup \left\{\varepsilon \right\}}$

${\displaystyle \rightarrow \quad L_{S_{3}}=\left(\left\{0\right\}\cup \left\{1\right\}\cdot \left\{0\right\}^{*}\cdot \left\{1\right\}\right)^{*}}$

${\displaystyle L_{S_{0}}=L_{S_{1}}\cup L_{S_{3}}=\left(\left\{1\right\}\cup \left\{0\right\}\cdot \left\{1\right\}^{*}\cdot \left\{0\right\}\right)^{*}\cup \left(\left\{0\right\}\cup \left\{1\right\}\cdot \left\{0\right\}^{*}\cdot \left\{1\right\}\right)^{*}}$

Since the starting state is , whatever corresponds to the language assigned to the regular expression applies . ${\displaystyle S_{0}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle L({\mathcal {A}})=L_{S_{0}}}$ ${\displaystyle (1+01^{*}0)^{*}+(0+10^{*}1)^{*}}$

literature

• DN Arden: Theory of Computing Machine Design: An Intensive Course for Engineers, Scientists, and Mathematicians , University of Michigan Press, Michigan, USA, 1960 (pp. 1–35)
• John E. Hopcroft: Introduction to Automata Theory, Languages, and Computation , Addison-Wesley, 1979. ISBN 0-201-02988-X
• Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk: Interactive Theorem Proving , Springer Science & Business Media, 2011
• Harold V. McIntosh: One Dimensional Cellular Automata , Luniver Press, 2009 (p. 87)
• A. Arnold, D. Niwinski: Rudiments of µ-calculus , Elsevier, 2001 (from p. 107)

Web links

• John Daintith: Ardens rule , Oxford University Press, 2004 (English)