Redex - constraining what is used to fill a hole

[Sam Caldwell]

Hi,

I'm working on a redex model where I want to constrain the shape of terms used

to fill the hole in an evaluation context. I thought it would be fairly

straightforward to do so using a `with` clause in my reduction-relation, but

I've run into some difficulty, and consulting the docs [1] left me unsure of

where I went wrong.

In the docs for `reduction-relation`, the old-arrow-name clause of shortcuts

are defined in terms of patterns and terms. However, the docs later say "The

left- and right-hand sides of a shortcut definition are identifiers, not

patterns and terms." I don't understand what is and is not allowed when using

shortcuts.

I have a small model that I think illustrates what I'm after. Say I have a

tiny addition language but for some reason I want to restrict reduction to

two-argument terms:

==================================================================

#lang racket

(require redex)

(define-language add

  (M (+ M ...) V)

  (V natural)

  (Add2 (+ V V))

  (E hole (+ V ... hole M ...)))

(define red

  (reduction-relation

   add

   (==> (+ V ...)

        ,(apply + (term (V ...)))

        +)

   with

   [(--> (in-hole E Add2) (in-hole E n))

    (==> Add2 n)]))

==================================================================

This does not behave as I would have expected, for example reducing

`(term (+ 1 2 (+ 3 4) 4 (+ 0 1)))` down to `15`.

It seems like the issue is that `Add2` in the shortcut is not being used as a

pattern. For example, if I replace `Add2` with its definition:

[(--> (in-hole E (name x (+ V V))) (in-hole E n))

    (==> x n)]

I get the following error message:

free-identifier=?: contract violation

  expected: identifier?

  given: #<syntax (name x any_2)>

  argument position: 2nd

  other arguments.:

So my question boils down to:

1) What is/is not allowed in each position when defining a shortcut?

2) How can I constrain what is used to fill a hole, as attempted in my example?

Thanks,

Sam Caldwell

[1] http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._reduction-relation%29%29

[Robby Findler]

I can see why you might have expected that to work that way.
Unfortunately, it doesn't. The identifiers in those places in
shortcuts (Add2, x, and n in your examples below) are not pattern
positions. They are simply identifiers.

In the code you wrote, one could change the rule's left-hand side to
(+ V_1 V_2) to achieve the desired effect, but maybe that doesn't work
in your larger model? Perhaps if you explained a little more why
something like that is problematic, we could be of more use.

Meanwhile, I've pushed a fix to the bug in the error-checking that you
found, added some more checking, and tried to emphasize this point
more clearly in the documentation. The commit cbb2d88b would probably
have been the most helpful to you, but it's backwards incompatible, so
it may need to be reverted.

Robby

> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Sam Caldwell]

Thanks for clarifying, Robby.

I'm modeling reduction on nested states. In addition to a collection of

straightforward rules, there is a rule that specifies when to reduce a

state-inside-a-state. I can specify this using evaluation contexts, but in

order for the relation to remain deterministic I need to restrict which

nested-states are reduced to a particular subclass.

I'm hoping this little model demonstrates what I'm trying to do:

==================================================================

#lang racket

(require redex)

(define-language L

  (State (number

          (Event ...)  ;; "incoming" events

          (Event ...)  ;; "outgoing" events

          (State ...)))

  (Event string)

  ;; states with no outgoing events

  (State-Q (number

            (Event ...)

            ()

            (State ...)))

  ;; states with no incoming or outgoing events

  (State-I (number

            ()

            ()

            (State ...)))

  ;; Evaluation Contexts

  (E hole

     (number

      ()

      (Event ...)

      (State-I ... E State-Q ...))))

(define red

  (reduction-relation

   L

   ;; incoming events just increase a counter

   (--> (number

         (Event_0 Event_n ...)

         (Event ...)

         (State ...))

        (,(add1 (term number))

         (Event_n ...)

         (Event ...)

         (State ...))

        handle)

   ;; once a State has processed all of its incoming Events, it can receive an

   ;; outgoing Event from nested States.

   (--> (number

         ()

         (Event_out ...)

         (State-Q ...

          (number_s

           (Event_si ...)

           (Event Event_so ...)

           (State_s ...))

          State ...))

        (number

         (Event Event_so ...)

         (Event_out ...)

         (State-Q ...

          (number_s

           (Event_si ...)

           ()

           (State_s ...))

          State ...))

        receive)))

#|

Want this to result in:

'((5 () () ((4 () () ()) (4 () () ()))))

|#

(apply-reduction-relation*

 red

 (term (0 ()

          ()

          ((1 ("hi" "hello" "ciao")

              ("zip" "zap" "zooey")

              ())

           (2 ("where" "fore")

              ("art" "thou")

              ())))))

==================================================================

That model allows the top-most State to process incoming Events and receive

Events from its direct children. But, I also want child States to reduce using

the same rules. To keep my relation deterministic, I only want to step child

States that are also State-Q's. This is how I ended up trying to add a

shortcut like:

[(--> (in-hole E State-Q) (in-hole E State))

 (==> State-Q State)]

I was able to get the behavior I want by calling apply-reduction-relation from

inside a rule:

(--> (in-hole E State-Q)

     (in-hole E State)

     (side-condition (not (redex-match? L hole (term E))))

     (where (State) ,(apply-reduction-relation red (term State-Q))))

But I can't say I felt great about doing so. (The side-condition is needed to

prevent infinite looping). Is there a cleaner way to achieve the same result?

Thanks,

Sam Caldwell

[Robby Findler]

I'm not completely following the design goals here because it seems
like the desire to reduce only State-Qs could be achieved by writing
rules that reduced only State-Qs (not arbitrary states). Or are you
saying that State-Qs are only allowed in the context? If so, then you
could write E differently? I think that all of this is expressible
without using a feature like you want in Redex, but I'm not really
getting precisely what you want so I'm hesitant to make more concrete
suggestions.

Regardless, if for some reason it is better to express your rewriting
relation in the way that has actual premises, then you could rewrite
it using define-judgment-form. Relations defined with
define-judgment-form that have the mode (I O) or (O I) can be used
with 'traces' and 'stepper' (as well as show-derivations).

hth,
Robby

[Sam Caldwell]

> I'm not completely following the design goals here because it seems

> like the desire to reduce only State-Qs could be achieved by writing

> rules that reduced only State-Qs (not arbitrary states). Or are you

> saying that State-Qs are only allowed in the context? If so, then you

> could write E differently?

I don't think I can constrain the rules to only operate on State-Qs

because the *outermost* State needs to reduce, and it does not need to

be a State-Q. I think this would lead to duplicating all of the

reduction rules; once for the outermost State and once for internal

State-Qs.

It's not clear to me how I would change the definition of E to achieve this.

> you could rewrite it using define-judgment-form

This seems fairly promising - looking at the docs I don't see any

reason define-judgment-form couldn't do what I want in a

straightforward manner.

Thanks for the help,

Sam Caldwell

[Robby Findler]

On Sunday, December 13, 2015, Sam Caldwell <sa...@ccs.neu.edu> wrote:

> I'm not completely following the design goals here because it seems

> like the desire to reduce only State-Qs could be achieved by writing

> rules that reduced only State-Qs (not arbitrary states). Or are you

> saying that State-Qs are only allowed in the context? If so, then you

> could write E differently?

I don't think I can constrain the rules to only operate on State-Qs

because the *outermost* State needs to reduce, and it does not need to

be a State-Q. I think this would lead to duplicating all of the

reduction rules; once for the outermost State and once for internal

State-Qs.

Oh I see. You could probably refactor your language grammar to avoid this but if define-judgment-form is a better fit then by all means do that.