I'm looking at Knuth-Bendix ordering in the context of theorem proving with the superposition calculus. The explanations of KBO that I've been able to find say among other things that each function symbol must be assigned a positive weight except that one unary function can be assigned a weight of zero.
Why would you want to do this? What is the benefit of singling out one unary function like that?
(I'm also curious as to why that much and no more is allowed - why does it break if your zero-weight function has arity greater than one, for example - but the primary question is why you would want to do it in the first place.)