\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 regularexpressions. They can be used for a very simple regular expressionmatching algorithm. Sulzmann and Lu cleverly extended this algorithmin order to deal with POSIX matching, which is the underlyingdisambiguation strategy for regular expressions needed in lexers. Inthe first part of this paper we give our inductive definition of whata POSIX value is and show $(i)$ that such a value is unique (for givenregular expression and string being matched) and $(ii)$ that Sulzmannand Lu's algorithm always generates such a value (provided that theregular expression matches the string). We also prove the correctnessof an optimised version of the POSIX matching algorithm. In thesecond part we show that $(iii)$ our inductive definition of a POSIXvalue is equivalent to an alternative definition by Okui and Suzukiwhich identifies POSIX values as least elements according to anordering 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: