lexing: thys/Paper/document/root.tex@4e3778f4a802 (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}
174 4e3778f4a802 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	12	%%\usepackage{stmaryrd}
95 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{url}
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{color}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	16	\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	17
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\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	19	\isabellestyle{it}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	20	\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	21	\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	22
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\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	25	\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	26	\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	27	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 152 diff changeset	28	\renewcommand{\isasymiota}{\makebox[0mm]{${}^{\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	29
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	30	\def\Brz{Brzozowski}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	31	\def\der{\backslash}
174 4e3778f4a802 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	32	\newtheorem{falsehood}{Falsehood}
4e3778f4a802 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	33	\newtheorem{conject}{Conjecture}
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\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	36
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	37	\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	38	\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	39	\institute{King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	40	\email{fahad.ausaf@icloud.com}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	41	\and University of St Andrews\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	42	\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	43	\and King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	44	\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	45	\maketitle
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	\begin{abstract}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	48
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	49	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	50	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	51	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	52	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	53	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	54	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	55	``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	56	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	57	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	58	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	59	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	60	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	61	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	62	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	63	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	64	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	65	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	66	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	67
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	68	{\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	69	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	70	\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	71
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	\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	73
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\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	75
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	%%% 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	77	%%% 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	78	%%% 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	79	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 09 May 2016 15:00:28 +0100
changeset 174	4e3778f4a802
parent 172	cdc0bdcfba3f
child 267	32b222d77fa0
permissions	-rwxr-xr-x