POSIX Lexing with Derivatives of Regular Expressions

TY - JOUR

T1 - POSIX Lexing with Derivatives of Regular Expressions

AU - Urban, Christian

N1 - Funding Information: I am very grateful to Martin Sulzmann for his comments on this work and moreover for patiently explaining the details in [4]. I am also very grateful to Fahad Ausaf who helped with this work and to Flavio Melinte Citea who pointed out omissions in the simplification rules. I am deeply saddened that Roy Dyckhoff, co-author of the original conference paper [1] and the supervisor of my master thesis in St Andrews, died in August 2018. This was the last scientific paper he worked on. Roy was a witty, extremely intelligent and a very pleasant researcher and friend. He is much missed by me and many colleagues. Publisher Copyright: © 2023, The Author(s).

PY - 2023/9

Y1 - 2023/9

N2 - 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. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string---that is, which part of the string is matched by which part of the regular expression. In this paper we give our inductive definition of what a POSIX value is and show that Sulzmann and Lu's algorithm always generates such a value. We also show that our inductive definition of a POSIX value is equivalent to an alternative definition by Okui and Suzuki which identifies POSIX values as least elements according to an ordering of values.

AB - 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. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string---that is, which part of the string is matched by which part of the regular expression. In this paper we give our inductive definition of what a POSIX value is and show that Sulzmann and Lu's algorithm always generates such a value. We also show that our inductive definition of a POSIX value is equivalent to an alternative definition by Okui and Suzuki which identifies POSIX values as least elements according to an ordering of values.

UR - http://www.scopus.com/inward/record.url?scp=85164255689&partnerID=8YFLogxK

U2 - 10.1007/s10817-023-09667-1

DO - 10.1007/s10817-023-09667-1

M3 - Article

SN - 0168-7433

VL - 67

JO - JOURNAL OF AUTOMATED REASONING

JF - JOURNAL OF AUTOMATED REASONING

IS - 3

M1 - 24

ER -