Redex Parameters
1 Examples
2 Reference
define-reduction-relation*
define-extended-reduction-relation*
define-metafunction*
define-extended-metafunction*
define-judgment-form*
define-extended-judgment*
define-reduction-relation
define-extended-reduction-relation
define-extended-metafunction
7.8

Redex Parameters

Cameron Moy

 (require redex/parameter) package: redex-parameter

This package implements forms for parameterized Redex objects (i.e. metafunctions, judgment forms, and reduction relations). When objects depend on one another, for example a reduction relation is defined using a metafunction, parameters can automatically lift dependencies from the lower language to a higher one.

1 Examples

Suppose we define a language L0, a metafunction L0-number-bad, and a reduction relation r0-bad. We will rely on this metafunction, defined for L0, in our reduction relation.

(define-language L0
  [m ::= number])
 
(define-metafunction L0
  L0-number-bad : m -> m
  [(L0-number-bad m) 0])
 
(define-reduction-relation r0-bad
  L0
  [--> m (L0-number-bad m)])

As expected, we can see what happens when we step with r0-bad.

> (apply-reduction-relation r0-bad 999)

'(0)

Why is r0-bad named as such? We’ve defined a reduction relation that depends on a language-specific metafunction. Unfortunately, extended reduction relations will break under these conditions. An extended reduction relation will lift all rules to the new language, but metafunction and judgment form dependencies will not be reinterpreted.

(define-extended-language L1 L0
  [m ::= .... string])
 
(define-extended-reduction-relation r1-bad r0-bad L1)

Here we’ve added to the m non-terminal. Since r1-bad extends r0-bad, every rule will be reinterpreted. The only case we have will match, but the metafunction L0-number-bad is undefined for strings. This will yield an error.

> (apply-reduction-relation r1-bad "hi")

L0-number-bad: (L0-number-bad "hi") is not in my domain

This package solve the problem by introducing parameters. We’ll instead define r0 with define-reduction-relation* and parameterize it by the metafunction defined with define-metafunction*.

(define-metafunction* L0
  L0-number : m -> m
  [(L0-number m) 0])
 
(define-reduction-relation* r0
  L0
  #:parameters ([lang-number L0-number])
  [--> m (lang-number m)])

We’ved replace the non-starred variants from earlier, with their starred counterparts. Using the starred form gets you two things:
  • Liftable. You can use the object as the value of a parameter.

  • Parameters. You can introduce parameters that will lift their values appropriately.

Here we introduce a parameter lang-number that is bound to L0-number. For L0 there is no difference between r0 and r0-bad.

> (apply-reduction-relation r0 999)

'(0)

However if we do the extension as before, the parameter’s default value will be lifted to the current language.

> (define-extended-reduction-relation* r1 r0 L1)
> (apply-reduction-relation r1 "hi")

'(0)

Now suppose instead of giving back a language level of 0, we’d like it to give back 1. One way to do this is to extend the original metafunction.

> (define-extended-metafunction* L0-number L1
    L1-number : m -> m
    [(L1-number m) 1])
> (define-extended-reduction-relation* r1* r0 L1)
> (apply-reduction-relation r1* "hi")

'(1)

As we just saw, if no metafunction extends the original parameter value, in our case L0-number, then it is lifted. However, if a metafunction does extend it, in this case L1-number, that will be used instead.

Parameters are not limited to just reduction relations. You can, for example, parameterize a judgment form by a metafunction or parameterize a metafunction by a reduction relation.

2 Reference

syntax

(define-reduction-relation* id
  language parameters
  domain codomain base-arrow
  reduction-case ...
  shortcuts)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines id as a parameterized reduction relation. Aside from parameters, the syntax is the same as in reduction-relation.

syntax

(define-extended-reduction-relation* id
  reduction-relation language parameters
  domain codomain base-arrow
  reduction-case ...
  shortcuts)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines id as a parameterized reduction relation that extends an existing one. Aside from parameters, the syntax is the same as in extend-reduction-relation.

syntax

(define-metafunction* language
  parameters
  metafunction-contract
  metafunction-case ...)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines a parameterized metafunction. Aside from parameters, the syntax is the same as in define-metafunction. Parameterized metafunctions must have a contract.

syntax

(define-extended-metafunction* metafunction-id language
  parameters
  metafunction-contract
  metafunction-case ...)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines a parameterized metafunction that extends metafunction-id. Aside from parameters, the syntax is the same as in define-metafunction/extension. Parameterized metafunctions must have a contract.

syntax

(define-judgment-form* language
  parameters
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines a parameterized judgment form. Aside from parameters, the syntax is the same as in define-judgment-form. Parameterized judgments may not be modeless.

syntax

(define-extended-judgment* judgment-id language
  parameters
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
 
parameters = 
  | #:parameters ([parameter default] ...)
Defines a parameterized judgment form that extends judgment-id. Aside from parameters, the syntax is the same as in define-extended-judgment-form. Parameterized judgments may not be modeless.

syntax

(define-reduction-relation id
  language
  domain codomain base-arrow
  reduction-case ...
  shortcuts)

syntax

(define-extended-reduction-relation id
  reduction-relation language
  domain codomain base-arrow
  reduction-case ...
  shortcuts)

syntax

(define-extended-metafunction metafunction-id language
  metafunction-contract
  metafunction-case ...)
These are non-parameterized variants of the above starred variants; they are provided only for consistency.