Hi all! I'm trying out redex, and I defined a simple language with (define v e) statements. I also defined an extended language, which allows expressions to be (lifted v' e'). A (lifted v' e') expression is replaced by v', and a definition (define v' e') is lifted to the top-level, just before the current statement.
I tried to define a reduction from the simple+lifted language to the simple language. It makes the lifted definitions bubble up until they reach the top-level, and inserts them before their containing statement. Unfortunately, my reduction is ambiguous: when reducing the program (define result (+ (lifted x 1) (lifted y 2))), both lifted definitions can bubble up first and be inserted before the other. Therefore, apply-reduction-relation* returns two valid results: (begin (define x 1) (define y 2) (define result (+ x y))) (begin (define y 2) (define x 1) (define result (+ x y))) How can I avoid this problem? See the attached file or http://pasterack.org/pastes/44574 for the full code. Thanks! Georges Dupéron -- 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+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
lifted-experiment.rkt
Description: Binary data
