Auxiliary function to define Completion.critical_pairs.

eq1 : formula<fol>

The first input equation.

eq2 : formula<fol>

The second input equation.

Returns: formula<fol> list

The list of all the critical pairs of the input equations.

Generate all critical pairs between two equations.

eq1 : formula<fol>

The first input equation.

eq2 : formula<fol>

The second input equation.

Returns: formula<fol> list

The list of all the critical pairs of the input equations.

Example

 let eq = !!"f(f(x)) = g(x)" 
 critical_pairs eq eq

Auxiliary function used to define Completion.overlaps.

fn : 'a -> ('b -> 'a -> 'c) -> 'd list

rfn : 'b -> 'a list -> 'c

lis : 'a list

acc : 'd list

Returns: 'd list

Finds all possibile `overlaps' of an equation with a term.

Defines all ways of overlapping an equation l = r with another term tm, where the additional argument rfn is used to create each overall critical pair from an instantiation i.

l : term

The LHS of the input equation.

r : term

The RHS of the input equation.

tm : term

The input term.

rfn : func<string, term> -> term -> 'a

The function that applied to the resulting instantiation gives the critical pair arising from that overlap.

Returns: 'a list

All possibile overlaps of the equation l = r with the tm.

Example

 overlaps 
   (!!!"f(f(x))",!!!"g(x)") !!!"f(f(y))" 
   (fun i t -> subst i (mk_eq t !!!"g(y)"))

Replaces the variables in a pair of two given formulas by schematic variables of the form xn.

fm1 : formula<fol>

The first input formula.

fm2 : formula<fol>

The second input formula.

Returns: formula<fol> * formula<fol>

The pair of the two input formulas with the variables renamed by schematic variables of the form xn.

Example

 (!!"i(x) * y = z", !!"z * t = y")
 |> renamepair

Completes a set of equations transforming it in a confluent term rewriting system, if the procedure has success.

It is a semi-decision algorithm.

ord : term -> term -> bool

The given ordering: actually an LPO's reflective version is expected.

eqs : formula<fol> list

The given set of equations.

def : formula<fol> list

The accumulator list of deferred critical pairs initially empty.

crits : formula<fol> list

The critical pairs, initially from the eqs equations.

Returns: formula<fol> list

The completed set of equations that defines a confluent term rewriting system, if the procedure has success.

Note

Prints to the stdout diagnostic informations of the current completion status.

Example

 let eqs = !!>[
         "1 * x = x"; 
         "i(x) * x = 1"; 
         "(x * y) * z = x * y * z"
 ]
 
 let ord = lpo_ge (weight ["1"; "*"; "i"])
 
 (eqs,[],unions(allpairs critical_pairs eqs eqs))
 |> complete ord

 ["`i(x4 * x5) = i(x5) * i(x4)`"; "`x1 * i(x5 * x1) = i(x5)`";
  "`i(x4) * x1 * i(x3 * x1) = i(x4) * i(x3)`";
  "`x1 * i(i(x4) * i(x3) * x1) = x3 * x4`";
  "`i(x3 * x5) * x0 = i(x5) * i(x3) * x0`";
  "`i(x4 * x5 * x6 * x3) * x0 = i(x3) * i(x4 * x5 * x6) * x0`";
  "`i(x0 * i(x1)) = x1 * i(x0)`"; "`i(i(x2 * x1) * x2) = x1`";
  "`i(i(x4) * x2) * x0 = i(x2) * x4 * x0`"; "`x1 * i(x2 * x1) * x2 = 1`";
  "`x1 * i(i(x4 * x5) * x1) * x3 = x4 * x5 * x3`";
  "`i(x3 * i(x1 * x2)) = x1 * x2 * i(x3)`";
  "`i(i(x3 * i(x1 * x2)) * i(x5 * x6)) * x1 * x2 * x0 = x5 * x6 * x3 * x0`";
  "`x1 * x2 * i(x1 * x2) = 1`"; "`x2 * x3 * i(x2 * x3) * x1 = x1`";
  "`i(x3 * x4) * x3 * x1 = i(x4) * x1`";
  "`i(x1 * x3 * x4) * x1 * x3 * x4 * x0 = x0`";
  "`i(x1 * i(x3)) * x1 * x4 = x3 * x4`";
  "`i(i(x5 * x2) * x5) * x0 = x2 * x0`";
  "`i(x4 * i(x1 * x2)) * x4 * x0 = x1 * x2 * x0`"; "`i(i(x1)) = x1`";
  "`i(1) = 1`"; "`x0 * i(x0) = 1`"; "`x0 * i(x0) * x3 = x3`";
  "`i(x2 * x3) * x2 * x3 * x1 = x1`"; "`x1 * 1 = x1`"; "`i(1) * x1 = x1`";
  "`i(i(x0)) * x1 = x0 * x1`"; "`i(x1) * x1 * x2 = x2`"; "`1 * x = x`";
  "`i(x) * x = 1`"; "`(x * y) * z = x * y * z`"]

 4 equations and 8 pending critical pairs + 0 deferred
 5 equations and 12 pending critical pairs + 0 deferred
 ...
 32 equations and 0 pending critical pairs + 1 deferred
 32 equations and 0 pending critical pairs + 0 deferred

Normalizes and orients a given equation w.r.t a given set of equations based on the given ordering.

ord : term -> term -> bool

The given ordering.

eqs : formula<fol> list

The given set of equations.

atm : formula<fol>

The input equation to normalize and orient.

Returns: term * term

The pair of LHS and RHS of the normalized and oriented equation.

Example

 let eqs = !!>[
         "1 * x = x"; 
         "i(x) * x = 1"; 
         "(x * y) * z = x * y * z"
 ]
 
 let ord = lpo_ge (weight ["1"; "*"; "i"])
 
 !!"i(y) * i(x) = i(x * (1 * y))"
 |> normalize_and_orient ord eqs

Auxiliary function to print the current status of the completion process.

eqs : 'a list

The current set of equations.

def : 'b list

The current list of deferred critical pairs.

crs : 'c list

The current list of critical pairs.

eqs0 : 'a list

The initial set of equations.

Completes a set of equations transforming it in a confluent term rewriting system, if the procedure has success. It also simplifies the result applying interreduction.

wts : string list

The list defining the function symbols' ordering.

eqs : formula<fol> list

The given set of equations.

Returns: formula<fol> list

The completed and interreduced set of equations, if the procedure has success.

Note

Prints to the stdout diagnostic informations of the current completion status.

Example

 [!!"i(a) * (a * b) = b"]
 |> complete_and_simplify ["1"; "*"; "i"]

 2 equations and 4 pending critical pairs + 0 deferred
 3 equations and 9 pending critical pairs + 0 deferred
 3 equations and 0 pending critical pairs + 0 deferred

Applies the interreduction refinement to an input set of equations.

• discards any equation whose LHS is reducible by any of the others (excluding itself);
• reduces the RHS of any equation with all the equations (including itself).

dun : formula<fol> list

The accumulator, initially empty, of the equations to be reduced

eqs : formula<fol> list

The input set of equations.

Returns: formula<fol> list

The set of equations interreduced.

Example

 !!>[
    "i(x4 * x5) = i(x5) * i(x4)"; "x1 * i(x5 * x1) = i(x5)";
    "i(x4) * x1 * i(x3 * x1) = i(x4) * i(x3)";
    "x1 * i(i(x4) * i(x3) * x1) = x3 * x4";
    "i(x3 * x5) * x0 = i(x5) * i(x3) * x0";
    "i(x4 * x5 * x6 * x3) * x0 = i(x3) * i(x4 * x5 * x6) * x0";
    "i(x0 * i(x1)) = x1 * i(x0)"; "i(i(x2 * x1) * x2) = x1";
    "i(i(x4) * x2) * x0 = i(x2) * x4 * x0"; "x1 * i(x2 * x1) * x2 = 1";
    "x1 * i(i(x4 * x5) * x1) * x3 = x4 * x5 * x3";
    "i(x3 * i(x1 * x2)) = x1 * x2 * i(x3)";
    "i(i(x3 * i(x1 * x2)) * i(x5 * x6)) * x1 * x2 * x0 = x5 * x6 * x3 * x0";
    "x1 * x2 * i(x1 * x2) = 1"; "x2 * x3 * i(x2 * x3) * x1 = x1";
    "i(x3 * x4) * x3 * x1 = i(x4) * x1";
    "i(x1 * x3 * x4) * x1 * x3 * x4 * x0 = x0";
    "i(x1 * i(x3)) * x1 * x4 = x3 * x4";
    "i(i(x5 * x2) * x5) * x0 = x2 * x0";
    "i(x4 * i(x1 * x2)) * x4 * x0 = x1 * x2 * x0"; "i(i(x1)) = x1";
    "i(1) = 1"; "x0 * i(x0) = 1"; "x0 * i(x0) * x3 = x3";
    "i(x2 * x3) * x2 * x3 * x1 = x1"; "x1 * 1 = x1"; "i(1) * x1 = x1";
    "i(i(x0)) * x1 = x0 * x1"; "i(x1) * x1 * x2 = x2"; "1 * x = x";
    "i(x) * x = 1"; "(x * y) * z = x * y * z"
]
|> interreduce []

 [
   "`i(x4 * x5) = i(x5) * i(x4)`"; 
   "`i(i(x1)) = x1`"; 
   "`i(1) = 1`"; 
   "`x0 * i(x0) = 1`";
   "`x0 * i(x0) * x3 = x3`"; 
   "`x1 * 1 = x1`"; 
   "`i(x1) * x1 * x2 = x2`"; 
   "`1 * x = x`"; 
   "`i(x) * x = 1`"; 
   "`(x * y) * z = x * y * z`""
 ]