Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
> On Nov 9, 2019, at 09:18, Jay McCarthy wrote: > > "remember that an evaluation context is just a way of describing more > succinctly what you could otherwise define by hand as a big, > complicated relation on individual terms." Yes, that makes sense — I wasn’t really considering what it would look like to define these rules without evaluation contexts until you mentioned that in your first email. They’re a very nice way of thinking about these things, though! I’m not sure if it is worth it to me right now to go to the effort to define the “big, complicated relation” in this particular case just to get an executable version of the rules I’ve written down with pen and paper, but maybe it would be a good exercise; I don’t know. > There is nothing special about evaluation contexts. I think they are > beautiful, but they don't, for example, automatically come with a set > of free theorems, like monads. The best thing they have going for them > is that they decouple the specification of evaluation rules and where > those rules occur (i.e. there are no "congruence" rules in the > reduction relation.) But, a reduction system can always have extra > rules that don't use them, so you don't get anything "for free". It is > possible that the thing you want can't be done using contexts, but > that doesn't mean redex or even redex's reduction-relation is wrong > tool to use. > > That said, I don't think the idea of a "first-class" context or > evaluation rule makes sense, because the whole point of a proof theory > is to have a fixed set of proof schemas which you can reason about. If > you want to take term data and turn that into new rule cases, then > you'll have to have a more general rule that inspects the term data > and acts on it. For example, if you wanted your term data to be able > to cause evaluation anywhere, then one technique would be to by > default have evaluation happen everywhere, but then the evaluation > rule will inspect the context to see if evaluation is enabled in any > specific case. I think that makes sense from an implementation > perspective too. I should be clear: the main reason I decided to think about this in terms of reduction rules defined using evaluation contexts in the first place is because I didn’t even know what I thought the system I was trying to build ought to do in the edge cases. Writing down rules in terms of evaluation contexts has been an exercise in figuring out what I think the system I’m building means, and specifically, it is an attempt to find a system that reflects the equational reasoning rules I already intuitively believe ought to hold. From that perspective, the “expressive power” of evaluation contexts is precisely what appeals to me — it makes it easier to sketch out variations on the rules I have and see how they interact with one another. I don’t think the set of rules I have is directly useful for either proving things about my effect system or actually practically implementing it. I just don’t know how to express some of the more complicated interactions I’m thinking about (such as, for example, distributivity of the continuation over nondeterministic choice) more clearly and simply than with evaluation contexts. If the takeaway here is that I am better served doing that with pen and paper, and maybe putting something in Redex once I have a firmer grasp on what I actually want to model, that’s fine; it’s helpful to know. > Maybe not useful, but I believe that delimited control was really made > by Matthias to solve the same problem as algebraic effects are solving > today. Read his papers again in that light and it may be helpful. Thanks, I will certainly do so. I read a couple of them several years ago when I was first learning about delimited control, but I think you’re right I would benefit from looking at them again. (Algebraic effects are appealing to me not because of their expressive power necessarily but because of certain implementation advantages, especially in a typed setting, but it is quite clear that they have an intimate relationship with delimited control. I could do to be more familiar with that literature.) Alexis -- 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/D19B5D53-7D2B-4513-820C-989F57B0727C%40gmail.com.
Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
That is an interesting idea. I want to emphasize this point again:
"remember that an evaluation context is just a way of describing more
succinctly what you could otherwise define by hand as a big,
complicated relation on individual terms."
There is nothing special about evaluation contexts. I think they are
beautiful, but they don't, for example, automatically come with a set
of free theorems, like monads. The best thing they have going for them
is that they decouple the specification of evaluation rules and where
those rules occur (i.e. there are no "congruence" rules in the
reduction relation.) But, a reduction system can always have extra
rules that don't use them, so you don't get anything "for free". It is
possible that the thing you want can't be done using contexts, but
that doesn't mean redex or even redex's reduction-relation is wrong
tool to use.
That said, I don't think the idea of a "first-class" context or
evaluation rule makes sense, because the whole point of a proof theory
is to have a fixed set of proof schemas which you can reason about. If
you want to take term data and turn that into new rule cases, then
you'll have to have a more general rule that inspects the term data
and acts on it. For example, if you wanted your term data to be able
to cause evaluation anywhere, then one technique would be to by
default have evaluation happen everywhere, but then the evaluation
rule will inspect the context to see if evaluation is enabled in any
specific case. I think that makes sense from an implementation
perspective too.
Maybe not useful, but I believe that delimited control was really made
by Matthias to solve the same problem as algebraic effects are solving
today. Read his papers again in that light and it may be helpful. I
have a series of blog posts from 2012 that attempt to explain this
perspective [1] through [2] and this is how my DOS package works [3].
DOS makes this really explicit because the state outside of the
handlers is specified as a monoid that combines the effects from each
of the contexts that can create effects.
Jay
1. https://jeapostrophe.github.io/2012-06-18-pipe-post.html
2. https://jeapostrophe.github.io/2012-07-12-cont-sys-post.html
3. https://docs.racket-lang.org/dos/index.html
--
Jay McCarthy
Associate Professor @ CS @ UMass Lowell
http://jeapostrophe.github.io
Vincit qui se vincit.
On Sat, Nov 9, 2019 at 7:30 AM Alexis King wrote:
>
> Hi Jay,
>
> I appreciate your pointers! However, I think either I didn’t make my question
> clear enough, or I misunderstand your explanation (or perhaps some of both).
>
> What I am trying to model is, indeed, a form of delimited control. I have
> already written a model that supports a couple classic control operators,
> namely exception handling and nondeterminism, plus some of the simpler
> algebraic operations from the algebraic effects literature such as mutable
> state. However, this isn’t quite sufficient for what I’m trying to do, as
> effect systems allow the programmer to define those kinds of control
> operators using more general primitives in the host language.
>
> Here’s an example of what an effect definition and an effect handler might
> look like in a hypothetical language that supports algebraic effect handlers:
>
> effect Error e where
> throw :: e -> a
>
> handleError :: (() ->{Error e} a) -> Either e a
> handleError f =
> handle Error where
> throw e _k = Left e
> in Right (f ())
>
> You can reasonably think of `effect` and `handle` in terms of delimited
> control. Each `effect` declaration declares a new prompt tag, and each
> operation of the effect aborts, passing its current continuation to the
> prompt handler. Likewise, each `handle` declaration installs a new prompt
> with the appropriate tag and handler. (In the above example, `throw` discards
> the continuation and simply returns.)
>
> This interpretation works well enough for algebraic effects, but this makes
> it impossible to support operations like `catch`, or `cut` (for some kind of
> backtracking effect) forcing them to be handlers instead. This turns out to
> cause trouble in practice., so some newer work handles so-called “scoped”
> effects as well, which support “scoping” operations like `catch` and `cut`. I
> have been working on an implementation of a scoped effect system in Haskell,
> but I have found many edge cases where the behavior of current systems
> produces nonsensical results given certain handler compositions.
>
> Fortunately, I have found that it is possible to produce a significantly more
> predictable semantics for scoped effect handlers by viewing them as kind of
> like “first class reduction rules.” A handler for an Error effect supporting
> both `throw` and `catch` can be expressed using the following three reduction
> rules:
>
> E[handleError v] -> E[Right v]
> E_1[handleError E_2[throw v]] -> E_1[Left v]
> E_1[handleError E_2[catch e v]] ->
> E_1[hand
Re: [racket-users] Evaluating to get the output with a specific lang
Modules don't evaluate to values. They have effects and they have exported symbols. If you want to observe the evaluation of your language's module, you'll have to look at one of those two things. Both are used by existing Racket languages and infrastructure: `raco test` relies on test modules making effects on a global box that counts how many tests ran and failed. `scribble` relies on inspecting an export named `doc`. In either case, I think you want to make `#%module-begin` capture the last expression and expose its value via an effect or an export. Jay -- Jay McCarthy Associate Professor @ CS @ UMass Lowell http://jeapostrophe.github.io Vincit qui se vincit. On Sat, Nov 9, 2019 at 9:54 AM Christopher Lemmer Webber wrote: > > (Caveat: I know the sandbox evaluator exists. I'm trying to understand > how to do this without it, to understand the evaluation machinery for > something.) > > Let's say I write "#lang foo". For whatever reason, I have programs > that are coming in from users that are not necessarily being saved > to a file on disk... they may be coming from a GUI, read over the > network, etc etc. The only important thing is that at the end of the > program, the last expression returns some value, and I want access to > that value. Simplest example, let's say we have the following program > > ``` > #lang foo > > (define bar 1) > > (+ bar 2) > ``` > > I'd like to read this in and evaluate it, so presumably I'd want to get > 3 returned. > > I've tried to figure out how to do this from trivial examples but I'm > not having success. I can see that I can read in a module: > > ``` > racket-sandbox.rkt> (parameterize ([read-accept-reader #t]) > (call-with-input-string "#lang racket/base > (+ 1 2)" > (lambda (ip) > (read-syntax 'foo ip > # 2)))> > ``` > > Cool, ok. > > But when I pass this module-wrapped structure to eval, the result is void. > > What should I do? Help appreciated! > > -- > 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 racket-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/8736exhzh8.fsf%40dustycloud.org. -- 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAJYbDak7zwYp8gCW2zA%2B3hNGLLqr3tjRks7bO47X0st94s0Hiw%40mail.gmail.com.
[racket-users] Evaluating to get the output with a specific lang
(Caveat: I know the sandbox evaluator exists. I'm trying to understand how to do this without it, to understand the evaluation machinery for something.) Let's say I write "#lang foo". For whatever reason, I have programs that are coming in from users that are not necessarily being saved to a file on disk... they may be coming from a GUI, read over the network, etc etc. The only important thing is that at the end of the program, the last expression returns some value, and I want access to that value. Simplest example, let's say we have the following program ``` #lang foo (define bar 1) (+ bar 2) ``` I'd like to read this in and evaluate it, so presumably I'd want to get 3 returned. I've tried to figure out how to do this from trivial examples but I'm not having success. I can see that I can read in a module: ``` racket-sandbox.rkt> (parameterize ([read-accept-reader #t]) (call-with-input-string "#lang racket/base (+ 1 2)" (lambda (ip) (read-syntax 'foo ip # ``` Cool, ok. But when I pass this module-wrapped structure to eval, the result is void. What should I do? Help appreciated! -- 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/8736exhzh8.fsf%40dustycloud.org.
Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
I am not sure how the details work out but I guess Jay's advice of writing
a judgement form that shows how terms reduce is the right thing (and that
judgment form may or may not use context decomposition patterns).
Robby
On Sat, Nov 9, 2019 at 6:31 AM Alexis King wrote:
> Hi Jay,
>
> I appreciate your pointers! However, I think either I didn’t make my
> question clear enough, or I misunderstand your explanation (or perhaps some
> of both).
>
> What I am trying to model is, indeed, a form of delimited control. I have
> already written a model that supports a couple classic control operators,
> namely exception handling and nondeterminism, plus some of the simpler
> algebraic operations from the algebraic effects literature such as mutable
> state. However, this isn’t quite sufficient for what I’m trying to do, as
> effect systems allow the programmer to define those kinds of control
> operators using more general primitives in the host language.
>
> Here’s an example of what an effect definition and an effect handler might
> look like in a hypothetical language that supports algebraic effect
> handlers:
>
> effect Error e where
> throw :: e -> a
>
> handleError :: (() ->{Error e} a) -> Either e a
> handleError f =
> handle Error where
> throw e _k = Left e
> in Right (f ())
>
> You can reasonably think of `effect` and `handle` in terms of delimited
> control. Each `effect` declaration declares a new prompt tag, and each
> operation of the effect aborts, passing its current continuation to the
> prompt handler. Likewise, each `handle` declaration installs a new prompt
> with the appropriate tag and handler. (In the above example, `throw`
> discards the continuation and simply returns.)
>
> This interpretation works well enough for algebraic effects, but this
> makes it impossible to support operations like `catch`, or `cut` (for some
> kind of backtracking effect) forcing them to be handlers instead. This
> turns out to cause trouble in practice., so some newer work handles
> so-called “scoped” effects as well, which support “scoping” operations like
> `catch` and `cut`. I have been working on an implementation of a scoped
> effect system in Haskell, but I have found many edge cases where the
> behavior of current systems produces nonsensical results given certain
> handler compositions.
>
> Fortunately, I have found that it is possible to produce a significantly
> more predictable semantics for scoped effect handlers by viewing them as
> kind of like “first class reduction rules.” A handler for an Error effect
> supporting both `throw` and `catch` can be expressed using the following
> three reduction rules:
>
> E[handleError v] -> E[Right v]
> E_1[handleError E_2[throw v]] -> E_1[Left v]
> E_1[handleError E_2[catch e v]] ->
> E_1[handleError E_2[
> case handleError e of
> Right a -> a
> Left b -> v b]]
>
> However, doing this also requires extending the definition of E itself so
> that reduction may proceed into the appropriate locations:
>
> E ::= ... | throw E | catch e E | handleError E
>
> Therefore, this encoding of scoped handlers requires that they operate at
> the level of the metalanguage, which is not enough — I want to come up with
> a model that pushes the above expressive power into the language by
> defining appropriately general-purpose `effect` and `handler` syntactic
> forms.
>
> It is possible that what you are telling me is I should not bother, and
> instead I should try to define a translation from my higher-level language
> into something simpler to actually implement, such as some well-known model
> of delimited control. However, the reason I have been hoping to avoid doing
> that is I think the translation is not as straightforward as it seems, and
> the main reason I want to model the higher-level interface directly is to
> better understand how I think it ought to work before I try and define a
> translation into something else (probably delimited continuations or
> monads).
>
> Does that help to give a little more context? I was trying not to drag too
> much of it in when writing my original email, but it’s possible that in
> doing so I omitted too much. :)
>
> Alexis
>
> > On Nov 9, 2019, at 04:53, Jay McCarthy wrote:
> >
> > First, any inductive definition could be defined with
> > `define-judgment-form` (although derivations will only be discoverable
> > if you can give a mode spec.) If the semantics you're talking about
> > can't be written as an inductive definition, then it probably doesn't
> > make any sense.
> >
> > Second, remember that an evaluation context is just a way of
> > describing more succinctly what you could otherwise define by hand as
> > a big, complicated relation on individual terms. (The beginning of
> > SEwPR explains this very well.) I feel like you'll get something from
> > thinking about existing semantics that structure the context in
> > different ways. For example, in "
Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
Hi Jay,
I appreciate your pointers! However, I think either I didn’t make my question
clear enough, or I misunderstand your explanation (or perhaps some of both).
What I am trying to model is, indeed, a form of delimited control. I have
already written a model that supports a couple classic control operators,
namely exception handling and nondeterminism, plus some of the simpler
algebraic operations from the algebraic effects literature such as mutable
state. However, this isn’t quite sufficient for what I’m trying to do, as
effect systems allow the programmer to define those kinds of control operators
using more general primitives in the host language.
Here’s an example of what an effect definition and an effect handler might look
like in a hypothetical language that supports algebraic effect handlers:
effect Error e where
throw :: e -> a
handleError :: (() ->{Error e} a) -> Either e a
handleError f =
handle Error where
throw e _k = Left e
in Right (f ())
You can reasonably think of `effect` and `handle` in terms of delimited
control. Each `effect` declaration declares a new prompt tag, and each
operation of the effect aborts, passing its current continuation to the prompt
handler. Likewise, each `handle` declaration installs a new prompt with the
appropriate tag and handler. (In the above example, `throw` discards the
continuation and simply returns.)
This interpretation works well enough for algebraic effects, but this makes it
impossible to support operations like `catch`, or `cut` (for some kind of
backtracking effect) forcing them to be handlers instead. This turns out to
cause trouble in practice., so some newer work handles so-called “scoped”
effects as well, which support “scoping” operations like `catch` and `cut`. I
have been working on an implementation of a scoped effect system in Haskell,
but I have found many edge cases where the behavior of current systems produces
nonsensical results given certain handler compositions.
Fortunately, I have found that it is possible to produce a significantly more
predictable semantics for scoped effect handlers by viewing them as kind of
like “first class reduction rules.” A handler for an Error effect supporting
both `throw` and `catch` can be expressed using the following three reduction
rules:
E[handleError v] -> E[Right v]
E_1[handleError E_2[throw v]] -> E_1[Left v]
E_1[handleError E_2[catch e v]] ->
E_1[handleError E_2[
case handleError e of
Right a -> a
Left b -> v b]]
However, doing this also requires extending the definition of E itself so that
reduction may proceed into the appropriate locations:
E ::= ... | throw E | catch e E | handleError E
Therefore, this encoding of scoped handlers requires that they operate at the
level of the metalanguage, which is not enough — I want to come up with a model
that pushes the above expressive power into the language by defining
appropriately general-purpose `effect` and `handler` syntactic forms.
It is possible that what you are telling me is I should not bother, and instead
I should try to define a translation from my higher-level language into
something simpler to actually implement, such as some well-known model of
delimited control. However, the reason I have been hoping to avoid doing that
is I think the translation is not as straightforward as it seems, and the main
reason I want to model the higher-level interface directly is to better
understand how I think it ought to work before I try and define a translation
into something else (probably delimited continuations or monads).
Does that help to give a little more context? I was trying not to drag too much
of it in when writing my original email, but it’s possible that in doing so I
omitted too much. :)
Alexis
> On Nov 9, 2019, at 04:53, Jay McCarthy wrote:
>
> First, any inductive definition could be defined with
> `define-judgment-form` (although derivations will only be discoverable
> if you can give a mode spec.) If the semantics you're talking about
> can't be written as an inductive definition, then it probably doesn't
> make any sense.
>
> Second, remember that an evaluation context is just a way of
> describing more succinctly what you could otherwise define by hand as
> a big, complicated relation on individual terms. (The beginning of
> SEwPR explains this very well.) I feel like you'll get something from
> thinking about existing semantics that structure the context in
> different ways. For example, in "boring" lambda calculus, rules are
> always of the form "E [ e ] -> E [ e' ]". But, in the traditional way
> to explain exception-handling, you have a reduction rule like "E [ try
> F [ throw v_x ] with catch v_h ] => "E [ v_h v_x ]" where you've
> structured the context (F is "catch"-less contexts.) Chapter 8 of
> SEwPR [1] covers this kind of thing. The delimited control example has
> more complicated things like
Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
First, any inductive definition could be defined with `define-judgment-form` (although derivations will only be discoverable if you can give a mode spec.) If the semantics you're talking about can't be written as an inductive definition, then it probably doesn't make any sense. Second, remember that an evaluation context is just a way of describing more succinctly what you could otherwise define by hand as a big, complicated relation on individual terms. (The beginning of SEwPR explains this very well.) I feel like you'll get something from thinking about existing semantics that structure the context in different ways. For example, in "boring" lambda calculus, rules are always of the form "E [ e ] -> E [ e' ]". But, in the traditional way to explain exception-handling, you have a reduction rule like "E [ try F [ throw v_x ] with catch v_h ] => "E [ v_h v_x ]" where you've structured the context (F is "catch"-less contexts.) Chapter 8 of SEwPR [1] covers this kind of thing. The delimited control example has more complicated things like this too [2] but it might be too complicated to understand just this piece of it. Another example to look at is the context-based semantics of call-by-need. Stephen's ESOP 2012 paper [3] is a great place to look because it talks about a standard old way and a clever new way, and is very readable, the key is a rule like: "(\x. E[x]) v -> (\x. E[v]) v" where the terms in the reduction relation don't use contexts only on the outside. I don't really understand what you're trying to do, but it may be possible to have a LHSes like PhiContext [ GammaContext [ (gamma f v ExprContext [ (f e) ]) ] ] to get what you want Jay 1. https://redex.racket-lang.org/sewpr-toc.html 2. https://github.com/racket/redex/tree/master/redex-examples/redex/examples/delim-cont 3. http://www.ccs.neu.edu/home/stchang/pubs/Chang-Felleisen-ESOP2012.pdf -- Jay McCarthy Associate Professor @ CS @ UMass Lowell http://jeapostrophe.github.io Vincit qui se vincit. -- Jay McCarthy Associate Professor @ CS @ UMass Lowell http://jeapostrophe.github.io Vincit qui se vincit. On Sat, Nov 9, 2019 at 4:10 AM Alexis King wrote: > > Hello, > > I am trying to model a (not quite algebraic) effect system in PLT Redex, but > I’m struggling to encode my evaluation contexts into Redex’s pattern > language. My question is best explained via example, so I’ll start with a > bog-standard call-by-value lambda calculus: > > (define-language lam > [v ::= boolean (λ x e)] > [e ::= x v (e e) (if e e e)] > [E ::= hole (E e) (v E) (if E e e)] > [x ::= variable-not-otherwise-mentioned] > #:binding-forms > (λ x e #:refers-to x)) > > My reduction relation for lam is the usual one. Next, I define an extended > language: > > (define-extended-language eff lam > [e ::= (ψ x e) (γ (x p ...) e) (x e ...)] > [E ::= (ψ x E) (γ (x p ...) E)] > [p ::= :v :e :E] > #:binding-forms > (ψ x e #:refers-to x)) > > This is a severe simplification of the actual language I’m trying to model, > but it’s enough to illustrate my problem: the definition for E I’ve given > above is inadequate. What I actually want is to have some kind of > “dynamic”/“context-sensitive” evaluation context, where γ can introduce > scoped evaluation rules for identifiers bound by ψ. > > To give an example, if I have the expression > > (ψ f > (γ (f :E :e) > (f (if #t #f #t) (if #t #f #t > > I would like it to reduce to > > (ψ f > (γ (f :E :e) > (f #f (if #t #f #t > > because (γ (f :E :e) e_1) effectively extends E with a new production rule (f > E e) inside e_1, allowing reduction to recur into the first argument to f, > but not the second. > > If I were to define these rules on pen and paper, without using Redex, my > instinct would be to create some kind of “parameterized” evaluation context. > That is, I would define something like this: > > r ::= (x p ...) > > (E r ...) ::= > hole ((E r ...) e) (v (E r ...)) (if (E r ...) e e) > (ψ x (E r ...)) (γ r_0 (E r_0 r ...)) > (E-r r r ...) ... > > (E-r (x p ...) r ...) ::= (x (E-p p r ...) ...) > > (E-p :v _ ...) ::= v > (E-p :e _ ...) ::= e > (E-p :E r ...) ::= (E r ...) > > Though a little complicated to define, I think decomposition using these > evaluation contexts is still entirely syntax-directed (assuming the r > arguments are only used as inputs; i.e. E, E-r, and E-p are “metapatterns”). > Proving anything in this system seems like it could be a massive headache, > but it’s much too soon for me to be worrying about that — I just want a > super-flexible model I can throw some examples at to see what it does. Redex > seems like it would be ideal for that, but I have no idea how to encode this > kind of complicated decomposition into Redex’s pattern language. > > I suspect that doing it directly is completely impossible, so I was wondering
[racket-users] Modeling a context-sensitive evaluation context with PLT Redex?
Hello, I am trying to model a (not quite algebraic) effect system in PLT Redex, but I’m struggling to encode my evaluation contexts into Redex’s pattern language. My question is best explained via example, so I’ll start with a bog-standard call-by-value lambda calculus: (define-language lam [v ::= boolean (λ x e)] [e ::= x v (e e) (if e e e)] [E ::= hole (E e) (v E) (if E e e)] [x ::= variable-not-otherwise-mentioned] #:binding-forms (λ x e #:refers-to x)) My reduction relation for lam is the usual one. Next, I define an extended language: (define-extended-language eff lam [e ::= (ψ x e) (γ (x p ...) e) (x e ...)] [E ::= (ψ x E) (γ (x p ...) E)] [p ::= :v :e :E] #:binding-forms (ψ x e #:refers-to x)) This is a severe simplification of the actual language I’m trying to model, but it’s enough to illustrate my problem: the definition for E I’ve given above is inadequate. What I actually want is to have some kind of “dynamic”/“context-sensitive” evaluation context, where γ can introduce scoped evaluation rules for identifiers bound by ψ. To give an example, if I have the expression (ψ f (γ (f :E :e) (f (if #t #f #t) (if #t #f #t I would like it to reduce to (ψ f (γ (f :E :e) (f #f (if #t #f #t because (γ (f :E :e) e_1) effectively extends E with a new production rule (f E e) inside e_1, allowing reduction to recur into the first argument to f, but not the second. If I were to define these rules on pen and paper, without using Redex, my instinct would be to create some kind of “parameterized” evaluation context. That is, I would define something like this: r ::= (x p ...) (E r ...) ::= hole ((E r ...) e) (v (E r ...)) (if (E r ...) e e) (ψ x (E r ...)) (γ r_0 (E r_0 r ...)) (E-r r r ...) ... (E-r (x p ...) r ...) ::= (x (E-p p r ...) ...) (E-p :v _ ...) ::= v (E-p :e _ ...) ::= e (E-p :E r ...) ::= (E r ...) Though a little complicated to define, I think decomposition using these evaluation contexts is still entirely syntax-directed (assuming the r arguments are only used as inputs; i.e. E, E-r, and E-p are “metapatterns”). Proving anything in this system seems like it could be a massive headache, but it’s much too soon for me to be worrying about that — I just want a super-flexible model I can throw some examples at to see what it does. Redex seems like it would be ideal for that, but I have no idea how to encode this kind of complicated decomposition into Redex’s pattern language. I suspect that doing it directly is completely impossible, so I was wondering if there are any tricks or techniques I might use to encode it indirectly. Is there something clever I can do with a judgment form? I’ve been thinking about ways I might define my reduction relation inductively or something like that, but I really want to have access to the evaluation context (actually multiple evaluation contexts) in my reduction rules, since I’m using the language to define complicated control operators. Thanks, Alexis -- 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/E7A24480-1E87-42AB-A580-33FB3A2B3C04%40gmail.com.
