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,
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
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
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
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,
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 )
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
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
8 matches
Mail list logo
