24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
27 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
25 \renewcommand{\isasymequiv}{$\dn$} |
28 \renewcommand{\isasymequiv}{$\dn$} |
26 \renewcommand{\isasymemptyset}{$\varnothing$} |
29 \renewcommand{\isasymemptyset}{$\varnothing$} |
27 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
30 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
28 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}} |
31 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}} |
|
32 \renewcommand{\isasymin}{\ensuremath{\,\in\,}} |
|
33 |
29 |
34 |
30 \def\Brz{Brzozowski} |
35 \def\Brz{Brzozowski} |
31 \def\der{\backslash} |
36 \def\der{\backslash} |
32 \newtheorem{falsehood}{Falsehood} |
37 \newtheorem{falsehood}{Falsehood} |
33 \newtheorem{conject}{Conjecture} |
38 \newtheorem{conject}{Conjecture} |
34 |
39 |
35 \begin{document} |
40 \begin{document} |
36 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a |
41 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a |
37 revised and expanded version of \cite{AusafDyckhoffUrban2016}. |
42 revised and expanded version of \cite{AusafDyckhoffUrban2016}. |
38 Compared with that paper we give a second definition for POSIX |
43 Compared with that paper we give a second definition for POSIX |
39 values and prove that it is equivalent to the original one. This |
44 values introduced by Okui Suzuki \cite{OkuiSuzuki2013} and prove that it is |
40 definition is based on an ordering of values and very similar to the |
45 equivalent to our original one. This |
|
46 second definition is based on an ordering of values and very similar to, |
|
47 but not equivalent with, the |
41 definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also |
48 definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also |
42 extend our results to additional constructors of regular |
49 extend our results to additional constructors of regular |
43 expressions.} \renewcommand{\thefootnote}{\arabic{footnote}} |
50 expressions.} \renewcommand{\thefootnote}{\arabic{footnote}} |
44 |
51 |
45 |
52 |
52 \and King's College London\\ |
59 \and King's College London\\ |
53 \email{christian.urban@kcl.ac.uk}} |
60 \email{christian.urban@kcl.ac.uk}} |
54 \maketitle |
61 \maketitle |
55 |
62 |
56 \begin{abstract} |
63 \begin{abstract} |
57 |
|
58 Brzozowski introduced the notion of derivatives for regular |
64 Brzozowski introduced the notion of derivatives for regular |
59 expressions. They can be used for a very simple regular expression |
65 expressions. They can be used for a very simple regular expression |
60 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
66 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
61 in order to deal with POSIX matching, which is the underlying |
67 in order to deal with POSIX matching, which is the underlying |
62 disambiguation strategy for regular expressions needed in lexers. In |
68 disambiguation strategy for regular expressions needed in lexers. In |
66 and Lu's algorithm always generates such a value (provided that the |
72 and Lu's algorithm always generates such a value (provided that the |
67 regular expression matches the string). We also prove the correctness |
73 regular expression matches the string). We also prove the correctness |
68 of an optimised version of the POSIX matching algorithm. In the |
74 of an optimised version of the POSIX matching algorithm. In the |
69 second part we show that $(iii)$ our inductive definition of a POSIX |
75 second part we show that $(iii)$ our inductive definition of a POSIX |
70 value is equivalent to an alternative definition by Okui and Suzuki |
76 value is equivalent to an alternative definition by Okui and Suzuki |
71 which identifies a POSIX value as least element according to an |
77 which identifies POSIX values as least elements according to an |
72 ordering of values. The advantage of the definition based on the |
78 ordering of values. The advantage of the definition based on the |
73 ordering is that it implements more directly the POSIX |
79 ordering is that it implements more directly the informal rules from the |
74 longest-leftmost matching semantics.\smallskip |
80 POSIX standard.\smallskip |
75 |
81 |
76 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
82 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
77 Isabelle/HOL |
83 Isabelle/HOL |
78 \end{abstract} |
84 \end{abstract} |
79 |
85 |