<!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>You mean this?</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>(write</FONT></DIV> <DIV><FONT face="Courier New" size=2> (time<BR>  (redex-check cλ T <BR>   (lambda (t) (< (length (apply-reduction-relation reductor t)) 2))<BR>   #:attempts 10000<BR>   #:source reductor<BR>   #:retries 100)))</FONT></DIV> <DIV><FONT face="Courier New" size=2><BR>cpu time: 46250 real time: 49094 gc time: 3810<BR>#<void></FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>Jos</FONT></DIV> <DIV> </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>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: Sunday, February 22, 2009 2:44 PM</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>On Sun, Feb 22, 2009 at 7:05 AM, 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>> Hi Robby,<BR>> This does the job. Now<BR>> (term(curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z)))<BR>> is reduced to (a(a(a(a z))) without any bifurcation.<BR>> May be the code should be simplified, but in this form it exposes my way of<BR>> thinking.<BR>> I thought you might like to see the results of your appreciated help. Thanks<BR>> very much.<BR><BR>Nice.<BR><BR>Now the thing to try to to formulate a property of this semantics and<BR>use redex-check to try to falsify it. I expect you'd want the property<BR>to be something like "each term is either a normal form or reduces to<BR>exactly one thing".<BR><BR>Robby</FONT></BODY></HTML>