The RegEqnsFm functor (preliminary)

Synopsis

functor RegEqnsFm ( ... ) : sig ... end


This functor combines a structure for regular equation systems with a structure for finite machines. Currently it only extends structure RegExpFm by fmToEqns. (Likely to have normalization functions for equation systems added, like GNF, LeftToRightRecursion, etc.)

Functor argument interface

structure E : REGEQNS
structure M : FM


Description

structure E : REGEQNS


a structure for regular equation systems; intended to be an extension of RegEqns.

structure M : FM


a structure for finite machines; intended to be an extension of Fm.

Functor result interface

structure E : REGEQNS
structure M : FM
type ''a machine = ''a M.machine
datatype re = datatype E.re
val accept : ''a machine -> ''a list -> bool
val retofm : ''a re -> ''a machine
val retominfm : ''a re -> ''a machine
val fmtore : ''a machine -> ''a re
val fmToEqns : ''a machine -> ''a re E.eqns


Description

type ''a machine = ''a M.machine


datatype re = datatype E.re


accept m l

returns true if m reaches an accepting state after executing instructions l.

retofm r

returns a finite automaton m accepting the language defined by expression r. The expression r must not have free variables. (no error message yet)

retominfm r

returns the state-minimal deterministic finite automaton m accepting the language defined by expression r. The expression r must not have free variables. (no error message yet)

fmtore m

returns a regular expression r definining the language accepted by machine m.

fmToEqns m

returns a right-linear system of regular recursion equations that defines the language accepted by m.

Discussion

This functor is used to construct in the same way both the structures RegEqnsFm and ppRegEqnsFm.

Regular recursion equation system should be translated to recursive finite automata, and these could be defined either via regular expressions extended by a simultaneous or a simple-fixed-point operator. Then right-linear recursion systems would translate to finite automata via tail-recursion elimination.