1424    of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates POSIX matches and is based on

  1424    of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates

  1425    derivatives \cite{verbatim}. In this case derivatives are not simplified.

  1425    POSIX matches and is based on

  1426    derivatives \cite{verbatim}. In this case derivatives are not even simplified.

  1427    They write: ``For a specific list of lexical rules, Verbatim has quadratic

  1428    theoretical time complexity with respect to the length of the input string.''

  1429    While their correctness proof for Verbatim is formalised in Coq, the claim about

  1430    the runtime complexity is only supported by emperical evidence.

  1431    When we

  1432    tried out their extracted OCaml code with our example

  1433    \mbox{@{text "(a + aa)\<^sup>*"}}, it took around 5 minutes to tokenise a

  1434    string of 40 $a$'s and that increased to approximately 19 minutes when the

  1435    string was 50 $a$'s long. Given that derivatives are not simplified in

  1436    the work on Verbatim, such numbers are not surprising. 

  1427    derivatives is rather weak in this context but we think such effeciency claims

  1438    derivatives might sound rather weak in this context but we think such effeciency claims

  1428    require further scrutiny.\medskip

  1439    really require further scrutiny.\medskip