2
$\begingroup$

I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness.

I'm taking a class, and according to my instructor:

Soundness is an analyzer's ability to prove the absence of errors. If a program is accepted by an analyzer, then the program is guaranteed to be safe.

On the other hand, completeness is an analyzer's ability to prove the presence of errors. If a program is rejected, then that program has errors.


An example that I thought of is: If an analyzer is designed to accept all programs, does this mean the analyzer's system is sound but incomplete? I'm not quite sure if my reasoning is correct.


I've taken a look at other answers on this community:

Is there a relationship between “sound and complete” in logic and “type safety” in PLs? and

Example of Soundness & Completeness of Inference

but still am not quite sure how the logical concepts apply to type systems of programming languages.

Would anyone be kind enough to explain the differences?


Thank you.

$\endgroup$
5
$\begingroup$

I'll focus on your question:

An example that I thought of is: If an analyzer is designed to accept all programs, does this mean the analyzer's system is sound but incomplete? I'm not quite sure if my reasoning is correct.

No, your reasoning is not correct. Let's take the definition your instructor gave you:

Soundness: [...] If a program is accepted by an analyzer, then the program is guaranteed to be safe.

If a sound analyzer accepts every program, by definition every program must be safe. This is not the case -- so a sound analyzer must not accept everything.

Completeness: [...] If a program is rejected, then that program has errors.

By definition, the always-accepting analyzer is complete: since it accepts everything, it rejects nothing, so all programs it rejects (i.e., none) have errors. This follows because from a false hypothesis ("a program is rejected") we can logically infer anything at all (including "the program has errors").

So, the always-accepting analyzer is complete, but not sound.

By contrast, an always-rejecting analyzer would be sound but not complete.


My preferred way to describe soundness and completeness is pretending we have an analyzer which, given an input program, returns "SAFE" (technically, accepts) or "NOT SAFE" (technically, rejects). A sound analyzer is one that can be trusted when it says "SAFE". A complete analyzer is one that can be trusted when it says "NOT SAFE".

A sound & complete analyzer can always be trusted, so (if it always halts) it is a decider for program safety. (Actually, by Rice's theorem, such a perfect analyzer can not exist.)

A sound but not complete analyzer, can be trusted only on "SAFE" answers. So, we can pretend it reliably answers "SAFE" or "DO NOT KNOW". (Indeed, "NOT SAFE" answers can not be trusted, so they actually mean "DO NOT KNOW")

A complete but not sound analyzer, can be trusted only on "NOT SAFE" answers. So, we can pretend it reliably answers "NOT SAFE" or "DO NOT KNOW". (Indeed, "SAFE" answers can not be trusted, so they actually mean "DO NOT KNOW")

$\endgroup$
2
$\begingroup$

I am really not an expert and just joined this site (I am a member of Stack Overflow C community for quite some time now), but this problem intrigues me and I tried to formulate an answer.

Soundness is an analyzer's ability to prove the absence of errors. If a program is accepted by an analyzer, then the program is guaranteed to be safe.

Seeing the analyzer as a Turing machine, it may not halt on a program that has errors.

On the other hand, completeness is an analyzer's ability to prove the presence of errors. If a program is rejected, then that program has errors.

Seeing the analyzer again as a Turing machine, and "reject" meaning the Turing machine halts (i.e. accepts), then it may not halt on a program without errors.

So if the analyzer is sound (accepts only true programs) and complete (rejects all false programs), then a program accepted by the analyzer is both true and not false. This means the Turing machine (analyzer) halts/decides on all input.

Note:

  • "accept" means a Turing machine that has consumed its inputs and that halts.

  • "reject" here also means a Turing machine that has consumed its inputs and that halts, but note we talk about an analyzer whose task is to detect invalid programs, so its task is to reject the program by saying "invalid" and then halt, i.e. accepts.

$\endgroup$
  • $\begingroup$ This perspective by Turing machine (TM) is nice. In the first case, do you mean "it may not accept a program that has errors"? The general view of a TM is, I believe, it may reject input by halting at non-accepting states. $\endgroup$ – Apass.Jack Dec 5 '18 at 18:00
  • $\begingroup$ May not halt means it can run forever - see Halting Problem. So on an incorrect progam "it may reject input by halting at non-accepting states" or it may run forever. $\endgroup$ – Paul Ogilvie Dec 5 '18 at 18:06
  • $\begingroup$ Not sure if you meant to agree to my point or not. My point is, an analyser with soundness as a TM may halt (at non-accepting states) on a program that has errors. If you agree to my point, you may want to update your answer to "it must not accept a program that has errors". $\endgroup$ – Apass.Jack Dec 5 '18 at 18:22
  • $\begingroup$ @Apass.Jack, I mean that, for soundness, a program without errors will cause the analyzer to stop in finite time. A program with errors could cause the analyzer to run forever. If it runs forever then it is undecided whether the program is correct. That is the point of "soundness". It does not mean "must not accept a program that has errors" because that is completeness. $\endgroup$ – Paul Ogilvie Dec 5 '18 at 18:34
  • $\begingroup$ @Apass.Jack, please see en.wikipedia.org/wiki/Halting_problem. Our problem is terminology, specifically the word "reject", which means "accept". $\endgroup$ – Paul Ogilvie Dec 5 '18 at 18:55
1
$\begingroup$

This definition of soundness and completeness could be helpful for you.

Soundness is the property of only being able to prove "true" things.

Completeness is the property of being able to prove all true things.

These are two properties of a logic system and about the ability of that system and not about any specific language or analyzer.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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