[Caml-list] beta-reduction rules

[Caml-list] beta-reduction rules

[Damien]

hello,

What are the rules for applying a function to its arguments ?

# let g f i = f i;;
	val g : ('a -> 'b) -> 'a -> 'b = <fun>

# let rec f0 x   = fun i -> (f x) i;;
	val f0 : 'a -> 'b -> 'c = <fun>
# let rec f1 x i = (f1 x) i;;
	val f1 : 'a -> 'b -> 'c = <fun>
# let rec f2 x   = g (f2 x);;
	val f2 : 'a -> 'b -> 'c = <fun>

# let a = f0 ();;
	val a : '_a -> '_b = <fun>
# let a = f1 ();;
	val a : '_a -> '_b = <fun>
# let a = f2 ();;
	Stack overflow during evaluation (looping recursion?).

I expected f0, f1 and f2 to be equivalent,
but,  f0 and f1 look like ['a * 'b->'c)]
and f2  looks like ['a->('b->'c)]

Is it a normal feature ?


damien


<http://www.ens-lyon.fr/~dpous>

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] beta-reduction rules

[David Monniaux]

On Mon, 24 Mar 2003, Damien wrote:

> I expected f0, f1 and f2 to be equivalent,

No, they are not.

To speak in a pretentious way: properties involving side effects or
non-termination are NOT preserved by eta-expansion. Incomplete
applications may yield different results.

In your example:

# let g f i = f i;;
        val g : ('a -> 'b) -> 'a -> 'b = <fun>
# let rec f0 x   = fun i -> (f0 x) i;; (* I assume you meant f0 here *)
        val f0 : 'a -> 'b -> 'c = <fun>
# let rec f1 x i = (f1 x) i;;
        val f1 : 'a -> 'b -> 'c = <fun>
# let rec f2 x   = g (f2 x);;
        val f2 : 'a -> 'b -> 'c = <fun>

f0 and f1 are equivalent up to syntactic sugar.
f2 is *NOT* equivalent.

Let me show you the evaluation chains:
f1 () evaluates to a closure representing fun i -> ...
f2 () starts looping.

Compare:
# let rec f x i = f x i;;
val f : 'a -> 'b -> 'c = <fun>
# let rec g x = ((g x) : 'a->'b);;
val g : 'a -> 'b -> 'c = <fun>

f 4 5 and g 4 5 do not terminate.
f 4 terminates (and yields a closure) while g 5 does not terminate.

Compare:
# let f x y = raise Exit;;
val f : 'a -> 'b -> 'c = <fun>
# let g x = raise Exit; fun y -> raise Exit;;
val g : 'a -> 'b -> 'c = <fun>

Complete applications are equivalent: f () () and g () () yield an
uncaught exception.

Incomplete applications are *not* equivalent: f () yields a function while
g () yields an uncaught exception.

> Is it a normal feature ?

Yes, it is normal in an eager functional programming language.

David Monniaux            http://www.di.ens.fr/~monniaux
Laboratoire d'informatique de l'École Normale Supérieure,
Paris, France




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners