The RegEqns structure


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.


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


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.

See Also

RegExp, RegMat, ppRegEqns


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


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

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.

Replace left-recursion by right-recursion, using n^2 additional equations, if the input system has n equations:

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

- val eLR = leftToRightRecursion E;
val eLR =
  [(0,Plus [Atom "b",Times [Atom "b",Var 2],Times [Atom "c",Var 4]]),
   (1,Plus [Atom "c",Times [Atom "b",Var 3],Times [Atom "c",Var 5]]),
   (2,Var 4),
   (3,Plus [Var 5,Times []]),
   (4,Plus [Times [Atom "a",Var 0,Var 2],Times [Atom "a",Var 0]]),
   (5,Times [Atom "a",Var 0,Var 3])] : string re eqns
While the old recursion variables no longer occur as left factors, some of the new recursion variables do. Using greibachNF replaces these (and other occurrences) by the right-hand sides of their recursion equations.