A question about KB with constants.

Stream: Equational

[Fan Zheng]

I'm playing with the online version of KBCV and I give it the following input:

m(x,y)=m(y,m(y,m(x,x))) (Equation 3352)
m(m(x,x),m(x,x))=o() (which I add myself)

and it outputs the completion:

Knuth-Bendix completion

K1 : m(m(x,x),m(x,m(x,x))) -> o()
R1 : m(x,m(x,m(y,y))) -> m(y,x)
R2 : m(m(x,x),m(x,x)) -> o()

Squier completion

C1

m(m(x,x),m(m(x,x),m(m(x,x),m(x,x)))) -R1(m(x,x),m(x,x))-> m(m(x,x),m(x,x)) -R2(x)-> o()
m(m(x,x),m(m(x,x),m(m(x,x),m(x,x)))) -m(m(x,x),R1(m(x,x),x))-> m(m(x,x),m(x,m(x,x))) -K1(x)-> o()

so is it saying that K1, R1 and R2 are complete?, but how about the following CR:

o=(xx)(xx)=(xx)((xx)((xx)(xx)))=(xx)((xx)o),

where the RHS seems irreducible?

[Fan Zheng]

And this even simpler one:
x(xx)=(xx)((xx)(xx))=(xx)o?

[Bhavik Mehta]

I'm not sure which version of KBCV you're using, but a local install terminates with error giving that one of the equations can't be oriented. Although I don't quite know why it's not orientable...

[Bhavik Mehta]

Playing with it by hand, I think I've shown that m(x,y) -> o() (which is clearly confluent)

[Cody Roux]

which version are you using?

[Cody Roux]

my guess is that it uses KB order or RPO/LPO/MPO, which for this kind of system is pretty much just size of terms

[Bhavik Mehta]

The version I'm using is LPO

[Cody Roux]

Yea so "lex term size" in this case

[Bhavik Mehta]

Does that justify why m(x,y)=m(y,m(y,m(x,x))) can't be oriented backwards? The term size looks pretty clearly decreasing to me! Or is the idea that x could be much larger than y in the general case

[Cody Roux]

swapping variables is a good way to confuse a lex

[Cody Roux]

mpo might owrk

[Cody Roux]

(I'll leave that typo)

[Cody Roux]

I have a little KB completion implementation and it was hard to get right, wouldn't be horribly shocked if there was a bug in the online version

[Fan Zheng]

@Bhavik Mehta I'm using the online version. Playing by hand I get (substituting xx for x in xy=y(y(xx)) ) (xx)y=y(yo()), which is not orientable, right?

[Cody Roux]

Not with LPO, I think

[Cody Roux]

I'm bad at this; sometimes I use https://aprove.informatik.rwth-aachen.de/interface/v-AProVE2023/trs_aprove to figure out if a TRS terminates; it's astronomically more powerful than LPO/MPO but it gives an idea