A Formalisation of Finite Automata using Hereditarily Finite Sets
Formal Languages and Automata Theory
2015-05-08 v1 Logic in Computer Science
Abstract
Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski's minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.
Keywords
Cite
@article{arxiv.1505.01662,
title = {A Formalisation of Finite Automata using Hereditarily Finite Sets},
author = {Lawrence C. Paulson},
journal= {arXiv preprint arXiv:1505.01662},
year = {2015}
}
Comments
Accepted to CADE-25 (International Conference on Automated Deduction), Berlin, August 2015