doc.txt

Reduction Semantics

_Reduction Semantics_
_reduction-semantics_

This collection provides three files:

  _reduction-semantics.ss_: the core reduction semantics
  library

  _gui.ss_: a _visualization tool for reduction sequences_.

  _subst.ss_: a library for _capture avoiding substitution_.

In addition, the examples subcollection contains several
small languages to demonstrate various different uses of
this tool:

  _arithmetic.ss_: an arithmetic language with every
  possible order of evaluation

  _church.ss_: church numerals with call by name
  normal order evaluation

  _combinators.ss_: fills in the gaps in a proof in
  Berendrecht that i and j (defined in the file) are
  a combinator basis

  _future.ss_: an adaptation of Cormac Flanagan's future
  semantics.

  _ho-contracts.ss_: computes the mechanical portions of a
  proof in the Contracts for Higher Order Functions paper
  (ICFP 2002). Contains a sophisticated example use of an
  alternative pretty printer.

  _macro.ss_: models macro expansion as a reduction semantics.

  _omega.ss_: the call by value lambda calculus with call/cc.
  Includes omega and two call/cc-based infinite loops, one of
  which has an ever-expanding term size and one of which has
  a bounded term size.

  _threads.ss_: shows how non-deterministic choice can be
  modeled in a reduction semantics. Contains an example use
  of a simple alternative pretty printer.

  _semaphores.ss_: a simple threaded language with semaphores


  iswim.ss : see further below.

======================================================================

The _reduction-semantics.ss_ library defines a pattern
language, used in various ways:

  pattern = any
          | number
          | string
          | variable
          | (variable-except <symbol> ...)
          | hole
          | (hole <symbol>)
          | <symbol>
          | (name <symbol> <pattern>)
          | (in-hole <pattern> <pattern>)
          | (in-named-hole <symbol> <symbol> <pattern> <pattern>)
          | (side-condition <pattern> <guard>)
          | (cross <symbol>>)
          | (pattern ...)
          | <scheme-constant>

The patterns match sexpressions. The _any_ pattern matches
any sepxression. The _number_ pattern matches any
number. The _string_ pattern matches any string. Those three
patterns may also be suffixed with an underscore and another
identifier, in which case they bind the full name (as if it
were an implicit `name' pattern) and match the portion
before the underscore.

The _variable_ pattern matches any symbol. The
_variable-except_ pattern matches any variable except those
listed in its argument. This is useful for ensuring that
keywords in the language are not accidentally captured by
variables.

The _hole_ pattern matches anything when inside a matching
in-hole pattern. The (hole <symbol>) variation on that
pattern is used in conjunction with in-named-hole to support
languages that require multiple patterns in a hole.

The _<symbol>_ pattern stands for a literal symbol that must
match exactly, unless it is the name of a non-terminal in a
relevant language or contains an underscore. 

If it is a non-terminal, it matches any of the right-hand
sides of that non-terminal.

If the symbol is a non-terminal followed by an underscore,
for example e_1, it is implicitly the same as a name pattern
that matches only the non-terminal, (name e_1 e) for the
example. If the symbol otherwise has an underscore, it is
an error.

_name_: The pattern:

  (name <symbol> <pattern>)

matches <pattern> and binds using it to the name <symbol>. 

_in-hole_: The (in-hole <pattern> <pattern>) matches the first
pattern. This match must include exactly one match against the `hole'
pattern. The `hole' pattern matches any sexpression. Then, the
sexpression that matched the hole pattern is used to match against the
second pattern.

_in-named-hole_: The pattern:

   (in-named-hole <symbol> <pattern> <pattern>) 

is similar in spirit to in-hole, except that it supports
languages with multiple holes in a context. The first
argument identifies which hole, using the (hole <symbol>)
pattern that this expression requires and the rest of the
arguments are just like in-hole. That is, if there are
multiple holes in a term, each matching a different (hole
<name>) pattern, this one selects only the holes that are
named by the first argument to in-named-hole.

_side-condition_: The (side-condition pattern guard) pattern matches
what the embedded pattern matches, and then the guard expression is
evaluated. If it returns #f, the pattern fails to match, and if it
returns anything else, the pattern matches. In addition, any
occurrences of `name' in the pattern are bound using `term-let'
(see below) in the guard.

_cross_: The (cross <symbol>) pattern is used for the compatible
closure functions. If the language contains a non-terminal with the
same name as <symbol>, the pattern (cross <symbol>) matches the
context that corresponds to the compatible closure of that
non-terminal.

The (pattern ...) pattern matches a sexpression list, where
each pattern matches an element of the list. In addition, if
a list pattern contains an ellipses that is not treated as a
literal, instead it matches any number of duplications of the
pattern that came before the ellipses (including 0). Furthermore,
each (name <symbol> <pattern>) in the duplicated pattern
binds a list of matches to <symbol>, instead of a single match.
(A nested duplicated pattern creates a list of list matches,
etc.) Ellipses may be placed anywhere inside the row of 
patterns,  except in the first position or immediately after
another ellipses.  Multiple ellipses are allowed.

> (language (non-terminal pattern ...) ...)     SYNTAX

This form defines a context-free language. As an example,
this is the lambda calculus:

  (define lc-lang
    (language (e (e e ...)
                 variable
                 v)
              (c (v ... c e ...)
                 hole)
              (v (lambda (variable ...) e))))

with non-terminals e for the expression language, c for the
evaluation contexts and v for values.

> compiled-lang? : (any? . -> . boolean?)

Returns #t if its argument was produced by `language', #f
otherwise.

> (term-let ([tl-pat expr] ...) body)           SYNTAX

Matches each given id pattern to the value yielded by
evaluating the corresponding expr and binds each variable in
the id pattern to the appropriate value (described
below). These bindings are then accessible to the `term'
syntactic form.

Identifier-patterns are terms in the following grammar:

    tl-pat ::= identifier
             | (tl-pat-ele ...)
tl-pat-ele ::= tl-pat
             | tl-pat ellipses

where ellipses is the literal symbol consisting of three
dots (and the ... indicates repetition as usual). If tl-pat
is an identifier, it matches any value and binds it to the
identifier, for use inside `term'. If it is a list, it
matches only if the value being matched is a list value and
only if every subpattern recursively matches the
corresponding list element. There may be a single ellipsis
in any list pattern; if one is present, the pattern before
the ellipses may match multiple adjacent elements in the
list value (possibly none).

> (term s-expr)                                 SYNTAX

This form is used for construction of new s-expressions in
the right-hand sides of reductions. It behaves identically
to quasiquote except that names bound by `term-let' are
implicitly substituted with the values that those names were
bound to, expanding ellipses as in-place sublists (in the
same manner as syntax-case patterns).

For example,

(term-let ([body '(+ x 1)]
           [(expr ...) '(+ - (values * /))]
           [((id ...) ...) '((a) (b) (c d))])
  (term (let-values ([(id ...) expr] ...) body)))

evaluates to

'(let-values ([(a) +] 
              [(b) -] 
              [(c d) (values * /)]) 
   (+ x 1))

It is an error for a term variable to appear in an
expression with an ellipsis-depth different from the depth
with which it was bound by `term-let'. It is also an error
for two `term-let'-bound identifiers bound to lists of
different lengths to appear together inside an ellipsis.

> (reduction language pattern bodies ...)       SYNTAX

This form defines a reduction. The first position must
evaluate to a language defined by the `language' form. The
pattern determines which terms this reductions apply to and
the last bodies are expressions that must evaluate to a new
sexpression corresponding to the reduct for this term. The
bodies are implicitly wrapped in a begin.

As an example, the reduction for the lambda calculus above
would be written like this:

     (reduction lc-lang
                (in-hole (name c c)
                         ((lambda (variable_i ...) e_body)
                          v_i ...))
                (plug 
                 (term c) 
                 (foldl lc-subst (term e_body) 
                                 (term (v_i ...)) 
                                 (term (variable_i ...)))))

The in-hole pattern matches a term against `c', and binds
what matches the hole to `hole'. Then, it matches what
matched the hole against ((lambda (variable) e) v).

Because of the name pattern and the subscripted variable names
we used, c, hole, variable_i, e_body, and v_i
are bound with `term-let' in the right hand side of the 
reduction. Then, when the reduction matches, the result is 
the result of evaluating the last argument to reduction. 
See `plug' below and lc-subst is defined by using the 
subst.ss library below.

> (reduction/name name language pattern bodies ...)  SYNTAX

The reduction/name form is the same as reduction, but
additionally evaluates the `name' expression and names the
reduction to be its result, which must be a string. The 
names are used by `traces'.

> (reduction/context language context pattern bodies ...)   SYNTAX

reduction/context is a short-hand form of reduction. It
automatically adds the `in-hole' pattern and the call to
`plug'. The equivalent reduction/context to the above
example is this:

     (reduction/context 
      lang
      c
      ((lambda (variable_i ...) e_body) v_i ...)
      (lc-subst (term (variable_i ...))
                (term (v_i ...))
                (term e_body))))

> (reduction/context/name name language context pattern bodies ...) SYNTAX

reduction/context/name is the same as reduction/context, but
additionally evaluates the `name' expression and names the
reduction to be its result, which must be a string.
The names are used by `traces'.


> red? : (any? . -> . boolean?)

Returns #t if its argument is a reduction (produced by `reduction',
`reduction/context', etc.), #f otherwise.

> compatible-closure : (red?
                        compiled-lang?
                        symbol?
                        . -> .
                        red?)

This function accepts a reduction, a language, the name of a
non-terminal in the language and returns the compatible
closure of the reduction for the specified non-terminal.

> context-closure : (red?
                     compiled-lang?
                     any
                     . -> .
                     red?)

This function accepts a reduction, a language, a pattern
representing a context (ie, that can be used as the first
argument to `in-hole'; often just a non-terminal) in the
language and returns the closure of the reduction
in that context.

> plug : (any? any? . -> . any)

The first argument to this function is an sexpression to
plug into. The second argument is the sexpression to replace
in the first argument. It returns the replaced term.

> reduce : ((listof red?) any? . -> . (listof any?))

Reduce accepts a list of reductions, a term, and returns a
list of terms that the term reduces to.

> language->predicate : (compiled-lang?
                         symbol?
                         . -> . 
                         (any? . -> . boolean?))

Takes a language and a non-terminal name and produces
a predicate that matches instances of the non-terminal.

> match-pattern : (compiled-pattern 
                   any/c
                   . -> .
                   (union false? (listof mtch?)))

This is mostly used to explore a particular pattern to
determine what is going wrong. It accepts a compiled pattern
and a and returns #f if the pattern doesn't match the term,
and returns a list of mtch structure if the terms do match.

> compile-pattern : (compiled-lang? any? . -> . compiled-pattern)

This is mostly used in conjunction with match-pattern to
explore particular patterns and terms when debugging. It
compiles a sexpression pattern to a pattern.

> mtch? : (any/c . -> . boolean?)

Determines if a value is a mtch structure.

> mtch-bindings : (mtch? -> bindings?)

This returns a bindings structure (see below) that
binds the pattern variables in this match.

> mtch-context : (mtch? . -> . any/c)

Returns the current context being built up for a
match. Usually, this is the same as the original term being
matched.

> mtch-hole : (mtch? . -> . (union none? any/c))

Returns the current contents of the hole for this match (if
there was a decomposition). Usually returns none.

> variable-not-in : (any? symbol? . -> . symbol?)

This helper function accepts an sexpression and a
variable. It returns a variable not in the sexpression with
a prefix the same as the second argument.

> make-bindings : ((listof rib?) . -> . bindings?)
> bindings? : (any? . -> . boolean?)
> bindings-table : (bindings? . -> . (listof rib?))

Constructor, predicate, and selector functions for the bindings values
returned by match-pattern.  Each bindings value represents the bindings
established for a single parse of the term; multiple such parses may be
possible in some situations.

> make-rib : (symbol? any? . -> . rib?)
> rib? : (any? . -> . boolean?)
> rib-name : (rib? . -> . symbol?)
> rib-exp : (rib? . -> . any?)

Constructor, predicate, and selector functions for the rib values contained
within a bindings.  Each rib associates a name with an s-expression from
the language, or a list of such s-expressions, if the (name ...) clause is
followed by an ellipsis.  Nested ellipses produce nested lists.

======================================================================

The _gui.ss_ library provides three functions:

> (traces language reductions expr [pp] [colors])

This function calls traces/multiple with language, reductions
and (list expr), and its optional arguments if supplied.

> (traces/multiple lang reductions exprs [pp] [colors])

This function calls traces/pred with the predicate
(lambda (x) #t)

> (traces/pred lang reductions exprs pred [pp] [colors])
  lang : language
  reductions : (listof reduction)
  exprs : (listof sexp)
  pred : (sexp -> boolean)
  pp : (any -> string)
     | (any port number (is-a?/c text%) -> void)
  colors : (listof (list string string))

This function opens a new window and inserts each
expr. Then, reduces the terms until either
reduction-steps-cutoff (see below) different terms are
found, or no more reductions can occur. It inserts each new
term into the gui. Clicking the `reduce' button reduces
until reduction-steps-cutoff more terms are found.

The pred function indicates if this term has a particular
property. If the function returns #t, the term is displayed
normally. If it returns #f, the term is displayed with a
red border.

If the pp function can take four arguments, it renders its
first argument into the port (its second argument) with 
width at most given by the number (its third argument). The
final argument is the text where the port is connected -- 
characters written to the port go to the end of the editor.
If the pp function cannot take four arguments, it is 
instead invoked with a single argument, the s-expression to
render, and it must return a string which the GUI will use
as a representation of the given expression for display.

The default pp, provided as default-pretty-printer, uses
MzLib's pretty-print function. See threads.ss in the
examples directory for an example use of the one-argument
form of this argument and ho-contracts.ss in the examples
directory for an example use of its four-argument form.

The colors argument, if provided, specifies a list of
reduction-name/color-string pairs. The traces gui will color
arrows drawn because of the given reduction name with the
given color instead of using the default color.

You can save the contents of the window as a postscript file
from the menus.

> (reduction-steps-cutoff)
> (reduction-steps-cutoff number)

A parameter that controls how many steps the `traces' function
takes before stopping.

> (initial-font-size)
> (initial-font-size number)

A parameter that controls the initial font size for the terms shown
in the GUI window.

> (initial-char-width)
> (initial-char-width number)

A parameter that determines the initial width of the boxes
where terms are displayed (measured in characters)

> (dark-pen-color color-or-string)
> (dark-pen-color) => color-or-string

> (dark-brush-color color-or-string)
> (dark-brush-color) => color-or-string

> (light-pen-color color-or-string)
> (light-pen-color) => color-or-string

> (light-brush-color color-or-string)
> (light-brush-color) => color-or-string

These four parameters control the color of the edges in the graph.

======================================================================

The _subst.ss_ library provides these names:

> (subst (match-pattern subst-rhs ...) ...)      SYNTAX

The result of this form is a function that performs capture
avoiding substitution for a particular (sexp-based)
language. The function accepts three arguments, a variable,
a term to substitute and a term to substitute into.

Each of the `match-pattern's specify the forms of
the language and the `subst-rhs's specify what kind of form
it is.  Each of the match-patterns are in (lib "match.ss"
"match")'s pattern language and any variable that they bind
are available in the <scheme-expression>'s described below.

The language of the subst-rhs follows.

> (variable)

  this means that the rhs for this form is a symbol that
  should be treated like a variable. Nothing may follow
  this.

> (constant)

  this means that the rhs for this form is a constant that
  cannot be renamed. Nothing may follow this.

> (all-vars <scheme-expression>)

This form indicates that this pattern in the language binds
the variables produced by the
<scheme-expression>. 

Immediately following this in a subst-rhs must be a (build
...) form and some number of (subterm ...) or (subterms ...)
forms.

> (build <scheme-expression>)

This form must come right after an (all-vars ...) form and
before any (subterm ...) or (subterms ...) forms.

This form tells subst how to reconstruct this term. The
<scheme-expression> must evaluate to a procedure that
accepts the (possibly renamed) variables from the all-vars
clause, and one argument for each of the subterms that
follow this declaration (with subterms flattened into the
argument list) in the same order that the subterm or
subterms declarations are listed.

> (subterm <scheme-expression> <scheme-expression>)

The first <scheme-expression> must be a list of variables
that is a sub-list of the variables in the all-vars
expression. The second expression must be an sexp
corresponding to one of the subexpressions of this
expression (matched by the match-patten for this clause of
subst).

> (subterms <scheme-expression> <scheme-expression>)

The first <scheme-expression> must be a list of variables
that is a sub-list of the variables in the all-vars
expression. The second expression must be an sexp
corresponding to one of the subexpressions of this
expression (matched by the match-patten for this clause of
subst).

Consider this example of a substitution procedure for the
lambda calculus:

  (define lc-subst
    (subst
     [`(lambda ,vars ,body)
      (all-vars vars)
      (build (lambda (vars body) `(lambda ,vars ,body)))
      (subterm vars body)]
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [`(,fun ,@(args ...))
      (all-vars '())
      (build (lambda (vars fun . args) `(,fun ,@args)))
      (subterm '() fun)
      (subterms '() args)]))

The first clause matches lambda expressions with any number
of arguments and says that there is one subterm, the body of
the lambda, and that all of the variables are bound in it.

The second clause matches symbols and indicates that they
are variables.

The third clause matches numbers and indicates that they are
constants.

The final clause matches function applications. The
`all-vars' shows that applications introduce no new
names. The build procedure reconstructs a new application
form. The subterm declaration says that the function
position is a subterm with no variables bound in it. The
subterms declaration says that all of the arguments are
subterms and that they do not introduce any new terms.

In this program, lc-subst is bound to a function that does
the substitution. The first argument is the variable to
substitute for, the second is the term to substitute and the
final argument is the term to substitute into. For example,
this call:

  (lc-subst 'q 
            '(lambda (x) y) 
            '((lambda (y) (y q)) (lambda (y) y)))

produces this output:

  '((lambda (y@) (y@ (lambda (x) y))) (lambda (y) y))

This library also provides:

> (plt-subst (match-pattern subst-rhs ...) ...)      SYNTAX

This is identical to subst, described above, except that
the pattern language used is that from (lib "plt-match.ss"), 
instead of (lib "match.ss").

> subst/proc
> alpha-rename 
> free-vars/memoize

Theses functions are the procedure-based interface to
substitution that subst expands to and uses.

======================================================================

The _iswim.ss_ module in the "examples" sub-collection defines a
grammar and reductions from "Programming Languages and Lambda Calculi"
by Felleisen and Flatt.

       Example S-expression forms of ISWIM expressions:
         Book                     S-expr
         ----                     ------
         (lambda x . x)           ("lam" x x)
         (+ '1` '2`)              ("+" 1 2)
         ((lambda y y) '7`)       (("lam" y y) 7)

       CK machine:
         Book                     S-expr
         ----                     ------
         <(lambda x . x), mt>     (("lam" x x) : "mt")

       CEK machine:
         Book                     S-expr
         ----                     ------
         <<(lambda x . x),        ((("lam" x x)
           {<X,<5,{}>>}>,           : ((X (5 : ()))))
          mt>                      : "mt")
         
       The full grammar:

         (language (M (M M)
                      (o1 M)
                      (o2 M M)
                      V)
                   (V X
                      ("lam" variable M)
                      b)
                   (X variable)
                   (b number)
                   (o1 "add1" "sub1" "iszero")
                   (o2 "+" "-" "*" "^")
                   (on o1 o2)
                   
                   ;; Evaluation contexts:
                   (E hole
                      (E M)
                      (V E)
                      (o1 E)
                      (o2 E M)
                      (o2 V E))
     
                   ;; Continuations (CK machine):
                   (k "mt"
                      ("fun" V k)
                      ("arg" M k)
                      ("narg" (V ... on) (M ...) k))
     
                   ;; Environments and closures (CEK):
                   (env ((X = vcl) ...))
                   (cl (M : env))
                   (vcl (V- : env))
                   
                   ;; Values that are not variables:
                   (V- ("lam" variable M)
                       b)
     
                   ;; Continuations with closures (CEK);
                   (k- "mt"
                       ("fun" vcl k-)
                       ("arg" cl k-)
                       ("narg" (vcl ... on) (cl ...) k-)))
     
       The following are provided by "iswim.ss" (case-insensitively):

               Grammar and substitution:
>                 iswim-grammar : compiled-lang?
>                 M? : (any? . -> . boolean?)
>                 V? : (any? . -> . boolean?)
>                 o1? : (any? . -> . boolean?)
>                 o2? : (any? . -> . boolean?)
>                 on? : (any? . -> . boolean?)
>                 k? : (any? . -> . boolean?)
>                 env? : (any? . -> . boolean?)
>                 cl? : (any? . -> . boolean?)
>                 vcl? : (any? . -> . boolean?)
>                 k-? : (any? . -> . boolean?)
>                 iswim-subst : (M? symbol? M? . -> . M?)
>                 empty-env : env?
>                 env-extend : (env? symbol? vcl? . -> . env?)
>                 env-lookup : (env? symbol? . -> . (union false? vcl?))
               Reductions:
>                 beta_v : red?
>                 delta : (listof red?)
>                 ->v : (listof red?)
>                 :->v : (listof red?)
               Abbreviations:
>                 if0 : (M? M? M? . -> . M?)
>                 true : M?
>                 false : M?
>                 mkpair : M?
>                 fst : M?
>                 snd : M?
>                 Y_v : M?
>                 sum : M?
               Helpers:
>                 delta*1 : (o1? V? . -> . (union false? V?))
                     delta as a function for unary operations.
>                 delta*2 : (o2? V? V? . -> . (union false? V?))
                     delta as a function for binary operations.
>                 delta*n : (on? (listof V?) . -> . (union false? V?))
                     delta as a function for any operation.

======================================================================

The _helper.ss_ module provides additional helper functions and syntax.

 ------- Memoization -------

> (define-memoized (f arg ...) expr ...)    SYNTAX

  Like `define' for function definitions, except that the function is
  "memoized": it automatically remembers each result, and when `eq?'
  arguments are provided later, the same result is returned
  immediately.

> (lambda-memoized (arg ...) expr)          SYNTAX

  Like `lambda' except that the resulting function is "memoized" (see
  `define-memoized' above).

 ------- Matching -------

> (lang-match-lambda (variable) grammar-expr 
    [pattern bodies ...] ...)                                SYNTAX

  Combines a pattern-matching dispatch with a `lambda', producing a
  function that takes a single argument and pattern-matches. Each
  `pattern' is as for `reduction', and the names that the pattern
  binds are visible in the `bodies'.

> (lang-match-lambda* (variable ...) main-variable grammar-expr 
    [pattern bodies ...] ...)                                SYNTAX

  Generalizes `lang-match-lambda' to create a multi-arity procedure.
  The `main-variable' must be one of the `variables', and it is the
  variable used for matching.

> lang-match-lambda-memoized                                 SYNTAX
> lang-match-lambda-memoized*                                SYNTAX

  Memoized versions of the above.

 ------- Backtracking -------

A function that supports backtracking must returns one of the
following:

  * #f to indicate failure
  * any other value to indicate simple success
  * (many-results l) to indicates success with any of the
    results in the list l
  * (explore-results ...) or (explore-parallel-results ...),
    which explores the results of recursive calls to generate
    one or more result values lazily

Whenever the backtracking function calls itself (or another
backtracking function in a cooperative set), it should use
`explore-results' or `explore-parallel-results' instead of
inspecting the value directly. To get a single result from
the backtracking function, uses `first-result'.

> many-results : ((listof any) . -> . any)

Aggregates potential results for future exploration.

> (explore-results (id) backtrackable-expr                   SYNTAX
        body-expr ...)

  Evaluates `backtrackable-expr'. In the simple case, `id' is bound to
  the result, the the result of the `explore-results' expression is
  the result of evaluating `body-expr's.

  If `backtrackable-expr' produces multiple alternatives (via
  `many-results') or if it produces a backtrackable computation, the
  result is a backtrackable computation. This backtrackable
  computation proceeds bey generating each successful result from
  `backtrackable-expr', and then feeding the result to the
  `body-expr's to refine the results. Naturally, `body-expr' can
  contain further uses of `explore-results' or `many-results' which are
  folded into the backtracking exploration.

> (explore-parallel-results (results-id) backtrackable-list-expr
     body-expr ...)

  Generalizes `explore-results' where `backtrackable-list-expr'
  produces a list of backtrackable results, and `body-expr' is called
  with successful combinations aggregated into `results-id' as a list.

> first-result : (any . -> . any)

  If the argument to `first-result' is a backtrackable computation, it
  is explored to obtain the first success, and that success is
  returned. If complete backtracking fails, the result is #f. If the
  argument to `first-result' is any other value, it is returned
  immediately.

 ------- Misc -------

> function-reduce* : ((listof red?)
                      any?
                      (any? . -> . boolean?)
                      number?
                      . -> . (listof any?))

   A poor-man's `gui' for test interaction. The first argument
   represents a set of reductions that define a function; the second
   argument is the starting expression; the third argument is a
   predicate to recognize ending expressions; the fourth argument
   limits the number of steps taken.  The function applies the
   reductions repeatedly until an ending expression is found, or until
   the reduction gets stuck. (If the reduction produces multiple
   results, an exception is raised.) The result is the list of
   expressions leading to the ending expression.

> unique-names? : ((listof symbol?) . -> . boolean?)

   Checks a list of symbols, returning #t if each symbol appears
   only once in the list, #f otherwise.

> generate-string : (-> string?)

   Returns a string that is generated by incrementing a counter.

> all-of : (any? (any? . -> . any) . -> . (listof any?))

   Takes an arbitrary S-expression as the first argument, and a
   predicate as the second argument. all-of' then traverses the pairs
   that make up the S-expression, calling the predicate on every pair
   and every value within a pair. The result is the list of values for
   which the predicate returned true. (If the predicate returns true
   for a pair, the search does not enter the pair.)

> transitive-closure : ((listof pair?) . -> . (listof (listof any?))

   Given the representation of a function as a list of pairs,
   `transitive-closure' produces the transitive closure as a list of
   lists. Each nested list begins with a domain item and continues
   with a list of range items. 

     Example: 
      (transitive-closure '((a . b) (b . c))) = '((a b c) (b c))

   The input function must be complete (i.e., all range elements
   should be in the domain).

   Element equality is determined by `eq?' (with the expectation that
   elements are usually symbols).

======================================================================

The _generator.ss_ module provides a tool for generating instances of
a grammar non-terminal.

> lang->generator-table : (lang?
                           (listof number?)
                           (listof symbol?)
                           (listof string?)
                           (listof symbol?)
                           number?
                           . -> .
                           generator-table?)

  Prepares generator information for a particular language,
  given a set of numbers to use for the `number' keyword, 
  a set of symbols for `variable' and `variable-except',
  and a set of string for `string'.

  The fifth argument lists keywords that appear in the grammar but
  that should be skipped (to limit the generation space). The last
  argument should be 0, and it is currently ignored.

> for-each-generated : (generator-table?
                        (any? number? . -> . any)
                        generator-table?
                        symbol?
                        . -> . any)

  The first argument is a procedure to call with a series of generated
  grammar instances and each term's size. Instances are generated from
  smallest to largest; the size of an instance is roughly the size of
  the proof tree that demonstrates grammar membership.

  The second argument is a generator table created with
  `lang->generator-table'.

  The third argument is a symbol, the name of a non-terminal for which
  instances should be generated.

> for-each-generated/size :  (generator-table?
                              (any? number? . -> . any)
                              generator-table?
                              symbol?
                              . -> . any)

  Like `for-each-generated', except minimum and maximum sizes are
  provided, and the order of generation is arbitrary (i.e., some
  larger instances may be generated before smaller instances).