[Redex] Side conditions in Reduction Relations

[Beatriz Moreira]

Hi !

I have a reduction relation where I have to match a pattern ts to two sequences, where the first one contains the other one. What I tried to do was something like this: 

1st seq:  (ts_all1 ... ts ts_all2 ...)     2nd seq:   (ts_x1 ... ts ts_x2 ...),  where ts_x ⊆ ts_all.

But the problem is that with the pattern matching is that ts_x1 doesn't match all elements of ts_all1 .

I'm trying to use side conditions but i can't seem to get it right :c .

Any advice?

Thank you , Beatriz :) 

[Robby Findler]

Is this what you have in mind? 

#lang racket
(require redex/reduction-semantics)

(define-language L
  (ts ::= variable number))

(define-judgment-form L
  #:mode (subsequence I I)
  #:contract (subsequence (ts ...) (ts ...))

  [----------------------------------------------
   (subsequence (ts_1 ...)
                (ts_2 ... ts_1 ... ts_3 ...))])

(test-judgment-holds
 (subsequence () (1 2 3 4)))

(test-judgment-holds
 (subsequence (1) (1 2 3 4)))

(test-judgment-holds
 (subsequence (2) (1 2 3 4)))

(test-judgment-holds
 (subsequence (1 2) (1 2 3 4)))

(test-judgment-holds
 (subsequence (2 3) (1 2 3 4)))

(test-judgment-holds
 (subsequence (3 4) (1 2 3 4)))

(test-judgment-holds
 (subsequence (2 3 4) (1 2 3 4)))

(test-judgment-holds
 (subsequence (1 2 3) (1 2 3 4)))

(test-judgment-holds
 (subsequence (1 2 3 4) (1 2 3 4)))

(test-equal
 (judgment-holds (subsequence (5) (1 2 3 4))) #f)

(test-equal
 (judgment-holds (subsequence (3 2) (1 2 3 4))) #f)

(test-equal
 (judgment-holds (subsequence (4 1) (1 2 3 4))) #f)

(test-results)

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%40googlegroups.com.

[Beatriz Moreira]

Yes, I had to make some adjustments to the judgement you sent me but this helped me a lot!

This was what I ended up using:

(define-judgment-form L

  #:mode (subsequence I I)

  #:contract (subsequence (ts ...) (ts ...))

  [----------------------------------------------

   (subsequence (ts_1 )

                (ts_2 ... ts_1  ts_3 ...))]

  

  [(subsequence (ts_1 ...)

                (ts_2 ... ts_3 ...))

   ----------------------------------------------

   (subsequence (ts_0 ts_1 ...)

                (ts_2 ... ts_0 ts_3 ...))])

Thank you so much! :D

[Robby Findler]

Oh, I see -- you want (1 2 3) to be a subsequence of (1 4 2 4 3 4), for example.

But does your definition allow you to go "backwards"? Maybe you need a helper judgment that captures "a subsequence that starts here"  and then subsequence can try that one at each position?

Robby

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com.

[Beatriz Moreira]

My definition allows it to go backwards because for what im trying to do the order does not matter. So I evaluate the head of the sequence, and then recursively the tail.

I tested your example you gave me just now and it passed :D

Beatriz

[Robby Findler]

You mean it should be a subset, not a subsequence? (And yes, the example I sent was one where I was guessing that mine did not do what you want!)

Robby

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/a2db87c0-ccfa-4a2f-86ed-ce9aac0fe37en%40googlegroups.com.

[Beatriz Moreira]

Yes a subset ! Sorry ! 

Yours didn't do exactly what i wanted but it helped a lot, as i didn't understand how i could also use judgments as guards in reduction relations. 

Thank you again :D

Beatriz Moreira

[Robby Findler]

Ah. And even more it is something like "submultiset" or something, since (term (1 1)) should not be considered a subthingy of (term (1)).

Great!

Robby

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/96aea2ed-4c83-454a-888e-fb605d69687dn%40googlegroups.com.