Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Two-Way Deterministic Finite A...

Email Gateway (Aug 08 2025 at 14:18):

From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

A new formalization explores DFAs that can change the reading direction as they like. Unfortunately (for the DFAs) this does not add expressiveness. This is what this entry proves:

Two-Way Deterministic Finite Automata
by Felipe Escallón and Tobias Nipkow

This theory presents a proof that two-way DFAs are as powerful as DFAs, i.e. they accept exactly the regular languages. The formalization follows Kozen.

https://www.isa-afp.org/entries/Two_Way_DFA_HF.html

Enjoy!

Last updated: Aug 20 2025 at 20:23 UTC