8.2

## Redex Parameters

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

### 1Examples

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.

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

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.

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.

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’ve replaced 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.

### 2Reference

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.