Skip to content

feat(Automata): Two-way automata accept exactly the regular languages - #888

Open
crei wants to merge 13 commits into
leanprover:mainfrom
crei:two_na_eq_na
Open

crei wants to merge 13 commits into
leanprover:mainfrom
crei:two_na_eq_na

Conversation

@crei

@crei crei commented Sep 9, 2026

Copy link
Copy Markdown
Collaborator

This implements Vardi's construction of a (one-way) finite automaton that accepts the complement of the language accepted by a two-way automaton. Together with closure of regular languages under complement and a simple mapping of one-way automata to two-way automata we get that two-way automata accept exactly the regular languages.

AI disclosure: Claude was used throughout bit in a tight review loop.

@crei
crei marked this pull request as ready for review September 10, 2026 10:16
@crei crei changed the title feat(Automata): Two-way automata accept only regular languages feat(Automata): Two-way automata accept exactly the regular languages Sep 10, 2026
Comment thread Cslib/Computability/Automata/TwoWayNA/Regular.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/Basic.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/OfNA.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/Regular.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean Outdated
Comment thread Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean Outdated
@ctchou

ctchou commented Sep 11, 2026

Copy link
Copy Markdown
Collaborator

@crei Could you mark the comments which you have fixed using the "resolve conversation" button? This way I don't have to re-read the code to figure out what you have done. Thanks!

@ctchou ctchou left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants