The RegEqns structure

The `RegEqns` structure

Synopsis

signature REGEQNS structure RegEqns : REGEQNS

The structure RegEqns extends RegExp to systems of recursion equations with regular expressions as right hand sides. Only those functions manipulating such systems are mentioned that do not change the least solution in all continuous Kleenean algebras.

Interface

include REGEXP_WEAK type 'b eqns = (int * 'b) list type 'a env = int -> 'a val maxVar : 'a re eqns -> int val nthVar : 'a re eqns * int -> 'a re val freeVars : 'a re eqns -> int list val recVars : 'a re eqns -> int list val eliminateStars : ''a re eqns -> ''a re eqns val convertToCFG : ''a re eqns -> ''a re eqns val greibachNF : ''a re eqns -> ''a re eqns val leftToRightRecursion : ''a re eqns -> ''a re eqns val isolateLeftVarFactors : ''a re eqns -> ''a RegMat.t * ''a RegMat.t val solveRightlinearEqns : ''a re eqns -> ''a re eqns val fix : ('a env -> 'b -> 'a) -> 'a env -> ('a env -> ''c) -> 'b eqns -> 'a env val solve : ('a env -> 'b -> 'a) -> 'a env -> ('a env -> ''c) -> 'b eqns -> 'a eqns val iter : ('a env -> 'b -> 'a) -> 'a env -> int -> 'b eqns -> 'a env val iterate : ('a env -> 'b -> 'a) -> 'a env -> int -> 'b eqns -> 'a eqns

Description


type 'b eqns = (int * 'b) list: the type of systems of recursion equations (i,e) between variables (represented by their indices i) and expressions or values e (of type 'b). Different equations are assumed to have different recursion variables i.

type 'a env = int -> 'a: the type of environments into type 'a.

maxVar eqs: returns the maximal integer used as variable index in eqs.

nthVar (eqs, i): returns the index of the recursion variable of the i-th equation in eqs.

freeVars eqs: returns a list of indices of those variables in eqs that are free but not recursion variables, i.e. do not occur on a left hand side. (Normally, there will be no such parameter variables.)

recVars eqs: returns the indices of the recursion variables of eqs

eliminateStars eqs: returns an equation system equivalent to eqs, but without expressions r*. All subexpressions in eqs of the form Star r are replaced by new variables x and new recursion equations x = rx + 1.

convertToCFG eqs: returns an equation system equivalent to eqs in which the right hand sides are sums of products. (This is done by first removing all expressions Star r and then taking a disjunctive normal form of right hand sides.)

greibachNF eqs: returns an equation system equivalent to eqs, in which right-hand sides are sums of products whose leftmost factor is not a recursion variable. (Assumes that 1 is not a summand of eqs, and eqs is in disjunctive normal form.)
Applies leftToRightRecursion and then substitutes (tY + t) for leading variables x in R of Y = RY + R.

leftToRightRecursion eqs: returns an equation system equivalent to eqs, which has no left recursion.
We write eqs as a matrix equation x = xR + t, whose least solution is the same as that for the system {x = tR* = t + tR+}, which is right-recursive when written with additional unknowns Y as {x = tY + t, Y = RY + R}, where R,t depend on x. Assuming t has no 1, all remaining leading recursion variables are from x in R. Note that the new recursion equations Y = RY + R are right-recursive in Y.

isolateLeftVarFactors eqs: to isolate left-recursion, writes eqs as a matrix equation x = xR + t and returns (R,t). (See previous function.)

solveRightlinearEqns eqs: if eqs is right-linear, returns an equation system equivalent to eqs where all right-hand sides are regular expressions without the recursion variables (solved form).

fix eval env test eqs: computes new environments env_0, ... ,env_m where env_0 is env and env_k+1 is the update of env_k by assigning the values of the right hand sides of eqs to the recursion variables, until test(env_k+1) = test(env_k). Returns the first such env_k.
test is intended to be an efficient way to determine wether all right hand sides of eqs evaluate to the same values under eval both with env_k and env_k+1.

solve eval env test eqs: returns a list of pairs (i,env'(i)) where i is (the index of) a recursion variable of eqs and env' is the environment returned by fix.

iter eval env i eqs: returns the environment obtained by iterating the evaluation function eval i times to evaluate the right-hand sides of eqs, starting with the inital environment env for the values of variables.

iterate eval env i eqs: returns the equations (between variables and values) obtained by iterating the evaluation function eval i times to evaluate the right-hand sides of eqs, starting with the inital environment env for the values of variables.

Discussion

To print recursion equation systems with names for variables and atoms provided by the user, see ppRegEqns.

Example:

Solve a right-linear system by regular expressions without recursion variables:

- val rlE = [(0,Plus[Times[Atom "a",Var 0],Atom "b"]),
             (1,Plus[Times[Atom "c",Var 0],Var 0,Var 1])];

- solveRightlinearEqns rlE;
val it =
  [(0,Times [Star (Atom "a"),Atom "b"]),
   (1,Times [Plus [Times [],Atom "c"],Star (Atom "a"),Atom "b"])]
  : string re eqns

Example:

Transform regular recursion equations to a context free grammar:
- val EBNF = [(0,Plus[Star(Times[Var 1,Atom "a",Var 0]),Atom "b"]),
              (1,Times[Plus[Atom "c",Var 0],Var 3])];

- convertToCFG EBNF;
val it =
  [(0,Plus [Var 4,Atom "b"]),
   (1,Plus [Times [Atom "c",Var 3],Times [Var 0,Var 3]]),
   (4,Plus [Times [Var 1,Atom "a",Var 0,Var 4],Times []])] : string re eqns
Since there was a non-recursion variable Var 3, the new recursion variable needed to eliminate the Star is Var 4.