In this section, we extend the JavaScript evaluator to support a programming paradigm called nondeterministic computing by building into the evaluator a facility to support automatic search. This is a much more profound change to the language than the introduction of lazy evaluation in section 4.2.
Nondeterministic computing, like stream processing, is useful for
generate and test
applications. Consider the task of
starting with two lists of positive integers and finding a pair of
integers—one from the first list and one from the second
list—whose sum is prime. We saw how to handle this with finite
sequence operations in section 2.2.3 and
with infinite streams in section 3.5.3.
Our approach was to generate the sequence of all possible pairs and filter
these to select the pairs whose sum is prime. Whether we actually generate
the entire sequence of pairs first as in chapter 2, or interleave the
generating and filtering as in chapter 3, is immaterial to the
essential image of how the computation is organized.
The nondeterministic approach evokes a different image. Imagine simply that we choose (in some way) a number from the first list and a number from the second list and require (using some mechanism) that their sum be prime. This is expressed by the following function:
function prime_sum_pair(list1, list2) {
const a = an_element_of(list1);
const b = an_element_of(list2);
require(is_prime(a + b));
return list(a, b);
}
The key idea here is that components in a nondeterministic language can have more than one possible value. For instance, an_element_of might return any element of the given list. Our nondeterministic program evaluator will work by automatically choosing a possible value and keeping track of the choice. If a subsequent requirement is not met, the evaluator will try a different choice, and it will keep trying new choices until the evaluation succeeds, or until we run out of choices. Just as the lazy evaluator freed the programmer from the details of how values are delayed and forced, the nondeterministic program evaluator will free the programmer from the details of how choices are made.
It is instructive to contrast the different images of time evoked by nondeterministic evaluation and stream processing. Stream processing uses lazy evaluation to decouple the time when the stream of possible answers is assembled from the time when the actual stream elements are produced. The evaluator supports the illusion that all the possible answers are laid out before us in a timeless sequence. With nondeterministic evaluation, a component represents the exploration of a set of possible worlds, each determined by a set of choices. Some of the possible worlds lead to dead ends, while others have useful values. The nondeterministic program evaluator supports the illusion that time branches, and that our programs have different possible execution histories. When we reach a dead end, we can revisit a previous choice point and proceed along a different branch.
The nondeterministic program evaluator implemented below is called the amb evaluator because it is based on a new syntactic form called amb. We can type the above declaration of prime_sum_pair at the amb evaluator driver loop (along with declarations of is_prime, an_element_of, and require) and run the function as follows:
amb-evaluate input:
prime_sum_pair(list(1, 3, 5, 8), list(20, 35, 110));
Starting a new problem amb-evaluate value: [3, [20, null]]
Section 4.3.1 introduces amb and explains how it supports nondeterminism through the evaluator's automatic search mechanism. Section 4.3.2 presents examples of nondeterministic programs, and section 4.3.3 gives the details of how to implement the amb evaluator by modifying the ordinary JavaScript evaluator.
pseudo-JavaScriptattempt to define the square-root function, which we described at the beginning of section 1.1.7. In fact, a square-root function along those lines can actually be formulated as a nondeterministic program. By incorporating a search mechanism into the evaluator, we are eroding the distinction between purely declarative descriptions and imperative specifications of how to compute answers. We'll go even farther in this direction in section 4.4.