
redex reduction rules work on whole programs, so if your program looks like (prog …) you have to match the whole (prog …) thing for the reduction rules to fire

if you have (in-hole E …) it only matches an E, not a P so it wouldn’t match the whole program

so you either have to use (in-hole P something) or (prog …whatever… (in-hole E something) …whatever…)

off-topic question. Which membership is preferable ACM or SIGPLAN? Maybe none? I haven’t friends in academia I could ask and haven’t a clue as to what the difference between the two, but I consider attending CUFP co-located with ICFP in Oxford this year and looks like memberships offer reduced rates. Any advice there is appreciated.

> I would think that (if true e_t e_f) -> e_t
would match regardless of what evaluation context you were declaring in the in-hole
match
(if true e_t e_f)
only matches E
, not P
. Similarly (prog (defun ___) ... (if true e_t e_f))
only matches P
and not E
.
I don’t think there’s a clean way to define the reduction relation for the extended language as an extension to the reduction relation for the original language. The reason being what I mentioned before, the notion of what constitutes a program in the extended language has changed. Moreover, the reduction of expressions (the e
in (prog ___ e)
) changed, it now interacts with the environment (the (defun ___) ...
in (prog (defun ___) ... e)
): expressions can refer to functions defined in the environment, can changed the environment via set!
, and so forth.

@zerusski Last I knew, SIGPLAN membership was less than the discount on registration, so joining SIGPLAN was definitely a good move. SIGPLAN is part of ACM, and I was never clear on why ACM-less SIGPLAN membership exists; still, assuming the price structure is still the same, you should join ACM only if you see some benefit besides the registration.

thanks!

Last I joined (PLDI 2016), it was still the case that the discount was far greater than the cost of membership (I think an order of magnitude difference).

@shu—hung I meant extended WRT the evaluation context grammar… I don’t think we extended E
except maybe to add let
… but my tuesday file is an absolute mess because I was scrambling to keep up with by-name / by-value / imperative defun / imperative defval… and in the end I have a thing that only sorta runs. :slightly_smiling_face:

> extended WRT the evaluation context grammar um… I don’t get this :disappointed:

IIRC, E
is something that does not include (prog defs ...)

and P
is (prog defs ... E)

@mflatt afaik, the only reason why you’d want SIGPLAN and not ACM is if you think the comms of the acm publication quality has gone downhill. I think having either SIGPLAN or ACM will still get you discounted entry into SPLASH and the like.

WHICH IS IN VANCOUVER BC! If you’re interested in SIGPLAN stuff at all, I highly recommend going. It is a gorgeous city and a great conference

I like to think of contexts as defining a way to reach inside a tree and pull out a sub tree. If your rules expect to start from an E, then there’s no way to stick your extraction tool through a P to get to the E underneath.

If you start from a P, and P tells you how to get to the E underneath, then you’re fine.

@shu—hung I think we’re on the same page but I’m not explaining myself well… I’m talking about using define-extended-language
to define the evaluation context grammar, and that includes both E
and P
(which refers to E
).

@twisol OK… so that statement is where my confusion lies

It’s like if you told a surgeon how to move your organs around without telling them how to get through the skin. The rule assumes a human with no skin.

if we have P
and it refers to E
… how can it NOT connect to all the various subtrees?

Sorry for the gross medical metaphor.

I’m the son of a surgeon… works for me. :wink:

If your rule talks about Es and you give it a P, it doesn’t know what to do. Ps have skin, and the rule assumes things without skin.

So you have to change the rule so that it knows about skin.

I’m still trying to digest what @sergej said… but I’ll keep up to present and work backwards

I guess I’m just confused as to what in-hole
is really saying. I read it as “when you’re dealing with an E
that matches xxx, this is what to do”…

Right. Fundamentally, a prog isn’t an E.

Sure, it contains an E, but that doesn’t help you pick the P apart.

right… it is a P
and we have an evaluation context grammar rule that points from P
to E
so it seems like it would connect… I think in-hole
isn’t really saying what I think it is saying… and here I thought I understood holes finally. :stuck_out_tongue:

in-hole X Y says that if I stick Y into the hole in X, I get the whole program back.

An E does not describe the whole program; E doesn’t know anything about prog.

no, not whole program?… subtree… in-hole
is always about subtrees… and some of those subtrees are the whole tree… (please correct me if I’m wrong, but that was emphasized a lot, I thought)

Y is the subtree involved, yes. The whole program is X[Y], that hole-plugging operation.

if I have a sentence “This is a red ball”, I can break it down into a subtree “red” and a context “This is a [] ball”. The whole sentence is represented in these two parts

(suppose E is "[] ball" and P is “This is a E”)

I think at this point I’m still not going to get it. I see a bridge that isn’t being used and don’t understand why… but I can accept it as-is and carry forth. It’ just seems a bit odd that my grammar extension is tiny, my evaluation context extension is tiny, but then I have to rewrite all the reduction rules in my “extension”. It seems incongruous to me but I’d rather have something that works and proves I understand something about this thing than understand all the mechanics underneath.

I think your analogy breaks down there… P
would be more like “paragraph is E+” and I would still think that [] could match ball once it crawls down to E’s in the EC grammar…. but again, I’m going to blithely forge ahead and worry about understanding this anomaly later. I still have several layers in this tower to implement as cleanly as I can… this just isn’t one of them.

Sure, sure. That’s fine. I don’t think the analogy does break down (you could implement that example in Redex directly), and maybe that’s related to the misunderstanding, but I can appreciate leaving it for later ;)