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: [email protected], 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 _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
