Sun, 5 Jul 2009 20:06:22 -0700 (PDT)

Related articles |
---|

on definition of soundness and completeness bxin@acm.org (Bin Xin) (2009-06-23) |

Re: on definition of soundness and completeness gene.ressler@gmail.com (Gene) (2009-07-05) |

Re: on definition of soundness and completeness gopi.onthemove@gmail.com (gopi) (2009-07-16) |

From: | Gene <gene.ressler@gmail.com> |

Newsgroups: | comp.compilers |

Date: | Sun, 5 Jul 2009 20:06:22 -0700 (PDT) |

Organization: | Compilers Central |

References: | 09-06-078 |

Keywords: | theory |

Posted-Date: | 06 Jul 2009 05:50:06 EDT |

On Jun 23, 11:58 pm, Bin Xin <b...@acm.org> wrote:

*> In the presentation of various program analysis techniques, we often*

*> read claims of "soundness" and "completeness" properties of those*

*> techniques. I often find the definitions I expected for these two*

*> concepts at odds with whatever is put down in the paper I am reading.*

*> (I can give some fresh examples from latest conference like pldi).*

*> So here is what I think these two concepts should be used, and I am*

*> interested in finding out whether there is a standard way of using*

*> these two terms or anything goes as long as they are defined in some*

*> way each time.*

*>*

*> My understanding is that: soundness and completeness are used to*

*> describe the relationship between a formal system, F, and its*

*> interpretations, I, in logic. For a given predicate, P, that we are*

*> interested in, if it's True under interpretation I, then denote it as:*

*> I \models P. If P can be proved or computed by the formal system F,*

*> then denote it as: F \vdash P. Then,*

*>*

*> Soundness property (of F) can be claimed when: F \vdash P \implies I*

*> \models P.*

*>*

*> and conversely,*

*>*

*> Completeness property (of F) can be claimed when: I \models P \implies*

*> F \vdash*

*>*

*> In program analysis, the interpretation corresponds to the original*

*> analysis problem we are trying to solve; the formal system is what is*

*> actually being used/implemented to compute a solution (approximation,*

*> often times) to the analysis problem.*

*>*

*> Strangely, in papers that I feel those two terms are misused, some*

*> used them in a reversed sense, i.e. calling what should be soundness*

*> as completeness, and vice versa. Of course, I have found other cases*

*> where the use of these two terms cannot be understand in the above*

*> conceptual framework at all.*

IMO the common thread among different usages of these terms is

intuitive rather than formal. They're used to label an algorithm or

symbolic system S and make a claim about its qualities with respect to

some theoretical ideal T. S is sound if whenever it produces an

answer, that answer tells you something useful (in some well-defined

sense) about T. S is complete if every useful fact about T is implied

by at least one of S's answers.

The tricky bit is that the choice of S and T will always be made to

suit the purpose at hand. For example the operational semantics of a

programming language might be T if S is a type system and you are

making claims about the type system's efficacy. In other cases, the

same operational semantics might be S if T is some "potentially more

powerful" kind of semantics (say denotational), and you are worried

about the predictive power of the operational semantics. In another

case, you might be worried about the soundness and completeness of

denotational semantics, this time serving as S, in predicting

operational behavior of a set of programs T, defined in terms of their

operational semantics.

The confusion is made worse by the need to use symbols to represent

both S and T. Yet the ones in T are somehow "distinguished": They are

usually meant to represent abstractions in the reader's head. The

symbols of S are "just symbols" to be mechanically manipulated in some

manner.

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.