\documentclass[runningheads]{llncs}
\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}



\titlerunning{POSIX Lexing with Derivatives of Regular Expressions}

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

\begin{document}
\renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a
  revised and expanded version of \cite{AusafDyckhoffUrban2016}.
  Compared with that paper we give a second definition for POSIX
  values introduced by Okui Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech}
  and prove that it is
  equivalent to our original one. This
  second definition is based on an ordering of values and very similar to,
  but not equivalent with, the
  definition given by Sulzmann and Lu~\cite{Sulzmann2014}.
  The advantage of the definition based on the
  ordering is that it implements more directly the informal rules from the
  POSIX standard.
  We also
  extend our results to additional constructors of regular
  expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}


\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}
\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}
\institute{King's College London\\
		\email{fahad.ausaf@icloud.com}
\and University of St Andrews\\
		\email{roy.dyckhoff@st-andrews.ac.uk}
\and King's College London\\
		\email{christian.urban@kcl.ac.uk}}
\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 matched a string---that is which part
of the string is matched by which part of the regular expression.  In
the first part of 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 also prove the correctness
of an optimised version of the POSIX matching algorithm.  In the
second part 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. \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: