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 <beatriz.smore...@gmail.com> 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 <beatriz....@gmail.com> >> 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 >>>>> <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 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 >>> <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 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 > <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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdOOy7wBbHUn8m3XF2VPHrVbaRv1Ka-nNHZKwDDgXqVgByQ%40mail.gmail.com.
