Redex Parameters
1 Examples
2 Reference
define-reduction-relation
define-extended-reduction-relation
define-extended-metafunction
define-extended-judgment
reduction-out
current-language
7.5

Redex Parameters

Cameron Moy

 (require redex/parameter) package: redex-parameter

This package implements forms for parameterized reduction relations. When extending reduction relations that depend on metafunctions, judgment forms, or other reduction relations, parameterized reduction relations can automatically lift forms at lower language levels.

1 Examples

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

(define-language L0
  [m ::= number])
 
(define-metafunction L0
  [(L0-number m) 0])
 
(define r0-bad
  (reduction-relation
    L0
    [--> m (L0-number 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 r1-bad
  (extend-reduction-relation r0-bad L1))

Here we’ve added a new form 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 is undefined for strings. This will yield an error.

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

L0-number: no clauses matched for (L0-number "hi")

Parameterized reduction relations solve this problem. We’ll instead define r0 with define-reduction-relation and parameterize it by the metafunction.

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

Here we introduce a parameter lang-number that by default is bound to L0-number as before. 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) 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.

If you want to set a parameter to a specific value, you can give an explicit parameterization.

> (define-metafunction L1
    [(silly m) "☺"])
> (apply-reduction-relation (r1 [lang-number silly]) "hi")

'("☺")

As a special case, you can provide #:disable to the parameterization and it will disable all the automatic lifting and we get back the original bad reduction relation’s behavior.

> (apply-reduction-relation (r1 #:disable) "hi")

L0-number: no clauses matched for (L0-number "hi")

You can also parameterize a reduction relation by another one. This is potentially useful if the base relation you’re extending may change.

> (define-reduction-relation r-13
    L0
    [--> m 13])
> (define-reduction-relation r-21
    L0
    [--> m 21])
> (define-extended-reduction-relation wrap
    (context-closure r current-language (over hole))
    L0
    #:parameters ([r r-13]))
> (apply-reduction-relation wrap (term (over 0)))

'((over 13))

> (apply-reduction-relation (wrap [r r-21]) (term (over 0)))

'((over 21))

Here we use current-language instead of hard-coding L0. This allows wrap to work properly if it’s automatically lifted to a language extension.

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. Each parameter is initially assigned to the default value. The remaining arguments are 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 which extends an existing one. The set of parameters is extended with any new parameters. The remaining arguments are as in extend-reduction-relation.

syntax

(define-extended-metafunction metafunction-id language
  metafunction-contract
  metafunction-case ...)
Defines a metafunction that extends metafunction-id. If metafunction-id serves as the default value for a parameter, then the defined metafunction will serve as the default value of the parameter for language.

syntax

(define-extended-judgment judgment-id language
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
Defines a judgment form that extends judgment-id. If judgment-id serves as the default value for a parameter, then the defined judgment form will serve as the default value of the parameter for language.

syntax

(reduction-out id)

Exports the parameterized reduction relation id and its parameters.

Bound to the current language with the definition of a parameterized reduction relation.