1
$\begingroup$

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.)

1 Answers 1

2

One possibler example. Let's have expression on natural numbers using symbols $0$ (arity 0), $S$ (arity 1) and some other operations like $+$ or $×$. If we give zero weight to $S$, the canonical form representing $n$ as $\underbrace{S(\ldots (S}_{n\mbox{ times}}(0))\ldots)$ will have the least weight - all canonical natural numbers will have the same weight as $0$.


The compatibility condition for a KBO says that if an unary symbol has zero weight, it has to be the greatest one wrt the ordering on symbols. This forces that there can be only one such a symbol. I would have to check the details, but violating this would cause the ordering to fail some of the required properties.