thys/Paper/Paper.thy
changeset 269 12772d537b71
parent 193 1fd7388360b6
child 362 e51c9a67a68d
equal deleted inserted replaced
268:6746f5e1f1f8 269:12772d537b71
   141 
   141 
   142 One limitation of Brzozowski's matcher is that it only generates a
   142 One limitation of Brzozowski's matcher is that it only generates a
   143 YES/NO answer for whether a string is being matched by a regular
   143 YES/NO answer for whether a string is being matched by a regular
   144 expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher
   144 expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher
   145 to allow generation not just of a YES/NO answer but of an actual
   145 to allow generation not just of a YES/NO answer but of an actual
   146 matching, called a [lexical] {\em value}. They give a simple algorithm
   146 matching, called a [lexical] {\em value}. \marginpar{explain what values are} They give a simple algorithm
   147 to calculate a value that appears to be the value associated with
   147 to calculate a value that appears to be the value associated with
   148 POSIX matching.  The challenge then is to specify that value, in an
   148 POSIX matching.  The challenge then is to specify that value, in an
   149 algorithm-independent fashion, and to show that Sulzmann and Lu's
   149 algorithm-independent fashion, and to show that Sulzmann and Lu's
   150 derivative-based algorithm does indeed calculate a value that is
   150 derivative-based algorithm does indeed calculate a value that is
   151 correct according to the specification.
   151 correct according to the specification.