Daily, 2010/09/20: revisiting substitution + functions

Announcement items:

• Tutorial #2: Resolving lazy scope error WITHOUT deep substitution (A#2 mat'l!)
• A#1 update: Please keep an eye on or forward your @ugrad.cs.ubc.ca e-mail!
  (For forwarding: http://www.cs.ubc.ca/ugrad/facilities/accounts/email_news.shtml )
• TestFest: available, helpful, but NOT required!  (Only set up for eager version)
• Extended office hours this week; see Vista Announcements
• Practice Midterm out by end of day today (final tuning in progress)

High-level comment:

I'm not sure today's redefinition of our core semantics for WAE made as much sense in class as it did to me before class.  I still think it's a lovely approach to define "ground truth", however.

Meanwhile, we got a bit cut off on functions.  I'll take a moment to revisit the code at the start of class Wednesday so we all see what I did wrong.  (A small, simple coding error, when in our discussion of the idea we had gotten that right.)


Details:


I love the part of the PLAI text where Shriram first explores the semantics of identifier binding.  It's an opportunity to try, fail, and patch semantics over and over again, discovering through hand-worked examples (and as we did it in class through code) what it really means to bind an identifier to a value.

On the other hand, our lazy interpreter kind of blew all that work away.  When we tried interpreting:

{with {x y}
  {with {y 1}
    x}}

The lazy interpreter happily chugged away and got the wrong answer.

The only solution available to us (assuming we think this code should fail, which we all did) given the way we established the semantics in the text is to do something messily pro-active, like check for free instances in the named expression up front before performing substitution (yuck!).  (Tutorial will propose a rather different way of accomplishing this, BTW.)

That led me to the conclusion that we had our base semantics wrong in the first place.  Looking back, a much more natural semantics to me is that substitution of an identifier for its name expression in the body only gets to happen after any additional substitutions pending in the body get their turn.  After all, any substitution in the body is "more immediate" or "closer to the action" than the outer one.

Once you have that semantics, then you can (1) ask the question "what sort of redundancy does binding identifiers get rid of", (2) discover that it does not rid us of the redundancy of repeatedly interpreting the named expression in a binding (but only of repeatedly writing that expression), (3) propose interpreting the named expression to a value right away so we can save that redundant calculation, (4) discover that that fails because there may still be free identifiers in the named expression waiting to be substituted out by outer with expressions, (5) name the "evaluate it later" version "lazy" and the "evaluate it now" version "eager", and (6) try to write a whole new style of substitution that yields eager evaluation but remains true to our defining semantics, which leads to that lovely discussion in PLAI.

Sadly, I think I may have confused the issue by suddenly calling our established defining semantics from PLAI (based on substitution working only on free instances) and trying to go back and do the previous paragraph retrospectively.  Ah, for time travel!

Hopefully, the function part made sense, at least.  And, although we had an unresolved error in the code at the end of class (as well as a "TODO" note in subst that we hadn't filled in), we got things exactly right in our planning and just made a typo in implementation.  I've commented and fixed that in the posted notes.

Next time, we'll again attempt to optimize binding, this time (conceptually) eliminating the n² worst-case performance of substitution on programs like:

{with {x1 1}
  {with {x2 2}

...

xn}...}}

Cheers,

Steve