Equational reasoning

Mircea Marin

Many equational theories of practical interest can be represented by terminating term rewriting systems (TRSs for short). Suppose

Two terms s and t are equal in a theory represented by R iff s(Subscript[↔, R]^( * ))t, where (1) (Subscript[->, R]) is the rewrite relation induced by R, (2) (Subscript[↔, R]) is the symmetric closure of (Subscript[->, R]); and (3) (Subscript[↔, R]^( * )) is the reflexive and transitive closure of (Subscript[↔, R]).

In RhoLog, non-commutative groups can be represented by the rule with strategy identifier “Grp”:

<<RRhoLog`;
(* A terminating but non-confluent TRS for group theory *)
DeclareRules[
(x^i)(Subscript[->, "Grp"])(y^i)⟸((x^i)(Subscript[->, "Or"["Grp-Assoc","Grp-id","Grp-inv"]])(y^i)),
((x^i)⊕(y^i))⊕(z^i)(Subscript[->, "Grp-Assoc"])(x^i)⊕((y^i)⊕(z^i)),
0⊕(x^i)(Subscript[->, "Grp-id"])(x^i),
i[(x^i)]⊕(x^i)(Subscript[->, "Grp-inv"])0]

Notice that (x^i)⊕i[(x^i)]=0 is redundant because it can be deduced from the other axioms:

(x^i)⊕i[(x^i)]=0⊕((x^i)⊕i[(x^i)])=(i[i[(x^i)]]⊕i[(x^i)])⊕((x^i)⊕i[(x^i)])=((i[i[(x^i)]]⊕i[(x^i)])⊕(x^i))⊕i[(x^i)]=(i[i[(x^i)]]⊕(i[(x^i)]⊕(x^i)))⊕i[(x^i)]=(i[i[(x^i)]]⊕0)⊕i[(x^i)]=i[i[(x^i)]]⊕(0⊕i[(x^i)])=i[i[(x^i)]]⊕i[(x^i)]=0

Another important relation between terms is R-joinability: s(Subscript[↓, R])t iff s(Subscript[->, R]^( * ))u and t(Subscript[->, R]^( * ))u for some term u. For an arbitrary TRS R, R-joinability can be defined with the strategy "Join"[R]  defined as follows:

(* Definitiom of R-joinability *)
DeclareRules[
"Join"[((_)^i)]∷(x^i)↓(x^i),
"Join"[(R^i)]∷(p^i)⟸(((p^i)(Subscript[->, "Rw"[(R^i)]])(q^i))&&"Join"[(R^i)]∷(q^i))]

Two terms are R-equal is they are R-joinable. For example, (i[(x^i)]⊕(x^i))⊕(y^i) and (y^i)are “Grp”-equal because they are “Grp”-joinable:

Request["Join"["Grp"]∷((i[x]⊕x)⊕y)↓y,Trace->True]

R-equal terms are not necessarily R-joinable. For example, (i[(x^i)]⊕((x^i)⊕(y^i)) and (y^i) are R-equal but they are not R-joinable:

Request["Join"["Grp"]∷(i[x]⊕(x⊕y))↓y,Trace->True]

Good news: if R is both confluent and terminating then two terms are R-equal iff they have the same R-normal form. We can check if two terms have the same R-normal form with the strategy

DeclareRule["SameNF"[(R^i)]∷{(x^i),(y^i)}⟸(((x^i)(Subscript[->, "NF"["Rw"[(R^i)]]])(n^i))&&((y^i)(Subscript[->, "NF"["Rw"[(R^i)]]])(n^i)))]

Therefore, for equational reasoning it is convenient to have theories represented by confluent and terminating TRSs.

Another good news: The Knuth-Bendix completion procedure can transform some terminating TRSs into confluent and terminating TRS for the same equational theory. In particular, Knuth-Bendix completion transforms the TRS

((x^i)⊕(y^i))⊕(z^i)->(x^i)⊕((y^i)⊕(z^i)),0⊕(x^i)->(x^i),i[(x^i)]⊕(x^i)->0

into a terminating and confluent TRS consisting of 10 rewrite rules:

0⊕(x^i)->(x^i)
i[(x^i)]⊕(x^i)->0
((x^i)⊕(y^i))⊕(z^i)->(x^i)⊕((y^i)⊕(z^i))
i[(x^i)]⊕((x^i)⊕(y^i))->(y^i)
i[0]->0
(x^i)⊕0->(x^i)
i[i[(x^i)]]->(x^i)
(x^i)⊕i[(x^i)]->0
(x^i)⊕(i[(x^i)]⊕(y^i))->(y^i)
i[(x^i)⊕(y^i)]->i[(y^i)]⊕i[(x^i)]

In RhoLog:

DeclareRules[
0⊕(x^i)(Subscript[->, "GrpC"])(x^i),
i[(x^i)]⊕(x^i)(Subscript[->, "GrpC"])0,
((x^i)⊕(y^i))⊕(z^i)(Subscript[->, "GrpC"])(x^i)⊕((y^i)⊕(z^i)),
i[(x^i)]⊕((x^i)⊕(y^i))(Subscript[->, "GrpC"])(y^i),
i[0](Subscript[->, "GrpC"])0,
(x^i)⊕0(Subscript[->, "GrpC"])(x^i),
i[i[(x^i)]](Subscript[->, "GrpC"])(x^i),
(x^i)⊕i[(x^i)](Subscript[->, "GrpC"])0,
(x^i)⊕(i[(x^i)]⊕(y^i))(Subscript[->, "GrpC"])(y^i),
i[(x^i)⊕(y^i)](Subscript[->, "GrpC"])i[(y^i)]⊕i[(x^i)]]

(* Check if (0⊕x)⊕(0⊕0) and 0⊕x have same "GrpC"-normal form *)
Request["SameNF"["GrpC"]∷{(0⊕x)⊕(0⊕0),0⊕x},Trace->True]

(* Check if (0⊕x)⊕(0⊕0) and 0⊕x have same "Grp"-normal form *)
Request["SameNF"["Grp"]∷{(0⊕x)⊕(0⊕0),0⊕x}]