Forlan Manual

The LP Module


signature LP
structure LP :> LP

This module defines the abstract type of labeled paths.


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


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.

is defined by:
  fun compare(Sym a1,            Sym a2)            =, a2)
    | compare(Sym _,             _)                 = LESS
    | compare(_,                 Sym _)             = GREATER
    | compare(Cons(a1, x1, lp1), Cons(a2, x2, lp2)) =
        case, a2) of
             LESS    => LESS
           | EQUAL   =>
               (case, 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:

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: 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: Otherwise, findValidPumpingDivisionOpt returns NONE

[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.12
Copyright © 2019 Alley Stoughton