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

From: John Clements (clements at brinckerhoff.org)
Date: Mon Sep 8 14:41:25 EDT 2008

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2484 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20080908/296a78ae/attachment.p7s>

Posted on the users mailing list.