63 expressions. Their algorithm generates POSIX values which encode |
63 expressions. Their algorithm generates POSIX values which encode |
64 the information of \emph{how} a regular expression matches a |
64 the information of \emph{how} a regular expression matches a |
65 string---that is, which part of the string is matched by which part |
65 string---that is, which part of the string is matched by which part |
66 of the regular expression. The purpose of the bitcodes is to generate POSIX values incrementally while |
66 of the regular expression. The purpose of the bitcodes is to generate POSIX values incrementally while |
67 derivatives are calculated. They also help with designing |
67 derivatives are calculated. They also help with designing |
68 an `aggressive' simplification function that keeps the size of |
68 an ``aggressive'' simplification function that keeps the size of |
69 derivatives small. Without simplification derivatives can grow |
69 derivatives small. Without simplification the size derivatives can grow |
70 exponentially resulting in an extremely slow lexing algorithm. In this |
70 exponentially resulting in an extremely slow lexing algorithm. In this |
71 paper we describe a variant of Sulzmann and Lu's algorithm: Our |
71 paper we describe a variant of Sulzmann and Lu's algorithm: Our |
72 algorithm is a recursive functional program, whereas Sulzmann |
72 algorithm is a recursive functional program, whereas Sulzmann |
73 and Lu's version involves a fixpoint construction. We \textit{(i)} |
73 and Lu's version involves a fixpoint construction. We \textit{(i)} |
74 prove in Isabelle/HOL that our program is correct and generates |
74 prove in Isabelle/HOL that our program is correct and generates |