Re: on definition of soundness and completeness

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.

Return to the comp.compilers page.
Search the comp.compilers archives again.