Formal Regular ExpressionsThe Language Your CS Professor Uses
A new flavor for the theoretical regular expressions from formal language theory and automata — built for CS students, educators, and anyone who wants to test textbook exercises directly in the browser.
Why this flavor exists
Every undergraduate CS curriculum covers formal languages and automata — the mathematical foundations of computation. In these courses, students encounter regular expressions that look familiar but behave very differently from the regex they know from programming.
The problem is concrete: when a student writes a+b in a textbook exercise, they mean "a or b" (alternation). If they paste that into any standard regex tester, it matches "one or more a's followed by b" — completely different semantics. There was no way to test formal RE exercises in a real engine.
The Core Problem
A student types a+b into a regex tester to verify their homework. The tester says it matches aab. The student thinks they made an error. They didn't — the tool was wrong for this context.
The Formal flavor bridges this gap. It translates formal notation to JavaScript regex on the fly, enforces full-string matching, and provides a sandboxed environment that speaks the same language as lectures and textbooks.
What is a formal regular expression?
In formal language theory, a regular expression over an alphabet Σ is defined inductively by exactly three rules:
The profound result — proved by Stephen Kleene in 1956 — is that these three operations are sufficient to describe exactly the class of regular languages, which coincides with the languages accepted by finite automata (DFAs and NFAs). This is Kleene's theorem.
This flavor adds one practical extension: Σ as a shorthand for "any single alphabet character" — analogous to . in programming regex, but restricted to exclude newlines (which separate test strings).
Syntax reference
| Symbol | Name | Meaning | JS equivalent |
|---|---|---|---|
| ∅ | Empty set | No string accepted, not even ε | (?!) |
| ε | Empty string | Accepts only the empty string | (?:) |
| a | Literal | One specific alphabet character | a |
| Σ | Any char | One char from alphabet (not newline) | [^\n] |
| rs or r·s | Concat. | r followed immediately by s | rs |
| r|s or r+s | Union | Either r or s (+ ≠ one-or-more!) | r|s |
| r* | Kleene star | Zero or more copies of r | r* |
| (r) | Grouping | Override precedence, no capture | (?:r) |
Operator Precedence (high → low)
So ab*|c parses as (a(b*))|c, not a(b*|c).
⚠ Critical Difference
In formal RE, + is alternation / union, not "one or more". a+b ≡ a|b = {a, b}. To express "one or more a's", write aa*.
Formal RE vs. Programming regex
Formal RE (CS theory)
- —3 operators only: · | *
- —+ means OR (alternation)
- —No [char-class] syntax
- —No ? or {n,m} quantifiers
- —No backreferences \1
- —No lookahead/lookbehind
- —No flags (i, g, m, s…)
- —Always full-string match
- —ε and ∅ are first-class
- —Maps directly to DFA/NFA
Programming Regex
- —Dozens of operators
- —+ means one-or-more
- —[a-zA-Z0-9] ranges
- —?, {n,m}, lazy, possessive
- —Backreferences \1 (?P=n)
- —Lookahead (?=…) (?<!…)
- —Flags modify behavior
- —Substring search by default
- —No ε / ∅ literals
- —Often exceeds regular power
Who is this for?
CS Students
Test homework from automata theory and formal languages courses. Verify your DFA/NFA→RE conversion before the exam.
Educators
Share live examples in lectures and problem sets. Students experiment with no setup required.
Self-learners
Working through Sipser, Hopcroft–Ullman, or Kozen? Use this as a live companion to the textbook.
Researchers
Quickly validate small language examples while working on papers about regular languages.
Tool Builders
Cross-check formal language definitions against test cases before implementing a DFA.
The Curious
Want to understand the theory behind all programming regex? This is the mathematical foundation.
44 Worked Examples
Expand any card to see its test strings. Click ▶ Open or any chip to open the example in the interactive editor with full SEO-optimised URL. Each example page supports linking, sharing, and embedding.
∅Empty set ∅εEmpty string εaSingle literal characterΣΣ — any single characterΣ*Σ* — the universal languageabConcatenation: aba⋅bExplicit concatenation: a⋅baεε is the concatenation identity: aε = aa∅∅ annihilates concatenation: a∅ = ∅abcThree-character string: abcabΣ*Fixed prefix + free suffix: abΣ*a*a* — zero or more a(ab)*(ab)* — zero or more "ab" pairs(aa)*(aa)* — even-length strings of a(a*)*Star is idempotent: (a*)* = a*aΣ*baΣ*b — starts with a, ends with baa*"One or more a": aa*a|bAlternation with |: a|ba+b+ means OR in formal RE: a+ba|∅∅ is the union identity: a|∅ = aa|εOptionality via ε: a|εa|b|cThree-way alternation: a|b|ccat|dog|fishWord alternation: cat|dog|fishb|aAlternation is commutative: b|a = a|b(a|b)*a(a|b)*a — strings over {a,b} ending in a(a|b)*b(a|b)*b — strings over {a,b} ending in b(a|b)*aa(a|b)*(a|b)*aa(a|b)* — contains substring "aa"(b|ab)*(a|ε)(b|ab)*(a|ε) — no two consecutive a'sΣΣΣΣΣΣ — exactly 3 charactersΣΣΣ*ΣΣΣ* — length ≥ 2a(b|c)Distributive law: a(b|c) = ab|ac(aaa)*(aaa)* — unary multiples of 3aa|bbaa|bb — length-2 palindromesa(a|b)*a|b(a|b)*b|a|bStarts and ends with the same character(a|b)*a(a|b)(a|b)(a|b)*a(a|b)(a|b) — 3rd from end is a(ΣΣ)*(ΣΣ)* — even-length stringsa*(ba+)*a*(ba+)* — no consecutive b'sa+b⚠ Formal + vs programming + quantifierabcNo substring search — full-string only0|1|2|3|4|5|6|7|8|9No [char-class] — enumerate explicitly(a|ε)bNo ? quantifier — use (r|ε)Σ*aΣ*No backreferences — strictly regularHelloNo flags — always case-sensitive(a|b)*b(a|b)*No lookaheads — restructure insteadImplementation
The formal flavor runs a three-stage pipeline — parse, rewrite, execute — entirely client-side, with no external runtime. The grammar is enforced by a real recursive-descent parser (compiled to WASM, with an equivalent TypeScript fallback), not by textual substitution, so operator precedence is guaranteed by construction and invalid syntax fails with a precise, positioned error.
Stage 3 — automata execution. The rewritten pattern runs on the RE2 engine (the Rust regex crate compiled to WASM), which simulates automata instead of backtracking — matching is linear-time, so catastrophic backtracking is structurally impossible. One rewrite keeps the pattern RE2-native: ∅’s (?!) becomes the never-matching class [^\s\S]. If that engine can’t load, execution falls back to a dedicated Web Worker under a one-second watchdog that is hard-terminated on timeout with an explicit Execution timeout error — so the page never freezes either way.
Known limitations
Two items from the original version of this post have since been resolved — the operator-precedence parser shipped, and catastrophic backtracking is now eliminated: formal patterns execute on a linear-time automata engine. What remains is listed below with its current status.
Catastrophic backtracking
EliminatedOriginally formal patterns executed on the backtracking JavaScript engine (contained only by a watchdog). They now run on the RE2 automata engine (the Rust regex crate compiled to WASM), which matches in linear time — adversarial patterns like (a*)*b on non-matching input, which could exhaust any time budget under backtracking, now complete in microseconds. If the RE2 wasm can't load (blocked network, no Worker support), execution falls back to the JS engine inside a dedicated Web Worker that is hard-terminated on timeout — degraded to 'contained' for that session, never a frozen tab.
Operator characters cannot be literals
Parser shippedFormal RE has no escape syntax — a stray backslash is rejected with a positioned error ('\' is not a formal RE operator). So +, |, *, (, ), Σ, ε, and ∅ always act as operators or symbols; an alphabet containing + as a literal character cannot be expressed. (An earlier version of this post described the + → | rewrite as a text substitution and promised a full operator-precedence parser 'for a future update' — that parser has since shipped, see the Implementation section above, so precedence is now enforced by the grammar itself.)
Complement is not a formal RE operator
The complement of a regular language (¬L) is regular, but complement is not part of formal RE syntax. You cannot write ¬(ab*) — you must construct the complementary RE directly, which can be exponentially larger.
Non-regular patterns cannot be expressed
By designBalanced parentheses, arbitrary-length palindromes, and {aⁿbⁿ | n≥0} are not regular languages. No formal RE can express them. This is a feature — it reflects the true power boundary of regular languages.