[racket] Redex Reduction rule

This rule:

(--> (⊕ Q_1 ... b_1 Q_2 ... b_2 Q_3 ... ((⊕ b_1 b_2) ≺ e) Q_4 ...)
     (⊕ Q_1 ... Q_2 ... e Q_3 ... Q_4 ...))

should allow the reduction you describe below (I didn't test it(!)),
but I'm not sure that it is the rule you really want.

Specifically, this rule requires the b_1 and b_2 to be before the ((⊕
b_1 b_2) ≺ e) in the sequence, and it also requires b_1 to appear
before b_2.

If you want to allow these to reduce regardless of the order they
appear, then you'd need either more rules that cover all the possible
orderings, or you would need some rules that normalize the order. In
other words, Redex doesn't support associative commutative matching,
which is what I guess you'd really want here.

Improving this is on the list of things to do with Redex, but I don't
have an improvement waiting in the wings yet, I'm sorry to say.

hth,
Robby

On Mon, Oct 1, 2012 at 9:48 AM, David Delfieu
<david.delfieu at univ-nantes.fr> wrote:
> Hello,
>
> I have bought the book on Redex, but i am still in difficulty on the following point :
>
> - I have defined a grammar describing processus (obtained from the unfolding of Petri nets).
> - I am blocked on the definition of a firing rule allowing to fire an event e_i when a set of condition ⊕ b_1 b_2 ... is present.
>
> (define-language Process-lang
>   [n variable bool b e (¬ n)] ; node
>   [bool t f] ; boolean
>   [e variable (¬ e)] ; event
>   [b variable (¬ b)] ; condition
>   [on ⊕ ⊥]  ; n-nary operators (building operator and exclusion)
>   [o2 ≺]  ; binary operators (causality)
>
> ; process
>  [P variable (⊕ Q ... )]
>   [Q variable P n]
>   [C-P (⊕ C-P P) (⊕ P C-P) hole]
>
> ; Conflicts
>  [X variable (⊥ Y ... )]
>   [Y variable X n ]
>   [C-X (⊥ C-X P) (⊥ P C-X) hole]
>
> ; Expression
>   [E variable (on F ...) (b o2 e) (P o2 X)]
>   [F variable E P ]
>   [C-E (on C-E E) (on E C-E) (E o2 C-E) (C-E o2 E) hole]
> )
>
> (define Process-red
>   (reduction-relation
>    Process-lang
>
> ...
>
>  (--> (in-hole C-E (⊕ b_1  ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...))
>        (in-hole C-E  ( ?????.....?????? ?) "Caus_1"))
> ....
>
> I want to find a rule allowing to reduce
>
>
> (⊕
>  b_4
>  b_2
>  b_3
>  (b_2 ≺ (⊥ e_3 e_2))
>  (e_2 ≺ b_6)
>  (e_6 ≺ b_7)
>  (b_7 ≺ e_7)
>  (e_4 ≺ b_5)
>  (b_5 ≺ e_5)
>  (b_3 ≺ (⊥ e_4 e_6))
>  ((⊕ b_3 b_6) ≺ e_6)
>  ((⊕ b_3 b_4) ≺ e_4))
>
>
> IN
>
> (⊕
>  e_4
>  b_2
>  (b_2 ≺ (⊥ e_3 e_2))
>  (e_2 ≺ b_6)
>  (e_6 ≺ b_7)
>  (b_7 ≺ e_7)
>  (e_4 ≺ b_5)
>  (b_5 ≺ e_5)
>  (b_3 ≺ (⊥ e_4 e_6))
>  ((⊕ b_3 b_6) ≺ e_6)
>  )
>
>
> b_3 and b_4 have been used to produce e_4
>
> Respectuously,
>
>
> (joined the entire files)
>
>
> *******************************************************
> David Delfieu, tel : 02 40 90 50 45
> EC à Polytech'Nantes - Département Génie Électrique
> Site de Gavy, 44603 Saint Nazaire Cedex
> Chercheur à L'IRCCyN
> *******************************************************
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>