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_.
_generator.ss_: automatically generates terms from a language
_schemeunit.ss_: a _plt-redex specific library of schemeunit checks_.
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
Barendregt 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> ...)
| (variable-prefix <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-sequence ...)
| <scheme-constant>
pattern-sequence = pattern
| ... ;; literal ellipsis
| ..._<id>
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 _variable-prefix_ pattern matches any symbol
that begins with the given prefix.
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. If the
hole pattern is not being matched as part of matching an
in-hole pattern, it only matches the hole (extracted as the
result of some earlier match of the in-hole pattern).
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. Accordingly, repeated uses of the same name are
constrainted to match the same expression.
If the symbol is a non-terminal followed by _!_, for example
e_!_1, it is also treated as a name pattern, but repeated
uses of the same pattern are constrained to be different.
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-sequence ...) pattern matches a sexpression
list, where each pattern-sequence element matches an element
of the list. In addition, if a list pattern contains an
ellipsis, the ellipsis 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. For example, this pattern:
((name x a) ... (name y a) ...)
matches this sexpression:
(a a)
three different ways. One where the first a in the pattern
matches nothing, and the second matches both of the
occurrences of `a', one where each named pattern matches a
single `a' and one where the first matches both and the
second matches nothing.
If the ellipses is named (ie, has an underscore and a name
following it, like a variable may), the pattern matcher
records the length of the list and ensures that any other
occurrences of the same named ellipses must have the same
length.
As an example, this pattern:
((name x a) ..._1 (name y a) ..._1)
only matches this sexpression:
(a a)
one way, with each named pattern matching a single a. Unlike
the above, the two patterns with mismatched lengths is ruled
out, due to the underscores following the ellipses.
Also, like underscore patterns above, if an underscore
pattern begins with ..._!_, then the lengths must be
different.
Thus, with the pattern:
((name x a) ..._!_1 (name y a) ..._!_1)
and the expression
(a a)
two matches occur, one where x is bound to '() and y is
bound to '(a a) and one where x is bound to '(a a) and y is
bound to '().
> (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 ...)
x
v)
(c (v ... c e ...)
hole)
(v (lambda (x ...) e))
(x (variable-except lambda))))
with non-terminals e for the expression language, x for
variables, 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 similarly to
quasiquote except for a few special forms that are
recognized (listed below) and 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.
The special forms recognized by term are:
(in-hole a b)
This is the dual to the pattern `in-hole' -- it accepts
a context and an expression and uses `plug' to combine
them.
hole
This produces the hole.
> (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 ...))
(term
(in-hole
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.
The right-hand-side uses `term' to re-build the context with
`in-hole' in the context `c'. The function 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.
> red-name : (red? . -> . (union #f string?))
Returns the name of a reduction, if any.
> 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.
> (metafunction <language-exp> [<pattern> <rhs-expression>] ...) SYNTAX
The `metafunction' builds a function on sexpressions
according to the pattern and right-hand-side
expressions. The first argument indicates the language used
to resolve non-terminals in the pattern expressions. Each of
the rhs-expressios is implicitly wrapped in `term'
As an example, this metafunction finds the free variables in
an expression in the lc-lang above:
;; free-vars : e -> (listof x)
(define free-vars
(metafunction
lc-lang
[(e_1 e_2 ...) ,(apply append (map free-vars (term (e_1 e_2 ...))))]
[x_1 ,(list (term x_1))]
[(lambda (x_1 ...) e_1)
,(foldr remq (free-vars (term e_1)) (term (x_1 ...)))]))
The first argument to metafunction is the grammar (defined
above). Following that are three cases, one for each
variation of expressions (e in lc-lang). The right-hand side
of each clause begins with a comma, since they are
implicitly wrapped in `term'. The free variables of an
application are the free variables of each of the subterms;
the free variables of a variable is just the variable
itself, and the free variables of a lambda expression are
the free variables of the body, minus the bound parameters.
> 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. This is
also used when a `term' sub-expression contains `in-hole'.
> 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.
> reduce-all : ((listof red?) any? . -> . (listof (listof any?))
Reduce-all accepts a list of reductions and a term. It
returns the results of following every reduction path from
the term. If there are infinite reduction sequences starting
at the term, this function will not terminate.
Along the way, if it encounters a term that reduces to
multiple terms and some of those terms are equal? to each
other, it signals an error.
_reduction semantics, performance issue_
This is best used in a test suite. Typically, when a term
parses in multiple different ways, or reduces to the same
thing in multiple different ways, that can be a big slowdown
(in general, if some term parses in two different ways,
nesting that term can end up with exponentially many
different parses, leading to really abysmal performance).
To avoid this situation, try using reduce-all in the test
suite for your semantics.
The most common source of multiple bad parses is using the
`variable' pattern. For example if your language is:
(language (e variable
(lambda (variable) e)
(e e)))
then the term '(lambda (x) x) parses two different way; once
as a lambda, and once as an application of a variable named
`lambda'. To avoid this problem define the grammar like
this, using the `variable-except' pattern:
(language (e x
(lambda (x) e)
(e e))
(x (variable-except lambda)))
> 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.
> (test-match lang pattern any) SYNTAX
Matches the pattern (in the language) against the third
expression. If it matches, this returns a list of mtch
structures describing the matches. If it fails, it returns
#f.
> (test-match lang pattern) SYNTAX
Builds a procedure for efficiently testing if expressions
match the pattern `pattern' in the language `lang'. The
procedures accepts a single expression and if the expresion
matches, it returns a list of mtch structures describing the
matches. If the match fails, the procedure returns #f.
> 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.
> set-cache-size! : (union #f positive-integer) -> void
Changes the cache size; a #f disables the cache
entirely. The default size is 350.
The cache is per-pattern (ie, each pattern has a cache of
size at most 350 (by default)) and is a simple table that
maps expressions to how they matched the pattern. When the
cache gets full, it is thrown away and a new cache is
started.
_Debugging PLT Redex Programs_
It is easy to write grammars and reduction rules that are
subtly wrong and typically such mistakes result in examples
that just get stuck when viewed in a `traces' window.
The best way to debug such programs is to find an expression
that looks like it should reduce but doesn't and try to find
out what pattern is failing to match. To do so, use the
test-match special form, described above.
In particular, first ceck to see if the term matches the
main non-terminal for your system (typically the expression
or program nonterminal). If it does not, try to narrow down
the expression to find which part of the term is failing to
match and this will hopefully help you find the problem. If
it does match, figure out which reduction rule should have
matched, presumably by inspecting the term. Once you have
that, extract a pattern from the left-hand side of the
reduction rule and do the same procedure until you find a
small example that shoudl work but doesn't (but this time
you might also try simplifying the pattern as well as
simplifying the expression).
======================================================================
The _gui.ss_ library provides the following 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 : (or/c (sexp -> boolean)
(sexp term-node? boolean?))
pp : (or/c (any -> string)
(any output-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 a 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 pred function accepts two arguments, a
term-node corresponding to the term is passed to the
predicate. This lets the predicate function explore the
(names of the) reductions that led to this term, using
term-node-parents and term-node-labels.
The pred function may be called more than once per node. In
particular, it is called each time an edge is added to a
node. The latest value returned determines the color.
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.
> term-node-parents : term-node -> (listof term-node)
Returns a list of the parents (ie, terms that reduced to the
current term) of the given node.
> term-node-labels : term-node -> (listof string)
Returns a list of the names of the reductions that led to
the given node, in the same order as the result of
term-node-parents.
> set-term-node-red?! : term-node boolean -> void?
Changes the highlighting of the node; its second argument is
treated like the last value returned from the predicate
passed to traces/pred.
> term-node-expr : term-node -> any
Returns the expression in this node.
> term-node? : any -> boolean
Recognizes term nodes.
> (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":
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).
======================================================================
_schemeunit.ss_: This library provides two 'check's (in
Schemeunit terminology):
> (check-reduces (listof red) any any)
This check reduces its second argument according to the
reductions in the first argument, and compares it to the
final argument. It expects the reductions to only produce
a single result.
It uses reduce-all to do the reductions (as above).
> (check-reduces/multiple (listof red) any (listof any))
This check reduces its second argument according to the
reductions in the first argument, and compares the
results to the final argument. The reductions may produce
multiple results and those results are expected to be the
same as the list in the last argument.
It uses reduce-all to do the reductions (as above).
![[logo]](/logo.png){kind=logo}