[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