pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for tomorrow's lecture

Browse source
This commit is contained in:
Adam Chlipala 2021-04-04 14:28:23 -04:00
parent 1664ddb531
commit d177e9fb6f
2 changed files with 26 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
TypesAndMutation.v
View file

@ -205,7 +205,7 @@ Module References.
-> heapty ht h. -> heapty ht h.
Hint Constructors value plug step0 step hasty heapty : core. Global Hint Constructors value plug step0 step hasty heapty : core.
(* Perhaps surprisingly, this language admits well-typed, nonterminating (* Perhaps surprisingly, this language admits well-typed, nonterminating
@ -222,7 +222,7 @@ Module References.
repeat (econstructor; simplify). repeat (econstructor; simplify).
Qed. Qed.
Hint Resolve lookup_add_eq : core. Global Hint Resolve lookup_add_eq : core.
Ltac loopy := propositional; subst; simplify; Ltac loopy := propositional; subst; simplify;
repeat match goal with repeat match goal with
@ -293,7 +293,7 @@ Module References.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 7. Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 7.
Hint Extern 2 (exists _ : _ * _, _) => eexists (_ $+ (_, _), _) : core. Global Hint Extern 2 (exists _ : _ * _, _) => eexists (_ $+ (_, _), _) : core.
(* Progress is quite straightforward. *) (* Progress is quite straightforward. *)
Lemma progress : forall ht h, heapty ht h Lemma progress : forall ht h, heapty ht h
@ -323,7 +323,7 @@ Module References.
cases (x ==v x'); simplify; eauto. cases (x ==v x'); simplify; eauto.
Qed. Qed.
Hint Resolve weakening_override : core. Global Hint Resolve weakening_override : core.
Lemma weakening : forall H G e t, Lemma weakening : forall H G e t,
hasty H G e t hasty H G e t
@ -333,7 +333,7 @@ Module References.
induct 1; t. induct 1; t.
Qed. Qed.
Hint Resolve weakening : core. Global Hint Resolve weakening : core.
Lemma hasty_change : forall H G e t, Lemma hasty_change : forall H G e t,
hasty H G e t hasty H G e t
@ -343,7 +343,7 @@ Module References.
t. t.
Qed. Qed.
Hint Resolve hasty_change : core. Global Hint Resolve hasty_change : core.
Lemma substitution : forall H G x t' e t e', Lemma substitution : forall H G x t' e t e',
hasty H (G $+ (x, t')) e t hasty H (G $+ (x, t')) e t
@ -353,7 +353,7 @@ Module References.
induct 1; t. induct 1; t.
Qed. Qed.
Hint Resolve substitution : core. Global Hint Resolve substitution : core.
(* A new property: expanding the heap typing preserves typing. *) (* A new property: expanding the heap typing preserves typing. *)
Lemma heap_weakening : forall H G e t, Lemma heap_weakening : forall H G e t,
@ -364,7 +364,7 @@ Module References.
induct 1; t. induct 1; t.
Qed. Qed.
Hint Resolve heap_weakening : core. Global Hint Resolve heap_weakening : core.
(* A property about extending heap typings *) (* A property about extending heap typings *)
Lemma heap_override : forall H h k t t0 l, Lemma heap_override : forall H h k t t0 l,
@ -378,7 +378,7 @@ Module References.
apply H2 in H0; t. apply H2 in H0; t.
Qed. Qed.
Hint Resolve heap_override : core. Global Hint Resolve heap_override : core.
(* A higher-level property, stated via [heapty] *) (* A higher-level property, stated via [heapty] *)
Lemma heapty_extend : forall H h l t v, Lemma heapty_extend : forall H h l t v,
@ -398,7 +398,7 @@ Module References.
linear_arithmetic. linear_arithmetic.
Qed. Qed.
Hint Resolve heapty_extend : core. Global Hint Resolve heapty_extend : core.
(* The old cases of preservation proceed as before, and we need to fiddle with (* The old cases of preservation proceed as before, and we need to fiddle with
* the heap in the new cases. Note a crucial change to the theorem statement: * the heap in the new cases. Note a crucial change to the theorem statement:
@ -444,7 +444,7 @@ Module References.
assumption. assumption.
Qed. Qed.
Hint Resolve preservation0 : core. Global Hint Resolve preservation0 : core.
(* This lemma gets more complicated, too, to accommodate heap typings. *) (* This lemma gets more complicated, too, to accommodate heap typings. *)
Lemma generalize_plug : forall H e1 C e1', Lemma generalize_plug : forall H e1 C e1',
@ -481,7 +481,7 @@ Module References.
eauto. eauto.
Qed. Qed.
Hint Resolve progress preservation : core. Global Hint Resolve progress preservation : core.
(* We'll need this fact for the base case of invariant induction. *) (* We'll need this fact for the base case of invariant induction. *)
Lemma heapty_empty : heapty $0 $0. Lemma heapty_empty : heapty $0 $0.
@ -489,7 +489,7 @@ Module References.
exists 0; t. exists 0; t.
Qed. Qed.
Hint Resolve heapty_empty : core. Global Hint Resolve heapty_empty : core.
(* Now there isn't much more to the proof of type safety. The crucial overall (* Now there isn't much more to the proof of type safety. The crucial overall
* insight is a strengthened invariant that quantifies existentially over a * insight is a strengthened invariant that quantifies existentially over a
@ -592,7 +592,7 @@ Module GarbageCollection.
-> step (h, e) (h', e). -> step (h, e) (h', e).
Hint Constructors step : core. Global Hint Constructors step : core.
Definition trsys_of (e : exp) := {| Definition trsys_of (e : exp) := {|
Initial := {($0, e)}; Initial := {($0, e)};
@ -631,10 +631,10 @@ Module GarbageCollection.
assumption. assumption.
Qed. Qed.
Hint Resolve reachableLocFromExp_trans : core. Global Hint Resolve reachableLocFromExp_trans : core.
Hint Extern 1 (_ \in _) => simplify; solve [ sets ] : core. Global Hint Extern 1 (_ \in _) => simplify; solve [ sets ] : core.
Hint Extern 1 (_ \subseteq _) => simplify; solve [ sets ] : core. Global Hint Extern 1 (_ \subseteq _) => simplify; solve [ sets ] : core.
Hint Constructors reachableLoc reachableLocFromExp : core. Global Hint Constructors reachableLoc reachableLocFromExp : core.
(* Typing is preserved by moving to a heap typing that only needs to preserve (* Typing is preserved by moving to a heap typing that only needs to preserve
* the mappings for *reachable* locations. *) * the mappings for *reachable* locations. *)
@ -730,7 +730,7 @@ Module GarbageCollection.
equality. equality.
Qed. Qed.
Hint Resolve progress preservation : core. Global Hint Resolve progress preservation : core.
(* The safety proof itself is anticlimactic, looking the same as before. *) (* The safety proof itself is anticlimactic, looking the same as before. *)
Theorem safety : forall e t, hasty $0 $0 e t Theorem safety : forall e t, hasty $0 $0 e t

14
frap_book.tex
View file

@ -3431,7 +3431,7 @@ Though we added a new kind of side effect, we did not need to modify a single ru
The open-ended abstraction of evaluation contexts helped us plan ahead for side effects without foreseeing them precisely. The open-ended abstraction of evaluation contexts helped us plan ahead for side effects without foreseeing them precisely.
For instance, it was critical that we could refer to a restricted context $C^-$ to consider exception bubbling past \emph{any} of the prior features for which we defined order-of-evaluation rules. For instance, it was critical that we could refer to a restricted context $C^-$ to consider exception bubbling past \emph{any} of the prior features for which we defined order-of-evaluation rules.
\section{Mutable Variables} \section{Mutable Variables\label{mutable_variables}}
Let's now consider another side effect and how we can add it without having to modify existing rules. Let's now consider another side effect and how we can add it without having to modify existing rules.
This one we will build on the lambda calculus with products and sums, not trying to harmonize it with exceptions. This one we will build on the lambda calculus with products and sums, not trying to harmonize it with exceptions.
@ -3535,8 +3535,8 @@ That's a pretty strong demonstration of modularity in semantics.
\chapter{Types and Mutation} \chapter{Types and Mutation}
The syntactic approach to type soundness continues to apply to \emph{impure} functional languages, which combine imperative side effects with first-class functions. As we glimpsed last chapter, the syntactic approach to type soundness continues to apply to \emph{impure} functional languages, which combine imperative side effects with first-class functions.
We'll study the general domain through its most common exemplar: $\lambda$-calculus with \emph{mutable references}\index{mutable references}\index{references}. We'll study the general domain through its most common exemplar: $\lambda$-calculus with \emph{mutable references}\index{mutable references}\index{references}, which generalize the mutable variables that we modeled in Section \ref{mutable_variables}.
\section{Simply Typed Lambda Calculus with Mutable References} \section{Simply Typed Lambda Calculus with Mutable References}
@ -3544,7 +3544,7 @@ We'll study the general domain through its most common exemplar: $\lambda$-calcu
\newcommand{\readref}[1]{!#1} \newcommand{\readref}[1]{!#1}
\newcommand{\writeref}[2]{#1 := #2} \newcommand{\writeref}[2]{#1 := #2}
Here is an extension of the lambda-calculus syntax from last chapter, with additions underlined. Here is an extension of the lambda-calculus syntax from Chapter \ref{types}, with additions underlined.
$$\begin{array}{rrcl} $$\begin{array}{rrcl}
\textrm{Variables} & x &\in& \mathsf{Strings} \\ \textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Numbers} & n &\in& \mathbb N \\ \textrm{Numbers} & n &\in& \mathbb N \\
@ -3567,7 +3567,7 @@ $$\elet{r}{\newref{0}}{\writeref{r}{\; \readref{r} + 1}; \readref{r}}$$
This program (1) allocates a new reference $r$ storing the value 0; (2) increments $r$'s value by 1; and (3) returns the new $r$ value, which is 1. This program (1) allocates a new reference $r$ storing the value 0; (2) increments $r$'s value by 1; and (3) returns the new $r$ value, which is 1.
To be more formal about the meanings of all programs, we extend the operational semantics from last chapter. To be more formal about the meanings of all programs, we extend the operational semantics from the start of last chapter.
First, we add some new kinds of evaluation contexts. First, we add some new kinds of evaluation contexts.
$$\begin{array}{rrcl} $$\begin{array}{rrcl}
\textrm{Evaluation contexts} & C &::=& \Box \mid C \; e \mid v \; C \mid C + e \mid v + C \\ \textrm{Evaluation contexts} & C &::=& \Box \mid C \; e \mid v \; C \mid C + e \mid v + C \\
@ -3575,7 +3575,7 @@ $$\begin{array}{rrcl}
\end{array}$$ \end{array}$$
Next we define the basic reduction steps of the language. Next we define the basic reduction steps of the language.
In contrast to last chapter's semantics for pure $\lambda$-calculus, here we work with states that include not just expressions but also \emph{heaps}\index{heaps} $h$, partial functions from references to their current stored values. Similarly to in Section \ref{mutable_variables}, we work with states that include not just expressions but also \emph{heaps}\index{heaps} $h$, partial functions from references to their current stored values.
We begin by copying over the two basic-step rules from last chapter, threading through the heap $h$ unchanged. We begin by copying over the two basic-step rules from last chapter, threading through the heap $h$ unchanged.
$$\infer{\smallstepo{(h, (\lambda x. \; e) \; v)}{(h, \subst{e}{x}{v})}}{} $$\infer{\smallstepo{(h, (\lambda x. \; e) \; v)}{(h, \subst{e}{x}{v})}}{}
\quad \infer{\smallstepo{(h, n + m)}{(h, n \textbf{+} m)}}{}$$ \quad \infer{\smallstepo{(h, n + m)}{(h, n \textbf{+} m)}}{}$$
@ -3779,7 +3779,7 @@ The final premise says that we have actually done some useful work: the new heap
It may not be clear why we must include the last premise. It may not be clear why we must include the last premise.
The reason has to do with our formulation of type safety, by saying that programs never get \emph{stuck}. The reason has to do with our formulation of type safety, by saying that programs never get \emph{stuck}.
We defined that $e$ is \emph{stuck} if it is not a value, but it also can't take a step. We defined that $e$ is \emph{stuck} if it is not a value but it also can't take a step.
If we omitted from the garbage-collection rule the premise $h' \neq h$, then this rule would \emph{always} apply, for any term, simply by setting $h' = h$. If we omitted from the garbage-collection rule the premise $h' \neq h$, then this rule would \emph{always} apply, for any term, simply by setting $h' = h$.
That is, \emph{no} term would ever be stuck, and type safety would be meaningless! That is, \emph{no} term would ever be stuck, and type safety would be meaningless!
Since the rule also requires that $h'$ be \emph{no larger than} $h$ (with the second premise), additionally requiring $h' \neq h$ forces $h'$ to \emph{shrink}, garbage-collecting at least one location. Since the rule also requires that $h'$ be \emph{no larger than} $h$ (with the second premise), additionally requiring $h' \neq h$ forces $h'$ to \emph{shrink}, garbage-collecting at least one location.