A related question is > to ask if maybe the parameter is intended to be so "dyanmic". Maybe > you should have to recompile the redex program to change the parameter > sometimes because, after all, if runs of the abstract machine with > different values of `k` interact with each other, maybe nothing makes > sense. >
Yes, I agree that runs of the abstract machine with different values of ‘k’ should be distinct and disallowed to interact. One thing I do often is interact with the model in the REPL: “Is ‘k = 1’ enough to capture a certain property of this program?” “How about ‘k = 2’?” And so forth. It sounds like having to recompile the model to change the parameter would not be compatible with this kind of exploration, in which case I don’t like the idea. -- 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 [email protected]. For more options, visit https://groups.google.com/d/optout.

