Re: [racket-users] Order of reduction rules in Redex

[Dupéron Georges]

Le mardi 6 septembre 2016 20:39:37 UTC+2, Sam Caldwell a écrit :
> I'm not sure what it is you want. Do you want the reduction relation to be 
> deterministic? If so then you need to decide which order is the "right" one.
> 
> You can do this by adding a "lifted-less expression" to your grammar

Thanks a lot, Sam, this works like a charm!

I wanted the relation order to be deterministic indeed, but I wasn't sure if it 
was the appropriate solution, or if this was an XY problem that needed a 
completely different approach.

Regards,
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.

Re: [racket-users] Order of reduction rules in Redex

[Sam Caldwell]

I'm not sure what it is you want. Do you want the reduction relation to be
deterministic? If so then you need to decide which order is the "right" one.

You can do this by adding a "lifted-less expression" to your grammar, such
as

(define-extended-language simple+lifted+hole+temp simple+lifted
  ;; elided
  (q v
 number
 (+ q q)))

and then restricting your definitions of contexts:

;; left-to-right
(C hole
 (begin σ ... C σ ...)
 (define v C)
 (+ C e)
 (+ q C))

or

;; right-to-left
(C hole
 (begin σ ... C σ ...)
 (define v C)
 (+ C q)
 (+ e C))

This is basically the same approach as defining a call-by-value lambda
calculus, except instead of values you have
expressions-that-do-not-contain-lifted. This is covered in the Long
Tutorial[1], specifically in section 2.4

[1] https://docs.racket-lang.org/redex/redex2015.html

- Sam Caldwell

On Tue, Sep 6, 2016 at 1:39 PM, Dupéron Georges  wrote:

> 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.
>

-- 
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.

[racket-users] Order of reduction rules in Redex

[Dupéron Georges]

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