Haskelleene

A simple encoding of automaton data, with no restriction on if it is deterministic or not. Essentially for convenience when moving between the different structures.

Comprised of a set of states, a subset of accepting states, and a function taking a letter and a state to a new state.

Similar to a DFA, except it can take a letter to a set of possible output states, or also take nothing to transition from one state to another.

Built using the syntax of Kleene Algebra, used to specify regular expressions. Implemented similarly to propositional logic, but with an even nicer show function.

detCheck is a function checking if a certain set of automaton data can actually specify a deterministic automaton (no empty transitions, transition function is deterministic at every state). If an data set can pass detCheck, then we can encode it as a DFA. For this purpose we have the function encodeDA, which produces an automaton if the data passes detCheck, and Nothing otherwise.

Because all data can be turned into a valid NFA, we have no need for such a check, and so we have the function encodeNA for turning

Note that we don't check at any point that the accepting states are a subset of the all states; in such a scenario all "accepting states" not specified as valid states are simply ignored.

We use the well-known power-set construction to turn a NFA into a DFA.

Because all DFAs can also be considered NFAs (by just ignoring the determinism requirement), we allow DFAs to be "lifted" directly to NFAs.

Our functions for translating between automata and data actually operate on automaton data, as it's much easier to handle tuples/lists than functions in such a setting. Therefore, we have the function decode to undo the work of encoding an automaton, by turning it into a data set.

This function operates on NFAs, so to decode a DFA, one can just compose this function with fromDA to turn it into an NFA.

Kleene's Algorithm, closely related to the Floyd-Warshall algorithm for shorted paths in a graph, generates a regular expression given some input automaton.

Generates an automaton to represent a regular expression.

Check if we encode deterministic data as both a DFA and NFA, it should accept the same words.

If we determinise an NFA, its determinised version should accept the same words.

An automaton and the regex it generates should accept the same words. Similarly, some regex and the automaton it generates should accept the same words.

An automaton, and the output of converting it into a regex and back to an automaton should accept the same words. Similarly with a regex and converting it into an automaton, and back into a regex.

Monadic second order logic with successor is equivalent to regex, DFAs, and NFAs,. There is an effective transformation between MSO formulas and automata, which we could implement.

Could implement hypothesis closure on automata and regular expression (in a subset of simple cases)