A formalisation of finite automata using hereditarily finite sets
Type
Conference Object
Change log
Authors
Paulson, LC
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.
Description
Keywords
cs.FL, cs.FL, cs.LO, F.4.1; F.1.1
Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
Journal ISSN
0302-9743
1611-3349
1611-3349
Volume Title
Publisher
Springer International Publishing