Certification Problem
Input (COPS 97)
We consider the TRS containing the following rules:
|
F(x,A(G(x))) |
→ |
G(F(x,x)) |
(1) |
|
F(x,G(x)) |
→ |
G(F(x,x)) |
(2) |
|
A(x) |
→ |
x |
(3) |
|
H(x) |
→ |
H(B(H(x))) |
(4) |
The underlying signature is as follows:
{F/2, A/1, G/1, H/1, B/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2023)
1 Persistent Decomposition (Many-Sorted)
Confluence
is proven, because
the maximal
systems
induced by the sorts in the following many-sorted sort attachment
are
confluent.
| F |
: |
1 ⨯ 1 → 1 |
| A |
: |
1 → 1 |
| G |
: |
1 → 1 |
| H |
: |
0 → 0 |
| B |
: |
0 → 0 |
The subsystems are(1.1)
(1.2)
|
F(x,A(G(x))) |
→ |
G(F(x,x)) |
(1) |
|
F(x,G(x)) |
→ |
G(F(x,x)) |
(2) |
|
A(x) |
→ |
x |
(3) |
1.1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
H(x) |
→ |
H(B(H(x))) |
(4) |
|
H(x) |
→ |
H(B(H(B(H(x))))) |
(5) |
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.1.1 Strongly closed
Confluence is proven since the TRS is strongly closed.
The joins can be performed using
7
step(s).
1.2 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
A(x) |
→ |
x |
(3) |
|
F(x,G(x)) |
→ |
G(F(x,x)) |
(2) |
|
F(x,A(G(x))) |
→ |
G(F(x,x)) |
(1) |
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.2.1 Locally confluent and terminating
Confluence is proven by showing local confluence and termination.
1.2.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [A(x1)] |
= |
1 · x1 + 7 |
| [G(x1)] |
= |
1 · x1 + 1 |
| [F(x1, x2)] |
= |
1 · x1 + 1 · x2 + 3 |
all of the following rules can be deleted.
|
A(x) |
→ |
x |
(3) |
|
F(x,A(G(x))) |
→ |
G(F(x,x)) |
(1) |
1.2.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [G(x1)] |
= |
1 · x1 + 1 |
| [F(x1, x2)] |
= |
1 · x1 + 4 · x2 + 3 |
all of the following rules can be deleted.
|
F(x,G(x)) |
→ |
G(F(x,x)) |
(2) |
1.2.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2.1.2 Local Confluence Proof
All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.