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

FWIW, Jonathan Schuster's encoding of NetCore (the Princeton-Cornell theory for routing, last popl) encountered a similar problem. The original paper uses the ChemAM and he encoded it with Redex with "propagated parts of patterns". 

So in general, models based on the Chem AM would be easier to encode in Redex, so perhaps we should look in the literature how they are typeset. 

-- Matthias




On Jun 19, 2012, at 7:08 PM, J. Ian Johnson 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