2 First Edition

9.3

Racket

2 First Edition🔗ℹ

This module implements the language of the first edition of The Reasoned Schemer on top of amb.

2.1 Implementation Basis🔗ℹ

The core follows microKanren: a goal returns one substitution and chooses among its answers with amb. There is no state and no variable counter (variables are created directly by fresh), disj and conj take any number of goals, and substitutions are immutable hash tables instead of association lists.

The user-level language provided by typed/miniKanren/amb/trs1 is that of the first edition of The Reasoned Schemer (Friedman, Byrd, and Kiselyov, MIT Press, 2005): run with a single query variable, conde with else, the interleaving forms condi and alli, and the committed-choice forms conda and condu. “Chapter n” below refers to that edition.

The differences from the book are:

There is no stream type, and ext-s performs the occurs check, signalling failure with (amb).
conde is depth-first, as in the first edition: it corresponds to unfair amb. The interleaving forms condi and alli are implemented separately (see Interleaving) after the first edition’s mplusi and bindi, and produce answers in the same order as the book.

2.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
procedure
(var=? x y) → Boolean
  x : Var
  y : Var

Logic variables. Variables are compared by identity (var=? is eq?); the name is only for printing.

type
Substitution

Defined as (Immutable-HashTable Var Term), with eq?-based keys. As in other miniKanren implementations, the substitution is triangular: a variable may be associated with a term containing other associated variables.

type
Goal

Defined as (→ Substitution Substitution). Applying a goal to a substitution returns one extension of it under which the goal holds, chosen with amb; the other extensions are explored when the search backtracks. A goal with no answer calls (amb). Goals must therefore be applied within the dynamic extent of an amb search such as in-amb/do.

Examples:

> (define x (var 'x))
> (for/list : (Listof Term)
            ([s : Substitution
                (in-amb/do ((disj (== x 1) (== x 2)) empty-s))])
    (walk x s))
- : (Listof Term)
'(1 2)

2.3 Running Programs🔗ℹ

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

n : (Option Real)
syntax
(run* (x) goal ...)

Introduces a fresh variable x, applies the conjunction of the goals to the empty substitution inside in-amb/do, and returns a list of at most n reified values of x. When n is #f, all values are returned, and the computation diverges if there are infinitely many. The limit is checked before each new answer is requested, so run never searches for an answer it will not return. (Chapter 1.)

Example:

> (run* (q) (fresh (a b) (== q (list a b)) (== a 'left)))
- : (Listof Term)
'((left _.0))

2.4 Goals🔗ℹ

value
succeed : Goal
value
fail : Goal

succeed is the identity function; fail calls (amb). (Chapter 1.)

procedure
(== u v) → Goal
u : Term
v : Term

The goal that extends the substitution by unifying u with v, and fails if they do not unify. (Chapter 1.)

Examples:

> (run* (q) (fresh (x) (== q (cons x 2)) (== x 1)))
- : (Listof Term)
'((1 . 2))
> (run* (q) (== q (list q)))
- : (Listof Term)
'()

syntax
(fresh (x ...) goal ...)

Binds each x to a new variable and behaves as (all goal ...). The variables are created each time the goal is applied. (Chapter 1.)

syntax
(project (x ...) goal ...)

Rebinds each x to its value under the current substitution (as by walk*) and then behaves as (all goal ...). This lets the goals inspect the values with ordinary Racket code. (Chapter 9.)

Example:

> (run* (q)
    (fresh (n)
      (conde [(== n 3)] [(== n 4)])
      (project (n)
        (if (exact-integer? n) (== q (* n n)) fail))))
- : (Listof Term)
'(9 16)

procedure
(disj g ...) → Goal
g : Goal
procedure
(conj g ...) → Goal
g : Goal

N-ary disjunction and conjunction of goals. disj chooses one of the goals with amb and applies it; conj applies the goals in order, each to the result of the previous one. Both simplify trivial cases: fail is dropped from a disjunction, a conjunction containing fail is fail, and succeed is dropped from a conjunction.

These are functions, so their arguments are evaluated before the goal is built. For recursive relations, use disj+ and conj+ or the forms below.

syntax
(Zzz goal)
syntax
(λG (s) body ...+)

(Zzz goal) is the η-expansion (λG (s) (goal s)): it delays the evaluation of the expression goal until the goal is applied, which keeps recursive relations from looping while they are being built. Unlike Zzz in microKanren, it does not suspend the computation: interleaving is provided by condi and alli instead. λG is λ annotated with the type Goal.

syntax
(disj+ goal ...)
syntax
(conj+ goal ...)

disj and conj applied to (Zzz goal) ....

syntax
(all goal ...)
syntax
(alli goal ...)

Conjunction. (all) is succeed and (all goal) is (Zzz goal); otherwise all is conj+ and alli is conji+. (Chapter 6.)

syntax
(conde clause ...)

clause = [goal ...+]
| [else goal ...]
syntax
(condi clause ...)

Disjunction of clauses, each of which is a conjunction. An else clause, if present, comes last. conde tries the clauses depth-first; condi interleaves their answers. (conde, Chapter 1; condi, Chapter 6.)

Examples:

> (: repeato (→ Term Term Goal))
> (define (repeato x l)
    (conde
      [(== l '())]
      [(fresh (d) (== l (cons x d)) (repeato x d))]))
> (run 6 (q) (conde [(repeato 'a q)] [(repeato 'b q)]))
- : (Listof Term)
'(() (a) (a a) (a a a) (a a a a) (a a a a a))
> (run 6 (q) (condi [(repeato 'a q)] [(repeato 'b q)]))
- : (Listof Term)
'(() () (a) (b) (a a) (b b))

syntax
(conda clause ...)
syntax
(condu clause ...)

Committed choice: the first goal of each clause is a test, and the first clause whose test succeeds is the only one used. conda continues with every answer of the test, condu with its first answer only. (Chapter 10.)

Examples:

> (run* (q) (conda [(conde [(== q 1)] [(== q 2)])] [(== q 3)]))
- : (Listof Term)
'(1 2)
> (run* (q) (condu [(conde [(== q 1)] [(== q 2)])] [(== q 3)]))
- : (Listof Term)
'(1)

syntax
(ife g0 g1 g2)
syntax
(ifi g0 g1 g2)
syntax
(ifa g0 g1 g2)
syntax
(ifu g0 g1 g2)
syntax
(cond-aux ifer clause ...)
syntax
(all-aux conj+ goal ...)
syntax
(if-aux disj+ g0 g1 g2)

The building blocks of the forms above, following the structure of the first edition’s implementation: cond-aux turns each clause into (ifer test (all goal ...) rest), and all-aux builds a conjunction from a conjunction form. ifa and ifu obtain the answers of the test with sequence-generate over in-amb/do, so that they can tell whether it has an answer before committing.

2.4.1 Interleaving🔗ℹ

procedure
(disji g ...) → Goal
g : Goal
procedure
(conji g ...) → Goal
g : Goal
syntax
(disji+ goal ...)
syntax
(conji+ goal ...)

Interleaving disjunction and conjunction, used by condi and alli. disji collects the answers of each goal as a sequence with in-amb/do, merges the sequences round-robin with mplusi, and chooses from the merged sequence with amb. conji collects the answers of its first goal as a sequence and passes it to bindi with the conjunction of the remaining goals, so that the answers obtained from different answers of the first goal are interleaved. An answer of a later goal is therefore reached even when an earlier goal has infinitely many answers.

In the example below, counto has an answer for every length, yet the answers with 'R are reached:

Examples:

> (: counto (→ Term Goal))
> (define (counto n)
    (conde
      [(== n '())]
      [(fresh (m) (== n (cons 'I m)) (counto m))]))
> (run 6 (q)
    (fresh (n side)
      (alli (counto n) (conde [(== side 'L)] [(== side 'R)]))
      (== q (cons side n))))
- : (Listof Term)
'((L) (L I) (R) (L I I) (R I) (L I I I))

procedure
(mplusi s* ...) → (Sequenceof Substitution)
  s* : (Sequenceof Substitution)
procedure
(bindi s* g) → (Sequenceof Substitution)
  s* : (Sequenceof Substitution)
  g : Goal

Sequence-level helpers corresponding to the first edition’s mplusi and bindi. mplusi merges sequences of substitutions round-robin. bindi merges the answers of g on the first element of s* with those of bindi on the rest of s*, which is computed only when it is needed.

2.5 Substitutions and Unification🔗ℹ

value
empty-s : Substitution
procedure
(s-empty? s) → Boolean
  s : Substitution
procedure
(s-has-key? x s) → Boolean
  x : Var
  s : Substitution
procedure
(apply-s s x) → Term
  s : Substitution
  x : Var
procedure
(size-s s) → Index
  s : Substitution
procedure
(ext-s x v s) → Substitution
  x : Var
  v : Term
  s : Substitution

Operations on substitutions. ext-s associates x with v, and fails with (amb) when x occurs in v.

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
(unify u v s) → Substitution
  u : Term
  v : Term
  s : Substitution

walk follows the associations of a variable until it reaches a term that is not an associated variable; walk* does so throughout a term. unify returns an extension of s that makes u and v equal, and calls (amb) if there is none. (Chapter 9.)

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

Reification: unassociated variables are replaced by '.0, '.1, and so on, in order of first appearance. (Chapter 9.)

procedure
(apply-goal g s) → Substitution
  g : Goal
  s : Substitution
procedure
(sequence->amb s) → a
  s : (Sequenceof a)
procedure
(list->amb l) → a
  l : (Listof a)

Small helpers: apply-goal applies a goal (for use with foldl); sequence->amb and list->amb choose an element with amb.

2.6 Symbolic Aliases🔗ℹ

syntax
run∞
syntax
⊤
syntax
⊥
syntax
≡
syntax
∃
syntax
∨
syntax
∧
syntax
∨i
syntax
∧i

Aliases for run*, succeed, fail, ==, fresh, disj+, conj+, disji+, and conji+.

Example:

> (run∞ (q) (∃ (a b) (∨ (≡ a 1) (≡ a 2)) (≡ b a) (≡ q (list a b))))
- : (Listof Term)
'((1 1) (2 2))

2.1	Implementation Basis
2.2	Types
2.3	Running Programs
2.4	Goals
2.5	Substitutions and Unification
2.6	Symbolic Aliases