patternMinor
Soundness and completeness w.r.t. programming languages
Viewed 0 times
languagesprogrammingsoundnesscompletenessand
Problem
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.
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.
Solution
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")
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")
Context
StackExchange Computer Science Q#101055, answer score: 8
Revisions (0)
No revisions yet.