\documentclass[runningheads]{lipics-v2021}

\usepackage{times}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{mathpartir}

\usepackage{tikz}

\usepackage{pgf}

\usetikzlibrary{positioning}

%\usepackage{pdfsetup}

%\usepackage{stmaryrd}

%\usepackage{url}

%\usepackage{color}

%\usepackage[safe]{tipa}

%\usepackage[sc]{mathpazo}

%\usepackage{fontspec}

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

\urlstyle{rm}

\isabellestyle{it}

\renewcommand{\isastyleminor}{\it}% 

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

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

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

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

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

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

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

\def\Brz{Brzozowski}

\def\der{\backslash}

\newtheorem{falsehood}{Falsehood}

\newtheorem{conject}{Conjecture}

\bibliographystyle{plainurl}

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

\titlerunning{POSIX Lexing with Bitcoded Derivatives}

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

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

\keywords{POSIX matching, Derivatives of Regular Expressions, Isabelle/HOL}

\category{}

\ccsdesc[100]{Design and analysis of algorithms}

\ccsdesc[100]{Formal languages and automata theory}

\Copyright{\mbox{}}

\nolinenumbers

\begin{document}

\maketitle

\begin{abstract}

  Sulzmann and Lu described a lexing algorithm that calculates

  Brzozowski derivatives using bit-sequences annotated to regular

  expressions.  Their algorithm generates POSIX values which encode

  the information of \emph{how} a regular expression matches a

  string---that is, which part of the string is matched by which part

  of the regular expression.  The purpose of the bit-sequences in

  Sulzmann and Lu's algorithm is to keep the size of derivatives small

  which is achieved by `aggressively' simplifying regular expressions.

  In this paper we describe a slight variant of Sulzmann and Lu's

  algorithm and \textit{(i)} prove that this algorithm generates

  unique POSIX values; \textit{(ii)} we also establish a cubic bound

  for the size of the derivatives---in earlier works, derivatives can

  grow exponentially even after simplification.

%Brzozowski introduced the notion of derivatives for regular

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

%matching algorithm.  Sulzmann and Lu cleverly extended this algorithm

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

%disambiguation strategy for regular expressions needed in lexers.

%Their algorithm generates POSIX values which encode the information of

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

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

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

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

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

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

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

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

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

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

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

%results to additional constructors for regular expressions.  \smallskip

\end{abstract}

\input{session}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: