1. Checklets: Result Checkers in A$\lambda$goVista

The A$\lambda$goVista database consists of a collection of result checkers which we call checklets. A checklet typically takes a user query input $\Rightarrow$output as input and either accepts or rejects. If the checklet accepts a query, it also returns a description of the problem it checks for.

     

Figure 2 shows some simple checklets. Simplest of all is the integer addition checklet intAdd of Figure 2 (a). Given the query $\ulcorner\hspace*{-2pt}$ $(15,6)\Rightarrow21$ $\hspace*{-2pt}\urcorner$ the checklet would accept and return the result ``http://www.cs.arizona.edu/~collberg/IntAdd.html.'' Figures 2 (b) and (c) show a straightforward (slow) and a more complex (faster) implementation of a sorting checklet.

Figure 2 (d), finally, shows a particularly interesting checklet for topological sorting. Any acyclic graph will typically have more than one topological order. It is therefore not possible for the checklet to simply run a topological sorting procedure on the input graph and compare the resulting list of nodes with the output list given in the query. Rather, the checklet must, as shown in Figure 2 (d), first check that every node in the input graph occurs in the output node list, and then check that if node f comes before node t in the output list then there is no path $t\leadsto f$ in the input graph.

In some cases it may be difficult to construct checklets which run in an acceptable length of time. This is particularly true of NP-hard problems for which it would seem to be impossible to find polynomial time result checking algorithms. In these cases we may have to use spot-checking [10], a recent development in result checking, to check hard problems probabilistically.

Writing checklets for floating point problems can also be challenging. For example, which, if any, of the queries $\ulcorner\hspace*{-2pt}$ $2.0\Rightarrow1.4142135623$ $\hspace*{-2pt}\urcorner$, $\ulcorner\hspace*{-2pt}$ $2.00000\Rightarrow1.4140$ $\hspace*{-2pt}\urcorner$, and $\ulcorner\hspace*{-2pt}$ $2.0\Rightarrow1.0$ $\hspace*{-2pt}\urcorner$ should a floating-point square root checklet accept? In all cases, the right hand side is an approximation of $\sqrt{2}$, but just how accurate should the approximation be in order to be acceptable to the checklet? In our current implementation, floating-point comparisons are done in the minimum precision of any floating-point number in the input query. Hence, $\ulcorner\hspace*{-2pt}$ $2.0\Rightarrow1.4142135623$ $\hspace*{-2pt}\urcorner$ will accept (since $1.4142135623^2=1.9999999997\approx2.0$ when comparing with a precision of one decimal digit), but $\ulcorner\hspace*{-2pt}$ $2.00000\Rightarrow1.4140$ $\hspace*{-2pt}\urcorner$will not (since $1.4140^2=1.999396\not\approx2.0000$ when comparing with four digits' precision).