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