Re: [racket-users] Redex Engine Internals

> I think you want to do this: > (current-cache-all? #t) Thank you, Robby! It mostly solves my problems. BR, Anton Podkopaev 2015-12-04 20:33 GMT+03:00 Robby Findler : > It looks like your semantics has a lot of different ways to reach the > same term (ie the

Re: [racket-users] Redex Engine Internals

>Anyways, here's the model: > https://github.com/ericmercer/4M/blob/master/4M/super_model/super-model.rkt > And here's Fedex: > https://github.com/ericmercer/4M/blob/master/4M/super_model/fedex.rkt Jay, it's really interesting. Thank you! BR, Anton Podkopaev 2015-12-04 20:05 GMT+03:00 Jay

Re: [racket-users] Redex Engine Internals

Thank you for your answer, Robby. Actually at the beginning I planned to implement another version of the semantics in Coq and prove something useful about it. But before spending (a lot of) time with Coq version, it's better to be sure that the semantics is something I want, as you mentioned.

Re: [racket-users] Redex Engine Internals

> One thing to check for is ambiguous patterns. Those can cause > exponential blowup internally in Redex. Yes, there are a lot of ambiguous patterns, but it's made intentionally. Most of the rules have such structure: (--> ((in-hole E operation) globalState) ((in-hole E (ret value))

Re: [racket-users] Redex Engine Internals

Well, maybe there is a bug somewhere; if you're trying to run paper-sized examples you should be able to get them to complete reasonably quickly. One thing to check for is ambiguous patterns. Those can cause exponential blowup internally in Redex. But just to double check: when you run one of

Re: [racket-users] Redex Engine Internals

Hi Anton, It wasn't really designed for general use, but I had a similar problem building a machine for evaluating Java. I made a revised version of Redex (called "Fedex") that removed a lot of features we weren't using (most importantly, evaluation contexts) and I got very good results. I found

Re: [racket-users] Redex Engine Internals

It looks like your semantics has a lot of different ways to reach the same term (ie the reduction graph has a lot of sharing in it). In it's default mode, test-->> (and apply-reduction-relation*) will not notice this sharing and explore all of the different paths, which can be very expensive. I

Re: [racket-users] Redex Engine Internals

Redex isn't really designed with performance in mind. Some future version of Redex will probably improve on this, but perhaps not enough for the use case you have in mind. My best advice (which is kind of depressing that this is the best I can do) is to experiment with the Redex version until

[racket-users] Redex Engine Internals

Hello, dear colleagues! Could you, please, answer some of my questions? 1) Is there any paper about how the Racket engine works? 2) Is there any guide or a paper about effective (in terms of semantics execution) Redex usage? I want to know it because I'm interested in optimizing my semantics in