Re: Puzzle

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Wed, 2 Dec 1998 18:11:30 +0100

Wolfgang Lux wrote:
> Anyway, here are two more cases. Given the definitions
>
> coin = 0
> coin = 1
> f6 h g = h g g
> f7 h g = h g0 g0 where g0 = g
>
> what are the solutions of:
>
> f6 (\x y -> x + y) coin
> f7 (\x y -> x + y) coin
>
> I suppose that 1 is a possible solution in the former case, while it isn't in the latter. (Or will the use of the parameter g for both arguments of h in f6 already introduce sharing?)

1 is not a solution in both cases. The point is that all
parameter variables are shared in a rule. Or, declaritively,
if a rule is applied, all parameters must be instantiated
to constructor terms, i.e., fully evaluated (but this is
implemented lazily via sharing). Since "g" is a parameter
in both cases, all occurrences of it will be shared.

BTW, the rule for f7 can be considered as syntactic sugar for
the top-level declarations

f7 h g = aux h g
aux h g0 = h g0 g0

which makes the sharing in the presence of local declarations clearer.

Best regards,

Michael
Received on Mi Dez 02 1998 - 18:15:00 CET