Published in

Springer, Lecture Notes in Computer Science, p. 231-245, 2015

DOI: 10.1007/978-3-319-21401-6_15

Links

Tools

Export citation

Search in Google Scholar

A Formalisation of Finite Automata using Hereditarily Finite Sets

Journal article published in 2015 by Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Red circle
Preprint: archiving forbidden
Orange circle
Postprint: archiving restricted
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

This is the accepted manuscript. It is currently embargoed pending publication. ; 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.