some implementation details

1 files changed, 23 insertions, 0 deletions

diff --git a/README.txt b/README.txt
index c9ebee5..ddfca3b 100644
--- a/README.txt
+++ b/README.txt
@@ -31,3 +31,26 @@ The following special symbols can be used, beyond the standard '()*|':
 
 I have *tried* to match the precdence from the slides, but not certain. When in
 doubt, please do use parentheses to disambiguate!
+
+===== Implementation Details
+Basic idea is to convert everything to DFAs, then construct the product DFA for
+the symmetric difference and then perform finite state model checking to see if
+there are any reachable accepting states.
+
+Of course, that blows up immediately to 2^{2n}. So, we instead do that
+procedure 'lazily,' i.e., convert everything only to NFAs and only materialize
+states in the final product DFA that are actually reachable.
+
+So, concretely what it looks like:
+
+    - For each $n$ we keep a list of states in the product DFA (which are pairs
+      of sets of states in the NFAs) that are first reachable on a string of
+      length $n$.
+
+    - If we ever encounter a state in the product DFA that would be accepting
+      in the symmetric difference DFA, we inform the user they're different.
+
+    - Compute that set recursively for each $n$ until the set is empty for some
+      $n$, i.e., every state in the product DFA that can be reached by a string
+      of length $n$ can also be reached by a string of length $k < n$. That
+      means we've reached fixedpoint, so we're done.