Recognizing regular patterns in mixed type sequences using Symbolic Finite Automata
summary
Library implements Regular Type Expressions as s-exprs and builds symbolic finite automata (using a Brzozowski-derivative style construction) to recognize mixed-type sequences in linear time. It embeds a SETS-style type algebra (union, intersection, complement, singleton, predicate types), partitions types into disjoint regions to guarantee deterministic DFA behavior even when subtype queries are undecidable, and exposes runtime pattern dispatch and unreachable-branch detection. Code is available as clojure-rte on GitHub; some automaton transitions may remain provably unsatisfiable or indeterminate.
AI-written summary · about
chapters (9)
- 0:00Introduction and background
- 3:05Motivating demo
- 10:07Regular type expressions
- 12:26Pattern matching mechanics
- 14:00Deterministic automata
- 16:12Type lattice challenges
- 18:56Construction and theory
- 22:40Advanced usage examples
- 28:28Conclusion
related talks
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
19mWell-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
01h 03mCompile-Time Regular Expressions
20mClojure Tools for Symbolic Artificial Intelligence
14mA Word Sampler for Well-Typed Functions
38mHybrid Automata and the Continuous Life
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi