Forlan Manual

The `LP` Module

Synopsis

signature LP structure LP :> LP

This module defines the abstract type of labeled paths.

Interface

datatype concr = Sym of Sym.sym | Cons of Sym.sym * Str.str * concr type lp val fromConcr : concr -> lp val toConcr : lp -> concr val fromString : string -> lp val input : string -> lp val toPP : lp -> PP.pp val toString : lp -> string val output : string * lp -> unit val compare : lp Sort.total_ordering val equal : lp * lp -> bool val sym : Sym.sym -> lp val cons : Sym.sym * Str.str * lp -> lp val startState : lp -> Sym.sym val endState : lp -> Sym.sym val label : lp -> Str.str val length : lp -> int val join : lp * lp -> lp val splitAt : lp * int -> lp * lp type pumping_division = lp * lp * lp val checkPumpingDivision : pumping_division -> unit val validPumpingDivision : pumping_division -> bool val strsOfValidPumpingDivision : pumping_division -> Str.str * Str.str * Str.str val pumpValidPumpingDivision : pumping_division * int -> lp val findValidPumpingDivision : lp -> pumping_division val findValidPumpingDivisionOpt : lp -> pumping_division option

Description

datatype concr = Sym of Sym.sym | Cons of Sym.sym * Str.str * concr

The concrete datatype of labeled paths. If q is a symbol, then Sym q is the labeled path with no transitions, and whose start and end states are q. And if q is a symbol, x is a string, and lp is a labeled path, then Cons(q, x, lp) is the labeled path whose start state is q, whose first transition is from q to the start state of lp, labeled by x, and whose remaining transitions and end state are as in lp.

type lp

The abstract type of labeled paths, consisting of the values of type concr.

fromConcr concr

returns concr.

toConcr lp

returns lp.

fromString s

inputs a labled path from s.

input fil

inputs a labeled path from the file named by fil.

toPP lp

returns a pretty-printing expression for lp.

toString lp

pretty-prints lp to a string.

output(fil, lp)

pretty-prints lp to the file named by fil.

compare

is defined by:

  fun compare(Sym a1,            Sym a2)            = Sym.compare(a1, a2)
    | compare(Sym _,             _)                 = LESS
    | compare(_,                 Sym _)             = GREATER
    | compare(Cons(a1, x1, lp1), Cons(a2, x2, lp2)) =
        case Sym.compare(a1, a2) of
             LESS    => LESS
           | EQUAL   =>
               (case Str.compare(x1, x2) of
                     LESS    => LESS
                   | EQUAL   => compare(lp1, lp2)
                   | GREATER => GREATER)
           | GREATER => GREATER

equal(lp1, lp2)

tests whether lp1 and lp2 are equal.

sym q

returns Sym q.

cons(q, x, lp)

returns Cons(q, x, lp).

startState lp

returns the start state of lp.

endState lp

returns the end state of lp.

label lp

returns the label of lp.

length lp

returns the length of lp.

join(lp1, lp2)

returns the join of lp1 and lp2. Issues an error message if the end state of lp1 is not equal to the start state of lp2.

splitAt(lp, n)

returns the pair (lp1, lp2) such that the length of lp1 is n and lp is the join of lp1 and lp2. Issues an error message if n is negative or is is greater than the length of lp.

type pumping_division = lp * lp * lp

The following functions on pumping divisions can be used to experiment with the pumping lemma for regular languages.

A pumping division (lp1, lp2, lp3) is valid iff:

the end state of lp1 is equal to the start state of lp2;
the start state and end states of lp2 are equal;
the end state of lp2 is equal to the start state of lp3;
the label of lp2 is nonempty.

checkPumpingDivision pd

checks whether pd is valid, silently returning (), if it is, and issuing an error message explaining why it's not, if it's not.

validPumpingDivision pd

tests whether pd is valid.

strsOfValidPumpingDivision pd

returns the triple consisting of the labels of the three components of pd, in order. Issues an error message if pd is not a valid pumping division.

pumpValidPumpingDivision(pd, n)

returns the labeled path consisting of the join of #1 pd, lp and #3 pd, where lp is the result of joining #2 pd with itself n times. (Joining a labeled path lp with itself 0 times results in Sym(startState lp). Joining lp with itself 1 time results in lp.) Issues an error message if pd isn't valid or n is negative.

findValidPumpingDivision lp

tries to find a pumping division (lp1, lp2, lp3) such that:

(lp1, lp2, lp3) is valid;
pumpValidPumpingDivision((lp1, lp2, lp3), 1) is lp; and
there is no repetition of states in the result of joining lp1 and splitAt(lp2, length lp2 - 1).

Issues an error message if lp lacks a repetition of states, so that such a pumping division doesn't exist.

findValidPumpingDivisionOpt lp

If lp has a repetition of states, then findValidPumpingDivisionOpt returns SOME of a pumping division (lp1, lp2, lp3) such that:

(lp1, lp2, lp3) is valid;
pumpValidPumpingDivision((lp1, lp2, lp3), 1) is lp; and
there is no repetition of states in the result of joining lp1 and splitAt(lp2, length lp2 - 1).

Otherwise, findValidPumpingDivisionOpt returns NONE

[ Top | Parent | Root | Contents | Index ]

Forlan Manual

The LP Module

Synopsis

Interface

Description

The `LP` Module