Return to Revisions

Both answers are correct.

Soundness in general means “nothing bad happens”. In the context of equational theories, the following would be sound phenomena:

1. A theory is sound (with respect to a given semantics) if derivable equalities are true.
2. An equality-checking algorithm is sound of it accepts only derivable equalities.

To see why these are soundness phenomena, think about what happens in the opposite case: a theory claims a false equality to hold, an algorithm accepts an underivable equality.

Soundness on its own is easy to achieve, consider an empty theory, or an algorithm that rejects all equalities.

Completeness in general means "as good as it gets". In the context of equational theories, the following would be complete phenomena:

1. A theory is complete (with respect to a given semantics) if it derives all true equations.
2. An equality-checking algorithm is complete if it accepts all derivable equalities.

Completeness on its own is easy to achieve, consider a theory that derives all equalities, or an algorithm that accepts all equalities.

Soundness and completeness balance each other out.

With regards to the question, we can think in terms of theories or in terms of an equality-checking algorithm.

In terms of theories and semantics based on normal forms, we think of the normal form nf(t) as the meaning of t. (For example, in a nice enough theory, the normal form of a closed term of type nat will be a numeral, i.e., a canonically represented natural number.) Under this view:

• the theory is sound (with respect to normal-form-semantics) if derivability of t ≡ u implies nf(t) = nf(u),
• the theory is complete if nf(t) = nf(u) implies t ≡ u.

As equality-checking algorithm based on normal forms accepts t ≡ u if the normal forms nf(t) and nf(u) are syntactically equal. Under this view:

• the algorithm is sound if nf(t) = nf(u) implies that t ≡ u is derivable,
• the algorithm is complete if derivability of t ≡ u implies nf(t) = nf(u).