\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}{}{}

\begin{document}

\maketitle

\begin{abstract}

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

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

Isabelle/HOL

\end{abstract}

\input{session}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: