thys3/document/root.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Sat, 30 Apr 2022 00:50:08 +0100
changeset 496 f493a20feeb3
child 499 6a100d32314c
permissions -rw-r--r--
updated to include the paper
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
496
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     1
\documentclass[runningheads]{lipics-v2021}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     2
\usepackage{times}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     3
\usepackage{isabelle}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     4
\usepackage{isabellesym}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     5
\usepackage{amsmath}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     6
\usepackage{amssymb}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     7
\usepackage{mathpartir}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     8
\usepackage{tikz}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     9
\usepackage{pgf}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    10
\usetikzlibrary{positioning}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    11
%\usepackage{pdfsetup}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    12
\usepackage{stmaryrd}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    13
%\usepackage{url}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    14
%\usepackage{color}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    15
%\usepackage[safe]{tipa}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    16
%\usepackage[sc]{mathpazo}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    17
%\usepackage{fontspec}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    18
%\setmainfont[Ligatures=TeX]{Palatino Linotype}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    19
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    20
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    21
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    22
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    23
\urlstyle{rm}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    24
\isabellestyle{it}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    25
\renewcommand{\isastyleminor}{\it}% 
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    26
\renewcommand{\isastyle}{\normalsize\it}%
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    27
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    28
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    29
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    30
\renewcommand{\isasymequiv}{$\dn$}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    31
\renewcommand{\isasymemptyset}{$\varnothing$}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    32
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    33
\renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    34
\renewcommand{\isasymin}{\ensuremath{\,\in\,}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    35
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    36
\addtolength{\oddsidemargin}{-1.5mm}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    37
\addtolength{\evensidemargin}{-1.5mm}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    38
\addtolength{\textwidth}{4mm}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    39
\addtolength{\textheight}{1.5mm}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    40
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    41
\def\lexer{\mathit{lexer}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    42
\def\mkeps{\mathit{mkeps}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    43
\def\inj{\mathit{inj}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    44
\def\Empty{\mathit{Empty}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    45
\def\Left{\mathit{Left}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    46
\def\Right{\mathit{Right}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    47
\def\Stars{\mathit{Stars}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    48
\def\Char{\mathit{Char}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    49
\def\Seq{\mathit{Seq}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    50
\def\Der{\mathit{Der}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    51
\def\nullable{\mathit{nullable}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    52
\def\Z{\mathit{Z}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    53
\def\S{\mathit{S}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    54
\newcommand{\ZERO}{\mbox{\bf 0}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    55
\newcommand{\ONE}{\mbox{\bf 1}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    56
\def\rs{\mathit{rs}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    57
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    58
\def\Brz{Brzozowski}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    59
\def\der{\backslash}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    60
\newtheorem{falsehood}{Falsehood}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    61
\newtheorem{conject}{Conjecture}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    62
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    63
\bibliographystyle{plainurl}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    64
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    65
\title{{POSIX} {L}exing with {B}itcoded {D}erivatives}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    66
\titlerunning{POSIX Lexing with Bitcoded Derivatives}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    67
\author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    68
\author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    69
\authorrunning{C.~Tan and C.~Urban}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    70
\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    71
\category{}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    72
\ccsdesc[100]{Design and analysis of algorithms}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    73
\ccsdesc[100]{Formal languages and automata theory}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    74
\Copyright{\mbox{}}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    75
\renewcommand{\DOIPrefix}{}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    76
\nolinenumbers
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    77
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    78
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    79
\begin{document}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    80
\maketitle
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    81
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    82
\begin{abstract}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    83
  Sulzmann and Lu describe a lexing algorithm that calculates
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    84
  Brzozowski derivatives using bitcodes annotated to regular
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    85
  expressions.  Their algorithm generates POSIX values which encode
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    86
  the information of \emph{how} a regular expression matches a
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    87
  string---that is, which part of the string is matched by which part
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    88
  of the regular expression. This information is needed in the
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    89
  context of lexing in order to extract and to classify tokens.
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    90
  The purpose of the bitcodes is to generate POSIX values incrementally while
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    91
  derivatives are calculated. They also help with designing
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    92
  an ``aggressive'' simplification function that keeps the size of
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    93
  derivatives finitely bounded. Without simplification the size of some derivatives can grow
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    94
  arbitrarily big, resulting in an extremely slow lexing algorithm.  In this
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    95
  paper we describe a variant of Sulzmann and Lu's algorithm: Our
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    96
  variant is a recursive functional program, whereas Sulzmann
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    97
  and Lu's version involves a fixpoint construction. We \textit{(i)}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    98
  prove in Isabelle/HOL that our algorithm is correct and generates
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    99
  unique POSIX values; we also \textit{(ii)} establish finite
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   100
  bounds for the size of the derivatives.
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   101
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   102
  %The size can be seen as a
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   103
  %proxy measure for the efficiency of the lexing algorithm: because of
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   104
  %the polynomial bound our algorithm does not suffer from
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   105
  %the exponential blowup in earlier works.
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   106
  
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   107
  % Brzozowski introduced the notion of derivatives for regular
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   108
  % expressions. They can be used for a very simple regular expression
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   109
  % matching algorithm.  Sulzmann and Lu cleverly extended this
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   110
  % algorithm in order to deal with POSIX matching, which is the
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   111
  % underlying disambiguation strategy for regular expressions needed
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   112
  % in lexers.  Their algorithm generates POSIX values which encode
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   113
  % the information of \emph{how} a regular expression matches a
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   114
  % string---that is, which part of the string is matched by which
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   115
  % part of the regular expression.  In this paper we give our
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   116
  % inductive definition of what a POSIX value is and show $(i)$ that
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   117
  % such a value is unique (for given regular expression and string
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   118
  % being matched) and $(ii)$ that Sulzmann and Lu's algorithm always
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   119
  % generates such a value (provided that the regular expression
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   120
  % matches the string). We show that $(iii)$ our inductive definition
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   121
  % of a POSIX value is equivalent to an alternative definition by
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   122
  % Okui and Suzuki which identifies POSIX values as least elements
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   123
  % according to an ordering of values.  We also prove the correctness
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   124
  % of Sulzmann's bitcoded version of the POSIX matching algorithm and
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   125
  % extend the results to additional constructors for regular
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   126
  % expressions.  \smallskip
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   127
\end{abstract}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   128
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   129
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   130
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   131
\input{session}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   132
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   133
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   134
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   135
\end{document}
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   136
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   137
%%% Local Variables:
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   138
%%% mode: latex
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   139
%%% TeX-master: t
f493a20feeb3 updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   140
%%% End: