Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Based on the definition of a multiset and the information in this paper, why do we use multisets in proving the termination of a program? Is not the well-founded order enough?

share|improve this question
3  
Doesn't the abstract already answer your question? –  Juho Jan 20 '13 at 4:48
    
@Juho, NO! He does not –  M.A Jan 20 '13 at 13:05
    
Have you read the paper? If multisets are unnecessary, you should be able to do everything they do without them. I expect, though, that they include an example showing off their method. –  Raphael Jan 21 '13 at 10:52
add comment

1 Answer

As I understand the paper (and I was not familiar with it before) to prove termination of a program using the method of Floyd it is enough to find a function $\tau$ that maps the states of the program into some well-founded set $(S,\prec)$ such that this function is consistent with the program steps. Here consistency means that if a state $s$ follows $s^\prime$, then $\tau(s^\prime)\prec \tau(s)$.

Prior to Manna and Dershowitz the method of Floyd was used by mapping the states into the set of natural numbers or into the set of $n$-tuples thereof with lexicographic ordering (both sets are well-founded). The authors suggest a new source of well-founded sets for the Floyd method, that is the set of multisets of finite structures with multiset ordering and show how this can simplify termination proofs.

Note also that contrary to the sets of natural numbers and lexicographically ordered $n$-tuples, multisets ordering is only a partial ordering.

share|improve this answer
1  
Would be nice if you can add an example for how considering these orderings simplifies the termination proofs. –  Kaveh Jan 21 '13 at 9:08
add comment

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.