Deriving a Systolic Regular Language Recognizer
Matteo Vaccari, Roland Backhouse · 1996
We present a derivation of a regular language recognizing circuit originally developed by Foster and Kung [4]. We make use of pointfree relation algebra, in a style combining elements from earlier work in the Eindhoven Mathematics of Program Construction group [0], and from Ruby [6]. First we derive non-systolic recognizers, much in the same way as functional programs are derived. Then we make use of standard circuit transformation techniques, recast in the relation algebra framework, to obtain circuits that are very close to the ones presented by Foster and Kung. 0 Introduction In 1982, Foster and Kung [4] presented a specialised silicon compiler that constructs recognizers for regular languages. The compiler was presented without formal justification; indeed, they did not present a formal specification of the functionality of the compiler. Their informal description of the functioning left much room for alternative interpretations. Subsequently, Backhouse [1] verified the correctnes...