equal
deleted
inserted
replaced
86 derivatives finite. Without simplification the size derivatives can grow |
86 derivatives finite. Without simplification the size derivatives can grow |
87 arbitrarily big resulting in an extremely slow lexing algorithm. In this |
87 arbitrarily big resulting in an extremely slow lexing algorithm. In this |
88 paper we describe a variant of Sulzmann and Lu's algorithm: Our |
88 paper we describe a variant of Sulzmann and Lu's algorithm: Our |
89 algorithm is a recursive functional program, whereas Sulzmann |
89 algorithm is a recursive functional program, whereas Sulzmann |
90 and Lu's version involves a fixpoint construction. We \textit{(i)} |
90 and Lu's version involves a fixpoint construction. We \textit{(i)} |
91 prove in Isabelle/HOL that our program is correct and generates |
91 prove in Isabelle/HOL that our algorithm is correct and generates |
92 unique POSIX values; we also \textit{(ii)} establish a finite |
92 unique POSIX values; we also \textit{(ii)} establish a finite |
93 bound for the size of the derivatives. |
93 bound for the size of the derivatives. |
94 |
94 |
95 %The size can be seen as a |
95 %The size can be seen as a |
96 %proxy measure for the efficiency of the lexing algorithm: because of |
96 %proxy measure for the efficiency of the lexing algorithm: because of |