### 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. 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 (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). This holds also when optimisations are included. Finally we show that (iii) 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.

### License

BSD License

### History

June 17, 2022
  Christian Urban added a theory about the Posix definition by Okui and Suzuki.

### Topics

- Computer science/Automata and formal languages

### Session Posix-Lexing

- Lexer
- LexicalVals
- Simplifying
- Positions
- Regular_Exps3
- Derivatives3
- Lexer3
- LexicalVals3
- Simplifying3
- Positions3

### Depends on

- Regular Sets and Expressions

## Cite

×

Posix-Lexing-AFP

    @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{https://isa-afp.org/entries/Posix-Lexing.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 24, 2016 : Isabelle2016