Can PLT-Redex model these features?

StackOverflow https://stackoverflow.com/questions/17642316

  •  03-06-2022
  •  | 
  •  

Question

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,

Was it helpful?

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.

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top