Redex Parameters🔗ℹ

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

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🔗ℹ