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 Wednesday's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-02-20 12:29:17 -05:00
parent ddacd030e6
commit e3f0ada30e
2 changed files with 4 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
DataAbstraction.v
View file

@ -74,8 +74,8 @@ Module Algebraic.
(* Note that we use identifier [list] alone as a first-class type family, (* Note that we use identifier [list] alone as a first-class type family,
* without specifying a parameter explicitly. *) * without specifying a parameter explicitly. *)
(* We follow the convention of enqueuing onto the front of lists and (* We follow the convention of enqueuing onto the fronts of lists and
* dequeuing from the back, so the first two operations are just the first * dequeuing from the backs, so the first two operations are just the first
* two constructors of [list]. *) * two constructors of [list]. *)
Definition empty A : t A := nil. Definition empty A : t A := nil.
Definition enqueue A (q : t A) (x : A) : t A := x :: q. Definition enqueue A (q : t A) (x : A) : t A := x :: q.
@ -502,7 +502,7 @@ Module AlgebraicWithEquivalenceRelation.
| x :: dq => Some ({| EnqueueHere := q.(EnqueueHere); | x :: dq => Some ({| EnqueueHere := q.(EnqueueHere);
DequeueHere := dq |}, x) DequeueHere := dq |}, x)
| [] => | [] =>
(* Out of dequeuable elements. Reverse enqueued elements (* Ran out of dequeuable elements. Reverse enqueued elements
* and transfer to the other stack. *) * and transfer to the other stack. *)
match rev q.(EnqueueHere) with match rev q.(EnqueueHere) with
| [] => None | [] => None
@ -1166,7 +1166,7 @@ Module Type FINITE_SET.
End FINITE_SET. End FINITE_SET.
(* We want a generic implementation of finite sets, as found in the standard (* We want a generic implementation of finite sets, as found in the standard
* libaries of languages like Java. However, not just any key set will do. * libraries of languages like Java. However, not just any key set will do.
* We need enough computable operations. One sufficient operation is an * We need enough computable operations. One sufficient operation is an
* equality test. *) * equality test. *)
Module Type SET_WITH_EQUALITY. Module Type SET_WITH_EQUALITY.

6
frap_book.tex
View file

@ -483,7 +483,6 @@ So-called \emph{client code}\index{client code} that relies on queues shouldn't
We should be able to formulate ``queue'' as an \emph{abstract data type}\index{abstract data type}, hiding implementation details. We should be able to formulate ``queue'' as an \emph{abstract data type}\index{abstract data type}, hiding implementation details.
In the setting of pure functional programming, as in Coq, here is our first cut at such a data type, as a set of types and operations, somewhat reminiscent of e.g. interfaces\index{interface} in Java\index{Java}. In the setting of pure functional programming, as in Coq, here is our first cut at such a data type, as a set of types and operations, somewhat reminiscent of e.g. interfaces\index{interface} in Java\index{Java}.
Type $\mt{t}(\alpha)$ stands for queues holding data values in some type $\alpha$. Type $\mt{t}(\alpha)$ stands for queues holding data values in some type $\alpha$.
\begin{eqnarray*} \begin{eqnarray*}
\mt{t}(\alpha) &:& \mt{Set} \\ \mt{t}(\alpha) &:& \mt{Set} \\
\mt{empty} &:& \mt{t}(\alpha) \\ \mt{empty} &:& \mt{t}(\alpha) \\
@ -501,19 +500,16 @@ In normal programming, we stop at this level of detail in defining an abstract d
However, when we're after formal correctness proofs, we must enrich data types with \emph{specifications}\index{specifications} or ``specs.''\index{specs} However, when we're after formal correctness proofs, we must enrich data types with \emph{specifications}\index{specifications} or ``specs.''\index{specs}
One prominent spec style is \emph{algebraic}\index{algebraic specifications}: write out a set of \emph{laws}, quantified equalities that use the operations of the data type. One prominent spec style is \emph{algebraic}\index{algebraic specifications}: write out a set of \emph{laws}, quantified equalities that use the operations of the data type.
For queues, here are two reasonable laws. For queues, here are two reasonable laws.
$$\begin{array}{l} $$\begin{array}{l}
\mt{dequeue}(\mt{empty}) = \cdot \\ \mt{dequeue}(\mt{empty}) = \cdot \\
\forall q. \; \mt{dequeue}(q) = \cdot \Rightarrow q = \mt{empty} \\ \forall q. \; \mt{dequeue}(q) = \cdot \Rightarrow q = \mt{empty} \\
\end{array}$$ \end{array}$$
Actually, the inference-rule notation from last chapter also makes algebraic laws more readable, so here is a restatement. Actually, the inference-rule notation from last chapter also makes algebraic laws more readable, so here is a restatement.
$$\infer{\mt{dequeue}(\mt{empty}) = \cdot}{} $$\infer{\mt{dequeue}(\mt{empty}) = \cdot}{}
\quad \infer{q = \mt{empty}}{\mt{dequeue}(q) = \cdot}$$ \quad \infer{q = \mt{empty}}{\mt{dequeue}(q) = \cdot}$$
One more rule suffices to give a complete characterization of behavior, with the familiar math notation for piecewise functions\index{piecewise functions}. One more rule suffices to give a complete characterization of behavior, with the familiar math notation for piecewise functions\index{piecewise functions}.
$$\infer{\mt{dequeue}(\mt{enqueue}(q, x)) = \begin{cases} $$\infer{\mt{dequeue}(\mt{enqueue}(q, x)) = \begin{cases}
(\mt{empty}, x), & \mt{dequeue}(q) = \cdot \\ (\mt{empty}, x), & \mt{dequeue}(q) = \cdot \\
(\mt{enqueue}(q', x), y), & \mt{dequeue}(q) = (q', y) (\mt{enqueue}(q', x), y), & \mt{dequeue}(q) = (q', y)
@ -628,7 +624,6 @@ Here is how we revise our type signature for queues.
\end{eqnarray*} \end{eqnarray*}
And here are the revised axioms. And here are the revised axioms.
$$\infer{\mt{rep}(\mt{empty}) = []}{} $$\infer{\mt{rep}(\mt{empty}) = []}{}
\quad \infer{\mt{rep}(\mt{enqueue}(q, x)) = \concat{[x]}{\mt{rep}(q)}}{}$$ \quad \infer{\mt{rep}(\mt{enqueue}(q, x)) = \concat{[x]}{\mt{rep}(q)}}{}$$
@ -648,7 +643,6 @@ Here's another classic abstract data type: finite sets\index{finite sets}, where
\end{eqnarray*} \end{eqnarray*}
A few laws characterize expected behavior, with $\top$ and $\bot$ the respective elements ``true'' and ``false'' of $\mathbb B$. A few laws characterize expected behavior, with $\top$ and $\bot$ the respective elements ``true'' and ``false'' of $\mathbb B$.
$$\infer{\mt{member}(\mt{empty}, k) = \bot}{} $$\infer{\mt{member}(\mt{empty}, k) = \bot}{}
\quad \infer{\mt{member}(\mt{add}(s, k), k) = \top}{} \quad \infer{\mt{member}(\mt{add}(s, k), k) = \top}{}
\quad \infer{\mt{member}(\mt{add}(s, k_1), k_2) = \mt{member}(s, k_2)}{k_1 \neq k_2}$$ \quad \infer{\mt{member}(\mt{add}(s, k_1), k_2) = \mt{member}(s, k_2)}{k_1 \neq k_2}$$