<!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>Hi Robby,</FONT></DIV> <DIV><FONT face="Courier New" size=2>This does the job. Now</FONT></DIV> <DIV><FONT face="Courier New" size=2>(term(curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z)))</FONT></DIV> <DIV><FONT face="Courier New" size=2>is reduced to (a(a(a(a z))) without any bifurcation.</FONT></DIV> <DIV><FONT face="Courier New" size=2>May be the code should be simplified, but in this form it exposes my way of thinking.</FONT></DIV> <DIV><FONT face="Courier New" size=2>I thought you might like to see the results of your appreciated help. Thanks very much.</FONT></DIV> <DIV><FONT face="Courier New" size=2>Jos</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>;leftmost order β reduction</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))<BR> (N (L (V) N) M) ; normal forms<BR> (M V (M N)) ; normal form but not an abstraction<BR> (H<BR>  (L (V) H)<BR>  (M H)<BR>  (side-condition (H_1 T) (not (term (abstr? H_1))))<BR>  hole))</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>(define reductor<BR> (reduction-relation cλ<BR>  (--> ; β contraction<BR>   (in-hole H ((λ (V_1) T_1) T_2))<BR>   (in-hole H (subst (V_1 T_2) T_1)))))</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>(define-extended-language bλ cλ<BR> (T .... any))<BR> <BR>(define-metafunction bλ abstr? : T -> any<BR> ((abstr? (λ (V) T)) #t)<BR> ((abstr? T) #f))</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <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>snip<BR>You should define a language that consists of the contexts in which<BR>you are allowed to reduce (say "L"). Mark the places where you can<BR>reduce an application by 'hole' in that language.<BR><BR>Then, when you write<BR><BR>  (in-hole L ((λ x T_1) T_2))<BR><BR>that pattern will only match when the entire term matches an "L" and<BR>the place where the "hole" was matches to "((λ x T_1) T_2)".<BR><BR>> Apparently I do not yet quite understand the working of<BR>> `hole' and `in-hole'. I'll study on it.<BR><BR>In general, when you match (in-hole P1 P2) you match P1 and you expect<BR>there to be a hole somewhere in P1. At that place, you match P2.<BR><BR></FONT></DIV></DIV></BODY></HTML>