<p>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?</p>

<lambda-calculus>
What are some useful corollaries of the preservation theorem?
CC BY-SA 4.0
2024-02-19T19:31:55.740Z
I think of progress more as saying that there is no undefined behavior, rather than saying something about concurrency and deadlocks. If you have type safety, every well-typed term in the language has a behavior given by your semantics. Note that this is not the case for some languages. For instance, C has a lot of undefined behavior (intentionally, in fact!)
David Young
CC BY-SA 4.0
2024-02-19T19:35:06.987Z
Furthermore, you don't typically define the behavior of things that would give a type error. So, when you say that every well-typed term has a well-defined behavior, you are saying that there are no runtime type errors (among other things).
David Young
CC BY-SA 4.0
2024-02-20T19:42:22.300Z
One more thing: I would associate being free of deadlocks with [safety and liveness properties of concurrent systems](https://en.wikipedia.org/wiki/Safety_and_liveness_properties) more than I would with progress (or type safety in general).
David Young
<p>In short: <em>Progress doesn't really matter if you don't have preservation.</em> Note that progress only applies to well-typed terms.</p>
<p>Without preservation, you could have a runtime type error. Progress says that a <em>well-typed</em> 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.</p>
<p>But a term could become <em>ill-typed</em> if we don't have preservation. Progress does not say anything about ill-typed terms.</p>
<p>Consider a bad multiply operation that starts out as returning type <code>Nat</code> but it becomes type <code>Bool</code> when it's evaluated. Before evaluation, it originally claims to give you a <code>Nat</code> but when it's actually evaluated it gives you a <code>Bool</code>. If you combine this with the typical subtraction operation, you will get a runtime type error.</p>
<p><a href="https://gist.github.com/roboguy13/72559290fa3a39e06a91d9a31b63d468" rel="nofollow noreferrer">Here</a> is some Agda code demonstrating this example. Here are some of the key parts (leaving out proofs):</p>
<pre><code>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
...
</code></pre>
<p>Even though we <em>technically</em> have progress, it kinda doesn't matter because we can have expressions that type check but get &quot;stuck&quot;: they eventually step to an expression that is not a value and cannot take a step.</p>

CC BY-SA 4.0
2024-02-19T19:15:59.197Z
2024-02-20T04:31:58.410Z
2024-02-20T04:31:58.410Z
David Young
# What are some useful corollaries of the preservation theorem?
Posted by: username_0 on 2024-02-19
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?
**Tags:** lambda-calculus
> **Comments:**
> **username_1**: I think of progress more as saying that there is no undefined behavior, rather than saying something about concurrency and deadlocks. If you have type safety, every well-typed term in the language has a behavior given by your semantics. Note that this is not the case for some languages. For instance, C has a lot of undefined behavior (intentionally, in fact!)  
> **username_1**: Furthermore, you don't typically define the behavior of things that would give a type error. So, when you say that every well-typed term has a well-defined behavior, you are saying that there are no runtime type errors (among other things).  
> **username_1**: One more thing: I would associate being free of deadlocks with [safety and liveness properties of concurrent systems](https://en.wikipedia.org/wiki/Safety_and_liveness_properties) more than I would with progress (or type safety in general).  
---
## 1 answers
### Answer by username_1 on 2024-02-19. Score: 4 | Accepted answer
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.
---
