Conflicting terminology for completeness/soundness of normalization algorithm

Question

While reading some articles about formalization of various normalization algorithms, I found that these two papers use the term completeness/soundness in opposite way.

1. Hereditary Substitutions for Simple Types, Formalized

completeness : (t : Tm Γ σ) → ⌈ nf t ⌉ βη-≡ t
soundness : {t u : Tm Γ σ} → t βη-≡ u → nf t ≡ nf u

(Theorem 1 and Theorem 2)

2. Normalization by Evaluation Dependent Types and Impredicativity

soundness : Γ ⊢ nf(t) = t : T
completeness : Γ ⊢ t = t' : T → nf(t) = nf(t')

(See p.10)

I guess this is due to different PoV, but which one is more popular terminology?

Answer 1

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 if it accepts only derivable equalities.

To see why these are soundness phenomena, think about what happens in the opposite case: a theory derives a false equality, or 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.

On the other hand, an 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).