26 nov 2011 kl. 11.44 skrev Rob Arthan:
On 24 Nov 2011, at 13:13, Lars-Henrik Eriksson wrote:
I have an implementation of the Y which crashes Poly/ML. Take the program below and evaluate "fact n" with n>3.
I expect you are interested in your particular least fixed point combinator, but if any least fixed point combinator will do, then you could try this one:
fun Y f x = f (Y f) x;
My interest is making a theoretical point -- not defining a Y combinator which is useful for practical programming.
The point of my definition is that it is an explicit definition of Y which is not recursive -- i.e. it is using val not val rec. A definition using fun is implicitly using val rec.
In the pure typed lambda calculus you can't define the Y combinator (as every term is strongly normalisable). Of course ML is strongly typed, but not pure, so I can go around that limitation by using the FT constructor as a "type converter".
Regards,
Lars-Henrik Eriksson, PhD, Senior Lecturer Computing Science, Dept. of Information Technology, Uppsala University, Sweden E-mail: lhe@it.uu.se, Web: http://www.it.uu.se/katalog/lhe?lang=en Phone: +46 18 471 10 57, Mobile: +46 705-36 39 16, Fax: +46 18 51 19 25