2.1 Implementation Basis🔗ℹ

The implementation follows the one described in the first edition: unification and reification are those of Chapter 9 (“Under the Hood”), and the stream operators and goal constructors are those of the appendix “Connecting the Wires”. The second edition is a different language (see Second Edition and Comparing the Editions).

The differences from the first edition are:

• Stream representation. The book represents “exactly one answer” by the answer itself and “an answer followed by more” by a pair whose cdr is a procedure. That union cannot be discriminated by occurrence typing for an arbitrary answer type, so here a single answer is wrapped in an immutable box and the empty stream is '(). See Streamof.

• Occurs check. The book’s ext-s never checks for circularity; a separate checked variant is introduced in Chapter 9. Here ext-s always performs the occurs check (skipping it when the value contains no variables), so == is the checked unification and there is no separate checked variant.

• Spelling. succeed and fail stand for the book’s #s and #u; λG and λF are typed versions of the book’s goal and thunk lambdas. Superscripts become suffixes: conde, condi, alli, ife, and so on.

• Omissions. The helper forms that the book introduces in passing to explain a point (such as the bounded lambda of Chapter 5 and project of Chapter 9) are not part of the library.

Throughout this section, “Chapter n” refers to the first edition.

2.2 Types🔗ℹ

(∪ Null

(Boxof a)

(Pair a (→ (Streamof a))))

A stream is empty, contains exactly one answer, or contains one answer followed by a suspended computation (a thunk) that produces the rest. The middle case is the book’s unit; the last is its choice.

2.3 Running Programs🔗ℹ

Unassociated variables in an answer are reified as the symbols '.0, '.1, and so on, in order of first appearance.

2.4 Goals🔗ℹ

all explores the answers of the first goal one at a time: for the first answer it exhausts the rest of the conjunction before moving to the second answer. alli (“all, interleaved”) alternates between the answers produced for different answers of the earlier goals, so a later answer of the first goal is reached even when an earlier one leads to infinitely many results. (all, Chapter 6; alli, Chapter 6.)

In the examples below, the first goal chooses 'L or 'R, and counto then relates n to a list of 'Is of any length. The first choice already has infinitely many answers, so all never reaches 'R; alli alternates between the two choices.

conde is depth-first: it produces all the answers of the first clause before any answer of the second, so a clause with infinitely many answers hides every clause after it. condi (“cond, interleaved”) alternates between the clauses. (conde, Chapter 1; condi, Chapter 6.)

In conda (“soft cut”), every answer of the chosen test is passed to the rest of its clause. In condu (“committed choice”), only the first answer of the test is kept. Neither form is relational in general: the result can depend on how much is already known about the variables. (Chapter 10.)

2.5 Substitutions and Unification🔗ℹ

These are the operations of Chapter 9.

2.6 Streams🔗ℹ

These are the operators of the appendix “Connecting the Wires”. They are exported so that goals can be written and examined at the level of streams.