🚀 go-pugleaf

In article <2531@wn1.sci.kun.nl> ge@wn3.sci.kun.nl (Ge' Weijers) writes:

   fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

   >C) I've never seen a programming language
   >   based on typed lambda calculus whose typechecking system
   >   permits the user to define a fixpoint combinator
   >   out of more primitive elements.  The type signature
   >   of the necessary lambda expression cannot be written
   >   as a finite combination of the primitive types
   >   (so Y-combinators must be added as primitives).

   I assume that languages like Miranda (TM) and ML are based on typed lambda
   calculus. In Miranda the Y combinator can be written as

   y f = g
	 where
	    g = f g

This is cheating. The interesting property of the Y operator is that
it does not make use of any primitive recursive definition mechanism.
The above definition does this in the expression "g = f g".

   fac = y fac1
	 where
	    fac1 f x = 1, x <= 1
		     = x * (fac1 (x-1)), otherwise

I assume that you meant "= x * (f (x-1)), otherwise" for that last
line.

   In Algol68 you can also write a Y combinator. The next example is not
   tested, as elas no implementation is available to me anymore:

   BEGIN
       MODE M = PROC(M,INT)INT;

       PROC fac1 = (M f, INT x)INT:
       IF x <= 1
       THEN 1
       ELSE x * f(x-1)
       FI;

       PROC y = (M f, INT x)INT:
	 f (f,x);

       print((y(fac1,5), newline))
   END

This is a red herring. The above y is not the Y operator of interest to
us; it does not create a procedure (i.e. a closure). The difficulties in
writing and type checking the Y operator occur with higher order
functions (i.e.  first class procedures.)  If Algol68 has them, try
writing the "real" Y operator.

Also, I assume you meant "ELSE x * f(f, x-1)".

-Mark
--

Mark Friedman
MIT Artificial Intelligence Lab
545 Technology Sq.
Cambridge, Ma. 02139

markf@zurich.ai.mit.edu