> 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? >
When defining metafunctions/reduction relations/judgment forms and so on, authors generally say something to the effect of “this forms a family of analyses parameterized over a choice of ‘k’; we may elide ‘k’ where it’s implicit.” Alternatively, sometimes ‘k’ appears as a sub/superscript on the metafunction name, for example, ‘firstₖ(list)’. In this case, the role of ‘k’ as a parameter is more evident, but it’s special, justifying the special notation and sometimes even omission. Then, to parameterize ‘k’, I can show you one example from the same line of research I cited in the original message: Gilray, Thomas, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. 2016. “Pushdown Control-Flow Analysis for Free.” In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 691–704. POPL ’16. New York, NY, USA: ACM. https://doi.org/10.1145/2837614.2837631. I also have a couple from my own work, which are even more explicit: > 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. > That’s half-way there, yes. But it wouldn’t hurt to have a ‘parameterize’ form that percolates a different value through the rest of the model, like a dynamically bound variable. Say we’re developing a adaptive analysis that tweaks ‘k’ according to some policy: ‘my-policyₖ(…) = firstₖ₊₁(…) if condition-holds’. Now all forms called by ‘first’ have access to the new ‘k+1’. Aside: I know this special typesetting of ‘k’ can be accomplished with rewrite rules for ‘lw’. That’s beyond my concern: I’m interested in being able to *elide* ‘k’ when it doesn’t matter. > > 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? > Hmmm, clunckyness for clunckyness I think I’d prefer to bite the bullet and thread ‘k’ instead of extending all my definitions. -- 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.
