lexing: thys/Paper/document/root.tex@8b41d01b5e5d (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{$\_\!\_$}}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\definecolor{mygrey}{rgb}{.80,.80,.80}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	31	\def\Brz{Brzozowski}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	32	\def\der{\backslash}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	33	\newcommand{\eps}{\varepsilon}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	34	\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	35
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	\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	37
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	38	\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	39	\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	40	\institute{King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	41	\email{fahad.ausaf@icloud.com}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	42	\and University of St Andrews\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	43	\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	44	\and King's College London\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	45	\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	46	\maketitle
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\begin{abstract}
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	49
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	50	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	51	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	52	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	53	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	54	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	55	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	56	``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	57	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	58	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	59	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	60	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	61	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	62	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	63	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	64	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	65	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	66	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	67	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	68	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	69
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	70	{\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	71	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	72	\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	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	\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	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	\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	77
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	%%% 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	79	%%% 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	80	%%% 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	81	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sat, 05 Mar 2016 05:41:51 +0000
changeset 114	8b41d01b5e5d
parent 109	2c38f10643ae
child 148	702ed601349b
permissions	-rwxr-xr-x