13 in chapter \ref{Introduction}. |
13 in chapter \ref{Introduction}. |
14 This is a quite deep problem, |
14 This is a quite deep problem, |
15 with theoretical work on them being |
15 with theoretical work on them being |
16 fairly recent. |
16 fairly recent. |
17 |
17 |
18 Campaneu gave |
18 Campaneu et al. studied regexes with back-references |
|
19 in the context of formal languages theory in |
|
20 their 2003 work \cite{campeanu2003formal}. |
|
21 They devised a pumping lemma for Perl-like regexes, |
|
22 proving that the langugages denoted by them |
|
23 is properly contained in context-sensitive |
|
24 languages. |
|
25 More interesting questions such as |
|
26 whether the language denoted by Perl-like regexes |
|
27 can express palindromes ($\{w \mid w = w^R\}$) |
|
28 are discussed in \cite{campeanu2009patterns} |
|
29 and \cite{CAMPEANU2009Intersect}. |
|
30 Freydenberger \cite{Frey2013} investigated the |
|
31 expressive power of back-references. He showed several |
|
32 undecidability and decriptional complexity results |
|
33 of back-references, concluding that they add |
|
34 great power to certain programming tasks but are difficult to harness. |
|
35 An interesting question would then be |
|
36 whether we can add restrictions to them, |
|
37 so that they become expressive enough, but not too powerful. |
|
38 Freydenberger and Schmid \cite{FREYDENBERGER20191} |
|
39 introduced the notion of deterministic |
|
40 regular expressions with back-references to achieve |
|
41 a better balance between expressiveness and tractability. |
19 |
42 |
20 |
43 |
21 See \cite{AHO1990255} for a survey |
44 Fernau and Schmid \cite{FERNAU2015287} and Schmid \cite{Schmid2012} |
|
45 investigated the time complexity of different variants |
|
46 of back-references. |
|
47 |
|
48 See \cite{BERGLUND2022} for a survey |
22 of these works and comparison between different |
49 of these works and comparison between different |
23 flavours (e.g. whether references can be circular, |
50 flavours of back-references syntax (e.g. whether references can be circular, |
24 can labels be repeated etc.) of back-references syntax. |
51 can labels be repeated etc.). |
25 |
52 |
26 |
53 |
27 \subsection{Matchers and Lexers with Mechanised Proofs} |
54 \subsection{Matchers and Lexers with Mechanised Proofs} |
28 We are aware |
55 We are aware |
29 of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by |
56 of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by |