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 <[email protected]> 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 <[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 > <https://groups.google.com/d/msgid/racket-users/96aea2ed-4c83-454a-888e-fb605d69687dn%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/CAL3TdOOu9u0mPu%2Bj_RY5-5nDBrym9Y-D3sf6vokarcHqfbdhbw%40mail.gmail.com.
