equal
deleted
inserted
replaced
68 \begin{abstract} |
68 \begin{abstract} |
69 Brzozowski introduced the notion of derivatives for regular |
69 Brzozowski introduced the notion of derivatives for regular |
70 expressions. They can be used for a very simple regular expression |
70 expressions. They can be used for a very simple regular expression |
71 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
71 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
72 in order to deal with POSIX matching, which is the underlying |
72 in order to deal with POSIX matching, which is the underlying |
73 disambiguation strategy for regular expressions needed in lexers. In |
73 disambiguation strategy for regular expressions needed in lexers. |
|
74 Their algorithm generates POSIX values which encode the information of |
|
75 \emph{how} a regular expression matched a string---that is which part |
|
76 of the string is matched by which part of the regular expression. In |
74 the first part of this paper we give our inductive definition of what |
77 the first part of this paper we give our inductive definition of what |
75 a POSIX value is and show $(i)$ that such a value is unique (for given |
78 a POSIX value is and show $(i)$ that such a value is unique (for given |
76 regular expression and string being matched) and $(ii)$ that Sulzmann |
79 regular expression and string being matched) and $(ii)$ that Sulzmann |
77 and Lu's algorithm always generates such a value (provided that the |
80 and Lu's algorithm always generates such a value (provided that the |
78 regular expression matches the string). We also prove the correctness |
81 regular expression matches the string). We also prove the correctness |