5 Other Relations

(define-metafunction language
  metafunction-contract
  [(name pattern ...) term metafunction-extras ...]
  ...)

metafunction-contract =
| id : pattern ... -> range

range = pattern
| pattern or range
| pattern ∨ range
| pattern ∪ range

metafunction-extras = (side-condition racket-expression)
| (side-condition/hidden racket-expression)
| (where pat term)
| (where/hidden pat term)
|
(judgment-holds
(judgment-form-id pat/term ...))

The define-metafunction form 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-expressions is implicitly wrapped in term.

The side-condition, hidden-side-condition, where, and where/hidden clauses behave as in the reduction-relation form.

Raises an exception recognized by exn:fail:redex? if no clauses match, if one of the clauses matches multiple ways (and that leads to different results for the different matches), or if the contract is violated.

Note that metafunctions are assumed to always return the same results for the same inputs, and their results are cached, unless caching-enabled? is set to #f. Accordingly, if a metafunction is called with the same inputs twice, then its body is only evaluated a single time.

As an example, these metafunctions finds the free variables in an expression in the lc-lang above:

(define-metafunction lc-lang
  free-vars : e -> (x ...)
  [(free-vars (e_1 e_2 ...))
   (∪ (free-vars e_1) (free-vars e_2) ...)]
  [(free-vars x) (x)]
  [(free-vars (lambda (x ...) e))
   (- (free-vars e) (x ...))])

The first argument to define-metafunction is the grammar (defined above). Following that are three cases, one for each variation of expressions (e in lc-lang). 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.

Here are the helper metafunctions used above.

(define-metafunction lc-lang
  ∪ : (x ...) ... -> (x ...)
  [(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...)
   (∪ (x_1 ... x_2 ...) (x_3 ...) ...)]
  [(∪ (x_1 ...))
   (x_1 ...)]
  [(∪) ()])

(define-metafunction lc-lang
  - : (x ...) (x ...) -> (x ...)
  [(- (x ...) ()) (x ...)]
  [(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...))
   (- (x_1 ... x_3 ...) (x_2 x_4 ...))
   (side-condition (not (memq (term x_2) (term (x_3 ...)))))]
  [(- (x_1 ...) (x_2 x_3 ...))
   (- (x_1 ...) (x_3 ...))])

Note the side-condition in the second case of -. It ensures that there is a unique match for that case. Without it, (term (- (x x) x)) would lead to an ambiguous match.

(define-metafunction/extension f language
  metafunction-contract
  [(g pattern ...) term metafunction-extras ...]
  ...)

Defines a metafunction g as an extension of an existing metafunction f. The metafunction g behaves as if f’s clauses were appended to its definition (with occurrences of f changed to g in the inherited clauses).

For example, define-metafunction/extension may be used to extend the free-vars function above to the forms introduced by the language lc-num-lang.

(define-metafunction/extension free-vars lc-num-lang
  free-vars-num : e -> (x ...)
  [(free-vars-num number)
   ()]
  [(free-vars-num (+ e_1 e_2))
   (∪ (free-vars-num e_1)
      (free-vars-num e_2))])

(in-domain? (metafunction-name term ...))

Returns #t if the inputs specified to metafunction-name are legtimate inputs according to metafunction-name’s contract, and #f otherwise.

(define-judgment-form language
option ...
rule ...)

option = mode-spec
| contract-spec

mode-spec = #:mode (form-id pos-use ...)

contract-spec = #:contract (form-id pattern ...)

pos-use = I
| O

rule =
[conclusion
premise
...]
|
[premise
...
dashes
conclusion]

conclusion = (form-id pat/term ...)

premise = (judgment-form-id pat/term ...) maybe-ellipsis
| (where pattern term)
| (where/hidden pattern term)

pat/term = pattern
| term

maybe-ellipsis =
| ...

dashes = ---
| ----
| -----
| etc.

Defines form-id as a relation on terms via a set of inference rules. Each rule must be such that its premises can be evaluated left-to-right without “guessing” values for any of their pattern variables. Redex checks this property using the mandatory mode-spec declaration, which partitions positions into inputs I and outputs O. Output positions in conclusions and input positions in premises must be terms with no uses of unquote; input positions in conclusions and output positions in premises must be patterns. When the optional contract-spec declaration is present, Redex dynamically checks that the terms flowing through these positions match the provided patterns, raising an exception recognized by exn:fail:redex if not.

For example, the following defines addition on natural numbers:

> (define-language nats
    (n z (s n)))
> (define-judgment-form nats
    #:mode (sum I I O)
    #:contract (sum n n n)
    [(sum z n n)]
    [(sum (s n_1) n_2 (s n_3))
     (sum n_1 n_2 n_3)])

The judgment-holds form checks whether a relation holds for any assignment of pattern variables in output positions.

Examples:

> (judgment-holds (sum (s (s z)) (s z) (s (s (s z)))))
#t
> (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))))
#t
> (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n))))))
#f

Alternatively, this form constructs a list of terms based on the satisfying pattern variable assignments.

Examples:

> (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) n)
'(z)
> (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n))))) n)
'()
> (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) (s n))
'((s z))

Declaring different modes for the same inference rules enables different forms of computation. For example, the following mode allows judgment-holds to compute all pairs with a given sum.

> (define-judgment-form nats
    #:mode (sumr O O I)
    #:contract (sumr n n n)
    [(sumr z n n)]
    [(sumr (s n_1) n_2 (s n_3))
     (sumr n_1 n_2 n_3)])
> (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))
'(((s (s z)) z) ((s z) (s z)) (z (s (s z))))

A rule’s where and where/hidden premises behave as in reduction-relation and define-metafunction.

Examples:

> (define-judgment-form nats
    #:mode (le I I)
    #:contract (le n n)
    [(le z n)]
    [(le (s n_1) (s n_2))
     (le n_1 n_2)])
> (define-metafunction nats
    pred : n -> n or #f
    [(pred z) #f]
    [(pred (s n)) n])
> (define-judgment-form nats
    #:mode (gt I I)
    #:contract (gt n n)
    [(gt n_1 n_2)
     (where n_3 (pred n_1))
     (le n_2 n_3)])
> (judgment-holds (gt (s (s z)) (s z)))
#t
> (judgment-holds (gt (s z) (s z)))
#f

A literal ellipsis may follow a judgment premise when a template in one of the judgment’s input positions contains a pattern variable bound at ellipsis-depth one.

Examples:

> (define-judgment-form nats
    #:mode (even I)
    #:contract (even n)
    [(even z)]
    [(even (s (s n)))
     (even n)])
> (define-judgment-form nats
    #:mode (all-even I)
    #:contract (all-even (n ...))
    [(all-even (n ...))
     (even n) ...])
> (judgment-holds (all-even (z (s (s z)) z)))
#t
> (judgment-holds (all-even (z (s (s z)) (s z))))
#f

Redex evaluates premises depth-first, even when it doing so leads to non-termination. For example, consider the following definitions:

> (define-language vertices
    (v a b c))
> (define-judgment-form vertices
    #:mode (edge I O)
    #:contract (edge v v)
    [(edge a b)]
    [(edge b c)])
> (define-judgment-form vertices
    #:mode (path I I)
    #:contract (path v v)
    [(path v v)]
    [(path v_1 v_2)
     (path v_2 v_1)]
    [(path v_1 v_3)
     (edge v_1 v_2)
     (path v_2 v_3)])

Due to the second path rule, the follow query fails to terminate:

> (judgment-holds (path a c))

The "examples" directory demonstrates three use cases:

"typing-rules.rkt" — defines a type system in a way that supports mechanized typesetting. When a typing judgment form can be given a mode, it can also be encoded as a metafunction using where clauses as premises, but Redex cannot typeset that encoding as inference rules.
"sos.rkt" — defines an SOS-style semantics in a way that supports mechanized typesetting.
"multi-val.rkt" — defines a judgment form that serves as a multi-valued metafunction.

(judgment-holds judgment)
(judgment-holds judgment term)

judgment = (judgment-form-id pat/term ...)

In its first form, checks whether judgment holds for any assignment of the pattern variables in judgment-id’s output positions. In its second form, produces a list of terms by instantiating the supplied term template with each satisfying assignment of pattern variables. See define-judgment-form for examples.

I

Recognized specially within define-judgment-form, the I keyword is an error elsewhere.

O

Recognized specially within define-judgment-form, the O keyword is an error elsewhere.

(define-relation language
  relation-contract
  [(name pattern ...)
   term ...
   metafunction-extras ...] ...)

relation-contract =
| form-id ⊂ pattern x ... x pattern
| form-id ⊆ pattern × ... × pattern

Similar to define-judgment-form but suitable only when every position is an input. There is no associated form corresponding to judgment-holds; querying the result uses the same syntax as metafunction application.

The contract specification for a relation restricts the patterns that can be used as input to a relation. For each argument to the relation, there should be a single pattern, using x or × to separate the argument contracts.

Examples:
> (define-language types
    ((τ σ) int
           num
           (τ → τ)))
> (define-relation types
    subtype ⊆ τ × τ
    [(subtype int num)]
    [(subtype (τ_1 → τ_2) (σ_1 → σ_2))
     (subtype σ_1 τ_1)
     (subtype τ_2 σ_2)]
    [(subtype τ τ)])
> (term (subtype int num))
#t
> (term (subtype (int → int) (num → num)))
#f
> (term (subtype (num → int) (num → num)))
#t

Note that relations are assumed to always return the same results for the same inputs, and their results are cached, unless caching-enable? is set to #f. Accordingly, if a relation is called with the same inputs twice, then its right-hand sides are evaluated only once.

(current-traced-metafunctions) → (or/c 'all (listof symbol?))
(current-traced-metafunctions traced-metafunctions) → void?
traced-metafunctions : (or/c 'all (listof symbol?))

Controls which metafunctions are currently being traced. If it is 'all, all of them are. Otherwise, the elements of the list name the metafunctions to trace.

The tracing looks just like the tracing done by the racket/trace library, except that the first column printed by each traced call indicate if this call to the metafunction is cached. Specifically, a c is printed in the first column if the result is just returned from the cache and a space is printed if the metafunction call is actually performed.

Defaults to '().

top← prev up next →

1	Patterns
2	Terms
3	Languages
4	Reduction Relations
5	Other Relations
6	Testing
7	GUI
8	Typesetting
	Index