# [plt-scheme] redex is great

This does not reduce T in (x T) and (λ x T), I think
You probably get a head normal form, but not a normal form, I think
Jos
----- Original Message -----
From: "Robby Findler" <robby at eecs.northwestern.edu>
To: "Jos Koot" <jos.koot at telefonica.net>
Cc: <plt-scheme at list.cs.brown.edu>
Sent: Saturday, February 21, 2009 3:41 PM
Subject: Re: [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