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 2020)
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 Critical Pair Closing System
Confluence is proven using the following terminating critical-pair-closing-system R:
There are no rules.
1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
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
| [F(x1, x2)] |
= |
1 · x1 + 4 · x2 + 4 |
| [A(x1)] |
= |
4 · x1 + 4 |
| [G(x1)] |
= |
1 · x1 + 0 |
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
| [F(x1, x2)] |
= |
1 · x1 + 2 · x2 + 4 |
| [G(x1)] |
= |
1 · x1 + 1 |
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.