67 lines
10 KiB
Markdown
67 lines
10 KiB
Markdown
**N.B.** The definition of multistep reduction I use is composed of a reflexive case (`t →* t`) and a transitive case (`t₁ → t₂ →* t₃`). I need the following two lemmas throughout.
|
|
|
|
**Lemma** (transitivity): If `t₁ →* t₂ →* t₃` then `t₁ →* t₃`.
|
|
**Proof**: By induction on `t₁ →* t₂`. The reflexive case is trivial and the transitive case uses the induction hypothesis to combine the two multistep reductions.
|
|
|
|
**Lemma** (congruence): Multistep reduction is congruent in head positions, i.e. if `t₁ →* t₁'` then `if t₁ then t₂ else t₃ →* if t₁' then t₂ else t₃`, and similarly for `succ`, `pred`, and `iszero`.
|
|
**Proof**: If the reduction is reflexive, then the proof is trivial. Otherwise, the reduction is of the form `t₁ → t₁' →* t₁''`. By `E-If` (likewise `E-Succ`, `E-Pred`, `E-Iszero`), we have `if t₁ then t₂ else t₃ → if t₁' then t₂ else t₃`. By the induction hypothesis, we have `if t₁' then t₂ else t₃ →* if t₁'' then t₂ else t₃` (likewise for`succ`, `pred`, `iszero`). We have our goal by combining the two by transitivity.
|
|
|
|
----
|
|
|
|
**Exercise 3.5.16**: The two treatments of run-time errors agree if the following hold:
|
|
1. If `t` evaluates to a stuck state (using the rules without `E-*-Wrong`), then it evaluates to `wrong` (using the rules with `E-*-Wrong`). More precisely, if `t →* t' ↛` and `t ≠ v`, then `t →* wrong`.
|
|
2. If `t` evaluates to `wrong` and does not contain `wrong` as a subterm, then `t` evaluates to a stuck state. This is the converse of the first statement, except we exclude cases where `t` was wrong to begin with.
|
|
|
|
**Lemma 0**: If `t ↛` (using the rules without `E-*-Wrong`) and `t ≠ v` then `t → wrong` (using the rules with `E-*-Wrong`).
|
|
**Proof**: By induction on the shape of `t`. The cases where `t` is `true`, `false`, `0`, or `succ nv` are impossible.
|
|
* Case `t = if t₁ then t₂ else t₃`: The term does not step by `E-IfTrue`, `E-IfFalse`, nor `E-If`, so `t₁` is not `true` nor `false`, and does not step. If `t₁` is a value, then it is either a numeric value `nv`; otherwise, if it is not a value, then by the induction hypothesis, it steps to `wrong`. In both cases, `t₁` is a `badbool`, so the whole expression steps to `wrong` by `E-If-Wrong`.
|
|
* Case `t = succ t₁` where `t₁ ≠ nv`: The term does not step by `E-Succ`, so `t₁` does not step. If `t₁` is a value, then it must be `true` or `false`; otherwise, if it is not a value, then by the induction hypothesis, it steps to `wrong`. In both cases, `t₁` is a `badnat`, so the whole expression steps to `wrong` by `E-Succ-Wrong`.
|
|
* Case `t = pred t₁`: The term does not step by `E-PredZero`, `E-PredSucc`, nor `E-Pred`, so `t₁ ≠ nv` and does not step. Then the argument for the previous case follows, using instead `E-Pred-Wrong`.
|
|
* Case `t = iszero t₁`: The argument for the previous case follows, noting that the term does not step by `E-IszeroZero`, `E-IszeroSucc`, nor `E-Iszero`, and using `E-Iszero-Wrong` to step.
|
|
|
|
**Lemma 1**: If `t → t'` (using the rules with `E-*-Wrong`) and `t'` contains a `wrong` subterm, then either `t` contains a `wrong` subterm, or `t ↛` (using the rules without `E-*-Wrong`) and `t ≠ v`.
|
|
**Proof**: By induction on `t → t'`.
|
|
* Cases `E-If-True`, `E-If-False`: The reduction is `if true then t₁ else t₂ → t₁` or `if false then t₁ else t₂ → t₂`. If the RHS contains a `wrong` subterm, then evidently the LHS does as well.
|
|
* Cases `E-If`, `E-Pred`, `E-Iszero`: The three cases are similar; I use `E-Iszero` as representative. The reduction is `iszero t₁ → iszero t₂`, where `t₁ → t₂`, and `t₂` must contain a `wrong` subterm. By the induction hypothesis, either `t₁` contains a `wrong` subterm, in which case so does `iszero t₁`, or `t₁ ↛` and `t₁ ≠ v`. In this latter case, we have `iszero t₁ ↛`, since none of `E-Iszero-Zero`, `E-Iszero-Succ`, and `E-Iszero` apply, and `iszero t₁` is obviously not a value.
|
|
* Case `E-Succ`: The reduction is `succ t₁ → succ t₂`, where `t₁ → t₂`, and `t₂` must contain a `wrong` subterm. By the induction hypothesis, either `t₁` contains a wrong subterm, in which case so does `succ t₁`, or `t₁ ↛` and `t₁ ≠ v`. In this latter case, we have `succ t₁ ↛` since `E-Succ` does not apply, and we know that `succ t₁` is not a value since `t₁` is not a value.
|
|
|
|
**Lemma 2**: If `t →* wrong` (using the rules with `E-*-Wrong`), then either `t` contains a `wrong` subterm, or `t →* t' ↛` (using the rules without `E-*-Wrong`) and `t' ≠ v`.
|
|
**Proof**: By induction on `t →* wrong`. The reflexive case `wrong →* wrong` is trivial. In the transitive case `t → t' →* wrong`, by the induction hypothesis, either `t'` contains a `wrong` subterm, or `t' →* t'' ↛` and `t'' ≠ v`. In the former case, we use Lemma 1 on the reduction `t → t'`. In the latter case, we have `t → t' →* t'' ↛` and `t'' ≠ v` as required.
|
|
|
|
**Proof of 3.5.16** (Condition 1): Suppose `t →* t' ↛` and `t' ≠ v`. Then `t' → wrong` by Lemma 0, and `t →* wrong` by transitivity.
|
|
**Proof of 3.5.16** (Condition 2): Suppose `t →* wrong` and `t` does not contain a `wrong` subterm. Then by Lemma 2, it must be that `t →* t' ↛` and `t' ≠ v`.
|
|
|
|
----
|
|
|
|
**Exercise 3.5.17**: `t →* v` iff `t ⇓ v`.
|
|
|
|
**Lemma 3**: If `t₁ → t₂` and `t₂ ⇓ v`, then `t₁ ⇓ v`.
|
|
**Proof**: By induction on `t₁ → t₂`.
|
|
* Case `E-IfTrue`: The reduction is `if true then t₄ else t₅ → t₂`, with `t₂ ⇓ v`. By `B-Value`, `true ⇓ true`. Then by `B-IfTrue`, we construct `if true then t₄ else t₅ ⇓ v`.
|
|
* Case `E-IfFalse`: Similar as above, but using `B-IfFalse`.
|
|
* Case `E-If`: The reduction is `if t₃ then t₄ else t₅ → if t₃' then t₄ else t₅`, where `t₃ → t₃'`, with `if t₃' then t₄ else t₅ ⇓ v`. By inversion on the latter, the only possible cases are `B-IfTrue` and `B-IfFalse`.
|
|
* Subcase `B-IfTrue`: We have `t₃' ⇓ true` and `t₄ ⇓ v`. By the induction hypothesis, we have `t₃ ⇓ true`. Then by `B-IfTrue`, we construct `if t₃ then t₄ else t₄ ⇓ true`.
|
|
* Subcase `B-IfFalse`: Similar as above, but the induction hypothesis gives `t₃ ⇓ false`, and we use `B-IfFalse` instead.
|
|
* Case `E-Succ`: The reduction is `succ t₁ → succ t₂`, where `t₁ → t₂`, with `succ t₂ ⇓ v`. By inversion on the latter, the only possible case is `B-Succ`, with `t₂ ⇓ v`. By the induction hypothesis, we have `t₁ ⇓ v`. Then by `B-Succ`, we construct `succ t₁ ⇓ v`.
|
|
* Case `E-PredZero`: The reduction is `pred 0 → 0`, with `0 ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = 0`. The goal `pred 0 ⇓ 0` holds directly by `B-PredZero`.
|
|
* Case `E-PredSucc`: The reduction is `pred (succ nv) → nv`, with `nv ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = nv`. The goal `pred (succ nv) ⇓ nv` holds directly by `B-PredSucc`, whose premise `succ nv ⇓ succ nv` holds by `B-succ`, whose premise `nv ⇓ nv` holds by `B-Value`.
|
|
* Case `E-Pred`: The reduction is `pred t₁ → pred t₂`, where `t₁ → t₂`, with `pred t₂ ⇓ v`. By inversion on the latter, the only possible cases are `B-PredZero` and `B-PredSucc`.
|
|
* Subcase `B-PredZero`: We have `pred t₂ ⇓ 0`, where `t₂ ⇓ 0`. By the induction hypothesis, we have `t₁ ⇓ 0`. Then by `B-PredZero`, we construct `pred t₁ ⇓ 0`.
|
|
* Subcase `B-PredSucc`: We have `pred t₂ ⇓ nv`, where `t₂ ⇓ succ nv`. By the induction hypothesis, we have `t₁ ⇓ succ nv`. Then by `B-PredSucc`, we construct `pred t₁ ⇓ nv`.
|
|
* Case `E-IszeroZero`: The reduction is `iszero 0 → true`, with `true ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = true`. The goal `iszero 0 ⇓ true` holds directly by `B-IszeroZero`, whose premise `0 ⇓ 0` holds by `B-Value`.
|
|
* Case `E-IszeroSucc`: The reduction is `iszero (succ nv) → false`, with `false ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = false`. The goal `iszero (succ nv) ⇓ false` holds directly by `B-IszeroSucc`, whose premise `succ nv ⇓ succ nv` holds by `B-Succ`, whose premise `nv ⇓ nv` holds by `B-Value`.
|
|
* Case `E-Iszero`: The reduction is `iszero t₁ → iszero t₂`, where `t₁ → t₂`, with `iszero t₂ ⇓ v`. By inversion on the latter, the only possible cases are `B-IszeroZero` and `B-IszeroSucc`.
|
|
* Subcase `B-IszeroZero`: We have `iszero t₂ ⇓ true`, where `t₂ ⇓ 0`. By the induction hypothesis, we have `t₁ ⇓ 0`. Then by `B-IszeroZero`, we construct `iszero t₁ ⇓ true`.
|
|
* Subcase `B-IszeroSucc`: We have `iszero t₂ ⇓ false`, where `t₂ ⇓ succ nv`. By the induction hypothesis, we have `t₁ ⇓ succ nv`. Then by `B-IszeroSucc`, we construct `iszero t₁ ⇓ false`.
|
|
|
|
**Proof of 3.5.17** (LtR direction): By induction on `t →* v`. In the reflexive case, we have `v → v`, and `v ⇓ v` holds by `B-Value`. In the transitive case, we have `t₁ → t₂ →* v`. By the induction hypothesis, we have `t₂ ⇓ v`. Then by Lemma 3, we have `t₁ ⇓ v`.
|
|
|
|
**Proof of 3.5.17** (RtL direction): By induction on `t ⇓ v`. I freely use the transitivity and congruence lemmata to combine multistep reductions.
|
|
* Case `B-Value`: By reflexivity.
|
|
* Case `B-IfTrue`: The evaluation is `if t₁ then t₂ else t₃ ⇓ v`, where `t₁ ⇓ true` and `t₂ ⇓ v`. By the induction hypothesis, we have `t₁ →* true` and `t₂ →* v`. Then we have `if t₁ then t₂ else →* if true then t₂ else t₃ →* t₂ →* v`, the middle step by `E-IfTrue`.
|
|
* Case `B-IfFalse`: Similar as above, but using `E-IfFalse`.
|
|
* Case `B-Succ`: The evaluation is `succ t ⇓ succ v`, where `t ⇓ v`. By the induction hypothesis, we have `t →* v`. Then we have `succ t →* succ v` by congruence.
|
|
* Case `B-PredZero`: The evaluation is `pred t ⇓ 0`, where `t ⇓ 0`. By the induction hypothesis, we have `t →* 0`. Then we have `pred t →* pred 0 →* 0`, the last step by `E-PredZero`.
|
|
* Case `B-PredSucc`: The evaluation is `pred t ⇓ nv`, where `t ⇓ succ nv`. By the induction hypothesis, we have `t →* succ nv`. Then we have `pred t →* pred (succ nv) →* nv`, the last step by `E-PredSucc`.
|
|
* Case `B-IszeroZero`: The evaluation is `iszero t ⇓ true`, where `t ⇓ 0`. By the induction hypothesis, we have `t →* 0`. Then we have `iszero t →* iszero 0 →* true`, the last step by `E-IszeroZero`.
|
|
* Case `B-IszeroSucc`: The evaluation is `iszero t ⇓ false`, where `t ⇓ succ nv`. By the induction hypothesis, we have `t →* succ nv`. Then we have `iszero t →* iszero (succ nv) →* false`, the last step by `E-IszeroSucc`. |