Hi,
I have an implementation of the Y which crashes Poly/ML. Take the program below and evaluate "fact n" with n>3.
I've tried it on both x86 and SPARC Solaris systems with Poly/ML 5.3, as well as on a (x86) MacOSX system with Poly/ML 5.4.1.
The program works in both Moscow ML and SMLNJ, so I'm pretty sure it is correct SML.
Best 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
--------
(* The Y combinator in ML *)
abstype 'a ft = FT of 'a ft -> 'a with val Y = fn f => (fn (FT x) => (f (fn a => x (FT x) a))) (FT (fn (FT x) => (f (fn a => x (FT x) a)))) end
(* Y is the fixed point operator, i.e. fix F = Y(F) *) (* Y has type (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b) *)
(* Recursive definitions such as val rec f = ... can be written val f = Y (fn f => ...) *)
fun Fact f n = if n = 0 then 1 else n * f(n-1)
val fact = Y Fact
Hi Lars, Thanks for reporting that. I did actually receive your previous email but it took a while for me to look at it. It definitely is a bug in Poly/ML and I have an idea where the problem is but I haven't looked at it in enough detail to see how to fix it. A work-around is to reduce the maximum inline function size using: PolyML.Compiler.maxInlineSize := 20; Your example then works fine.
Best regards, David
On 24/11/2011 13:13, Lars-Henrik Eriksson wrote:
Hi,
I have an implementation of the Y which crashes Poly/ML. Take the program below and evaluate "fact n" with n>3.
I've tried it on both x86 and SPARC Solaris systems with Poly/ML 5.3, as well as on a (x86) MacOSX system with Poly/ML 5.4.1.
The program works in both Moscow ML and SMLNJ, so I'm pretty sure it is correct SML.
Best regards,
Lars-Henrik Eriksson, PhD, Senior Lecturer
On 24 Nov 2011, at 13:13, Lars-Henrik Eriksson wrote:
Hi,
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;
Regards,
Rob.
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
-
David.Matthews＠prolingua.co.uk -
lhe＠it.uu.se -
rda＠lemma-one.com