[plt-scheme] redex question: use ordering to force determinism?

From: Robby Findler (robby at cs.uchicago.edu)
Date: Mon Sep 8 14:42:58 EDT 2008

There is no way to do that, sorry. (metafunctions do have that property, tho)

Robby

On Mon, Sep 8, 2008 at 1:41 PM, John Clements <clements at brinckerhoff.org> wrote:
> Redex is designed to handle one-to-many reduction relations gracefully.  Is
> there some way to squelch this and specify that only the first applicable
> rule is to be used?  That is, I would like to implicitly quantify each
> reduction rule with a side-condition that specifies that none of the
> textually earlier rules match.
>
> My conjecture is that no such mechanism exists, because the beginner.ss
> example includes things like this:
>
>  ((symbol=? 'x_1 'x_2) . ==> . ,(if (eq? (term x_1) (term x_2)) (term true)
> (term false)))
>   ((side-condition (symbol=? v_1 v_2)
>                    (or (not (and (pair? (term v_1))
>                                  (eq? (car (term v_1)) 'quote)))
>                        (not (and (pair? (term v_2))
>                                  (eq? (car (term v_2)) 'quote)))))
>    . e==> .
>    "symbol=?: expects argument of type <symbol>")
>
>
> ... yikes!
>
> Is there some reason not to allow relations to be ordered in this way?  Am I
> missing some newer feature?
>
> Many thanks,
>
> John
>
>
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
>


Posted on the users mailing list.