Can someone help guide my intuition on this aspect of reduction relations? I’m trying to implement the CEK machine as given in chapter 6.4 of SEwPR. I don’t know how to handle the “if V [not in] X” line. I think I could use a (side-condition ???) but I don’t know how to form it. Also, It seems strange to need to do additional “type checking” on terms in the LHS.

I’m trying to decide whether to change the abstract syntax to make that particular relation distinct, or use a side-condition. If i were to change the syntax, then I guess I would separate V={b X (λX.M)} into two, one with variables and one without. Like V={b (λX.M)} and V+ = {V X}

(I’m also thinking about what forms are easiest to translate into Java)

can you replace “V” in your reduction rules LHS with “X”?

(foo V) -> (bar) if V not in X <=> (foo X) -> (bar)

?

(just guessing, don’t have SEwPR on hand)

oh

not in

duh

i see what you’re getting at tho yeah

er, there has been at least one mailing list thread about this: http://lists.racket-lang.org/users/archive/2012-August/053641.html

like, i just want that term to match the other things in V that aren’t X. I don’t have a good sense of how to solve this kind of thing, because there seems to be multiple valid approaches

ah, thanks, I’ll read up on that mail

it just occurred to me that maybe type-systems are the solution to this kind of problem. if the expressions were typed you’d have the ability to make more precise matches.. (?)

@thinkmoore thanks for talking it out with me. The mailing list item helped — i didn’t realize that you could used redex-match in the side-condition to test for things. I was jammed up on how to test if something was a variable. symbol? worked, but that is just a coincidence, like, there is nothing saying that a variable has to be a symbol. so now i’m doing (side-condition (not (redex-match iswim-mach-cek X (term V)))) and that gets rid of the ambiguity I saw.

@stamourv I was actually in the middle of a second draft on the blog post, whoops

@notjack: Oh. Oops.

Should have checked with you.

We can always update it.

@stamourv I’ll finish it up tonight and we can update it, no worries