lexing: thys/Paper/document/root.tex@cdc0bdcfba3f (annotated)

95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[runningheads]{llncs}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	2	\usepackage{times}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage{isabelle}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	\usepackage{isabellesym}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\usepackage{amsmath}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	\usepackage{amssymb}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage{mathpartir}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{tikz}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{pgf}
114 8b41d01b5e5d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 109 diff changeset	10	\usetikzlibrary{positioning}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\usepackage{pdfsetup}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	\usepackage{ot1patch}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usepackage{stmaryrd}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\usepackage{url}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\usepackage{color}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 152 diff changeset	17	\usepackage{mathtools}
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 152 diff changeset	18
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	19	\titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	\urlstyle{rm}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	\isabellestyle{it}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	23	\renewcommand{\isastyleminor}{\it}%
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\renewcommand{\isastyle}{\normalsize\it}%
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\renewcommand{\isasymequiv}{$\dn$}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\renewcommand{\isasymemptyset}{$\varnothing$}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 152 diff changeset	31	\renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 152 diff changeset	32	%%\makebox[0mm]{$\mbox{}\mbox{$\,^\prime$}$}}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\definecolor{mygrey}{rgb}{.80,.80,.80}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	35	\def\Brz{Brzozowski}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	36	\def\der{\backslash}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	37	\newcommand{\eps}{\varepsilon}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	38	\newcommand{\mts}{\eps}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\begin{document}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	42	\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	43	\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	44	\institute{King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	45	\email{fahad.ausaf@icloud.com}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	46	\and University of St Andrews\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	47	\email{roy.dyckhoff@st-andrews.ac.uk}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	48	\and King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	49	\email{christian.urban@kcl.ac.uk}}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	\maketitle
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	\begin{abstract}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	53
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	54	Brzozowski introduced the notion of derivatives for regular
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	55	expressions. They can be used for a very simple regular expression
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	56	matching algorithm. Sulzmann and Lu cleverly extended this algorithm
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	57	in order to deal with POSIX matching, which is the underlying
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	58	disambiguation strategy for regular expressions needed in lexers.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	59	Sulzmann and Lu have made available on-line what they call a
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	60	``rigorous proof'' of the correctness of their algorithm w.r.t.\ their
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	61	specification; regrettably, it appears to us to have unfillable gaps.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	62	In the first part of this paper we give our inductive definition of
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	63	what a POSIX value is and show $(i)$ that such a value is unique (for
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	64	given regular expression and string being matched) and $(ii)$ that
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	65	Sulzmann and Lu's algorithm always generates such a value (provided
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	66	that the regular expression matches the string). We also prove the
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	67	correctness of an optimised version of the POSIX matching
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	68	algorithm. Our definitions and proof are much simpler than those by
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	69	Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	70	second part we analyse the correctness argument by Sulzmann and Lu and
172 cdc0bdcfba3f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	71	explain why the gaps in this argument cannot be filled easily.\smallskip
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	73	{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	74	Isabelle/HOL
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\end{abstract}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77	\input{session}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	\end{document}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	%%% Local Variables:
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	%%% mode: latex
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	%%% TeX-master: t
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 09 May 2016 12:09:56 +0100
changeset 172	cdc0bdcfba3f
parent 154	2de3cf684ba0
child 174	4e3778f4a802
permissions	-rwxr-xr-x