lexing: thys/Paper/document/root.tex@e3eb82ea2244 (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
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	17	\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	18
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\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	20	\isabellestyle{it}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	21	\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	22	\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	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
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\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	26	\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	27	\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	28	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
152 e3eb82ea2244 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	29	%%\renewcommand{\isacharprime}{\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	30
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	\definecolor{mygrey}{rgb}{.80,.80,.80}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	32	\def\Brz{Brzozowski}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	33	\def\der{\backslash}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	34	\newcommand{\eps}{\varepsilon}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	35	\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	36
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\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	38
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	39	\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	40	\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	41	\institute{King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	42	\email{fahad.ausaf@icloud.com}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	43	\and University of St Andrews\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	44	\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	45	\and King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	46	\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	47	\maketitle
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	\begin{abstract}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	50
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	51	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	52	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	53	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	54	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	55	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	56	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	57	``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	58	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	59	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	60	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	61	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	62	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	63	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	64	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	65	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	66	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	67	second part we analyse the correctness argument by Sulzmann and Lu and
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	68	explain why it seems hard to turn it into a proof rigorous enough to
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	69	be accepted by a system such as Isabelle/HOL.\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	70
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	71	{\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	72	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	73	\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	74
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\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	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	\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	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	%%% 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	80	%%% 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	81	%%% 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	82	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Wed, 16 Mar 2016 07:15:12 +0000
changeset 152	e3eb82ea2244
parent 148	702ed601349b
child 154	2de3cf684ba0
permissions	-rwxr-xr-x