[plt-scheme] redex is great

Thanks for your explanation.
I dont understand the rule
> (--> (in-hole E ((λ x T_1) (λ x T_2)))
>     (in-hole E (subst x T_1 T_2)))
If I replace it by:
> (--> (in-hole E ((λ x T_1) T_2))
>     (in-hole E (subst x T_1 T_2)))
I get multiple contractions again.

I can define the language of normal forms:
(nf var (λ var nf) (non-abstr-nf nf))
(non-abstr-nf var (non-abstr-nf nf))
But I dont see how this can help me.
Apparently I do not yet quite understand the working of
`hole' and `in-hole'. I'll study on it.
Thanks again, 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 4:07 PM
Subject: Re: [plt-scheme] redex is great


Yes, that's what I meant with the comments at the end. The example was
just in response to your comments about T and (T T), etc. The final
paragraph suggests how to make your example work.

Robby

On Sat, Feb 21, 2009 at 8:55 AM, Jos Koot <jos.koot at telefonica.net> wrote:
> 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
>