<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> <HTML><HEAD> <META http-equiv=Content-Type content="text/html; charset=iso-8859-1"> <META content="MSHTML 6.00.6000.16809" name=GENERATOR> <STYLE></STYLE> </HEAD> <BODY bgColor=#ffffff> <DIV><FONT face="Courier New" size=2> <DIV><FONT face="Courier New" size=2>Lately I have played with redex. It is very nice. </FONT><FONT face="Courier New" size=2>Although redex can be used for a bigger set of languages, I played with lambda calculus only, making procedures such as to find normal forms (if possible within a reasonable amount of steps), checking equality of terms modulo alpha congruence, currying of uncurried shorthand, and a predicate for equality of lambda terms (reflexive and transitive and symmetrized closure of beta and eta reduction) </FONT><FONT face="Courier New" size=2>The last predicate is incomplete of course and I have made it to halt if no answer can be found within a reasonable number of steps. I have the pleasure to share my code with you. You can download it from:</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2><A href="">http://www.telefonica.net/web2/koot/rdx.scm</A></FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>Thanks to Robby Findler and the PLT team.</FONT></DIV> <DIV><FONT face="Courier New" size=2></FONT> </DIV> <DIV><FONT face="Courier New" size=2>Would it be possible to add a in-left-most-hole to the reduction rules of redex? (same as in-hole, but applying to the leftmost one only) May be I should try to add iyt myself?</FONT></DIV> <DIV><FONT face="Courier New" size=2>Jos</FONT></DIV></FONT></DIV></BODY></HTML>