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 <[email protected]> > 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 <[email protected]> >>> 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 < >>>>> [email protected]> 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 [email protected]. >>>>>> To view this discussion on the web visit >>>>>> https://groups.google.com/d/msgid/racket-users/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%40googlegroups.com >>>>>> >>>>>> <https://groups.google.com/d/msgid/racket-users/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>> . >>>>>> >>>>> -- >>>> 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 [email protected]. >>>> >>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- >> 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 [email protected]. >> > To view this discussion on the web visit >> https://groups.google.com/d/msgid/racket-users/a2db87c0-ccfa-4a2f-86ed-ce9aac0fe37en%40googlegroups.com >> >> <https://groups.google.com/d/msgid/racket-users/a2db87c0-ccfa-4a2f-86ed-ce9aac0fe37en%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/96aea2ed-4c83-454a-888e-fb605d69687dn%40googlegroups.com.
