An Enhancement of  LCNC

2. Definition of a Signature

Constructor

\(\(
Constructor[fs___]\  := \ 
\ \ \ 
      \((Scan[Function[x, 
            \((IsFunctionSymbol[x]\  = \ True; 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IsConstructor[x] = \ True)
              \)], 
\ \ \ \ \ \ {fs}]; {fs})\)\)\)

Defined-function Symbol

\(\(
DefinedFunctionSymbol[fs___]\  := \ 
\ \ \ \ \ \ \ \ \ 
      \((Scan[Function[x, \ 
            \((IsFunctionSymbol[x]\  = \ True; 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              IsDefinedFunctionSymbol[x] = \ True)\)], \ 

          \ \ \ \ \ \ \ \ \ \ \ \ \ {fs}]; {fs})\)\)\)

Variable

\(\(
IsVar[s_Symbol]\  := \ Attributes[s]\  === \ {Temporary}\)\)

Function Term

\(\(
IsFunctionTerm[f_[___]] /; \ IsDefinedFunctionSymbol[f]\  := \ True
      \)\)

Defining a Signature

\(\(
DefineSignature[]\  := \ 
\ \ \ 
      \((IsConstructor[s_] /; \ \((s[\([0]\)] =!= Symbol)\) && \ AtomQ[s]\  = 
          \ True; 
\ \ \ \ 
        IsFunctionSymbol[s_] /; \((s[\([0]\)] =!= Symbol)\) && \ AtomQ[s]\  = 
          \ True; 
\ \ \ \ Constructor[List, Sequence, eq, ppeq]; )\)\)\)

3. Defining a RewriteRule

RewriteRule

\(
RewriteRule[s : symb_[___], \ t_, \ c___]\  := \ 
\ 
      Module[{parameter, condition, patternV, dummyV, localV}, 

        \ \ \ \ \ \ \ IsDefinedFunctionSymbol[symb]\  = \ True; 

        \ \ \ \ \ \ \ IsFunctionSymbol[symb]\  = \ True; 

        \ \ \ \ \ \ \ {parameter, condition, patternV, dummyV} = Uniform[s]; 
        
\ \ \ \ \ \ \ 
        localV = Union[Complement[Var[{c}], dummyV], patternV]; 

        \ \ \ \ \ \ \ PrintVarDecl[Var[{s, c}]]; 
\ \ \ \ \ \ \ 
        AppendTo[RewriteRuleList[symb], 
\ \ \ \ \ \ \ \ \ 
          FormFunction[parameter, localV, t, Join[condition, {c}]]]]\)\(PrintVarDecl[vset_]\  := 
\ 
      Switch[vset, 
\ \ \ \ \ \ \ \ {}, \ \(-1\), \ 
\ \ \ \ \ \ \ \ {_}, \ 
        Print["Symbol ", \ vset[\([1]\)], \ 
          " declared as variable."], 
\ \ \ \ \ \ \ \ {__}, \ 
        Print["Symbols ", Infix[vset, ","], 

          \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
          " declared as variable."]]\)

FormFunction[par_,localVar_, t_, {c___}]:=
   Function[par,Module[localVar,RewritesTo[t,c]]]
Uniform[s:_[___]] :=
 Block[{Cond={},PatternVar={},DummyVar={}},
       {ReplacePart[Map[Flattening,s],List,0],
        Cond,PatternVar,DummyVar}]
Flattening[x_]/;IsFunctionSymbol[x] :=
    Module[{w=Module[{a},a]}, AppendTo[Cond,ppeq[w,x]];w]
Flattening[x_]/;AtomQ[x] := (AppendTo[DummyVar,x];x)
Flattening[s_] :=
    Module[{w}, AppendTo[Cond,ppeq[w,s]];
           PatternVar=Join[PatternVar,Var[s]];w]

Auxiliary function definitions

Var[_]

\(
Var[term_Symbol]\  := \ 
\ \ \ 
      If[IsFunctionSymbol[term], {}, {}, {term}]
 (*\ 
      Recall\ our\ definition\ of\ a\ \(variable . \)\ *) 
 (*\ 
      Also\ note\ that\ IsFunctionSymbol[term]\ never\ reduces\ to\ 
        \(False . \)*) \)Var[s_ /; AtomQ[s]]  :=  {}\(Var[f_[term___]]\  := \ 
\ \ 
      Union[ReplacePart[Map[Var, \ {term}], Sequence, 0], \ Var[f]]\)

4. Definition of  LCNC

[t] Removal of trivial equations & Variable elimination

\(\(
Lcnc[{eq[x_ /; IsVar[x], y_ /; IsVar[y]], \ eqns___}]\  := \ 
\ 
      Module[{mapsTo}, 
\ \ \ \ \ \ \ \ 
        If\ [x\  === \ y, \ Lcnc[{eqns}], 
\ \ \ \ \ \ \ \ \ \ \ \ 
          \((mapsTo = \ x\  -> \ y; \ 
\ \ \ \ \ \ \ \ \ \ \ \ \ 
            PrependTo[Substitution, mapsTo]; 
\ \ \ \ \ \ \ \ \ \ \ \ \ 
            Lcnc[{eqns}\  /. \ mapsTo])\)]]\)\)

[on] Outermost narrowing

\(
Lcnc[{eq[s_ /; \ IsFunctionTerm[s], \ t_], \ eqns___}]\  := 
\ \ 
      Scan[NewLcnc[#, t, eqns]&, VariantsRule[s]]\)\(Lcnc[{eq[s_, t_ /; \ IsFunctionTerm[t]], \ eqns___}]\  := 
\ 
      Scan[NewLcnc[#, s, eqns]&, \ VariantsRule[t]]\)

[i] Imitation & Variable elimination

\(
Lcnc[{eq[x_ /; IsVar[x], s_ /; AtomQ[s]], \ eqns___}] := \ 
\ 
      With[{mapsTo = \ x\  -> \ s}, 
\ \ \ \ \ \ \ \ \ 
        PrependTo[Substitution, \ mapsTo]; 
\ \ \ \ \ \ \ \ \ 
        Lcnc[{eqns}\  /. \ mapsTo]]\)\(Lcnc[{eq[x_ /; IsVar[x], s_], \ eqns___}] := \ 
\ \ \ \ \ 
      Module[{cs\  = \ Map[Function[{}, Module[{c}, c]], \ s], mapsTo}, 

        \ \ \ \ \ \ \ \ \ \ mapsTo\  = \ x\  -> \ cs; 
\ \ \ \ \ \ \ \ \ \ 
        PrependTo[Substitution, \ mapsTo]; 
\ \ \ \ \ \ \ \ \ \ 
        Lcnc[{NewEqns[eq, s, cs], \ eqns} /. \ mapsTo]]\)\(Lcnc[{eq[s_ /; AtomQ[s], x_ /; IsVar[x]], \ eqns___}]\  := \ 
\ \ \ 
      With[{mapsTo = \ x\  -> \ s}, 
\ \ \ \ \ \ \ \ \ 
        PrependTo[Substitution, \ mapsTo]; 
\ \ \ \ \ \ \ \ \ 
        Lcnc[{eqns}\  /. \ mapsTo]]\ \)\(Lcnc[{eq[s_, x_ /; IsVar[x]], \ eqns___}]\  := \ 
\ \ \ \ \ 
      Module[{cs\  = \ Map[Function[{}, Module[{c}, c]], \ s], mapsTo}, 

        \ \ \ \ \ \ \ \ \ \ \ \ \ mapsTo\  = \ x\  -> \ cs; 

        \ \ \ \ \ \ \ \ \ \ \ \ \ PrependTo[Substitution, \ mapsTo]; 

        \ \ \ \ \ \ \ \ \ \ \ \ \ 
        Lcnc[{NewEqns[eq, \ s, \ cs], \ eqns}\  /. \ mapsTo]]\)

[de] Decomposition

\(
Lcnc[{eq[s_ /; AtomQ[s], \ t_], \ eqns___}]\  := \ 
\ \ \ 
      If[s === t, \ Lcnc[{eqns}]]\)\(Lcnc[{eq[s_, t_], \ eqns___}]\ \  := 
	
      If[s[\([0]\)]\  === \ t[\([0]\)], Lcnc[{NewEqns[eq, s, t], \ eqns}]]
        \)

[vp] Variable elimination  for parameter passing equations

\(
Lcnc[{ppeq[s_, x_ /; IsVar[x]], \ eqns___}]\ \  := \ 
\ 
      With[{mapsTo = \ x\  -> \ s}, 
\ \ \ \ \ \ \ 
        PrependTo[Substitution, mapsTo]; 
\ \ \ \ \ \ \ 
        Lcnc[{eqns}\  /. \ mapsTo]]\)\(Lcnc[{ppeq[x_ /; IsVar[x], s_], \ eqns___}]\  := \ 
\ 
      With[{mapsTo = \ x\  -> \ s}, 
\ \ \ \ \ \ \ 
        PrependTo[Substitution, mapsTo]; 
\ \ \ \ \ \ \ 
        Lcnc[{eqns}\  /. \ mapsTo]]\)

[onp] Outermost narrowing for parameter passingt equations

\(\(
Lcnc[{ppeq[s_ /; \ IsFunctionTerm[s], \ t_], \ eqns___}]\  := 
\ 
      Scan[NewLcncPP[#, t, eqns]&, \ VariantsRule[s]]\)\)

[dp] Decomposition for parameter passing equations

\(
Lcnc[{ppeq[s_ /; AtomQ[s], \ t_], \ eqns___}]\  := \ 
\ \ \ 
      If[s === t, \ Lcnc[{eqns}]]\)\(Lcnc[{ppeq[s_, t_], \ eqns___}]\ \  := 
	
      If[s[\([0]\)]\  === \ t[\([0]\)], Lcnc[{NewEqns[ppeq, s, \ t], \ eqns}]]
        \)

Base case of induction over the equations (goal)

\(
Lcnc[{}]\  := \ 
\ \ 
      \((AnswerList\  = \ Union[AnswerList, {ComputedAnswer[]}]; 
\ \ 
        If[\((NSolutions -= 1)\) == 0, Throw[AnswerList], \ AnswerList])
        \)\)\(ComputedAnswer[]\  := \ 
\ \ 
      With[{newSubst\  = \ 
            Substitution
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  /. \ 
              Inner[Rule, NewGoalVar, GoalVar, List]}, 
\ \ \ \ \ \ \ 
        FormSubst[{GoalVar, \ FixedPoint[#\  /. \ newSubst&, GoalVar]}]]\)\(EmptySequence\  = \ Sequence[]; 

    FormSubst[x_]\  := \ 
\ \ \ 
      MapThread[Function[{v, t}, \ If[v === t, \ EmptySequence, v\  -> t]], x]
        \)

Auxiliary Definitions

\(\(
NewEqns[h_, s_, t_]\  := 
\ \ 
      ReplacePart[Table[h[s[\([i]\)], t[\([i]\)]], {i, Length[s]}], Sequence, 
        0]
 (*\ NewEqns[h_, _[s___], _[t___]]\  := 
\ \ 
        ReplacePart[MapThread[h, {{s}, {t}}], Sequence, 0]\ *) 

    \ \  (*\ Inner[h, s, t, Sequence, 1]\ *) 

    \ \  (*\ possible\ only\ Ver . \ 3.0\ *) \)\)

\(\(
NewLcncPP[RewritesTo[t_, \ c___], rhs_, \ eqns___]\  := 
	
      Block[{Substitution = Substitution}, 
	\ 
        Lcnc[{c, ppeq[t, rhs], eqns}]]\)\)

\(\(
NewLcnc[RewritesTo[t_, c___], rhs_, \ eqns___]\  := 
	
      Block[{Substitution = Substitution}, 
\ \ \ \ \ \ \ 
        Lcnc[{c, eq[t, rhs], eqns}]]\)\)

\(
VariantsRule[f_[arg___]]\  := \ 
\ 
      ApplyListOfFunctions[RewriteRuleList[f], {arg}]\)\(ApplyListOfFunctions[{f___}, arg_]\  := 
\ 
      Map[Function[{g}, Apply[g, arg]], {f}]\)

5. Usage of the System

Term Algebra Solver

\(
Clear[TSolve]\)\(Options[TSolve]\  = 
      \ {NSolution -> \ 256, \ Rule\  :> \ {}, \ Initialize -> \ False, 

        \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Constructor\  -> \ {}, \ 
        DefinedFunctionSymbol\  -> \ {}}\)\(TSolve[goal_List, \ varList_List, \ opts___]\  := 
\ \ \ \ 
      Block[{AnswerList\  = \ {}, 
\ \ \ \ \ \ \ \ \ \ \ 
          GoalVar\  = \ varList, 
\ \ \ \ \ \ \ \ \ \ \ 
          NSolutions\  = \ \(NSolution /. {opts}\) /. Options[TSolve], 

          \ \ \ \ \ \ \ \ \ \ \ NewGoalVar}, 
\ \ \ \ \ \ 
        If[NSolutions <= 0, {}, 
\ \ \ \ \ \ \ \ 
          Module[{saveRewriteRuleList = DownValues[RewriteRuleList], 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              saveFunctionSymbol = DownValues[IsFunctionSymbol], 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              saveDefinedFunctionSymbol = 

                \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
                DownValues[IsDefinedFunctionSymbol], 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              saveConstructor = DownValues[IsConstructor], 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ newGoal}, 

            \ \ \ \ \ \ \ \ \ {newGoal, NewGoalVar} = 
              Module[varList, {goal, \ varList}]; 
\ \ \ \ \ \ \ \ \ 
            If[\(Initialize /. {opts}\) /. Options[TSolve], \ BeginRule[]]; 

            \ \ \ \ \ \ \ \ \ 
            Scan[Constructor, \ 
              \(Constructor /. {opts}\) /. Options[TSolve]]; 

            \ \ \ \ \ \ \ \ \ 
            Scan[DefinedFunctionSymbol, \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              \(DefinedFunctionSymbol /. {opts}\) /. Options[TSolve]]; 

            \ \ \ \ \ \ \ \ \ \(Rule /. {opts}\) /. Options[TSolve]; 

            \ \ \ \ \ \ \ \ \ 
            Block[{Substitution\  = \ {}}, \ Catch[Lcnc[newGoal]]]; 

            \ \ \ \ \ \ \ \ \ 
            DownValues[RewriteRuleList]\  = \ saveRewriteRuleList; 

            \ \ \ \ \ \ \ \ \ 
            DownValues[IsFunctionSymbol]\  = \ saveFunctionSymbol; 

            \ \ \ \ \ \ \ \ \ 
            DownValues[IsDefinedFunctionSymbol]\  = \ 

              \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
              saveDefinedFunctionSymbol; 
\ \ \ \ \ \ \ \ \ 
            DownValues[IsConstructor]\  = \ saveConstructor]; 
\ AnswerList]]
        \)TSolve[eqn_,  varList_List, opts___]  :=  
      TSolve[{eqn}, varList, opts]\(TSolve[goal_List, \ var_, opts___]\  := \ 
\ \ \ 
      TSolve[goal, {var}, \ opts]\)TSolve[eqn_,  var_,  opts___]  :=  
      TSolve[{eqn}, {var},  opts]

Typical Session

\(\(
BeginRule[]\  := \ 
      \((Clear[RewriteRuleList, IsConstructor, 

          \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
          IsDefinedFunctionSymbol, IsFunctionSymbol]; 
        \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
        RewriteRuleList[_] := \ {}; 
        \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ DefineSignature[]; )\)\)\)

Extensions

\(\(
SetAttributes[RuleList, HoldRest]; 

    RuleList[{f___}, {rule___}]\  := 
\ \ 
      \((Scan[Function[x, RewriteRuleList[x] = {}], \ {f}]; 
\ \ \ {rule})
        \)
\ \ \)\)

Input Form

SetAttributes[LongRightArrow, HoldAll]
SetAttributes[DoubleLongLeftArrow, HoldAll]

lhs_⟶ rhs_ ⟸ {c___} := 
        RewriteRule[lhs,  rhs, c]
lhs_⟶ rhs_  := RewriteRule[lhs,  rhs]

x_ ≈  y_ := eq[x, y]