[plt-scheme] redex is great

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. The following does a leftmost reduction to normal form, but is very inefficient.

(define-language cλ
 (T (L (V) T) (T T) V) ; lambda terms
 (L λ lambda) ; lambda symbols
 (V (variable-except λ lambda))) ; variables

(define-extended-language nλ cλ (T .... any)) ; llow booleans for internal use.

(define reductor
 (reduction-relation cλ
  (--> T (reduction-step T)
   (side-condition (not (term (nf? T)))))))

(define-metafunction nλ nf? : T -> any ; In fact T -> boolean.
 ((nf? V) #t)
 ((nf? (λ (V) T_1)) (nf? T_1))
 ((nf? ((λ (V) T_1) T_2)) #f)
 ((nf? (T_1 T_2)) ,(and (term (nf? T_1)) (term (nf? T_2)))))

(define-metafunction cλ reduction-step : T -> T
 ((reduction-step V_1) _1)
 ((reduction-step (λ (V_1) T_1)) (λ (V_1) (reduction-step T_1)))
 ((reduction-step ((λ (V_1) T_1) T_2)) (subst (V_1 T_2) T_1))
 ((reduction-step (T_1 T_2)) ((reduction-step T_1) T_2)
  (side-condition (not (term (nf? T_1)))))
 ((reduction-step (T_1 T_2)) (T_1 (reduction-step T_2))))

...

(traces reductor (term (curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z))))
Produces a straight line reduction path to (a (a (a (a z))))

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: Friday, February 20, 2009 1:42 AM
Subject: Re: [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
>>>
>>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090221/53be8b0b/attachment.html>