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 <lexi.lam...@gmail.com> 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 
> 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.

-- 
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/CAJYbDaniRQGwZrCA7GCG1c2wOfr%2BzWihhVp8KAh92VmWChPQHQ%40mail.gmail.com.

Reply via email to