The Fm structure

Synopsis

signature FM
structure Fm :> FM


The structure Fm deals with finite machines, i.e. finite non-deterministic automata without epsilon-transitions.

All functions to build machines or to manipulate them are polymorphic in the type of the alphabet. Implicitly, we assume the alphabet of instructions to consist of those mentioned in the machine's transitions. To display automata, see ppFm.

Interface

type ''a machine
val Atom : ''a -> ''a machine
val Plus : ''a machine list -> ''a machine
val Star : ''a machine -> ''a machine
val Times : ''a machine list -> ''a machine
val accept : ''a machine -> ''a list -> bool
val make : {
               final : int list,
               trans : (int * ''a * int) list,
               start : int list
             } -> ''a machine
val show : ''a machine
             -> {
               final : int list,
               trans : (int * ''a * int) list,
               start : int list
             }
val states : ''a machine -> int
val nextstates : ''a machine -> int -> ''a -> int list
val reach : ''a machine -> int list -> ''a list -> int list
val determine : ''a machine -> ''a machine
val determineWithStateAssoc : ''a machine
                                -> ''a machine
                                * (int * int list) list
val minimize : ''a machine -> ''a machine
val minimizeWithStateAssoc : ''a machine
                               -> ''a machine
                               * (int * int list) list
val minimizeWithHistory : ''a machine
                            -> ((''a
                            * int list) machine
                            * (int * int list) list) list


Description

type ''a machine


the type parameter ''a gives the type of labels or instructions

Atom a

returns the machine with a single transition for instruction a.

Plus l

returns a machine for the alternative execution of the machines in the list l

Star m

returns a machine for the feedback of machine m

Times l

returns a machine for the sequential composition of the machines in the list l

accept m l

returns true if the machine m, when executing the sequence l, reaches an accepting state. Returns false otherwise.

make {final, trans, start}

constructs a machine from a list start of start states, a list final of accepting states, and a list trans of transitions.

show m

shows the lists of start states, transitions and final states.

states m

returns an upper bound for the number of states of m, used when composing machines.

nextstates m i a

returns a list of all states which m reaches from state i when executing a.

reach m is l

returns a list of all states which m reaches from states is when executing the sequence l of instructions.

determine m

returns a deterministic machine equivalent to m.

determineWithStateAssoc m

returns a deterministic machine equivalent to m, and an association list relating states of the deterministic machine to corresponding sets of states of m.

minimize m

returns a state-minimal (total) deterministic machine equivalent to m, provided m is deterministic and has no unreachable states. (The minimal machine may have a sink-state, which is needed only to make the transition relation total.)

minimizeWithStateAssoc m

returns a state-minimal (total) deterministic machine equivalent to m, provided m is deterministic and has no unreachable states. Additionally, returns an association list relating states of the minimal machine to lists of equivalent states of m.

minimizeWithHistory m

returns a list of machines paired with an association list relating its states i to lists of states Q.i of m. The list consists of machines approximating the minimal machine equivalent to m, where the first one is a machine with state 0 corresponding to the set of final states of m, and state 1, the set of non-final states of m. The last is the minimal machine equivalent to m. (The initial and final states are not shown.) The transitions between Q.i and Q.j have besides labels a of m the list of states in Q.i that have an a-transition in m to some member of Q.j. The history is displayed using ppFm.

See Also

ppFm, ppRegExpFm, RegEqnsFm

Discussion

Deterministic machines are here treated as non-deterministic machines with functional transition relation. To avoid the overhead of interpreting these relations, a separate signature for deterministic machines, implementing the deterministic transition relation as a function, would be useful .

As with regular expressions, associative binary operations (alternative and sequential composition) are treated as operations having a finite list of arguments. (In particular, a zero and a unit machine are the Plus resp. Times of an empty list of machines.)

An isomorphism test for minimal deterministic machines has to be added.

Example:

val M = Fm.make{trans=[(0,"a",1),(1,"b",2),(0,"c",2)],start=[0],final=[2]}

Fm.show (Fm.Star M)
val it =
  {final=[0,3],start=[0,1],
   trans=[(1,"a",2),(2,"b",3),(1,"c",3),(1,"c",1),(2,"b",1)]}

Fm.determineWithStateAssoc (Fm.Star M)
val it = (-,[(0,[0,1]),(1,[3,1]),(2,[]),(3,[2])])
  : string Fm.machine * (int * int list) list