274 \mbox{@{term "SEQ (SEQ (STAR (ALT a b)) a) (NTIMES (ALT a b) n)"}} |
274 \mbox{@{term "SEQ (SEQ (STAR (ALT a b)) a) (NTIMES (ALT a b) n)"}} |
275 where the minimal DFA requires at least $2^{n + 1}$ states (see |
275 where the minimal DFA requires at least $2^{n + 1}$ states (see |
276 \cite{CountingSet2020}). Therefore regular expression matching |
276 \cite{CountingSet2020}). Therefore regular expression matching |
277 libraries that rely on the classic notion of DFAs often impose |
277 libraries that rely on the classic notion of DFAs often impose |
278 adhoc limits for bounded regular expressions: For example in the |
278 adhoc limits for bounded regular expressions: For example in the |
279 regular expression matching library in the Go language the regular expression |
279 regular expression matching library in the Go language and also in Google's RE2 library the regular expression |
280 @{term "NTIMES a 1001"} is not permitted, because no counter can be |
280 @{term "NTIMES a 1001"} is not permitted, because no counter can be |
281 above 1000, and in the built-in Rust regular expression library |
281 above 1000; and in the built-in regular expression library in Rust |
282 expressions such as @{text "a\<^bsup>{1000}{100}{5}\<^esup>"} give an error |
282 expressions such as @{text "a\<^bsup>{1000}{100}{5}\<^esup>"} give an error |
283 message for being too big. These problems can of course be solved in matching |
283 message for being too big. These problems can of course be solved in matching |
284 algorithms where automata go beyond the classic notion and for |
284 algorithms where automata go beyond the classic notion and for |
285 instance include explicit counters (see~\cite{CountingSet2020}). |
285 instance include explicit counters (see~\cite{CountingSet2020}). |
286 The point here is that Brzozowski derivatives and the algorithms by |
286 The point here is that Brzozowski derivatives and the algorithms by |