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/CAL3TdOOy7wBbHUn8m3XF2VPHrVbaRv1Ka-nNHZKwDDgXqVgByQ%40mail.gmail.com.
