[plt-scheme] redex is great

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

Yes, that's to be expected.

> I can define the language of normal forms:
> (nf var (λ var nf) (non-abstr-nf nf))
> (non-abstr-nf var (non-abstr-nf nf))

Good.

> But I dont see how this can help me.

You should define a language that consists of the contexts in which
you are allowed to reduce (say "L"). Mark the places where you can
reduce an application by 'hole' in that language.

Then, when you write

  (in-hole L ((λ x T_1) T_2))

that pattern will only match when the entire term matches an "L" and
the place where the "hole" was matches to "((λ x T_1) T_2)".

> Apparently I do not yet quite understand the working of
> `hole' and `in-hole'. I'll study on it.

In general, when you match (in-hole P1 P2) you match P1 and you expect
there to be a hole somewhere in P1. At that place, you match P2.

> 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
>>
>
>