1 \documentclass[runningheads]{lipics-v2021}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 \usepackage{mathpartir}

     8 \usepackage{tikz}

     9 \usepackage{pgf}

    10 \usetikzlibrary{positioning}

    11 %\usepackage{pdfsetup}

    12 %\usepackage{stmaryrd}

    13 %\usepackage{url}

    14 %\usepackage{color}

    15 %\usepackage[safe]{tipa}

    16 %\usepackage[sc]{mathpazo}

    17 %\usepackage{fontspec}

    18 %\setmainfont[Ligatures=TeX]{Palatino Linotype}

    19 

    20 

    21 

    22 

    23 \urlstyle{rm}

    24 \isabellestyle{it}

    25 \renewcommand{\isastyleminor}{\it}% 

    26 \renewcommand{\isastyle}{\normalsize\it}%

    27 

    28 

    29 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    30 \renewcommand{\isasymequiv}{$\dn$}

    31 \renewcommand{\isasymemptyset}{$\varnothing$}

    32 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    33 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}

    34 \renewcommand{\isasymin}{\ensuremath{\,\in\,}}

    35 

    36 

    37 \def\Brz{Brzozowski}

    38 \def\der{\backslash}

    39 \newtheorem{falsehood}{Falsehood}

    40 \newtheorem{conject}{Conjecture}

    41 

    42 \bibliographystyle{plainurl}

    43 

    44 \title{{POSIX} {L}exing with {B}itcoded {D}erivatives}

    45 \titlerunning{POSIX Lexing with Bitcoded Derivatives}

    46 \author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}

    47 \author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}

    48 

    49 

    50 \begin{document}

    51 \maketitle

    52 

    53 \begin{abstract}

    54 Brzozowski introduced the notion of derivatives for regular

    55 expressions. They can be used for a very simple regular expression

    56 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm

    57 in order to deal with POSIX matching, which is the underlying

    58 disambiguation strategy for regular expressions needed in lexers.

    59 Their algorithm generates POSIX values which encode the information of

    60 \emph{how} a regular expression matches a string---that is, which part

    61 of the string is matched by which part of the regular expression.  In

    62 this paper we give our inductive definition of what a POSIX value is

    63 and show $(i)$ that such a value is unique (for given regular

    64 expression and string being matched) and $(ii)$ that Sulzmann and Lu's

    65 algorithm always generates such a value (provided that the regular

    66 expression matches the string). We show that $(iii)$ our inductive

    67 definition of a POSIX value is equivalent to an alternative definition

    68 by Okui and Suzuki which identifies POSIX values as least elements

    69 according to an ordering of values.  We also prove the correctness of

    70 Sulzmann's bitcoded version of the POSIX matching algorithm and extend the

    71 results to additional constructors for regular expressions.  \smallskip

    72 

    73 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,

    74 Isabelle/HOL

    75 \end{abstract}

    76 

    77 

    78 

    79 \input{session}

    80 

    81 

    82 

    83 \end{document}

    84 

    85 %%% Local Variables:

    86 %%% mode: latex

    87 %%% TeX-master: t

    88 %%% End: