On Wed, Jun 20, 2012 at 7:48 AM, J. Ian Johnson <i...@ccs.neu.edu> wrote:
> My papers have been using record notation. Say for lookup:
> s{C = x, E = rho} --> s[C := v, E := rho_0] where rho(x) = (v rho_0)Can you explain this line in a little more detail? > Is this not good enough? I don't think I said it wasn't. Robby > -Ian > ----- Original Message ----- > From: Robby Findler <ro...@eecs.northwestern.edu> > To: J. Ian Johnson <i...@ccs.neu.edu> > Cc: dev <dev@racket-lang.org>, n...@ccs.neu.edu > Sent: Wed, 20 Jun 2012 01:27:18 -0400 (EDT) > Subject: Re: [racket-dev] Redex for abstract machines / analysis prototypes > > I have thought about adding something that would solve this problem to > Redex off and on for a few years and am circling something I think is > reasonable. (The main thing I think you've not considered below is how > to typeset things, but that said I have in mind something similar in > spirit to what you write.) > > Unfortunately, I don't see myself getting to it in the short term (ie > the coming month or two), but your message will definitely move it up > on my list. > > Robby > > On Tue, Jun 19, 2012 at 6:08 PM, J. Ian Johnson <i...@ccs.neu.edu> wrote: >> Machine semantics for real machines (like the JVM or Racket's VM) or >> non-standard semantics for an abstract interpretation (like what I end up >> getting into) can get up to monstrous numbers of components for each state >> that usually don't matter. I and I'm sure many others would appreciate a >> reduction relation language that is a little more like UIUC's K. >> >> Here is a concrete suggestion of what I imagine (some support for patterns >> on hashes): >> 1) Add a pattern (hash (literal pat) ...) to match hashes up to the >> specified keys (hashes with more keys are still accepted). >> 2) Add rewrite rules for changing the current state. >> -- (next-state (r r) ...) >> -- (get r r) >> -- (set r r r) >> -- (set* r (r r) ...) >> Where >> (get r_0 r_1) is ,(hash-ref (term r_0) (term r_1) >> 'something-that-never-matches) >> (set r_0 r_1 r_2) is ,(hash-set (term r_0) (term r_1) (term r_2)) >> (set* r_0 (r_k r_v) ...) is the obvious extension of set, but is annoying to >> write. >> And assuming the LHS is named state, >> (next-state (r_k r_v) ...) is (set* state (r_k r_v) ...) >> >> Not-the-best-example-since-it's-so-minimal: >> >> (define-language CEK >> [e x (e e) lam] >> [lam (lambda (x) e)] >> [rho (hash)] >> [kont mt (ar e rho kont) (fn e rho kont))]) >> >> (define R >> (machine-step CEK >> [--> (hash (C x) (E rho)) >> (next-state (C lam) (E rho*)) >> (where (lam rho*) (get rho x))] >> >> [--> (hash (C (e_0 e_1)) (E rho) (K kont)) >> (next-state (C e_0) (K (ar e_1 rho kont)))] >> >> [--> (hash (C lam) (E rho) (K (ar e rho_0 kont))) >> (next-state (C e) (E rho_0) (K (fn lam rho kont)))] >> >> [--> (hash (C v) (K (fn (lambda (x) e) rho kont))) >> (next-state (C e) (E (set rho x (v rho))) (K kont))])) >> >> (define (inject e) (term (set* #hash() (C ,e) (E #hash()) (K mt)))) >> >> Is this reasonably simple to add to Redex? It would be a very welcome >> addition. >> -Ian >> _________________________ >> Racket Developers list: >> http://lists.racket-lang.org/dev > > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev _________________________ Racket Developers list: http://lists.racket-lang.org/dev
