The notion of a program context can be used to describe a number of ideas. So you could approach it from a number of angles.
- Compatible closure - the β-reduction rule isn't useful until you extend it to operate within the context of a whole program.
- Observational equivalence - even non-PL programmers are familiar with the idea of "substituting equals for equals" -- Liskov made the substitution principle famous to OO programmers, for example. So you can talk about being able to place two different expressions into the same context and observing the results.
- Quasiquotation - a quasiquoted code template constructs a term with holes in it where you can splice in code.
- Macros - similarly, the template in a syntax-rules macro, for example, is an expression context with named holes for all the pattern variables.
- Evaluation order - this goes along with the idea of compatible closure; since understanding how β-reduction applies within the context of a whole program requires knowing how to find the next expression to reduce, the grammar of evaluation contexts is a specification for the algorithm that finds the redex.
Although I found the phrase "an expression with a hole" opaque as a first year grad student, I do like the metaphor of a hole. But it's important to motivate it with an application. For PL students learning about semantics, it's probably useful to take the compatible closure angle. Otherwise, observational equivalence is probably the most accessible approach.
1 comment:
Nice blog, Dave.
You're right that "expression with a hole" is too informal, and not usually much help (though I guess it's more help than turning it around and saying "an expression is a context with an expression in its hole").
I share your peeve, and have a related one: reduction systems that leave decomposition of a term into a context and potential redex implicit; and have not even a sketch of a unique decomposition lemma.
Post a Comment