Regular Expressions #
This file contains the formal definition for regular expressions and basic lemmas. Note these are regular expressions in terms of formal language theory. Note this is different to regex's used in computer science such as the POSIX standard.
- Show that this regular expressions and DFA/NFA's are equivalent.
attribute [pattern] has_mul.mulhas been added into this file, it could be moved.
- zero : Π (α : Type u), regular_expression α
- epsilon : Π (α : Type u), regular_expression α
- char : Π (α : Type u), α → regular_expression α
- plus : Π (α : Type u), regular_expression α → regular_expression α → regular_expression α
- comp : Π (α : Type u), regular_expression α → regular_expression α → regular_expression α
- star : Π (α : Type u), regular_expression α → regular_expression α
This is the definition of regular expressions. The names used here is to mirror the definition of a Kleene algebra (https://en.wikipedia.org/wiki/Kleene_algebra).
zero) matches nothing
epsilon) matches only the empty string
char amatches only the string 'a'
star Pmatches any finite concatenation of strings which match
P + Q(
plus P Q) matches anything which match
P * Q(
comp P Q) matches
x ++ yif
matches P provides a language which contains all strings that
match_epsilon P is true if and only if
P matches the empty string
P.deriv a matches
a :: x, the Brzozowski derivative of
P with respect