pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for tomorrow's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-02-06 12:35:54 -05:00
parent f428750fdf
commit bec1b1b919
2 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Interpreters.v
View file

@ -220,7 +220,7 @@ Proof.
* an induction hypothesis. Let's ask Coq to search its library for lemmas * an induction hypothesis. Let's ask Coq to search its library for lemmas
* that would justify such a rewrite, giving a pattern with wildcards, to * that would justify such a rewrite, giving a pattern with wildcards, to
* specify the essential structure that the rewrite should match. *) * specify the essential structure that the rewrite should match. *)
SearchRewrite ((_ ++ _) ++ _). Search ((_ ++ _) ++ _).
(* Ah, we see just the one! *) (* Ah, we see just the one! *)
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
rewrite IHe1. rewrite IHe1.
@ -251,8 +251,8 @@ Proof.
(* To match the form of our lemma, we need to replace [compile e] with (* To match the form of our lemma, we need to replace [compile e] with
* [compile e ++ nil], adding a "pointless" concatenation of the empty list. * [compile e ++ nil], adding a "pointless" concatenation of the empty list.
* [SearchRewrite] again helps us find a library lemma. *) * [Search] again helps us find a library lemma. *)
SearchRewrite (_ ++ nil). Search (_ ++ nil).
rewrite (app_nil_end (compile e)). rewrite (app_nil_end (compile e)).
(* Note that we can use [rewrite] with explicit values of the first few (* Note that we can use [rewrite] with explicit values of the first few
* quantified variables of a lemma. Otherwise, [rewrite] picks an * quantified variables of a lemma. Otherwise, [rewrite] picks an

10
frap_book.tex
View file

@ -711,7 +711,6 @@ We apply the following notations throughout the book: \\
As the name advertises, finite maps are functions with finite domains, where the domain may be expanded by each extension operation. As the name advertises, finite maps are functions with finite domains, where the domain may be expanded by each extension operation.
Two axioms explain the essential interactions of the basic operators. Two axioms explain the essential interactions of the basic operators.
$$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{} $$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
\quad \quad
\infer{\msel{\mupd{m}{k_1}{v}}{k_2} = m(k_2)}{ \infer{\msel{\mupd{m}{k_1}{v}}{k_2} = m(k_2)}{
@ -723,7 +722,7 @@ $$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
With these operators in hand, we can write a semantics for arithmetic expressions. With these operators in hand, we can write a semantics for arithmetic expressions.
This is a recursive function that \emph{maps variable valuations to numbers}. This is a recursive function that \emph{maps variable valuations to numbers}.
We write $\denote{e}$ for the meaning of $e$; this notation is often referred to as \emph{Oxford brackets}\index{Oxford brackets}. We write $\denote{e}$ for the meaning of $e$; this notation is often referred to as \emph{Oxford brackets}\index{Oxford brackets}.
Recall that we allow notations like this as syntactic sugar for arbitrary functions, even when giving the equations that define those functions. Recall that we allow this kind of notation as syntactic sugar for arbitrary functions, even when giving the equations that define those functions.
We write $v$ for a valuation (finite map). We write $v$ for a valuation (finite map).
\encoding \encoding
\begin{eqnarray*} \begin{eqnarray*}
@ -758,7 +757,6 @@ We can prove a key compatibility property of these two recursive functions.
That is, in some sense, the operations of interpretation and substitution \emph{commute} with each other. That is, in some sense, the operations of interpretation and substitution \emph{commute} with each other.
That intuition gives rise to the common notion of a \emph{commuting diagram}\index{commuting diagram}, like the one below for this particular example. That intuition gives rise to the common notion of a \emph{commuting diagram}\index{commuting diagram}, like the one below for this particular example.
\[ \[
\begin{tikzcd} \begin{tikzcd}
(e, v) \arrow{r}{\subst{\ldots}{x}{e'}} \arrow{d}{\mupd{\ldots}{x}{\denote{e'}v}} & (\subst{e}{x}{e'}, v) \arrow{d}{\denote{\ldots}} \\ (e, v) \arrow{r}{\subst{\ldots}{x}{e'}} \arrow{d}{\mupd{\ldots}{x}{\denote{e'}v}} & (\subst{e}{x}{e'}, v) \arrow{d}{\denote{\ldots}} \\
@ -916,7 +914,7 @@ We'll write $\opt{\ldots}$ for this and other optimizations, which move neither
Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches. Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.
Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics preserving}\index{semantics preservation}. Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics-preserving}\index{semantics preservation}.
\begin{theorem}\label{unroll} \begin{theorem}\label{unroll}
$\denote{\opt{c}}v = \denote{c}v$. $\denote{\opt{c}}v = \denote{c}v$.
@ -925,7 +923,6 @@ Let's prove that this optimization preserves program behavior; that is, we prove
It all looks so straightforward from that statement, doesn't it? It all looks so straightforward from that statement, doesn't it?
Indeed, there actually isn't so much work to do to prove this theorem. Indeed, there actually isn't so much work to do to prove this theorem.
We can also present it as a commuting diagram much like the prior one. We can also present it as a commuting diagram much like the prior one.
\[ \[
\begin{tikzcd} \begin{tikzcd}
c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denote{\ldots}} \\ c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denote{\ldots}} \\
@ -933,14 +930,13 @@ c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denot
\end{tikzcd} \end{tikzcd}
\] \]
The statement of Theorem \ref{unroll} happens to already be in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics. The statement of Theorem \ref{unroll} happens to be already in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
\begin{lemma} \begin{lemma}
$\denote{^nc} = \denote{c}^n$. $\denote{^nc} = \denote{c}^n$.
\end{lemma} \end{lemma}
Let us end the chapter with the commuting-diagram version of the lemma statement. Let us end the chapter with the commuting-diagram version of the lemma statement.
\[ \[
\begin{tikzcd} \begin{tikzcd}
c \arrow{r}{^n\ldots} \arrow{d}{\denote{\ldots}} & ^nc \arrow{d}{\denote{\ldots}} \\ c \arrow{r}{^n\ldots} \arrow{d}{\denote{\ldots}} & ^nc \arrow{d}{\denote{\ldots}} \\