# [plt-scheme] redex is great

On Sat, Feb 21, 2009 at 8:22 AM, Jos Koot <jos.koot at telefonica.net> wrote:
>* Suppose we have a language and a reductor that uses in-hole. Then if term T
*>* matches the in-hole clause, the term (T T) has two matches. As far as I can
*>* see both matches are returned by apply-reduction-relation (which in general
*>* is nice, of course, but here I am talking about leftmost reduction). Hence
*>* this reductor does not limit itself to leftmost redices only.
*
I'm not completely sure I'm getting your meaning above, but consider
this grammar:
T = (λ x T) | (T T) | x
E = hole | ((λ x T) E) | (E T)
x = variables
with this rule:
(--> (in-hole E ((λ x T_1) (λ x T_2)))
(in-hole E (subst x T_1 T_2)))
and this example input:
(((λ x x) (λ y y))
((λ p p) (λ q q)))
It reduces to this:
((λ y y)
((λ p p) (λ q q)))
but it does not reduce to this:
(((λ x x) (λ y y))
(λ q q))
because the decomposition of the term does not allow the hole to be on
the second application. That is, the context is restricting
applicability of the rule to only a subset of the places where it
might otherwise apply.
I didn't go thru the exercise and try it out myself, but reading over
your definition of nf? and reduction-step, you should be able to
formulate them as contexts. nf? could clearly be formulated as a
non-terminal in the grammar that matches only things that nf? returns
true for, and then reduction-step can be turned into a definition of a
context that has the hole at the point where (in the definition of
reduction-step) you call subst (ie, case 3).
Robby