POSIX Lexing with Derivatives of Regular Expressions

Title:	POSIX Lexing with Derivatives of Regular Expressions
Authors:	Fahad Ausaf, Roy Dyckhoff and Christian Urban
Submission date:	2016-05-24
Abstract:	Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. In this entry we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu's algorithm always generates such a value (provided that the regular expression matches the string). We also prove the correctness of an optimised version of the POSIX matching algorithm.
BibTeX:	@article{Posix-Lexing-AFP, author = {Fahad Ausaf and Roy Dyckhoff and Christian Urban}, title = {POSIX Lexing with Derivatives of Regular Expressions}, journal = {Archive of Formal Proofs}, month = may, year = 2016, note = {\url{http://isa-afp.org/entries/Posix-Lexing.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Regular-Sets
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.