Certification Problem
Input (COPS 1157)
We consider the TRS containing the following rules:
|
a(b(x)) |
→ |
b(c(x)) |
(1) |
|
a(c(x)) |
→ |
c(a(x)) |
(2) |
|
b(b(x)) |
→ |
a(c(x)) |
(3) |
|
c(b(x)) |
→ |
b(c(x)) |
(4) |
|
c(b(x)) |
→ |
c(c(x)) |
(5) |
|
c(c(x)) |
→ |
c(b(x)) |
(6) |
|
P(x) |
→ |
Q(Q(p(x))) |
(7) |
|
p(p(x)) |
→ |
q(q(x)) |
(8) |
|
p(Q(Q(x))) |
→ |
Q(Q(p(x))) |
(9) |
|
Q(p(q(x))) |
→ |
q(p(Q(x))) |
(10) |
|
q(q(p(x))) |
→ |
p(q(q(x))) |
(11) |
|
q(Q(x)) |
→ |
x |
(12) |
|
Q(q(x)) |
→ |
x |
(13) |
|
p(P(x)) |
→ |
x |
(14) |
|
P(p(x)) |
→ |
x |
(15) |
The underlying signature is as follows:
{a/1, b/1, c/1, P/1, Q/1, p/1, q/1}Property / Task
Prove or disprove confluence.Answer / Result
No.Proof (by csi @ CoCo 2023)
1 Persistent Decomposition (Many-Sorted)
Non-confluence
is proven, because
a
system
induced by the sorts in the following many-sorted sort attachment
is not
confluent.
| a |
: |
1 → 1 |
| b |
: |
1 → 1 |
| c |
: |
1 → 1 |
| P |
: |
0 → 0 |
| Q |
: |
0 → 0 |
| p |
: |
0 → 0 |
| q |
: |
0 → 0 |
The subsystem is(1.1)
|
a(b(x)) |
→ |
b(c(x)) |
(1) |
|
a(c(x)) |
→ |
c(a(x)) |
(2) |
|
b(b(x)) |
→ |
a(c(x)) |
(3) |
|
c(b(x)) |
→ |
b(c(x)) |
(4) |
|
c(b(x)) |
→ |
c(c(x)) |
(5) |
|
c(c(x)) |
→ |
c(b(x)) |
(6) |
1.1 Non-Joinable Fork
The system is not confluent due to the following forking derivations.
| t0
|
= |
a(b(b(x1845))) |
|
→
|
a(a(c(x1845))) |
|
→
|
a(c(a(x1845))) |
|
→
|
c(a(a(x1845))) |
|
= |
t3
|
| t0
|
= |
a(b(b(x1845))) |
|
→
|
b(c(b(x1845))) |
|
→
|
b(b(c(x1845))) |
|
→
|
a(c(c(x1845))) |
|
→
|
c(a(c(x1845))) |
|
→
|
c(c(a(x1845))) |
|
→
|
c(b(a(x1845))) |
|
→
|
b(c(a(x1845))) |
|
= |
t7
|
The two resulting terms cannot be joined for the following reason:
- When applying the cap-function on both terms (where variables may be treated like constants)
then the resulting terms do not unify.