--- a/doc-src/Nitpick/nitpick.tex Wed Jan 04 00:32:02 2012 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Jan 04 10:47:07 2012 +0100
@@ -998,9 +998,6 @@
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
-Limit reached: arity 11 of Kodkod relation associated with
-``\textit{Set.insert\/}'' too large for universe of cardinality 9. Skipping scope.
-\\[2\smallskipamount]
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak
depth}~= 1:
@@ -1020,11 +1017,15 @@
the segment leading to the binder is the stem.
A salient property of coinductive datatypes is that two objects are considered
-equal if and only if they lead to the same observations. For example, the lazy
-lists $\textrm{THE}~\omega.\; \omega =
-\textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
-$\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
-\textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
+equal if and only if they lead to the same observations. For example, the two
+lazy lists
+%
+\begin{gather*}
+\textrm{THE}~\omega.\; \omega = \textit{LCons}~a~(\textit{LCons}~b~\omega) \\
+\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = \textit{LCons}~b~(\textit{LCons}~a~\omega))
+\end{gather*}
+%
+are identical, because both lead
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
concept of equality for coinductive datatypes is called bisimulation and is
@@ -1037,9 +1038,7 @@
bisimilarity check is then performed \textsl{after} the counterexample has been
found to ensure correctness. If this after-the-fact check fails, the
counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
-again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
-check for the previous example saves approximately 150~milli\-seconds; the speed
-gains can be more significant for larger scopes.
+again with \textit{bisim\_depth} set to a nonnegative integer.
The next formula illustrates the need for bisimilarity (either as a Kodkod
predicate or as an after-the-fact check) to prevent spurious counterexamples:
@@ -1067,7 +1066,8 @@
\postw
In the first \textbf{nitpick} invocation, the after-the-fact check discovered
-that the two known elements of type $'a~\textit{llist}$ are bisimilar.
+that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting
+Nitpick to label the example ``quasi genuine.''
A compromise between leaving out the bisimilarity predicate from the Kodkod
problem and performing the after-the-fact check is to specify a lower
@@ -1156,20 +1156,21 @@
2 := \textit{Var}~0, \\[-2pt]
& 3 := \textit{Var}~0,\>
4 := \textit{Var}~0,\>
- 5 := \textit{Var}~0)\end{aligned}$ \\
+ 5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
-Total time: 3.56 s.
+Total time: 3.08 s.
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
-$\lambda$-term notation, $t$~is
-$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
+$\lambda$-calculus notation, $t$ is
+$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is (wrongly) $\lambda x\, y.\> y$.
The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
replaced with $\textit{lift}~(\sigma~m)~0$.
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
-cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$.
+cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$
+of the higher-order argument $\sigma$ of \textit{subst}.
For the formula of interest, knowing 6 values of that type was enough to find
the counterexample. Without boxing, $6^6 = 46\,656$ values must be
considered, a hopeless undertaking:
@@ -1291,7 +1292,7 @@
\textit{rat}, and \textit{real}. Thus, given the
cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
-consider only 10~scopes instead of $10\,000$. On the other hand,
+consider only 10~scopes instead of $10^4 = 10\,000$. On the other hand,
\textbf{typedef}s and quotient types are generally nonmonotonic.
\subsection{Inductive Properties}
@@ -1434,7 +1435,10 @@
\hbox{}\qquad\qquad $t = \xi_1$ \\
\hbox{}\qquad\qquad $u = \xi_2$ \\
\hbox{}\qquad Datatype: \nopagebreak \\
-\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
+\hbox{}\qquad\qquad $'a~\textit{bin\_tree} =
+\{\!\begin{aligned}[t]
+& \xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \\[-2pt]
+& \textit{Branch}~\xi_1~\xi_2,\> \unr\}\end{aligned}$ \\
\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
\hbox{}\qquad\qquad $\textit{labels} = \unkef
(\!\begin{aligned}[t]%