Partial Correctness and Divergent Predicates (§2.3, Lemmas 2.1–2.3)

These theorems establish the metatheoretic properties of accepting non-terminating refinement predicates under the partial-correctness semantics. They include the lemmas of §2.3 of the paper:

• Lemma 2.1 (And-True): sem_implies_and_true
• Lemma 2.2 (And-False): sem_implies_and_false_terminating, with diverge_and_false_not_implies_false showing that its termination hypothesis is necessary
• Lemma 2.3 (diverging predicates are vacuous): refine_diverge_eq_refine_true and refine_true_eq_base (part 1), no_converging_term_has_refine_false (part 2), and diverge_not_sub_false (part 3)

The key observations are:

• A refinement {x: A | false} is uninhabited (equivalent to Bot).
• A refinement {x: A | true} is equivalent to its base type A.
• A refinement with a diverging predicate is *vacuous*: it adds no constraint, so {x: A | diverge} is equivalent to {x: A | true} (and thus to A), for any A.
• However, a diverging predicate is *not* the same as a false predicate: {x: A | diverge} is inhabited but {x: A | false} is not.
• This holds even when the diverging predicate appears inside a larger expression that would otherwise be false, e.g. diverge() && false.
• Entailment rules differ in whether they need termination: Γ ⊨ t && true ⟹ t holds for arbitrary (possibly diverging) t, whereas Γ ⊨ t && false ⟹ false fails for diverging t and is recovered when t terminates.

In short: a diverging predicate cannot be used to prove false.

tdiverge never reduces to a value, regardless of fuel or environment.

0a. Bot and {T | false} have the same interpretation, for any T.

A refinement whose predicate evaluates to false is uninhabited, just like Bot — regardless of the base type.

0b. Unit and {Unit | true} have the same interpretation.

A trivially-true predicate adds no constraint, so the refinement collapses to its base type.

1a. No value inhabits Bot.

1b. No converging term has type Bot.

If t evaluates to a value v in any well-formed environment, then t cannot be semantically typed at Bot.

2. {Unit | true} and {Unit | diverge} have the same interpretation.

A diverging predicate is *vacuous*: the partial-correctness reading (if the predicate terminates, then it returns true) is trivially satisfied. So diverge and true are interchangeable as refinement predicates.

3a. {Unit | diverge} is not a semantic subtype of {Unit | false}

(Lemma 2.3, part 3). vunit inhabits the first but not the second, so the system is not degenerate: a diverging predicate is not equivalent to false.

3b. {Unit | diverge && false} is not a subtype of {Unit | false}.

Strict left-to-right evaluation means diverge && false still diverges: the outer false is unreachable. So the refinement is vacuously satisfied, and vunit inhabits it even though the conjunction "would have been" false under a more eager semantics.

Helper: evaluation of t && b in terms of the evaluation of t.

If t terminates with result r, then t && b terminates at one more unit of fuel: with the boolean andb r b if r is a boolean value, and stuck otherwise.

4. Entailment Γ ⊨ t && true ⟹ t holds for arbitrary t

(Lemma 2.1, And-True). No termination assumption on t is needed: if t && true evaluates to true whenever it terminates, then so does t. A case analysis shows the two sides line up, including the vacuous case where t diverges (then t && true diverges too, and both sides hold vacuously).

5a. Entailment Γ ⊨ t && false ⟹ false fails for diverging t.

With t = diverge, the left-hand side diverges, so it is vacuously true under the partial-correctness reading, while false is not. This shows that the termination hypothesis of Lemma 2.2 is necessary.

5b. Entailment Γ ⊨ t && false ⟹ false holds when t terminates

(Lemma 2.2, And-False). A term t semantically terminates in a context if it evaluates to a value in every well-formed environment.

If t terminates, the entailment is recovered: t && false then evaluates to false (or is stuck), so its eval_to_true assumption is contradictory.

6. {x: A | diverge} and {x: A | true} have the same interpretation,

for any base type A (Lemma 2.3, part 1). This generalizes example 2 above: a diverging predicate is vacuous, so it is interchangeable with true as a refinement predicate. Together with example 7 below, this shows that allowing diverging predicates is sound and not degenerate: a diverging predicate cannot be used to prove false.

As a corollary, the two types are semantic subtypes of each other (<:>, two-way subtyping) in any context.

{x: A | true} moreover collapses to its base type A, so {x: A | diverge} is also equivalent to A itself. This generalizes example 0b above.

Hence {x: A | true}, {x: A | diverge}, and A are all semantic subtypes of each other, in any context.

7. No converging term has type {x: A | false}, for any A

(Lemma 2.3, part 2). This generalizes example 1b above: if t evaluates to a value in some well-formed environment, then t cannot be semantically typed at {x: A | false}.