[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