Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question

1 Answer 1

up vote 2 down vote accepted

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.