<!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>Ok. I have two checks, nf1? and nf2?. If
the definition of N can be trusted only nf2? is needed.</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>(define-metafunction bλ nf1? : T ->
any<BR> ((nf1? ((L (V) T) T)) #f)<BR> ((nf1? (L (V) T)) (nf?
T))<BR> ((nf1? (T_1 T_2)) ,(and (not (term (abstr? T_1))) (term (nf? T_1))
(term (nf? T_2)))))</FONT></DIV>
<DIV> </DIV>
<DIV><FONT face="Courier New" size=2>(define-metafunction bλ nf2? : T ->
any<BR> ((nf2? N) #t)<BR> ((nf2? T) #f))</FONT></DIV>
<DIV> </DIV>
<DIV><FONT face="Courier New" size=2>(write<BR> (time<BR>
(redex-check cλ T <BR> (lambda (t)<BR> (case
(length (apply-reduction-relation reductor t))<BR> ((1)
#t)<BR> ((0) (and (term (nf1? t)) (term (nf2?
t))))<BR> (else #f)))<BR> #:attempts
10000<BR> #:source reductor<BR> #:retries
100)))</FONT></DIV>
<DIV> </DIV>
<DIV><FONT face="Courier New" size=2>cpu time: 46375 real time: 47094 gc time:
4196<BR>#<void></FONT></DIV>
<DIV><FONT face="Courier New" size=2></FONT> </DIV>
<DIV><FONT face="Courier New" size=2>
<DIV><FONT face="Courier New" size=2>
<DIV><FONT face="Courier New" size=2></FONT></DIV>
<DIV></FONT></FONT><FONT face="Courier New" size=2>Thanks,
Jos</FONT></DIV></DIV></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>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 4:13
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>That's half of the property but I expect it to be the
interesting half<BR>(that doesn't check that all non-reducing forms are normal
forms).<BR><BR>Robby<BR><BR><BR>On 2/22/09, 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>> You mean this?<BR>><BR>> (write<BR>>
(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)))<BR>><BR>> cpu
time: 46250 real time: 49094 gc time: 3810<BR>> #<void><BR>><BR>>
Jos<BR>><BR>> ----- Original Message -----<BR>> 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>><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: Sunday, February 22, 2009 2:44 PM<BR>> Subject: Re:
[plt-scheme] redex is great<BR>><BR>><BR>> 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<BR>>> of<BR>>> thinking.<BR>>> I thought you
might like to see the results of your appreciated help.<BR>>>
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>