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

That line is how I would render the lookup rule for the CEK machine (in the below example).
I actually use \equiv to match structure instead of = in this LHS:

s{C \equiv x, E \equiv rho}

That is, I say that for whatever is in C, there exists an x of the type of x's nonterminal (in this case variable-not-otherwise-mentioned) such that C = x. This kind of implicit quantification is not always necessary. Indeed, others might lift the existential quantification over the entire reduction relation definition and make them universal. That said, I think that a visual distinction between matching and rewriting is important.

And I use braces to note selection of multiple fields. For a single field (let's say E), I would say

s.E

This selection is also written a different way in some texts (indeed in a draft I've written) as

E_s

Though cascading nesting leads to vanishingly small notation. I thus abandoned that notation.

As for the RHS, I use brackets and := to note substitutions. Usual substitution notation like e[v/x] has been ambiguous across texts (are we substituting v for x or x for v?) and its extension to many substitutions is also comma separated. Seeing as a field of a record should not be considered an identifier, lambda calculus-style substitution notation makes less sense.

As for the "rho(x)" in the "where" clause, I treat finite maps as primitive in most of by machines, and I lament having to escape to hash-ref or hash-set. Thus I suggested a special form for environment look-ups and functional extension. In fact that reminds me of another piece of notation I use.

Suppose I have a starting store sigma, and I construct what I see as the extension to sigma due to many allocations in one step, sigma'. To denote the store that is sigma with all mappings of sigma' preferred before going to sigma, I write

sigma \triangleleft sigma'

I would also want to override that notation, since when I move to an abstract interpretation, that would become a join,

sigma \sqcup sigma'

This is just how I note such record/environment manipulations. I would be interested if any other heavy users of Redex for machine semantics have a different opinion.

-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: Wednesday, June 20, 2012 9:20:35 AM GMT -05:00 US/Canada Eastern
Subject: Re: [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