on definition of soundness and completeness
Bin Xin
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.
What is your take?
regards,
-b
Gene
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.
gopi
> \models P.
>
> and conversely,
>
> Completeness property (of F) can be claimed when: I \models P \implies
> F \vdash
This agrees with the concepts of soundness and completeness I am
familiar with. Going back to basics, When the formal system is an
algorithm, this translates to something like this in simple english:
An algorithm is said to be sound if for every problem P, every
solution the algorithm finds is a correct solution.
An algorithm is said to be complete if for every problem P, if a
solution exists, the algorithm will find it (in finite time).
These are fairly important properties (for example in the AI
Planning / Planner space), and I will be surprised if any one gets
them wrong !
Gopi
---
Sankhya Technologies Private Limited
http://www.sankhya.com
Mobile: +91 94408 78042
US (Voice-Mail)