ka_completeness: completeness of Kleene algebra

We mostly follow Dexter Kozen's proof: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, May 1994. We proceed as follows: 1. convert regular expressions into matricial NFA with epsilon transitions, using a simple and compositional construction (Thompson). 2. remove epsilon transitions (algebraically, using Kleene star on matrices to compute their reflexive transitive closure) 3. determinise matricial NFA using the powerset construction (without performing the "accessible" subsets optimisation, for the sake of simplicity) 4. exploit decidability of DFA language inclusion to conclude (this is where our proof slightly differs from that of Kozen: he first minimises the DFA, and then compare them up to isomorphism) Again, the implicit underlying algorithm is not efficient ; we don't care since this is not the one we execute in the end.

locally prevent simpl from unfolding relation algebra projections

1. constructing eNFA out of regular expressions (Thompson)

Thompson construction is straightfoward once we have block matrix operations

construction

empty automaton for 0

one state automaton for 1

two states automata for variables

for pls, we take the disjoint union of the two automata

for dot, we take the disjoint union, and we add epsilon transitions from accepting states of the first automaton to starting states of the second one

strict iteration is obtained simply by adding epsilon transitions from accepting states to initial ones

Kleene star is derived from the other operations

summing up all together, we get the final construction

correctness

algebraic correcteness of each construction

algebraic correcteness of the global construction

the produced matricial automaton actually is an NFA with epsilon transitions (i.e., the transition matrix is simple, and starting and accepting vectors are 01)

2. removing espilon-transitions

again, this is straightfoward once we have the Kleene algebra of matrices

construction

correctness

the produced matricial automaton is actually a NFA (i.e., the transition matrix is pure, and starting and accepting vectors are 01)

3. determinisation

we use the standard powerset construction, and we exploit the bijection we defined in ordinals between the powerset on ord n (ord n → bool) and ord (pow2 n). This allows us to index states of the determinised automaton in a seemless way.

construction

we slightly generalise the construction, by specifying a finite subset of letters which have to be considered whether or not the NFA mention them. This allows us in the sequel to handle easily the case where the compared automata have different alphabets. list of letters to include

NFA to determinise

alphabet of the generated DFA: those appearing in M, plus the imposed ones

(unlabelled) transition matrix of the NFA, restricted to a

transition matrix of the NFA restricted to a

decoding matrix, establishing the link between the state of the determinised automaton (i.e., sets of states), with those of the starting one. We exploit for this the aforementioned bijection ; X_(x,i) holds iff i\in x.

determinised automaton:

• the initial state is the set of intial states
• the transition function is obtained by reading the transition matrix in a "parallel" way: along a, the set x maps to the set {j / i -a→ j for some i\in x}. this computation is performed matricially.
• the accepting states are those containing at least one accepting state again, this computation is done matricially, using the decoding matrix X.

correctness

the correctness is establish by using the bisimulation rule, to let the decoding matrix X go through u ⋅ M^* ⋅ v: denoting by (u',M',v') the determinised automaton, we easily deduce u⋅M^*⋅v ≡ u'⋅M'^*⋅v' from u ≡u'⋅X, X⋅M ≡ M'⋅X, and X⋅v ≡ v'.

algebraic correctness of determinisation

Kleene theorem as a corollary

summing up the above three constructions, we can build DFA out of a regular expression

since the Kleene algebra of matrices allows us to compute a regular expression out of any finite automaton, we obtain Kleene theorem as a consequence: ``the languages recognised by a regular expression are those recognised by a (deterministic) finite automaton''.

4. algebraic correctness of language inclusion checking for DFA

rather than minimising DFA, and comparing them up to isomorphism, we take a shorter path here, by focusing on language inclusion rather than equivalence, and by avoiding minimisation and isomophisms Our goal is to prove that for any two DFA A and B, dfa.lang A ≦ dfa.lang B entails eval A ≦ eval B (The premisse is a language inclusion, while the conclusion is a KA derivation.) The corresponding result on language equivalence and KA equality follows easily. We use the same kind of trick as in Kozen's minimisation proof, except that we consider the matrix of language inclusions rather than the matrix of the Mihyll-Nerode relation.

thanks to the previous generalisation of the determinisation construction, we can assume w.l.o.g. that vars A ≦ vars B. This is required by our reduction of language inclusion to language emptiness (dfa.lang_incl_dec), but also to prove Lemma R_M below

language inclusion matrix: R_(j,i) holds iff dfa.lang A i ≦ dfa.lang B j (Note that this matrix goes from B to A.)

the algebraic proof is quite similar to that of determinisation: we use the bisimulation rule for inclusions, with R: from A^u ≦ B^u ⋅ R, R ⋅ A^M ≦ B^M ⋅ R, and R ⋅ A^v ≦ B^v, we deduce A^u⋅A^M^*⋅A^v ≦ B^u⋅B^M^*⋅B^v the second and third hypotheses always hold, while the first one holds only if the language of A is contained in that of B.

algebraic correctness of language inclusion test

Completeness of KA

summing up all together, we obtain completeness of KA for language inclusion

and thus for language equivalence

since languages form a model of KA, the converse directions trivially hold, so that we actually have equivalences

Decidability of KA

as additional corollaries, we obtain decidability of (in)equations in Kleene algebra