A Formalisation of Finite Automata using Hereditarily Finite Sets

TL;DR

This paper formalizes finite automata within hereditarily finite set theory, enabling a rigorous set-theoretic foundation for automata theory and regular languages, including key theorems and algorithms.

Contribution

It introduces a novel formalization of automata states as HF sets, integrating automata theory with hereditarily finite set theory for the first time.

Findings

Automata states are represented as HF sets constructed by set operations.

The formalization includes proofs of the Myhill-Nerode theorem and minimization algorithms.

Demonstrates the utility of HF set theory in automata and language theory.

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.