996 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1, |
996 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1, |
997 and \textit{bisim\_depth}~= 0. \\ |
997 and \textit{bisim\_depth}~= 0. \\ |
998 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] |
998 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] |
999 \hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10, |
999 \hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10, |
1000 and \textit{bisim\_depth}~= 9. \\[2\smallskipamount] |
1000 and \textit{bisim\_depth}~= 9. \\[2\smallskipamount] |
1001 Limit reached: arity 11 of Kodkod relation associated with |
|
1002 ``\textit{Set.insert\/}'' too large for universe of cardinality 9. Skipping scope. |
|
1003 \\[2\smallskipamount] |
|
1004 Nitpick found a counterexample for {\itshape card}~$'a$ = 2, |
1001 Nitpick found a counterexample for {\itshape card}~$'a$ = 2, |
1005 \textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak |
1002 \textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak |
1006 depth}~= 1: |
1003 depth}~= 1: |
1007 \\[2\smallskipamount] |
1004 \\[2\smallskipamount] |
1008 \hbox{}\qquad Free variables: \nopagebreak \\ |
1005 \hbox{}\qquad Free variables: \nopagebreak \\ |
1018 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment |
1015 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment |
1019 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas |
1016 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas |
1020 the segment leading to the binder is the stem. |
1017 the segment leading to the binder is the stem. |
1021 |
1018 |
1022 A salient property of coinductive datatypes is that two objects are considered |
1019 A salient property of coinductive datatypes is that two objects are considered |
1023 equal if and only if they lead to the same observations. For example, the lazy |
1020 equal if and only if they lead to the same observations. For example, the two |
1024 lists $\textrm{THE}~\omega.\; \omega = |
1021 lazy lists |
1025 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and |
1022 % |
1026 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = |
1023 \begin{gather*} |
1027 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead |
1024 \textrm{THE}~\omega.\; \omega = \textit{LCons}~a~(\textit{LCons}~b~\omega) \\ |
|
1025 \textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = \textit{LCons}~b~(\textit{LCons}~a~\omega)) |
|
1026 \end{gather*} |
|
1027 % |
|
1028 are identical, because both lead |
1028 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or, |
1029 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or, |
1029 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This |
1030 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This |
1030 concept of equality for coinductive datatypes is called bisimulation and is |
1031 concept of equality for coinductive datatypes is called bisimulation and is |
1031 defined coinductively. |
1032 defined coinductively. |
1032 |
1033 |
1035 observations. This precaution is somewhat expensive and often unnecessary, so it |
1036 observations. This precaution is somewhat expensive and often unnecessary, so it |
1036 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The |
1037 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The |
1037 bisimilarity check is then performed \textsl{after} the counterexample has been |
1038 bisimilarity check is then performed \textsl{after} the counterexample has been |
1038 found to ensure correctness. If this after-the-fact check fails, the |
1039 found to ensure correctness. If this after-the-fact check fails, the |
1039 counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try |
1040 counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try |
1040 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the |
1041 again with \textit{bisim\_depth} set to a nonnegative integer. |
1041 check for the previous example saves approximately 150~milli\-seconds; the speed |
|
1042 gains can be more significant for larger scopes. |
|
1043 |
1042 |
1044 The next formula illustrates the need for bisimilarity (either as a Kodkod |
1043 The next formula illustrates the need for bisimilarity (either as a Kodkod |
1045 predicate or as an after-the-fact check) to prevent spurious counterexamples: |
1044 predicate or as an after-the-fact check) to prevent spurious counterexamples: |
1046 |
1045 |
1047 \prew |
1046 \prew |
1065 {\upshape\textbf{nitpick}} \\[2\smallskipamount] |
1064 {\upshape\textbf{nitpick}} \\[2\smallskipamount] |
1066 \slshape Nitpick found no counterexample. |
1065 \slshape Nitpick found no counterexample. |
1067 \postw |
1066 \postw |
1068 |
1067 |
1069 In the first \textbf{nitpick} invocation, the after-the-fact check discovered |
1068 In the first \textbf{nitpick} invocation, the after-the-fact check discovered |
1070 that the two known elements of type $'a~\textit{llist}$ are bisimilar. |
1069 that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting |
|
1070 Nitpick to label the example ``quasi genuine.'' |
1071 |
1071 |
1072 A compromise between leaving out the bisimilarity predicate from the Kodkod |
1072 A compromise between leaving out the bisimilarity predicate from the Kodkod |
1073 problem and performing the after-the-fact check is to specify a lower |
1073 problem and performing the after-the-fact check is to specify a lower |
1074 nonnegative \textit{bisim\_depth} value than the default one provided by |
1074 nonnegative \textit{bisim\_depth} value than the default one provided by |
1075 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to |
1075 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to |
1154 & 0 := \textit{Var}~0,\> |
1154 & 0 := \textit{Var}~0,\> |
1155 1 := \textit{Var}~0,\> |
1155 1 := \textit{Var}~0,\> |
1156 2 := \textit{Var}~0, \\[-2pt] |
1156 2 := \textit{Var}~0, \\[-2pt] |
1157 & 3 := \textit{Var}~0,\> |
1157 & 3 := \textit{Var}~0,\> |
1158 4 := \textit{Var}~0,\> |
1158 4 := \textit{Var}~0,\> |
1159 5 := \textit{Var}~0)\end{aligned}$ \\ |
1159 5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\ |
1160 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount] |
1160 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount] |
1161 Total time: 3.56 s. |
1161 Total time: 3.08 s. |
1162 \postw |
1162 \postw |
1163 |
1163 |
1164 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t = |
1164 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t = |
1165 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional |
1165 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional |
1166 $\lambda$-term notation, $t$~is |
1166 $\lambda$-calculus notation, $t$ is |
1167 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$. |
1167 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is (wrongly) $\lambda x\, y.\> y$. |
1168 The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be |
1168 The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be |
1169 replaced with $\textit{lift}~(\sigma~m)~0$. |
1169 replaced with $\textit{lift}~(\sigma~m)~0$. |
1170 |
1170 |
1171 An interesting aspect of Nitpick's verbose output is that it assigned inceasing |
1171 An interesting aspect of Nitpick's verbose output is that it assigned inceasing |
1172 cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$. |
1172 cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$ |
|
1173 of the higher-order argument $\sigma$ of \textit{subst}. |
1173 For the formula of interest, knowing 6 values of that type was enough to find |
1174 For the formula of interest, knowing 6 values of that type was enough to find |
1174 the counterexample. Without boxing, $6^6 = 46\,656$ values must be |
1175 the counterexample. Without boxing, $6^6 = 46\,656$ values must be |
1175 considered, a hopeless undertaking: |
1176 considered, a hopeless undertaking: |
1176 |
1177 |
1177 \prew |
1178 \prew |
1289 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes |
1290 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes |
1290 are normally monotonic and treated as such. The same is true for record types, |
1291 are normally monotonic and treated as such. The same is true for record types, |
1291 \textit{rat}, and \textit{real}. Thus, given the |
1292 \textit{rat}, and \textit{real}. Thus, given the |
1292 cardinality specification 1--10, a formula involving \textit{nat}, \textit{int}, |
1293 cardinality specification 1--10, a formula involving \textit{nat}, \textit{int}, |
1293 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to |
1294 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to |
1294 consider only 10~scopes instead of $10\,000$. On the other hand, |
1295 consider only 10~scopes instead of $10^4 = 10\,000$. On the other hand, |
1295 \textbf{typedef}s and quotient types are generally nonmonotonic. |
1296 \textbf{typedef}s and quotient types are generally nonmonotonic. |
1296 |
1297 |
1297 \subsection{Inductive Properties} |
1298 \subsection{Inductive Properties} |
1298 \label{inductive-properties} |
1299 \label{inductive-properties} |
1299 |
1300 |
1432 \hbox{}\qquad\qquad $a = a_1$ \\ |
1433 \hbox{}\qquad\qquad $a = a_1$ \\ |
1433 \hbox{}\qquad\qquad $b = a_2$ \\ |
1434 \hbox{}\qquad\qquad $b = a_2$ \\ |
1434 \hbox{}\qquad\qquad $t = \xi_1$ \\ |
1435 \hbox{}\qquad\qquad $t = \xi_1$ \\ |
1435 \hbox{}\qquad\qquad $u = \xi_2$ \\ |
1436 \hbox{}\qquad\qquad $u = \xi_2$ \\ |
1436 \hbox{}\qquad Datatype: \nopagebreak \\ |
1437 \hbox{}\qquad Datatype: \nopagebreak \\ |
1437 \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\}$ \\ |
1438 \hbox{}\qquad\qquad $'a~\textit{bin\_tree} = |
|
1439 \{\!\begin{aligned}[t] |
|
1440 & \xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \\[-2pt] |
|
1441 & \textit{Branch}~\xi_1~\xi_2,\> \unr\}\end{aligned}$ \\ |
1438 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\ |
1442 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\ |
1439 \hbox{}\qquad\qquad $\textit{labels} = \unkef |
1443 \hbox{}\qquad\qquad $\textit{labels} = \unkef |
1440 (\!\begin{aligned}[t]% |
1444 (\!\begin{aligned}[t]% |
1441 & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt] |
1445 & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt] |
1442 & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\ |
1446 & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\ |