1 \documentclass[runningheads]{llncs}

     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 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}

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

    43 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a

    44   revised and expanded version of \cite{AusafDyckhoffUrban2016}.

    45   Compared with that paper we give a second definition for POSIX

    46   values introduced by Okui Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech}

    47   and prove that it is

    48   equivalent to our original one. This

    49   second definition is based on an ordering of values and very similar to,

    50   but not equivalent with, the

    51   definition given by Sulzmann and Lu~\cite{Sulzmann2014}.

    52   The advantage of the definition based on the

    53   ordering is that it implements more directly the informal rules from the

    54   POSIX standard.

    55   We also prove Sulzmann \& Lu's conjecture that their bitcoded version

    56   of the POSIX algorithm is correct. Furthermore we extend our results to additional constructors of regular

    57   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}

    58 

    59 

    60 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}

    61 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}

    62 \institute{King's College London\\

    63 		\email{fahad.ausaf@icloud.com}

    64 \and University of St Andrews\\

    65 		\email{roy.dyckhoff@st-andrews.ac.uk}

    66 \and King's College London\\

    67 		\email{christian.urban@kcl.ac.uk}}

    68 \maketitle

    69 

    70 \begin{abstract}

    71 Brzozowski introduced the notion of derivatives for regular

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

    73 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm

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

    75 disambiguation strategy for regular expressions needed in lexers.

    76 Their algorithm generates POSIX values which encode the information of

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

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

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

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

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

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

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

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

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

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

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

    88 results to additional constructors for regular expressions.  \smallskip

    89 

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

    91 Isabelle/HOL

    92 \end{abstract}

    93 

    94 \input{session}

    95 

    96 \end{document}

    97 

    98 %%% Local Variables:

    99 %%% mode: latex

   100 %%% TeX-master: t

   101 %%% End: