thys3/Paper.thy
changeset 617 3ea6a38c33b5
parent 616 8907d4b6316d
child 642 6c13f76c070b
equal deleted inserted replaced
616:8907d4b6316d 617:3ea6a38c33b5
  1553 uses derivatives for obtaining an automaton (it essentially bounds
  1553 uses derivatives for obtaining an automaton (it essentially bounds
  1554 the number of states). However, this result does \emph{not}
  1554 the number of states). However, this result does \emph{not}
  1555 transfer to our setting where we are interested in the \emph{size} of the
  1555 transfer to our setting where we are interested in the \emph{size} of the
  1556 derivatives. For example it is not true for our derivatives that the
  1556 derivatives. For example it is not true for our derivatives that the
  1557 set of of derivatives $r \backslash s$ for a given $r$ and all strings
  1557 set of of derivatives $r \backslash s$ for a given $r$ and all strings
  1558 $s$ is finite. This is because for our annotated regular expressions
  1558 $s$ is finite (even when simplified). This is because for our annotated regular expressions
  1559 the bitcode annotation is dependent on the number of iterations that
  1559 the bitcode annotation is dependent on the number of iterations that
  1560 are needed for STAR-regular expressions. This is not a problem for us: Since we intend to do lexing
  1560 are needed for STAR-regular expressions. This is not a problem for us: Since we intend to do lexing
  1561 by calculating (as fast as possible) derivatives, the bound on the size
  1561 by calculating (as fast as possible) derivatives, the bound on the size
  1562 of the derivatives is important, not the number of derivatives.
  1562 of the derivatives is important, not the number of derivatives.
  1563 
  1563