<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> <HTML><HEAD> <META http-equiv=Content-Type content="text/html; charset=utf-8"> <META content="MSHTML 6.00.6000.16809" name=GENERATOR> <STYLE></STYLE> </HEAD> <BODY> <DIV><FONT face="Courier New" size=2>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.</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>(define-language cλ<BR> (T (L (V) T) (T T) V) ; lambda terms<BR> (L λ lambda) ; lambda symbols<BR> (V (variable-except λ lambda))) ; variables</FONT></DIV> <DIV> </DIV> <DIV><FONT face="Courier New" size=2>(define-extended-language nλ cλ (T .... any)) ; llow booleans for internal use.</FONT></DIV> <DIV> </DIV> <DIV><FONT face="Courier New" size=2>(define reductor<BR> (reduction-relation cλ<BR>  (--> T (reduction-step T)<BR>   (side-condition (not (term (nf? T)))))))</FONT></DIV> <DIV> </DIV> <DIV><FONT face="Courier New" size=2>(define-metafunction nλ nf? : T -> any ; In fact T -> boolean.<BR> ((nf? V) #t)<BR> ((nf? (λ (V) T_1)) (nf? T_1))<BR> ((nf? ((λ (V) T_1) T_2)) #f)<BR> ((nf? (T_1 T_2)) ,(and (term (nf? T_1)) (term (nf? T_2)))))</FONT></DIV> <DIV> </DIV> <DIV><FONT face="Courier New" size=2>(define-metafunction cλ reduction-step : T -> T<BR> ((reduction-step V_1) _1)<BR> ((reduction-step (λ (V_1) T_1)) (λ (V_1) (reduction-step T_1)))<BR> ((reduction-step ((λ (V_1) T_1) T_2)) (subst (V_1 T_2) T_1))<BR> ((reduction-step (T_1 T_2)) ((reduction-step T_1) T_2)<BR>  (side-condition (not (term (nf? T_1)))))<BR> ((reduction-step (T_1 T_2)) (T_1 (reduction-step T_2))))</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>...</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>(traces reductor (term (curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z))))</FONT></DIV> <DIV><FONT face="Courier New" size=2>Produces a s</FONT><FONT face="Courier New" size=2>traight line reduction path to (a (a (a (a z))))</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>Jos</DIV> <DIV><BR></DIV></FONT> <DIV><FONT face="Courier New" size=2>----- Original Message ----- </FONT> <DIV><FONT face="Courier New" size=2>From: "Robby Findler" <</FONT><A href="mailto:robby@eecs.northwestern.edu"><FONT face="Courier New" size=2>robby@eecs.northwestern.edu</FONT></A><FONT face="Courier New" size=2>></FONT></DIV> <DIV><FONT face="Courier New" size=2>To: "Jos Koot" <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>></FONT></DIV> <DIV><FONT face="Courier New" size=2>Cc: <</FONT><A href="mailto:plt-scheme@list.cs.brown.edu"><FONT face="Courier New" size=2>plt-scheme@list.cs.brown.edu</FONT></A><FONT face="Courier New" size=2>></FONT></DIV> <DIV><FONT face="Courier New" size=2>Sent: Friday, February 20, 2009 1:42 AM</FONT></DIV> <DIV><FONT face="Courier New" size=2>Subject: Re: [plt-scheme] redex is great</FONT></DIV></DIV> <DIV><FONT face="Courier New"><BR><FONT size=2></FONT></FONT></DIV><FONT face="Courier New" size=2>THe hole can't be anywhere in the example; it can't be inside a<BR>lambda, for example. It also can't be to the right of an application.<BR><BR>Here's one quick thought. I bet it is broken (because these things<BR>always are when you just write them down :), but perhaps it gives you<BR>an idea? My thought is that L should find the left-most outermost<BR>redex, and so it uses 'n' as an expression that does not have a redex<BR>in order to do that. (Perhaps you should also include (λ x L) in L and<BR>(λ x n) in n).<BR><BR>Anyways, if that kind of a thing were added to Redex, the way to do it<BR>would be to sort out the definition like that, and you're just as<BR>equipped as I am to do that!<BR><BR>Robby<BR><BR>(define-language lc<BR>  (e (λ x e)<BR>     (e e)<BR>     x)<BR>  (x variable-not-otherwise-mentioned)<BR>  (L hole<BR>     (L e)<BR>     (n L))<BR>  (n (x n)<BR>     (n (λ x n))<BR>     (n x)))<BR><BR>(define red<BR>  (reduction-relation<BR>   lc<BR>   (--> (in-hole L ((λ x e_1) e_2))<BR>        (in-hole L (subst x e_1 e_2)))))<BR><BR>On Thu, Feb 19, 2009 at 4:21 PM, Jos Koot <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>> wrote:<BR>> I have studied this example extensively. However, in the example, hole E may<BR>> be anywhere. I just want the leftmost hole only. I am sure I'll find a way<BR>> to do that.<BR>> Thanks, Jos<BR>><BR>> ----- Original Message ----- From: "Robby Findler"<BR>> <</FONT><A href="mailto:robby@eecs.northwestern.edu"><FONT face="Courier New" size=2>robby@eecs.northwestern.edu</FONT></A><FONT face="Courier New" size=2>><BR>> To: "Jos Koot" <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>><BR>> Cc: <</FONT><A href="mailto:plt-scheme@list.cs.brown.edu"><FONT face="Courier New" size=2>plt-scheme@list.cs.brown.edu</FONT></A><FONT face="Courier New" size=2>><BR>> Sent: Thursday, February 19, 2009 10:33 PM<BR>> Subject: Re: [plt-scheme] redex is great<BR>><BR>><BR>>> You can define a grammar for where reductions are allowed, indicating<BR>>> that with 'hole' and then use 'in-hole' in your reduction rules. For<BR>>> example, the E defined here:<BR>>><BR>>> </FONT><A href="http://redex.plt-scheme.org/lam-v.html"><FONT face="Courier New" size=2>http://redex.plt-scheme.org/lam-v.html</FONT></A><BR><FONT face="Courier New" size=2>>><BR>>> allows reductions in only certain places.<BR>>><BR>>> Robby<BR>>><BR>>> On Thu, Feb 19, 2009 at 3:26 PM, Jos Koot <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>> wrote:<BR>>>><BR>>>> May be toy just gave me a ckue how ti do this,<BR>>>> Thanks, Jos<BR>>>><BR>>>> ----- Original Message ----- From: "Robby Findler"<BR>>>> <</FONT><A href="mailto:robby@eecs.northwestern.edu"><FONT face="Courier New" size=2>robby@eecs.northwestern.edu</FONT></A><FONT face="Courier New" size=2>><BR>>>> To: "Jos Koot" <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>><BR>>>> Cc: <</FONT><A href="mailto:plt-scheme@list.cs.brown.edu"><FONT face="Courier New" size=2>plt-scheme@list.cs.brown.edu</FONT></A><FONT face="Courier New" size=2>><BR>>>> Sent: Thursday, February 19, 2009 8:44 PM<BR>>>> Subject: Re: [plt-scheme] redex is great<BR>>>><BR>>>><BR>>>>> Thanks for the kind words, Jos.<BR>>>>><BR>>>>> On Thu, Feb 19, 2009 at 12:27 PM, Jos Koot <</FONT><A href="mailto:jos.koot@telefonica.net"><FONT face="Courier New" size=2>jos.koot@telefonica.net</FONT></A><FONT face="Courier New" size=2>><BR>>>>> wrote:<BR>>>>>><BR>>>>>> Would it be possible to add a in-left-most-hole to the reduction rules<BR>>>>>> of<BR>>>>>> redex? (same as in-hole, but applying to the leftmost one only) May be<BR>>>>>> I<BR>>>>>> should try to add iyt myself?<BR>>>>><BR>>>>> If I'm understanding correctly, I think the easiest thing would be to<BR>>>>> define a context like that and then just use it instead of adding<BR>>>>> something more general to Redex.<BR>>>>><BR>>>>> Robby<BR>>>><BR>>>><BR>><BR>></FONT></BODY></HTML>