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