On this page:
define-metafunction
define-metafunction/  extension
in-domain?
define-judgment-form
define-extended-judgment-form
define-overriding-judgment-form
judgment-holds
judgment-form->rule-names
build-derivations
derivation
I
O
define-relation
judgment-form?
IO-judgment-form?
current-traced-metafunctions
8.15.0.9

4.5 Other Relations🔗ℹ

syntax

(define-metafunction language
  metafunction-contract
  [(name pattern ...) term metafunction-extras ...]
  ...)
 
metafunction-contract = 
  | 
id : pattern-sequence ... -> range
maybe-pre-condition
maybe-post-condition
     
maybe-pre-condition = #:pre term
  | 
     
maybe-post-condition = #:post term
  | 
     
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)
  | (where/error pat term)
  | 
(judgment-holds
 (judgment-form-id pat/term ...))
  | 
(judgment-holds
 (relation-id term ...))
  | (clause-name name)
  | or term
A metafunction is a function on terms. The define-metafunction form builds a metafunction 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 contract, if present, is matched against every input to the metafunction and, if the match fails, an exception is raised. If a metavariable is repeated in a contract, it does not require the terms to be equal, unless there is an underscore subscript (i.e., the binding works like it does in define-language, not how it works in the patterns in the left-hand sides of the metafunction clauses).

If present, the term inside the maybe-pre-condition is evaluated after a successful match to the input pattern in the contract (with any variables from the input contract bound). If it returns #f, then the input contract is considered to not have matched and an error is also raised. When a metafunction returns, the expression in the maybe-post-condition is evaluated (if present), with any variables from the input or output contract bound.

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

The resulting metafunction raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways (and that leads to different results for the different matches).

The side-condition extra is evaluated after a successful match to the corresponding argument pattern. If it returns #f, the clause is considered not to have matched, and the next one is tried. The side-condition/hidden extra behaves the same, but is not typeset.

The where and where/hidden extra are like side-condition and side-condition/hidden, except the match guards the clause. The where/error extra is like where, except that the pattern must match.

The judgment-holds clause is like side-condition and where, except the given judgment or relation must hold for the clause to be taken.

The clause-name is used only when typesetting. See metafunction-cases.

The or clause is used to define piecewise conditional metafunctions. In particular, if any of the where or side-condition clauses fail, then evaluation continues after an or clause, treating the term that follows as the result (subject to any subsequent where clauses or side-conditions. This construction is equivalent to simply duplicating the left-hand side of the clause, once for each or expression, but signals to the typesetting library to use a large left curly brace to group the conditions in the or.

For example, here are two equivalent definitions of a biggest metafunction that typeset differently:

Examples:
> (define-metafunction lc-lang
    biggest : natural natural -> natural
    [(biggest natural_1 natural_2)
     natural_2
     (side-condition (< (term natural_1) (term natural_2)))]
    [(biggest natural_1 natural_2)
     natural_1])
> (render-metafunction biggest)

image

> (define-metafunction lc-lang
    biggest : natural natural -> natural
    [(biggest natural_1 natural_2)
     natural_2
     (side-condition (< (term natural_1) (term natural_2)))
  
     or
  
     natural_1])
> (render-metafunction biggest)

image

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 (λ (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 λ 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.

Changed in version 1.4 of package redex-lib: Added #:post conditions.
Changed in version 1.5: Added or clauses.

syntax

(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))])

syntax

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

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

syntax

(define-judgment-form language
  mode-spec
  contract-spec
  invariant-spec
  rule rule ...)
 
mode-spec = 
  | #:mode (form-id pos-use ...)
     
contract-spec = 
  | #:contract (form-id pattern-sequence ...)
     
invariant-spec = 
  | #:inv term
     
pos-use = I
  | O
     
rule = 
[premise
 ...
 dashes rule-name
 conclusion]
  | 
[conclusion
 premise
 ...
 rule-name]
     
conclusion = (form-id pat/term ...)
     
premise = (judgment-form-id pat/term ...) maybe-ellipsis
  | (relation-id pat/term ...) maybe-ellipsis
  | (where pattern term)
  | (where/hidden pattern term)
  | (where/error pattern term)
  | (side-condition term)
  | (side-condition/hidden term)
     
rule-name = 
  | string
  | non-ellipsis-non-dashes-var
     
pat/term = pattern
  | term
     
maybe-ellipsis = 
  | ...
     
dashes = ---
  | ----
  | -----
  | etc.
Defines form-id as a relation on terms via a set of inference rules.

If a mode-spec appears, 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 mode-spec declaration, which partitions positions into inputs I and outputs O. Output positions in conclusions and input positions in premises must be terms; input positions in conclusions and output positions in premises must be patterns. The rule-names are used by build-derivations and by render-judgment-form.

If a mode-spec is not present, Redex cannot compute a derivation for the judgment form, instead it can check that a given derivation is valid according to the rules.

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. The term in the optional invariant-spec is evaluated after the output positions have been computed and the contract has matched successfully, with variables (that have underscores) from the contract bound; a result of #f is considered to be a contract violation and an exception is raised.

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)
    [-----------  "zero"
     (sum z n n)]
  
    [(sum n_1 n_2 n_3)
     ------------------------- "add1"
     (sum (s n_1) n_2 (s n_3))])

When a judgment form has a mode, the judgment-holds form checks whether a judgment form 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)
    [------------ "z"
     (sumr z n n)]
  
    [(sumr n_1 n_2 n_3)
     -------------------------- "s"
     (sumr (s n_1) n_2 (s 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))))

In some situations, there is no mode that could be specified that Redex accepts. It is possible to leave off the mode in that case, as in this judgment form:
> (define-extended-language nat-exprs nats
    (e ::= (+ e e) n))
> (define-judgment-form nat-exprs
    #:contract (same-exp e e)
  
    [(sum n_1 n_2 n_3)
     -------------------------- "add"
     (same-exp (+ n_1 n_2) n_3)]
  
    [-------------- "refl"
     (same-exp e e)]
  
    [(same-exp e_1 e_2) (same-exp e_2 e_3)
     ------------------ "trans"
     (same-exp e_1 e_3)]
  
    [(same-exp e_2 e_1)
     ------------------ "sym"
     (same-exp e_1 e_2)]
  
    [(same-exp e_1 e_2)
     ---------------------------------- "compat-l"
     (same-exp (+ e_1 e_3) (+ e_2 e_3))]
  
    [(same-exp e_1 e_2)
     ---------------------------------- "compat-r"
     (same-exp (+ e_3 e_1) (+ e_3 e_2))])

With a modeless judgment form, Redex cannot compute the entire derivation for you, but it can check that a given derivation is valid according to the rules in the judgment form. Here is one such derivation:
> (define same-exp-derivation
    (let* ([one `(s z)]
           [two `(s ,one)]
           [three `(s ,two)]
           [four `(s ,three)]
           [five `(s ,four)]
           [six `(s ,five)])
      (derivation
       `(same-exp (+ ,four ,two)
                  (+ ,one (+ ,two ,three)))
       "trans"
       (list
        (derivation `(same-exp (+ ,four ,two) ,six)
                    "add"
                    (list (car (build-derivations (sum ,four ,two n)))))
        (derivation
         `(same-exp ,six
                    (+ ,one (+ ,two ,three)))
         "sym"
         (list
          (derivation
           `(same-exp (+ ,one (+ ,two ,three))
                      ,six)
           "trans"
           (list
            (derivation
             `(same-exp (+ ,one (+ ,two ,three))
                        (+ ,one ,five))
             "compat-r"
             (list
              (derivation `(same-exp (+ ,two ,three)
                                     ,five)
                          "add"
                          (list (car (build-derivations (sum ,two ,three n)))))))
            (derivation `(same-exp (+ ,one ,five)
                                   ,six)
                        "add"
                        (list (car (build-derivations (sum ,one ,five n)))))))))))))
It is a bit hard to read in that form; here it is in a more traditional tree rendering:
> (parameterize ([pretty-print-columns 20])
    (derivation->pict nat-exprs same-exp-derivation))

image

And using judgment-holds, we see that Redex agrees it is a valid derivation for same-exp.
> (judgment-holds same-exp same-exp-derivation)

#t

The premises must be in the same order in the derivation struct’s subs field as they appear in the definition of the judgment form.

A rule’s where, where/hidden, and where/error 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 n_1 n_2)
     --------------------
     (le (s n_1) (s 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)
    [(where n_3 (pred n_1))
     (le n_2 n_3)
     ----------------------
     (gt n_1 n_2)])
> (judgment-holds (gt (s (s z)) (s z)))

#t

> (judgment-holds (gt (s z) (s z)))

#f

A rule’s side-condition and side-condition/hidden premises are similar to those in reduction-relation and define-metafunction, except that they do not implicitly unquote their right-hand sides. In other words, a premise of the form (side-condition term) is close to the premise (where #t term), except it does not typeset with the “#t = ”, as that would and it holds whenever the expression evaluates to any non #f value (not just #t).

Judgments with exclusively I mode positions may also be used in terms in a manner similar to metafunctions, and evaluate to a boolean.

Examples:
> (term (le (s z) (s (s z))))

#t

> (term (le (s z) 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)
  
    [-------- "evenz"
     (even z)]
  
    [(even n)
     ---------------- "even2"
     (even (s (s n)))])
> (define-judgment-form nats
    #:mode (all-even I)
    #:contract (all-even (n ...))
    [(even n) ...
     ------------------
     (all-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_2 v_1)
     --------------
     (path v_1 v_2)]
  
    [(edge v_1 v_2)
     (path v_2 v_3)
     --------------
     (path v_1 v_3)])
Due to the second path rule, the follow query fails to terminate:

> (judgment-holds (path a c))

There are three example files that come with Redex that 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.

These files can be found via DrRacket’s File|Open Require Path... menu item. Type redex/examples/d/ into the dialog and then choose one of the names listed above. Or, evaluate the expression
(collection-file-path «filename.rkt»
                      "redex"
                      "examples"
                      "define-judgment-form")
replacing «filename.rkt» with one of the names listed above.

Note that current-traced-metafunctions also traces judgment forms and is helpful when debugging.

syntax

(define-extended-judgment-form language judgment-form-id
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
Defines a new judgment form that extends judgment-form-id with additional rules. The mode-spec, contract-spec, invariant-spec, and rules are as in define-judgment-form.

The mode specification in this judgment form and the original must be the same.

syntax

(define-overriding-judgment-form language judgment-form-id
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
Defines a new judgment form that extends judgment-form-id with additional rules, replacing rules from judgment-form-id that have the same name as any of the new rules.

The mode-spec, contract-spec, invariant-spec, and rules are as in define-judgment-form.

The mode specification in this judgment form and the original must be the same.

syntax

(judgment-holds judgment-or-relation)

(judgment-holds judgment-or-relation term)
(judgment-holds judgment-form-id derivation-expr)
 
judgment-or-relation = (judgment-form-id pat/term ...)
  | (relation-id pat/term ...)
In its first form, checks whether judgment-or-relation holds for any assignment of the pattern variables in judgment-form-id’s output positions (or just that it holds in the case that a relation from define-relation is used).

In its second form, produces a list of terms by instantiating the supplied term template with each satisfying assignment of pattern variables. In the second case, if a relation is supplied, there are no pattern variables, so the result is either a list with one element or the empty list.

In both of the first two forms, any given judgment form must have a mode.

In its third form, the judgment-form-id must not have a mode, and the derivation-expr must produce a derviation struct. The result of judgment-holds is #t when the derivation is valid, according to the rules of the judgment form, and #f otherwise. Note that the premises of the derivation must appear in the same order as the premises in the definition of the judgment form.

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

#t

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

'((s (s (s z))))

See define-judgment-form for more examples.

procedure

(judgment-form->rule-names r)  (listof symbol?)

  r : judgment-form?
Returns the names of the judgment form’s named clauses.

syntax

(build-derivations judgment-or-relation)

Constructs all of the derivation trees for judgment-or-relation.

Example:
> (build-derivations (even (s (s z))))

(list

 (derivation

  '(even (s (s z)))

  "even2"

  (list (derivation '(even z) "evenz" '()))))

struct

(struct derivation (term name subs)
    #:extra-constructor-name make-derivation)
  term : any/c
  name : (or/c string? #f)
  subs : (listof derivation?)
Represents a derivation from a judgment form.

The term field holds an s-expression based rendering of the conclusion of the derivation, the name field holds the name of the clause with term as the conclusion, and subs contains the sub-derivations.

See also build-derivations.

syntax

I

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

syntax

O

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

syntax

(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. Querying the result uses judgment-holds or 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 τ τ)])
> (judgment-holds (subtype int num))

#t

> (judgment-holds (subtype (int  int) (num  num)))

#f

> (judgment-holds (subtype (num  int) (num  num)))

#t

procedure

(judgment-form? v)  boolean?

  v : any/c
Identifies values bound to identifiers introduced by define-judgment-form and define-relation.

procedure

(IO-judgment-form? v)  boolean?

  v : any/c
Identifies values bound to identifiers introduced by define-judgment-form when the mode is (I O) or (O I).

parameter

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

(current-traced-metafunctions traced-metafunctions)  void?
  traced-metafunctions : (or/c 'all (listof symbol?))
Controls which metafunctions and judgment forms are currently being traced. If it is 'all, all of them are. Otherwise, the elements of the list name the metafunctions and judgments 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 or judgment call is actually performed.

Defaults to '().

Examples:
> (define-judgment-form nats
    #:mode (odd I)
    #:contract (odd n)
  
    [-------- "oddsz"
     (odd (s z))]
  
    [(odd n)
     ---------------- "odd2"
     (odd (s (s n)))])
> (parameterize ([current-traced-metafunctions '(odd)])
    (judgment-holds (odd (s (s (s z))))))

 >(odd (s (s (s z))))

 > (odd (s z))

 < ((odd (s z)))

 <((odd (s (s (s z)))))

#t

> (parameterize ([current-traced-metafunctions '(odd)])
    (judgment-holds (odd (s (s (s (s (s z))))))))

 >(odd (s (s (s (s (s z))))))

c> (odd (s (s (s z))))

 < ((odd (s (s (s z)))))

 <((odd (s (s (s (s (s z)))))))

#t