Soundness and completeness

Data

Data represent information:

Data are built using data constructors:

• A representation is sound when using constructors correctly always yields a piece of data that correctly represents the information it is meant to represent. (Otherwise this representation is unsound.)

• A representation is complete when all the information we wish to represent can be represented using the data constructors. (Otherwise this representation is incomplete.)

For a first example, the representation of booleans is both sound and complete.

For a second example, in OCaml, the default representation of integers has a fixed size, and so only integers between, e.g., -4611686018427387904 and 4611686018427387903 can be represented. This representation is sound in that the representation of any integer between -4611686018427387904 and 4611686018427387903 does correspond to a mathematical integer, but it is incomplete since integers smaller than -4611686018427387904 or greater than 4611686018427387903 cannot be represented.

For a third example, in Chez Scheme, the default representation of integers does not have a fixed size: this representation is complete... up to the size of the memory of our computer.

Programs

A terminating batch program implements a function from input information to output information:

• Such a program is sound (or again: correct) if running it on a piece of data that represents some input information yields a piece of data that represents some other output information implies that applying the function computed by the program to this input information yields this output information.

  More concretely, assuming that processing the input data d1 yields the output data d2, then if d1 represents a piece of information i1 and d2 represents a piece of information i2, then the program is said to be sound if we wanted to map i1 to i2.

• Such program is complete if applying the function computed by the program to some input information yields some output information implies that running it on a piece of data that represents the input information yields a piece of data that represents the other output information.

  More concretely, assuming we want to map a piece of information i1 to a piece of information i2, then if i1 is represented by d1 and i2 is represented by d2, then the program is said to be complete if running it on d1 yields d2.

For example, consider a predicate (i.e., a function that returns a boolean) for prime numbers. Applying this predicate to a prime number returns true and applying it to a composite number returns false. Consider also a program that implements this predicate:

• This program is sound if running it on a number yields true implies that this number is prime.

• This program is complete if running it on a prime number yields true.

Interlude

Pablito: And that’s it?

Dana: That’s it.

Pablito: What about running this program on a composite number?

Halcyon: I think that should yield false.

Anton: Right. Shouldn’t we also have that if running this program on a number yields false, then this number is composite? Shouldn’t this be part of soundness?

Pablito: Yes. And shouldn’t we also have that running this program on a composite number should yield false? Shouldn’t this be part of completeness?

Dana: You are both right. And the two implications you have just listed are not missing: They are consequences of soundness and completeness.

Mimer: And you guys will prove that in not very long.

Alfrothul: I can’t wait.

Bong-sun (in thoughts): So each of soundness and completeness is an implication.

Mimer: Yes.

Bong-sun: May I make that explicit by adding parentheses?

Mimer: Pray do.

Bong-sun: Lemme see... A program is sound whenever (running it on a piece of data that represents the input information yields a piece of data that represents the output information) implies that (applying the function computed by the program to this input information yields this output information).

Mimer: Yes.

Pablito: That’s an implication all right.

Bong-sun: It is, isn’t it. Now for the converse... A program is complete whenever (applying the function computed by the program to some input information yields some output information) implies that (running it on a piece of data that represents the input information yields a piece of data that represents the output information).

Mimer: Yes.

Pablito: Another implication.

Halcyon (cleverly): Your parentheses are not parenthetical.

Bong-sun: That is correct. And now I can see that soundness and completeneness are converse implications.

Mimer: Which is a good observation. Well done, Bong-sun!

Bong-sun: Thank you.

Alfrothul: Can we be pedantic?

Mimer: Sure.

Alfrothul: Thanks. Just above, the example about detecting prime numbers says “This program is sound if running it on a number yields true implies that this number is prime.”

Anton: But really it should be “(Running [this program] on the representation of a given number yields the representation of true) implies that (the given number is prime).”

Mimer: Yes.

Anton: And still just above, the example about detecting prime numbers says “This program is complete if running it on a prime number yields true.”

Alfrothul: But really it should be “Given a number that is prime, running this program on the representation of this given number yields the representation of true).”

Mimer: Yes. Feels good?

Alfrothul and Anton: Yes, thank you.

Mimer: You guys are going to do fine with tCPA.

Version

Added a diagram for programs, tightened the narrative, and expanded the interlude [17 Jan 2025]

Added the example of booleans [15 Jan 2025]

Created [14 Jan 2025]