michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

small revision up through preservation

Browse source
This commit is contained in:
wadler 2018-06-28 12:28:01 -03:00
parent fdd4f4922e
commit b717459556
1 changed files with 16 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/plta/PandP.lagda
View file

@ -328,15 +328,16 @@ In symbols,
----------------------- -----------------------
Γ ⊢ M ⦂ A → Δ ∋ M ⦂ A Γ ⊢ M ⦂ A → Δ ∋ M ⦂ A
Special cases of renaming include the _weaken_ lemma (a term Three important corollaries follow. The _weaken_ lemma asserts a term
well-typed in the empty context is also well-typed in an arbitary well-typed in the empty context is also well-typed in an arbitary
context) the _drop_ lemma (a term well-typed in a context where the context. The _drop_ lemma asserts a term well-typed in a context where the
same variable appears twice remains well-typed if we drop the shadowed same variable appears twice remains well-typed if we drop the shadowed
occurrence) and the _swap_ lemma (a term well-typed in a context occurrence. The _swap_ lemma asserts a term well-typed in a context
remains well-typed if we swap two variables). Renaming is similar to remains well-typed if we swap two variables.
the _context invariance_ lemma in _Software Foundations_, but it does
not require the definition of `appears_free_in` nor the Renaming is similar to the _context invariance_ lemma in _Software
`free_in_context` lemma. Foundations_, but it does not require the definition of
`appears_free_in` nor the `free_in_context` lemma.
The second step is to show that types are preserved by The second step is to show that types are preserved by
_substitution_. _substitution_.
@ -647,7 +648,6 @@ Now that naming is resolved, let's unpack the first three cases.
Γ ⊢ ⌊ x ⌋ ⦂ A Γ ⊢ ⌊ x ⌋ ⦂ A
which follows by the typing rule for variables. which follows by the typing rule for variables.
* In the abstraction case, we must show * In the abstraction case, we must show
@ -677,7 +677,7 @@ Now that naming is resolved, let's unpack the first three cases.
The typing rule for abstractions then yields the required conclusion. The typing rule for abstractions then yields the required conclusion.
+ If the variables are unequal then after simplification we must show + If the variables are distinct then after simplification we must show
∅ ⊢ V ⦂ B ∅ ⊢ V ⦂ B
Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
@ -722,12 +722,12 @@ Now that naming is resolved, let's unpack the first three cases.
Applying the induction hypothesis for `L` and `M` and the typing Applying the induction hypothesis for `L` and `M` and the typing
rule for applications yields the required conclusion. rule for applications yields the required conclusion.
The remaining cases, for zero, successor, case, and fixpoint, The remaining cases are similar, using induction for each subterm.
are similar. Case and fixpoint are similar to lambda abstaction, Where the construct introduces a bound variable we need to compare it
in that we need to test whether the variables are equal, applying with the substituted variable, applying the drop lemma if they are
the drop lemma in one case and the swap lemma in the other. equal and the swap lemma if they are distinct.
### Main Theorem ## Preservation
Once we have shown that substitution preserves types, showing Once we have shown that substitution preserves types, showing
that reduction preserves types is straightforward. that reduction preserves types is straightforward.
@ -800,7 +800,8 @@ Let's unpack the cases for two of the reduction rules.
from which the typing of the right-hand side follows immediately. from which the typing of the right-hand side follows immediately.
The remaining cases are similar The remaining cases are similar. Each `ξ` rule follws by induction,
and each `β` rule follows by the substitution lemma.
## Normalisation ## Normalisation