racketplt-redex

Can PLT-Redex model these features?

Just starting to learn PLT-Redex... Two questions come up:

  1. Can we use PLT-Redex to model side effects? For example: simple increment construct i++?
  2. What about thread? All the constructs introduced so far does not involve something like creating an thread? synchronization of the thread? is it doable in PLT-Redex (syntax as well as reduction rule?

Thanks in advance,

Solution

  • I'm new to PLT Redex myself, but if no-one else is answering:

    1. Yes: See the “Why PLT Redex?” page, where they give an example using mutable state: http://redex.racket-lang.org/why-redex.html

    2. I should think so, given that the solution they give for 1 seems so general. Your program state would include a number of terms, each of which is the state of one thread. Creating a thread would simply add a new term to the list. Synchronization is trickier, though in principle it should be possible to model the π-calculus in PLT Redex and then you've got all the threading primitives you could want and more. I can't tell you quite yet just what any of this would look like in Redex, but it looks like all the tools are there.