Certification Problem
Input (COPS 1039)
We consider two TRSs R and S where R contains the rules
|
f(a) |
→ |
b |
(1) |
| a |
→ |
a' |
(2) |
|
f(b) |
→ |
c |
(3) |
and S contains the following rules:
|
f(g(f(x))) |
→ |
x |
(4) |
|
f(g(x)) |
→ |
g(f(x)) |
(5) |
The underlying signature is as follows:
{a/0, b/0, c/0, f/1, g/1, a'/0}Property / Task
Prove or disprove commutation.Answer / Result
No.Proof (by ACP @ CoCo 2023)
1 Non-Joinable Fork
The systems are not commuting due to the following forking derivations.
| t0
|
= |
f(g(f(a))) |
|
→S
|
a |
|
= |
s1
|
and
| t0
|
= |
f(g(f(a))) |
|
→R
|
f(g(b)) |
|
= |
t1
|
There is no possibility to join
s1→R*·←S*
t1
for the following reason:
- We take the usable rules of the first term (w.r.t. the TRS for the first term)
and the usable rules of the second term (w.r.t. the TRS for the second term).
Then the terms are not joinable w.r.t. the resulting TRSs.
- We filter all terms and rules w.r.t. the following argument filter.
| π(a) |
= |
[] |
| π(b) |
= |
[] |
| π(f) |
= |
1 |
| π(g) |
= |
1 |
| π(a') |
= |
[] |
Then the resulting terms are not joinable w.r.t. the resulting TRSs.
- We take the usable rules of the first term (w.r.t. the TRS for the first term)
and the usable rules of the second term (w.r.t. the TRS for the second term).
Then the terms are not joinable w.r.t. the resulting TRSs.
- The first mentioned term is strictly larger than the second one (or vice versa). Here, the following discrimination pair has
been used w.r.t. the following interpretation.
Moreover, the (reversed) rules are weakly decreasing.
The discrimination pair is given by a