What are some useful corollaries of the preservation theorem?

Question

I was told that in a lambda calculus, if you have the notion of locks and concurrency, and you can prove it progress, then it means it's free of deadlocks. But is there any useful corollaries of preservation? I think it's kinda ok to change your type during reduction?

Answer 1

In short: Progress doesn't really matter if you don't have preservation. Note that progress only applies to well-typed terms.

Without preservation, you could have a runtime type error. Progress says that a well-typed term is either a value or it can take a step. It says that there is no undefined behavior when we only consider well-typed terms. Incidentally, I think of progress more in terms of not having undefined behavior, rather than not having deadlocks.

But a term could become ill-typed if we don't have preservation. Progress does not say anything about ill-typed terms.

Consider a bad multiply operation that starts out as returning type Nat but it becomes type Bool when it's evaluated. Before evaluation, it originally claims to give you a Nat but when it's actually evaluated it gives you a Bool. If you combine this with the typical subtraction operation, you will get a runtime type error.

Here is some Agda code demonstrating this example. Here are some of the key parts (leaving out proofs):

data _⟶_ : Expr → Expr → Set where

  -- The bad evaluation rule:
  E-mult : ∀ {a b} →
    ----
    mult a b ⟶ true

  ...

-- We do have progress!
progress : ∀ {a t} →
  a ⦂ t →
  Value a ⊎ (∃[ a′ ] (a ⟶ a′))
...

-- This becomes ill-typed in one step
example : Expr
example = sub (nat 5) (mult (nat 1) (nat 2))

-- It starts out well-typed...
example-well-typed :
  example ⦂ Nat
...

-- ... but then it steps to this expression:
ill-typed : Expr
ill-typed = sub (nat 5) true

ill-typed-step : example ⟶ ill-typed
...

-- We don't have preservation:
¬preservation : ¬ ∀ {a b t} →
  a ⦂ t →
  a ⟶ b →
  b ⦂ t
...

-- Even though we have progress and the initial example expression type checks,
-- once we have evaluated it one step we can no longer take a step:
ill-typed-example-errors :
  ¬ (∃[ b ] (ill-typed ⟶ b))
...

-- But it's also not a value:
¬ill-typed-example-value : ¬ Value ill-typed
...

Even though we technically have progress, it kinda doesn't matter because we can have expressions that type check but get "stuck": they eventually step to an expression that is not a value and cannot take a step.