[plt-scheme] redex is great

THe hole can't be anywhere in the example; it can't be inside a
lambda, for example. It also can't be to the right of an application.

Here's one quick thought. I bet it is broken (because these things
always are when you just write them down :), but perhaps it gives you
an idea? My thought is that L should find the left-most outermost
redex, and so it uses 'n' as an expression that does not have a redex
in order to do that. (Perhaps you should also include (λ x L) in L and
(λ x n) in n).

Anyways, if that kind of a thing were added to Redex, the way to do it
would be to sort out the definition like that, and you're just as
equipped as I am to do that!

Robby

(define-language lc
  (e (λ x e)
     (e e)
     x)
  (x variable-not-otherwise-mentioned)
  (L hole
     (L e)
     (n L))
  (n (x n)
     (n (λ x n))
     (n x)))

(define red
  (reduction-relation
   lc
   (--> (in-hole L ((λ x e_1) e_2))
        (in-hole L (subst x e_1 e_2)))))

On Thu, Feb 19, 2009 at 4:21 PM, Jos Koot <jos.koot at telefonica.net> wrote:
> I have studied this example extensively. However, in the example, hole E may
> be anywhere. I just want the leftmost hole only. I am sure I'll find a way
> to do that.
> Thanks, 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: Thursday, February 19, 2009 10:33 PM
> Subject: Re: [plt-scheme] redex is great
>
>
>> You can define a grammar for where reductions are allowed, indicating
>> that with 'hole' and then use 'in-hole' in your reduction rules. For
>> example, the E defined here:
>>
>> http://redex.plt-scheme.org/lam-v.html
>>
>> allows reductions in only certain places.
>>
>> Robby
>>
>> On Thu, Feb 19, 2009 at 3:26 PM, Jos Koot <jos.koot at telefonica.net> wrote:
>>>
>>> May be toy just gave me a ckue how ti do this,
>>> Thanks, 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: Thursday, February 19, 2009 8:44 PM
>>> Subject: Re: [plt-scheme] redex is great
>>>
>>>
>>>> Thanks for the kind words, Jos.
>>>>
>>>> On Thu, Feb 19, 2009 at 12:27 PM, Jos Koot <jos.koot at telefonica.net>
>>>> wrote:
>>>>>
>>>>> Would it be possible to add a in-left-most-hole to the reduction rules
>>>>> of
>>>>> redex? (same as in-hole, but applying to the leftmost one only) May be
>>>>> I
>>>>> should try to add iyt myself?
>>>>
>>>> If I'm understanding correctly, I think the easiest thing would be to
>>>> define a context like that and then just use it instead of adding
>>>> something more general to Redex.
>>>>
>>>> Robby
>>>
>>>
>
>