Stepping back a little bit here, if you were to write this down in a way that were to make sense to a reader of a paper, how would you communicate with them how/when this parameter changes?
I think we've already agreed that one can think of the entire paper and its development having exactly one choice of `k` made at the very beginning, and I think we agree Redex can support that using something like define-term (so you have to click "run" to change the parameter). That clearly has some advantages because you never conflate two parts of the model that come with different values of `k`. That said, it is pretty clunky. Here is a second idea: what if you did this: (define-language L (k ::= 1) ...all the other stuff...) and we tweaked Redex in some way so that definitions like that could be used not just in pattern positions, but also in term positions (since there is only only possibility for `k`, after all). THEN, with that definition we could use define-extended-language and define-extended-metafunction and friends to change the value of `k`. This has its own clunkyness, but it is a clunkyness that we have seriously thought about and for which there are plans to do better (basically designing a module system for Redex). Is this a fruitful path to follow? Robby On Thu, Mar 15, 2018 at 8:22 AM, 'Leandro Facchinetti' via Racket Users <[email protected]> wrote: > >> > 1. The cache for the reduction relation is invalid. >> >> >> How so? > > > > (apply-reduction-relation go (term a)) ;; => (the clock is 96) > (apply-reduction-relation go (term a)) ;; => (the clock is 99) > > The user hasn’t changed any parameters, but the results are different. The > second call didn’t go through the cache as it was supposed to. > >> > 2. There’s no way to parameterize ‘clock’ when calling the reduction >> > relation (I think it’d really help to think of ‘k’ instead of ‘clock’). >> >> >> That’s what #:initial gives you. > > > No, ‘#:initial’ let’s you parameterize ‘clock’ when *defining* the reduction > relation (‘r-r/tick’), not when *calling* it (‘traces’, > ‘apply-reduction-relation’ and friends). > >> >> > 3. ‘clock’ isn’t available to metafunctions called from the reduction >> > relation. >> >> >> Give me an example. > > > Sure. Let the reduction relation depend on the metafunction > ‘my-metafunction’, which uses ‘clock’: > > #lang racket > > (require redex) > (require (for-syntax syntax/parse)) > > (define-syntax (r-r/tick stx) > (syntax-parse stx > [(_ PL #:domain x #:initial go #:observe o #:update u ((~literal -->) > lhs rhs) ...) > #'(let ((clock (go))) > (reduction-relation > PL > #:domain x > (--> lhs rhs (where _ ,(begin (set! clock (u clock)) (o clock)))) > ...))])) > > ; > ----------------------------------------------------------------------------- > > (define-language X > (e ::= a b c)) > > (define-metafunction X > [(my-metafunction _) clock]) ;; <= ‘clock’ is just a symbol here, not a > bound (meta-)variable > > (define go > (r-r/tick > X > #:domain e > #:initial (lambda () (random 100)) > #:observe (lambda (clock) (displayln `(the clock is ,clock))) > #:update (curry + 3) > (--> a b) > (--> b (my-metafunction c)) > (--> c a))) > > (traces go (term a)) > > > > > * * * > > The point I’m bringing up is “Parameterized Redex models,” which I don’t > think is exactly the “state monad.” I guess I could hack my way with the > state monad if that’s all I had, but it’s too big a hammer because the > “state” never changes throughout a series of steps. Coming back to the > original example of ‘tick’, I’m not interested in abstracting time-stamp > tracking from the abstract machine (CESKₜ); I’m interested in abstracting > the implicit variable ‘k’ from the *abstract* abstract machine (CESKₜ^). I > choose ‘k’ before I start the machine, and then it remains constant > throughout evaluation. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
