<!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,&nbsp;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>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>(define-language cλ<BR>&nbsp;(T (L (V) T) 
(T T) V) ; lambda terms<BR>&nbsp;(L λ lambda) ; lambda symbols<BR>&nbsp;(V 
(variable-except λ lambda))) ; variables</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>(define-extended-language nλ cλ (T .... 
any)) ; llow booleans for internal use.</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>(define 
reductor<BR>&nbsp;(reduction-relation cλ<BR>&nbsp; (--&gt; T (reduction-step 
T)<BR>&nbsp;&nbsp; (side-condition (not (term (nf? T)))))))</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>(define-metafunction nλ nf? : T -&gt; any ; 
In fact T -&gt; boolean.<BR>&nbsp;((nf? V) #t)<BR>&nbsp;((nf? (λ (V) T_1)) (nf? 
T_1))<BR>&nbsp;((nf? ((λ (V) T_1) T_2)) #f)<BR>&nbsp;((nf? (T_1 T_2)) ,(and 
(term (nf? T_1)) (term (nf? T_2)))))</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>(define-metafunction cλ reduction-step : T 
-&gt; T<BR>&nbsp;((reduction-step V_1) _1)<BR>&nbsp;((reduction-step (λ (V_1) 
T_1)) (λ (V_1) (reduction-step T_1)))<BR>&nbsp;((reduction-step ((λ (V_1) T_1) 
T_2)) (subst (V_1 T_2) T_1))<BR>&nbsp;((reduction-step (T_1 T_2)) 
((reduction-step T_1) T_2)<BR>&nbsp; (side-condition (not (term (nf? 
T_1)))))<BR>&nbsp;((reduction-step (T_1 T_2)) (T_1 (reduction-step 
T_2))))</FONT></DIV>
<DIV><FONT face="Courier New" size=2></FONT>&nbsp;</DIV>
<DIV><FONT face="Courier New" size=2>...</FONT></DIV>
<DIV><FONT face="Courier New" size=2></FONT>&nbsp;</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&nbsp;reduction path to (a (a (a (a z))))</FONT></DIV>
<DIV><FONT face="Courier New" size=2></FONT>&nbsp;</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" &lt;</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>&gt;</FONT></DIV>
<DIV><FONT face="Courier New" size=2>To: "Jos Koot" &lt;</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>&gt;</FONT></DIV>
<DIV><FONT face="Courier New" size=2>Cc: &lt;</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>&gt;</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>&nbsp; (e (λ x 
e)<BR>&nbsp;&nbsp;&nbsp;&nbsp; (e e)<BR>&nbsp;&nbsp;&nbsp;&nbsp; x)<BR>&nbsp; (x 
variable-not-otherwise-mentioned)<BR>&nbsp; (L hole<BR>&nbsp;&nbsp;&nbsp;&nbsp; 
(L e)<BR>&nbsp;&nbsp;&nbsp;&nbsp; (n L))<BR>&nbsp; (n (x 
n)<BR>&nbsp;&nbsp;&nbsp;&nbsp; (n (λ x n))<BR>&nbsp;&nbsp;&nbsp;&nbsp; (n 
x)))<BR><BR>(define red<BR>&nbsp; (reduction-relation<BR>&nbsp;&nbsp; 
lc<BR>&nbsp;&nbsp; (--&gt; (in-hole L ((λ x e_1) 
e_2))<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (in-hole L (subst x e_1 
e_2)))))<BR><BR>On Thu, Feb 19, 2009 at 4:21 PM, Jos Koot &lt;</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>&gt; 
wrote:<BR>&gt; I have studied this example extensively. However, in the example, 
hole E may<BR>&gt; be anywhere. I just want the leftmost hole only. I am sure 
I'll find a way<BR>&gt; to do that.<BR>&gt; Thanks, Jos<BR>&gt;<BR>&gt; ----- 
Original Message ----- From: "Robby Findler"<BR>&gt; &lt;</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>&gt;<BR>&gt; To: "Jos Koot" &lt;</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>&gt;<BR>&gt; Cc: &lt;</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>&gt;<BR>&gt; Sent: Thursday, February 19, 2009 10:33 PM<BR>&gt; Subject: 
Re: [plt-scheme] redex is great<BR>&gt;<BR>&gt;<BR>&gt;&gt; You can define a 
grammar for where reductions are allowed, indicating<BR>&gt;&gt; that with 
'hole' and then use 'in-hole' in your reduction rules. For<BR>&gt;&gt; example, 
the E defined here:<BR>&gt;&gt;<BR>&gt;&gt; </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>&gt;&gt;<BR>&gt;&gt; allows reductions in only certain 
places.<BR>&gt;&gt;<BR>&gt;&gt; Robby<BR>&gt;&gt;<BR>&gt;&gt; On Thu, Feb 19, 
2009 at 3:26 PM, Jos Koot &lt;</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>&gt; 
wrote:<BR>&gt;&gt;&gt;<BR>&gt;&gt;&gt; May be toy just gave me a ckue how ti do 
this,<BR>&gt;&gt;&gt; Thanks, Jos<BR>&gt;&gt;&gt;<BR>&gt;&gt;&gt; ----- Original 
Message ----- From: "Robby Findler"<BR>&gt;&gt;&gt; &lt;</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>&gt;<BR>&gt;&gt;&gt; To: "Jos Koot" &lt;</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>&gt;<BR>&gt;&gt;&gt; Cc: &lt;</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>&gt;<BR>&gt;&gt;&gt; Sent: Thursday, February 19, 2009 8:44 
PM<BR>&gt;&gt;&gt; Subject: Re: [plt-scheme] redex is 
great<BR>&gt;&gt;&gt;<BR>&gt;&gt;&gt;<BR>&gt;&gt;&gt;&gt; Thanks for the kind 
words, Jos.<BR>&gt;&gt;&gt;&gt;<BR>&gt;&gt;&gt;&gt; On Thu, Feb 19, 2009 at 
12:27 PM, Jos Koot &lt;</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>&gt;<BR>&gt;&gt;&gt;&gt; 
wrote:<BR>&gt;&gt;&gt;&gt;&gt;<BR>&gt;&gt;&gt;&gt;&gt; Would it be possible to 
add a in-left-most-hole to the reduction rules<BR>&gt;&gt;&gt;&gt;&gt; 
of<BR>&gt;&gt;&gt;&gt;&gt; redex? (same as in-hole, but applying to the leftmost 
one only) May be<BR>&gt;&gt;&gt;&gt;&gt; I<BR>&gt;&gt;&gt;&gt;&gt; should try to 
add iyt myself?<BR>&gt;&gt;&gt;&gt;<BR>&gt;&gt;&gt;&gt; If I'm understanding 
correctly, I think the easiest thing would be to<BR>&gt;&gt;&gt;&gt; define a 
context like that and then just use it instead of adding<BR>&gt;&gt;&gt;&gt; 
something more general to Redex.<BR>&gt;&gt;&gt;&gt;<BR>&gt;&gt;&gt;&gt; 
Robby<BR>&gt;&gt;&gt;<BR>&gt;&gt;&gt;<BR>&gt;<BR>&gt;</FONT></BODY></HTML>