Relational Kleene Lattices

Software : Kleenelattices

Kleenelattices is composed of libraries and tools written in OCaml to compare identity-free regular expressions with intersection.

The webpage dedidated to this is located here : link. You will find there links to download the sources, access the github repository or look up the documentation.

Some online applications are also available below.

Equation checker

How to use this :

Write down equations in the left-hand side fields of the applet, and see their validity just to their right (a green tick meaning yes and a red cross meaning no). The rightmost button allow you to see more details, and to hide them afterwards.

Equations should be entered like this: `<expr1> <cmp> <expr2>`.

An expression can use strings as variables/letters, and the operations:

• `<expr1> | <expr2>`: the set union
• `<expr1> & <expr2>`: the set intersection
• `<expr1> . <expr2>`: the composition of relations
• `<expr1>+`: the transitive closure of a relation.
• `<expr1>{int}` : the iteration of a relation. For instance, `(a.b){3}` is a shorthand for `(a.b).(a.b).(a.b)`.

You can also use brackets `(...)`. The valid comparaisons `<cmp>` are:

• `<=`: loose inclusion
• `>=`: converse of the loose inclusion
• `<`: strict inclusion
• `>`: converse of the strict inclusion
• `=`: equality
• `=/=`: negation of the equality
• `<>`: means that the two expressions are incomparable, i.e. neither one of them is included in the other.

For instance, `(a|b)+.C & d < d & a.b.C & (d|a)` is an acceptable equation.