Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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


On Fri, Feb 5, 2021 at 2:18 PM Beatriz Moreira 
wrote:

> 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
>
> A quarta-feira, 3 de fevereiro de 2021 à(s) 22:17:50 UTC, Robby Findler
> escreveu:
>
>> 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
>>
>>
>> On Wed, Feb 3, 2021 at 4:14 PM Beatriz Moreira 
>> wrote:
>>
>>> 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
>>>
>>> A quarta-feira, 3 de fevereiro de 2021 à(s) 18:41:53 UTC, Robby Findler
>>> escreveu:
>>>
 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


 On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira 
 wrote:

> 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
>
> A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler
> escreveu:
>
>> 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)
>>
>>
>>
>> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira <
>> beatriz@gmail.com> wrote:
>>
>>> 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 :)
>>>
>>> --
>>> 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
>>> 
>>> .
>>>

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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

A quarta-feira, 3 de fevereiro de 2021 à(s) 22:17:50 UTC, Robby Findler 
escreveu:

> 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
>
>
> On Wed, Feb 3, 2021 at 4:14 PM Beatriz Moreira  
> wrote:
>
>> 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
>>
>> A quarta-feira, 3 de fevereiro de 2021 à(s) 18:41:53 UTC, Robby Findler 
>> escreveu:
>>
>>> 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
>>>
>>>
>>> On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira  
>>> wrote:
>>>
 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

 A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler 
 escreveu:

> 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)
>
>
>
> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira <
> beatriz@gmail.com> wrote:
>
>> 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 :) 
>>
>> -- 
>> 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
>>  
>> 
>> .
>>
> -- 
 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 
 

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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


On Wed, Feb 3, 2021 at 4:14 PM Beatriz Moreira 
wrote:

> 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
>
> A quarta-feira, 3 de fevereiro de 2021 à(s) 18:41:53 UTC, Robby Findler
> escreveu:
>
>> 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
>>
>>
>> On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira 
>> wrote:
>>
>>> 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
>>>
>>> A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler
>>> escreveu:
>>>
 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)



 On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira 
 wrote:

> 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 :)
>
> --
> 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
> 
> .
>
 --
>>> 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/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com
>>> 
>>> .
>>>
>> --
> 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.
> To view this discussion on the web visit
> 

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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

A quarta-feira, 3 de fevereiro de 2021 à(s) 18:41:53 UTC, Robby Findler 
escreveu:

> 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
>
>
> On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira  
> wrote:
>
>> 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
>>
>> A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler escreveu:
>>
>>> 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)
>>>
>>>
>>>
>>> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira  
>>> wrote:
>>>
 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 :) 

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

>>> -- 
>> 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/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com
>>  
>> 
>> .
>>
>

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

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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


On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira 
wrote:

> 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
>
> A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler escreveu:
>
>> 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)
>>
>>
>>
>> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira 
>> wrote:
>>
>>> 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 :)
>>>
>>> --
>>> 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
>>> 
>>> .
>>>
>> --
> 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.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com
> 
> .
>

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAL3TdOOB-KE3OnF3rHUnYHyGnavSpYR_4QjBhgSFbmDyRGQ4mg%40mail.gmail.com.

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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

A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler escreveu:

> 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)
>
>
>
> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira  
> wrote:
>
>> 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 :) 
>>
>> -- 
>> 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
>>  
>> 
>> .
>>
>

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

Re: [racket-users] [Redex] Side conditions in Reduction Relations

[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)



On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira 
wrote:

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

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAL3TdOMKZrDQ%2BUh0u9bVe6H2dzfS%3DcYDhx26yHSFCb3nzOpJTA%40mail.gmail.com.

[racket-users] [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 :) 

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