\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}+ −
\usepackage[sc]{mathpazo}+ −
\usepackage{fontspec}+ −
\setmainfont[Ligatures=TeX]{Palatino Linotype}+ −
+ −
+ −
\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 prove Sulzmann \& Lu's conjecture that their bitcoded version+ −
of the POSIX algorithm is correct. Furthermore we 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 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:+ −