Confused about Semantics Engineering Exercise 12.6

[Mike MacHenry]

Hey everyone,

I am a little confused about Exercise 12.6 from Semantics Engineering with PLT-Redex. The exercise is as follows:

"Formulate a general reduction relation for ISWIM using a with clause. Use traces to demonstrate that programs may be reduced to values along several different paths in a reduction graph. "

The problem I'm having with this is that to accomplish this goal, I needed to make a change to the ISWIM language definition on page 217 at the beginning of this chapter, particularly in the contexts section, and I made absolutely no change to the reduction relation given on page 225 directly above this exercise.

So for me, that language definition from 217, along with the reduction relation on 225, as well as the definitions for the meta functions in this chapter, I get the standard reduction, which permits only one reduction path for, say, an expression like (+ (1 1) (+ 1 1)). The left-most (+ 1 1) reduces to 2 first.

When I make the change to the contexts in the language definition, and change it from

(E hole (V E) (E M) (o V ... E M ...))

to

(E hole (M E) (E M) (o M ... E M ...))

My traces for the above expression gives what I think the exercise is expecting. I have a diamond shaped in my reduction DAG.

The problem I have with this is that I haven't done anything to the reduction relation to do this. The exercise seems pretty explicit to create a reduction relation using a with clause. so it seems like the purpose of the exercise is to get you to understand the with clause by developing something new using it. Now granted my reduction relation does use a with clause, because it's the one I copied out of the book. But I didn't write that one and use the with clause in my own new way.

So is there a different way to get the reduction relation to support the general reduction that requires one to change the reduction relation and not the grammar?

Thanks for the help,

-mike

[Robby Findler]

Hi Mike: it looks to me like you have the right definition in the
sense that it relates the right terms to each other. The rest of the
exercise is just to get you to use Redex's `with` to express it and to
avoid using the name `E` for a non-evaluation context. These are very
minor things! What's being asked is that you use the name `C` for the
compatible closure context (not change `E` like you've done) and then
use `with` in the reduction relation definition to lift the axioms to
arbitrary contexts. You would also not call this new (racket-level)
definition `iswim-standard` (since it isn't the standard reduction).

Robby

> --
> 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...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAAzRdbcM9w9wi-mPzdpY_4tBWSWv_QaXvZDpgNiXSEr05OaMoA%40mail.gmail.com.

[Mike MacHenry]

Hm... so I guess I'm "using a with clause" like the book requests if I'm redeveloping the iswim-general reduction relation myself, even if the only difference from the book's version is to name it general and to make it reference the new iswim language I made that has the compatible closure context instead of the evaluation context. This makes more sense, thanks. It felt like I must have misunderstood because what I did, which was the quickest and easiest way to do this, was to change my original language definition, rather than make a new one and thus need to make a new reduction using a with clause.

-mike

[Mike MacHenry]

Also this is a *very* minor point, but I'm pretty sure exercise 13.2 should read "Compare with the full grammar from exercise 12.2." rather than to compare with 12.1. Maybe not worthy even of the errata page. I don't know. But if you're going to reprint ever it'd be nice to flag for clean up.

[Robby Findler]

Thanks, Mike. I (finally) updated the errata page.

Robby

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAAzRdbcTOohM%3DqLmO8ZyK6NED4Ggw8kVUykGuVu-53fotJW1dw%40mail.gmail.com.