equal
deleted
inserted
replaced
429 \begin{proposition} |
429 \begin{proposition} |
430 @{thm L_flat_Prf} |
430 @{thm L_flat_Prf} |
431 \end{proposition} |
431 \end{proposition} |
432 |
432 |
433 In general there is more than one value associated with a regular |
433 In general there is more than one value associated with a regular |
434 expression. In case of POSIX matching the problem is to calculate the |
434 expression (meaining regular expressions can typically match more |
435 unique value that satisfies the (informal) POSIX rules from the |
435 than one string). But even given a string from the language of the |
436 Introduction. Graphically the POSIX value calculation algorithm by |
436 regular expression, there are generally more than one way how the |
|
437 regular expression can match this string. POSIX lexing is about identifying |
|
438 a unique value that satisfies the (informal) POSIX. Graphically the POSIX value calculation algorithm by |
437 Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz} |
439 Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz} |
438 where the path from the left to the right involving @{term derivatives}/@{const |
440 where the path from the left to the right involving @{term derivatives}/@{const |
439 nullable} is the first phase of the algorithm (calculating successive |
441 nullable} is the first phase of the algorithm (calculating successive |
440 \Brz's derivatives) and @{const mkeps}/@{text inj}, the path from right to |
442 \Brz's derivatives) and @{const mkeps}/@{text inj}, the path from right to |
441 left, the second phase. This picture shows the steps required when a |
443 left, the second phase. This picture shows the steps required when a |