3 Second Edition

9.3

Racket

3 Second Edition🔗ℹ

This module implements the language of the second edition of The Reasoned Schemer (Friedman, Byrd, Kiselyov, and Hemann, MIT Press, 2018) on top of amb, without streams.

3.1 Implementation Basis🔗ℹ

The interface (run, defrel, fresh, conde, conda, condu, project) and the definitions of walk, unify, ifte, once, and reification follow the official code of the second edition. What changes is the representation of goals:

	second edition	typed/miniKanren/amb/trs2
goal	(→ Substitution (Streamof Substitution))	(→ Substitution Substitution)
disj2	append-inf	a choice made by amb
conj2	append-map-inf	function composition
suspension	an immature stream, (λ () ...)	suspend: a choice point sent to the back of the frontier

The second edition can switch away from a branch that never produces an answer, because defrel suspends every call to a relation and append-inf swaps its two streams at each suspension. Here, defrel calls suspend, which lets the computations already waiting in amb’s frontier run first:

Examples:

> (defrel (nevero) (nevero))
> (run 1 q (conde [(nevero)] [succeed]))
- : (Listof Term)
'(_0)

3.1.1 Order of Answers🔗ℹ

The two implementations produce the same answers but schedule suspended computations differently. append-inf swaps a suspended stream only with the other side of the disjunction it belongs to, so the search is a tree of binary interleavings in which deeper disjunctions receive exponentially smaller shares. suspend sends the computation to the back of a single, global frontier, which is closer to breadth-first search.

As a result, answers can come in a different order from the book, and the first n answers returned by run can differ even when all answers eventually appear. Of the 285 examples of chapters 1 to 9 of the book, 15 differ in this way: 9 return the same answers in a different order, and 6 return different answers for a bounded run; the book’s answers do appear when more answers are requested. The global frontier also keeps more partial computations alive, so programs that search deeply, such as the arithmetic relations of chapter 8, are noticeably slower than with streams.

3.2 Types🔗ℹ

type
Term

The type of terms: booleans, numbers, characters, byte strings, strings, keywords, symbols, '(), logic variables (Var), and pairs of terms.

type
Var
struct
(struct var (name)
#:transparent)
name : Symbol

Logic variables, compared by identity.

type
Substitution

Defined as (Immutable-HashTable Var Term), with eq?-based keys.

type
Goal

Defined as (→ Substitution Substitution). A goal returns one extension of the substitution, chosen with amb, and calls (amb) when it has none.

3.3 Running Programs🔗ℹ

syntax
(run n q goal ...)
(run n (x ...+) goal ...)

n : (Option Natural)

Runs the conjunction of the goals and returns at most n reified answers, or all of them when n is #f. In the second form, each answer is the list of the values of the xs. (Chapter 1.)

Example:

> (run* (x y) (conde [(== x 'a)] [(== x 'b)]) (== y x))
- : (Listof Term)
'((a a) (b b))

syntax
(run* q goal ...)

Like run with n equal to #f.

3.4 Goals and Relations🔗ℹ

value
succeed : Goal
value
fail : Goal
procedure
(== u v) → Goal
u : Term
v : Term

Success, failure, and unification with the occurs check. (Chapter 1.)

syntax
(defrel (name arg ...) goal ...)

arg = x
| [x : type]

Defines name as a relation whose result is a Goal that calls suspend before running the conjunction of the goals. A plain argument x has type Term; an argument written as [x : type] has the given type. (Chapter 1.)

procedure
(suspend) → Void

Gives up control: the rest of the current computation continues after the computations already waiting in amb’s frontier. It is implemented with two choice points of one alternative each: the first is created with current-amb-depth-first? set to #f, so that the second one, which holds the rest of the computation, is placed at the back of the frontier.

syntax
(fresh (x ...) goal ...)
syntax
(conde [goal ...+] ...)
syntax
(conda [goal ...+] ...+)
syntax
(condu [goal ...+] ...+)
syntax
(project (x ...) goal ...)

As in the second edition. conde is the disjunction of the conjunctions of its lines; conda and condu commit to the first line whose first goal succeeds, keeping all of its answers or only the first. (fresh and conde, Chapter 1; conda and condu, Chapter 9; project, Chapter 10.)

syntax
(disj goal ...)
syntax
(conj goal ...)
procedure
(disj2 g1 g2) → Goal
  g1 : Goal
  g2 : Goal
procedure
(conj2 g1 g2) → Goal
  g1 : Goal
  g2 : Goal

Disjunction and conjunction. disj2 applies the goal chosen by (amb g1 g2), and conj2 is function composition.

procedure
(ifte g1 g2 g3) → Goal
  g1 : Goal
  g2 : Goal
  g3 : Goal
procedure
(once g) → Goal
  g : Goal

The functions behind conda and condu. They search for the answers of g1 or g with in-amb/do, so that they can tell whether there is one before committing.

procedure
(call/fresh name f) → Goal
  name : Symbol
  f : (→ Var Goal)
procedure
(run-goal n g) → (Listof Substitution)
  n : (Option Natural)
  g : Goal

The functions behind fresh and run.

3.5 Substitutions and Unification🔗ℹ

value
empty-s : Substitution
procedure
(walk v s) → Term
  v : Term
  s : Substitution
procedure
(walk* v s) → Term
  v : Term
  s : Substitution
procedure
(occurs? x v s) → Boolean
  x : Var
  v : Term
  s : Substitution
procedure
(ext-s x v s) → Substitution
  x : Var
  v : Term
  s : Substitution
procedure
(unify u v s) → Substitution
  u : Term
  v : Term
  s : Substitution

As in the second edition, except that ext-s and unify call (amb) instead of returning #f.

procedure
(reify-name n) → Symbol
  n : Index
procedure
(reify-s v r) → Substitution
  v : Term
  r : Substitution
procedure
(reify v) → (→ Substitution Term)
  v : Term

Reification, with the names '0, '1, and so on.

3.1	Implementation Basis
3.2	Types
3.3	Running Programs
3.4	Goals and Relations
3.5	Substitutions and Unification