[racket-dev] Redex for abstract machines / analysis prototypes

On Wed, Jun 20, 2012 at 7:48 AM, J. Ian Johnson <ianj at 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 <robby at eecs.northwestern.edu>
> To: J. Ian Johnson <ianj at ccs.neu.edu>
> Cc: dev <dev at racket-lang.org>, nam at 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 <ianj at 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