An algebra of reversible computation
Proof
To prove that ({mathcal {E}}_{text {RPAP}}) is complete for RPAP modulo FR bisilumation equivalence, it means that (sunderline{leftrightarrow }^{fr} t) implies (s=t).
(1) We consider the introduction to the static ({text{parallel}},| ).
We consider reversible process terms contains +, (cdot , mid ) modulo associativity and commutativity (AC) of the + (RA1,RA2), and this equivalence relation is denoted by (=_{AC}). A reversible process term s then represents the collection of reversible process term t contains (+, cdot ), ({text{and}},|) such that (s =_{AC} t). Each equivalence class s modulo AC of the + can be represented in the form (s_{11}mid ldots mid s_{1l}+cdots +s_{k1}mid ldots mid s_{km}) with each (s_{ij}) either an atomic action or of the form (t_1cdot t_2). We refer to the subterms (s_{ij}) and (s_{ij}mid s_{i,j+1}) are the summands of s.
Then these rewrite rules are applied to the above reversible process terms modulo AC of the +.
We can see that the TRS is terminating modulo AC of the +.
Next, we prove that normal forms n and (n’) with (nunderline{leftrightarrow }^{fr} n’) implies (n=_{AC} n’). The proof is based on induction with respect to the sizes of n and (n’). Let (nunderline{leftrightarrow }^{fr} n’).
-
Consider a summand a of n. Then (nxrightarrow {a}a[m]+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’xrightarrow {a}a[m]+u), meaning that (n’) also contains the summand a.
-
Consider a summand a[m] of n. Then (nmathop {twoheadrightarrow}{a[m]}a+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’mathop {twoheadrightarrow}{a[m]}a+u), meaning that (n’) also contains the summand a[m].
-
Consider a summand (a_1ldots a_ildots a_k) of n. Then (nxrightarrow {a_1}cdots xrightarrow {a_i}cdots xrightarrow {a_k} a_1[m_1]ldots a_i[m_i]ldots a_k[m_k]+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’xrightarrow {a_1}cdots xrightarrow {a_i}cdots xrightarrow {a_k} a_1[m_1]ldots a_i[m_i]ldots a_k[m_k]+u), meaning that (n’) also contains the summand (a_1ldots a_ildots a_k).
-
Consider a summand (a_1[m_1]ldots a_i[m_i]ldots a_k[m_k]) of n. Then (nmathop {twoheadrightarrow }limits ^{a_k[m_k]}ldots mathop {twoheadrightarrow }limits ^{a_i[m_i]}ldots mathop {twoheadrightarrow }limits ^{a_1[m_1]}a_1ldots a_ildots a_k+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’mathop {twoheadrightarrow }limits ^{a_k[m_k]}ldots mathop {twoheadrightarrow }limits ^{a_i[m_i]}ldots mathop {twoheadrightarrow }limits ^{a_1[m_1]}a_1ldots a_ildots a_k+u), meaning that (n’) also contains the summand (a_1[m_1]ldots a_i[m_i]ldots a_k[m_k]).
-
Consider a summand (amid b) of n. Then (nxrightarrow {a}a[m]mid b+uxrightarrow {b}a[m]mid b[k]+u), or (nxrightarrow {b}amid b[k]+uxrightarrow {a}a[m]mid b[k]+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’xrightarrow {a}a[m]mid b+uxrightarrow {b}a[m]mid b[k]+u), or (n’xrightarrow {b}amid b[k]+uxrightarrow {a}a[m]mid b[k]+u), meaning that (n’) also contains the summand (amid b).
-
Consider a summand (a[m]mid b[k]) of n. Then (nmathop {twoheadrightarrow}{a[m]}amid b[k]+umathop {twoheadrightarrow }limits ^{b[k]}amid b+u), or (nmathop {twoheadrightarrow }limits ^{b[k]}a[m]mid b+umathop {twoheadrightarrow}{a[m]}amid b+u), so (nunderline{leftrightarrow }^{fr} n’) implies (n’mathop {twoheadrightarrow}{a[m]}amid b[k]+umathop {twoheadrightarrow }limits ^{b[k]}amid b+u), or (n’mathop {twoheadrightarrow }limits ^{b[k]}a[m]mid b+umathop {twoheadrightarrow}{a[m]}amid b+u), meaning that (n’) also contains the summand (a[m]mid b[k]).
-
The summands (asmid bt) and (a[m]smid b[k]t) are integrated cases of the above summands.
Hence, each summand of n is also a summand of (n’). Vice versa, each summand of (n’) is also a summand of n. In other words, (n=_{AC} n’).
Finally, let the reversible process terms s and t contains +, (cdot ), ({text{and}},|) be FR bisimilar. The TRS is terminating modulo AC of the +, so it reduces s and t to normal forms n and (n’), respectively. Since the rewrite rules and equivalence modulo AC of the + can be derived from the axioms, (s=n) and (t=n’). Soundness of the axioms then yields (sunderline{leftrightarrow }^{fr} n) and (tunderline{leftrightarrow }^{fr} n’), so (nunderline{leftrightarrow }^{fr} sunderline{leftrightarrow }^{fr} tunderline{leftrightarrow }^{fr} n’). We showed that (nunderline{leftrightarrow }^{fr} n’) implies (n=_{AC}n’). Hence, (s=n=_{AC} n’=t).
(2) We prove the completeness of the axioms involve the parallel operator (parallel ) and the communication merge (between ).
Then these rewrite rules are applied to the above reversible process terms modulo AC of the +.
We can see that the TRS is terminating modulo AC of the +.
We prove that normal forms n do not contain occurrences of the remaining two parallel operators (parallel ) and (between ). The proof is based on induction with respect to the size of the normal form n.
-
If n is an atomic action, then it does not contain any parallel operators.
-
Suppose (n =_{AC} s + t) or (n =_{AC} scdot t) or (n=_{AC}smid t). Then by induction the normal forms s and t do not contain (parallel ) and (between ), so that n does not contain (parallel ) and (between ) either.
-
n cannot be of the form (sparallel t), because in that case the directed version of RP1 would apply to it, contradicting the fact that n is a normal form.
-
Suppose (n =_{AC} sbetween t). By induction the normal forms s and t do not contain (parallel ) and (between ). We can distinguish the possible forms of s and t, which all lead to the conclusion that one of the directed versions of RC8-RC17 can be applied to n. We conclude that n cannot be of the form (sbetween t).
Hence, normal forms do not contain occurrences of parallel operators (parallel ) and (between ). In other words, normal forms only contains (+, cdot )
(text{and },| ).
Finally, let the reversible process terms s and t be FR bisimilar. The TRS is terminating modulo AC of the +, so it reduces s and t to normal forms n and (n’), respectively. Since the rewrite rules and equivalence modulo AC of the + can be derived from the axioms, (s=n) and (t=n’). Soundness of the axioms then yields (sunderline{leftrightarrow }^{fr} n) and (tunderline{leftrightarrow }^{fr} n’), so (nunderline{leftrightarrow }^{fr} sunderline{leftrightarrow }^{fr} tunderline{leftrightarrow }^{fr} n’). We showed that (nunderline{leftrightarrow }^{fr} n’) implies (n=_{AC}n’). Hence, (s=n=_{AC} n’=t). (square )