search

subttle / regular

Finite Automata and Regular Expressions for Regular Languages in Haskell
BSD 3-Clause "New" or "Revised" License
10 stars 1 forks source link

RE and ERE axiomization #5

Closed subttle closed 4 years ago

subttle commented 5 years ago

For now what I've convinced myself I want is Kozen axioms [1] for RE and Salomaa axioms [2] for ERE.

[1] A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events, Dexter Kozen https://www.cs.cornell.edu/~kozen/Papers/ka.pdf

[2] Two Complete Axiom Systems for the Extended Language of Regular Expressions, Salomaa and Tixier (01687431.pdf) Available free through https://ieeexplore.ieee.org/Xplore/home.jsp ("IEEE Transactions on Computers" C-17) with some school proxies.

subttle commented 5 years ago

Looks like Antimirov's AX axioms [1] [2] might be be preferable for extended regular expressions: [1] Manipulation of Extended Regular Expressions with Derivatives, Rafaela Carolina Ribeiro Bastos http://www.dcc.fc.up.pt/~nam/web/resources/rafaelamsc.pdf [2] Rewriting Extended Regular Expressions, Valentin M. Antimirov, Peter D. Moses https://hope.simons-rock.edu/~pshields/cs/cmpt320/antimirov94.pdf

subttle commented 5 years ago

This should come in handy when switching axioms :)

https://github.com/phadej/lattices/

subttle commented 4 years ago

Kozen axioms for Kleene Algebra in Agda https://github.com/subttle/kleene