Formal semantics of PLT Redex

[Mallku Ernesto Soldevila Raffa]

Hi community!,

I'm interested in understanding the semantics of PLT Redex, since we are working on a tool

to translate fragments of Redex models to Coq. At the moment, we just have a

mechanization in Coq of the semantics proposed in a ~10 years old paper [1]. Does

anybody know if there is an updated work on formal semantics of Redex?

Thanks in advance!,
Mallku

[1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27

[Robby Findler]

I think that might be it specifically about redex, I am sorry to say. 

Robby

--
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/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com.

[Mallku Ernesto Soldevila Raffa]

I beg your pardon!, I'm not understanding the answer, what is it that

might be specific of Redex?

I suspect that the answer is that there isn't some recent work on formal

semantics specifically about Redex. In that case, does anybody know if the

already mentioned paper [1] is still a good match for today's semantics of

Redex? The paper provides a mechanization of the model in Redex, together

with some tools to test it. Of interest is a tool that asks Redex to generate

random patterns and terms that match against them, and tests if the

mechanized model is capable of reproducing the matching (or that is what

I suspect that the tests are doing :P ). It was possible to run the mechanization

on a recent version of Redex, but the generated patterns are ill-formed

(e.g., in-hole p1 p2, where p1 contains more than 1 hole). Of course I could

provide more details about the error, but I don't know if it is of interest, it's

a mechanization written for the Redex version that comes with Racket 5.*

or something like that.

Thanks!,

Mallku

[1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27

[Robby Findler]

I'm sorry, my sentence was ambiguous! I'm saying that I don't know of any other work that is specifically focused on the semantics of Redex. (Of course, there may be work I'm not aware of.)

The paper is still a good match, I believe, yes. You're right that the syntactic checks for well-formed grammars have tightened since that era, but if the program is valid, then I think it should match; the underlying algorithms have not changed, only bug fixes have happened.

Of course, if you find that this isn't the case, I'd be very interested to hear more :)

Robby

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com.

[Mallku Ernesto Soldevila Raffa]

Thanks a lot for the info! If I found any mismatches, I'll report it.

Regards,
Mallku

[Mallku Ernesto Soldevila Raffa]

Hi to everyone!,

I'm trying to test the mechanization of Redex's semantics done in [1],

against the present version of racket, 8.3. I'm using the random-match-test.rkt

module from [1] to generate random grammars, patterns and terms, and to test them

using the proposed mechanization of Redex in [1] and the actual implementation of
it, in racket 8.3.

In doing it, I've found an example that I cannot explain in terms of my understanding

of the behavior of the name pattern:

(define-language L [A (name x B)]
                   [B (hole (name x (hole hole)))])

(redex-match L (name x A)
               (term (hole (hole hole))))

The result of the previous match is:

(list (match (list
              (bind 'A '(hole (hole hole)))
              (bind 'x '(hole hole))
              (bind 'x '(hole (hole hole)))
              (bind 'x '(hole (hole hole))))))

Which shows that 'x' is bound to different, non-equivalent, terms. While
I've never used the pattern name explicitly in such a way, while defining
grammars, I'm still curious about what is going on here. Even more, I would
have thought that the following match would return the same result as the
previous:

(redex-match L (name x (name x B))
               (term (hole (hole hole))))

where I just replaced the non-term A by the rhs of its only production, but
what I obtain is:

#f

As a side note, the mechanization of Redex in [1] just returns something
equivalent to:

(bind 'x '(hole (hole hole)))

In both cases. Does anyone understand the behavior of the shown example

under racket 8.3?

Thanks in advance!,

Mallku

[1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27

[Mallku Ernesto Soldevila Raffa]

Just to clarify, I understand that the several binds of x correspond to
the several patterns name in the productions, and the pattern against with
we are matching, but I would have expected for the firsts to be discarded,

or, if still considered in the resulting match for some reason, that I don't

know, I would have expected for the application of the constraint of names,

that would have rendered #f the match.

thanks!,

Mallku

[Robby Findler]

There was a bug in the matcher; I've pushed a fix.

With that fix, you'll get

(list
 (match
  (list
   (bind 'A '(hole (hole hole)))

   (bind 'x '(hole (hole hole))))))

as the result. That's different than the matcher because the pattern `A` is really shorthand for something like `(name A (nt A))`, where the `name` part introduces the name and the `nt` pattern matching construct matches only non-terminals without binding a name.

Thanks for finding the bug!

Robby

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1d7cb5b7-d7c2-44a7-b513-bb8280a54f13n%40googlegroups.com.

[Mallku Ernesto Soldevila Raffa]

Wow!, that was fast!
No need to thank, I'm just using your awesome tool to perform random testing.
Thanks,
Mallku

El martes, 21 de diciembre de 2021 a las 18:22:09 UTC-3, Robby Findler escribió:

There was a bug in the matcher; I've pushed a fix.

With that fix, you'll get

(list
 (match
  (list
   (bind 'A '(hole (hole hole)))

   (bind 'x '(hole (hole hole))))))

as the result. That's different than the matcher because the pattern `A` is really shorthand for something like `(name A (nt A))`, where the `name` part introduces the name and the `nt` pattern matching construct matches only non-terminals without binding a name.

Thanks for finding the bug!

Robby