[plt-scheme] redex question: use ordering to force determinism?
Then they wouldn't be relations, no?
On Mon, Sep 8, 2008 at 2: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
>
>