Grammar Formalization: Define Regex Syntax as a Context‑Free Grammar

(This issue is AI-generated an may contain an error. Please comment on the issue to discuss what we'll prove)

Difficulty: Intermediate (Phase 1, 2), Advanced (Phase 3, 4) Area: Regex syntax / parsing / formal verification

Summary

This issue proposes to formally specify the concrete syntax of the regex patterns language (things like [^a-c\d]+) as a context‑free grammar (CFG), and to connect it to the existing parser in regex/Regex/Syntax/Parser.
The end goal is to have:

• A clear grammar specification for the regex syntax used by this library.
• A corresponding Mathlib.Computability.ContextFreeGrammar value capturing the same language as a context-free grammar.

Stretch goals include defining LL(k) languages, checking whether this grammar is LL(1) (or close to it), and (eventually) rewriting the parser with a correctness proof against the formal grammar.

---

Current Status

Currently:

• ✅ We have a working recursive‑descent parser implemented in
  regex/Regex/Syntax/Parser/Basic.lean and its combinator infrastructure in
  regex/Regex/Syntax/Parser/Combinators*.lean.
• ✅ We have an AST for regex syntax in
  regex/Regex/Syntax/Ast.lean, and a translation from Ast to the semantic Expr (Ast.toRegex).
• ✅ The parser supports a reasonably rich syntax:
  • Primary constructs:
    • Literal characters
    • Character classes [ ... ] (with ranges, negation, Perl classes inside, etc.)
    • Dot . (any char except newline, per current semantics)
    • Anchors: ^, $, \b, \B
    • Grouping: (...)
    • Non‑capturing groups: (?:...)
  • Operators:
    • Alternation: |
    • Concatenation (implicit)
  • Repetition:
    • *, +, ?
    • {n}, {n,}, {n,m}
    • Greedy / non‑greedy via trailing ?
  • Escapes:
    • Simple escapes: \n, \t, \r, \a, \f, \v, \0, \-, \], \}, and any special metacharacter escaped.
    • Hex escapes: \xNN, \uNNNN
    • Perl classes: \d, \D, \s, \S, \w, \W
• ❌ There is no single, formal grammar (BNF / CFG) in the code or docs that precisely describes the accepted concrete syntax. Rather, the grammar is defined by the implementation.
• ❌ There is no ContextFreeGrammar value in Mathlib corresponding to this syntax.
• ❌ There is no machine‑checked statement that “the parser recognizes exactly the language of this grammar”.

This issue aims to fill that gap.

---

Goals

• Define a formal grammar of the regex concrete syntax (the syntax of strings like [^a-c\d]+), ideally:
  • As a human‑readable BNF (or equivalent) in this repository.
  • As a Lean definition closely mirroring that BNF.
• Confirm that the grammar is context‑free, and encode it as a Mathlib.Computability.ContextFreeGrammar:
  • Choose suitable types of terminals / nonterminals.
  • Provide the production rules as a value of ContextFreeGrammar.
  • Show that this value generates exactly the intended language of regex patterns.

Stretch goals:

• Define LL(k) languages and check whether this grammar is LL(1) (or close to LL(1)):
  • Formally define LL(k) in Lean (if not already provided).
  • Analyze / approximate FIRST / FOLLOW sets for this grammar.
  • Determine whether the grammar as written is LL(1), LL(k) for some k, or not LL(k) at all.
• Rewrite the parser and prove that it correctly implements the grammar:
  • Implement a new parser (e.g., a recursive-decent parser following the LL(1) structure) and prove:
    • Soundness: every parsed AST comes from a word in the CFG language.
    • Completeness: every word in the CFG language can be parsed into an AST accepted by the parser.

---

Target Syntax (Informal Overview)

The formal grammar should match the current behavior of Regex.Syntax.Parser.Basic as closely as possible. However, if small tweaks to the behavior makes the grammar context-free or LL(1), it's okay to change the grammar (please discuss with me).

Roughly, the surface language includes:

• Top‑level structure:
  • A regex is an alternation of concatenations, where concatenations are sequences of repeated primaries.
• Primaries (Primary in the informal grammar below):
  • Char (ordinary characters, excluding metacharacters unless escaped)
  • . (dot)
  • Anchors: ^, $, \b, \B
  • Character classes:
    • [ ... ] with:
      • Optional leading ^ (negation).
      • Single characters.
      • Ranges a-z.
      • Perl classes inside ranges cause errors (per implementation), so the grammar for valid patterns must account for that.
        • It's permissible to accept it in the grammar, but add a validation phase to reject it later.
  • Groups:
    • Capturing: ( R )
    • Non‑capturing: (?: R )
  • Escaped characters and classes:
    • Standard escapes (\n, \t, \\, etc.).
    • Hex and Unicode escapes (\xNN, \uNNNN).
    • Perl classes \d, \s, \w and their negations.
• Repetition operators:
  • *, +, ?
  • {n}, {n,}, {n,m} with trailing ? for non‑greedy.
• Alternation and concatenation:
  • A | B binds weaker than concatenation; concatenation is implicit between primaries / repetitions.

---

Proposed Formal Grammar (BNF Sketch)

The final grammar may evolve during the work, but a starting point for the core structure could look like:

Regex       ::= Alternate

Alternate   ::= Concat ('|' Concat)*

Concat      ::= Repetition*

Repetition  ::= Primary RepetitionOp*

RepetitionOp
  ::= '*' '?'?
   | '+' '?'?
   | '?' '?'?
   | '{' Number (',' Number?)? '}' '?'?

Primary
  ::= Char
   | '.'
   | Anchor
   | Class
   | Group
   | EscapedChar

Group
  ::= '(' Regex ')'
   | '(?:' Regex ')'

Anchor
  ::= '^'
   | '$'
   | '\b'
   | '\B'

Class
  ::= '[' '^'? ClassItem+ ']'

ClassItem
  ::= Range
   | ClassAtom

Range
  ::= ClassAtom '-' ClassAtom

ClassAtom
  ::= ClassChar
   | PerlClass

EscapedChar
  ::= SimpleEscape
   | HexEscape
   | UnicodeEscape
   | PerlClass

PerlClass
  ::= '\d' | '\D' | '\s' | '\S' | '\w' | '\W'

Number      ::= Digit+

Digit       ::= '0' | '1' | ... | '9'

(* Details of Char, ClassChar, SimpleEscape, HexEscape, UnicodeEscape, etc. should be specified. *)

This grammar description should:

• Be made precise enough that we can directly translate it into Lean.
• Explicitly document any intentional exclusions (e.g., invalid ranges, forbidden Perl classes in ranges) as either:
  • Part of the grammar of valid patterns, or
  • Separate “well‑formedness” predicates on parsed ASTs.

---

Context‑Free Grammar in Mathlib

Mathlib provides Computability.ContextFreeGrammar (and related definitions) for representing context‑free grammars in Lean. The goal here is to:

• Choose types:
  • Terminals: likely some representation of input characters / tokens (Char directly, or a token type if we want to separate lexing).
  • Nonterminals: an inductive type such as:

    inductive Nonterminal
    | regex | alternate | concat | repetition
    | primary | group | class | classItem | range | ...
    

• Instantiate a ContextFreeGrammar value:
  • start := Nonterminal.regex
  • productions listing all the rules corresponding to the BNF.
• Relate the grammar to the concrete syntax:
  • If terminals are Char, the language is a subset of List Char.
  • If a separate token type is introduced, the grammar will be over token lists, and we will separately specify a lexer from String to token lists.

At the end of this phase, we should have:

• A Lean definition regexGrammar : ContextFreeGrammar Nonterminal Terminal (names TBD).
• A brief explanation / comments linking each production back to its BNF counterpart and to the corresponding part of the existing parser.

---

Implementation Tasks

Below is a suggested phasing of the work. PRs do not need to strictly follow these phases, but this gives a rough roadmap.

Phase 1: Formal Grammar Definition at the BNF Level

• Carefully read the existing parser (Parser.Basic) and produce a list of accepted syntactic forms.
• Based on that analysis, write a BNF or EBNF‑style grammar for the regex syntax in this repository:
  • Use the sketch in this issue as a starting point and refine / extend it.
  • Decide whether to encode certain error cases (e.g. reversed ranges, Perl classes in ranges) as forbidden by the grammar or as allowed by the grammar but rejected later by a validation phase.
• For each nonterminal / production in the BNF, add comments indicating which Lean definitions (primary, repetition, concat, alternate, group, classes, etc.) correspond to it.

Phase 2: Grammar as Mathlib.Computability.ContextFreeGrammar

• Design and define the types Nonterminal and Terminal.
• Use Mathlib’s ContextFreeGrammar structure to define a grammar regexGrammar : ContextFreeGrammar Terminal Nonterminal corresponding to the BNF.
• Check (informally) whether the language generated by regexGrammar matches the BNF‑specified regex syntax.

Phase 3 (Stretch): LL(k) Languages and LL(1) Check

• Define LL(k) languages in Lean (or reuse existing definitions if they already exist).
• For regexGrammar:
  • Add definitions / lemmas that correspond to FIRST / FOLLOW sets or similar analyses.
  • Investigate whether the grammar is LL(1), LL(k) for some k, or not LL(k) at all; at minimum, identify where LL(1)‑ness fails.

Phase 4 (Stretch): Parser Rewrite and Correctness Proof

• Design a new parser whose structure directly reflects regexGrammar, e.g. a recursive‑descent parser with one function per nonterminal.
• Prove correctness of this parser with respect to the CFG:
  • Soundness: whenever the parser succeeds and returns an AST, the input string is in the language generated by regexGrammar.
  • Completeness: whenever a string is in the language generated by regexGrammar, the parser succeeds and produces an AST.
• (Ambitious optional extension) Define a pretty‑printer from ASTs back to strings, and explore round‑trip properties (e.g. that parsing then pretty‑printing yields a string in the same equivalence class of the grammar).

---

Acceptance Criteria

• The concrete regex syntax has a complete BNF (or equivalent formal grammar) checked into the repository.
• The relationship between the BNF and the existing parser (Parser.Basic) / AST (Ast) is explained via comments.
• A Mathlib.Computability.ContextFreeGrammar value (e.g. regexGrammar) is defined that represents this grammar.
• It is made clear, at least informally (and ideally with some Lean support), that this grammar is context‑free.
• Stretch: There is some LL(1) / LL(k) analysis of regexGrammar recorded in the code or documentation.
• Stretch: There is at least a plan, and possibly partial proofs, connecting the new parser to regexGrammar via soundness and completeness properties.

---

Resources & References

• regex/Regex/Syntax/Parser/Basic.lean
  Main recursive‑descent parser definitions (group, primary, repetition, concat, alternate, regex, etc.).
• regex/Regex/Syntax/Ast.lean
  Syntax tree Ast for regular expressions, and Ast.toRegex for translation to semantic Expr.
• regex/Regex/Data/Expr.lean
  Semantic (expression‑level) representation of regular expressions.
• Mathlib: the Computability.ContextFreeGrammar definitions and related modules.
  (See the Mathlib repository for precise types and APIs.)
• Standard references on formal language theory (e.g. Hopcroft–Ullman) and any existing formal grammars for regex‑like languages.

---

Notes for Contributors

• Difficulty: Intermediate-Advanced
  • Prior exposure to formal language theory (CFGs, LL(k), etc.) will help a lot.
  • Experience with Lean / Mathlib formalizations is very valuable, but not strictly required; the issue aims to give enough pointers to get started.
• Estimated effort:
  • Phases 1–2 (grammar definition + CFG instantiation) are already a non‑trivial project and may take days to weeks of focused effort.
  • The stretch goals (LL(1) analysis, parser correctness proofs) are likely to be a longer‑term effort.