# Re: Puzzle

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Wed, 2 Dec 1998 12:25:29 +0100

Wolfgang Lux wrote:
> However, I'm a bit more worried about another point, viz. the syntactic sugar of interpreting f = g as f x = g x in case f and g are of functional type. This makes the sharing of a functional result from a non-deterministic function impossible, except if I can convince the type system into using a more general type (i.e. \forall a.a) to the local variable. With your proposed restriction, we still have for
>
> g = incr
> g = decr
> f4 x = h (h x) where h = g
>
> that f4 3 has the solutions 1, 3, and 5 in constrast to the example above which has only 2 solutions for f 3. If I really want to exclude the solution 3 (i.e. make a consistent choice for g in the program), I have to resort to something like
>
> f5 h g x = h g g x
>
> and
>
> f5 (.) g 3

Unfortunately (or suprisingly), even this does not work
as long as we interpret f = g as f x = g x at the top-level:

f5 (.) g 3 ->* g (g 3)
-> incr (g 3) (with rule g x = incr x)
-> (g 3) + 1
-> (decr 3) + 1 (with rule g x = decr x)
->* 3

Thus, sharing of functional results is impossible if all rules
are first-order. In order to enable sharing of functional values,
you must allow higher-order rewrite rules, but as I wrote before,
I am not aware of a calculus for functional logic programs
which deals with h.o. rules. Thus, I am in favor of being
a bit conservative and restrict Curry to first-order rules
(which does not exclude the use of higher-order functions!).
Of course, some later extension could also allow h.o. rules
and h.o. unification (I already have a name for this extension:
"HOT Curry").

Note that a calculus with h.o. rules and ND functions has also

g = incr
g = decr
f4 x = h (h x) where h = g

is not equivalent to the eta-expanded version

g = incr
g = decr
f4 x = h (h x) where h x = g x

due to a different sharing behavior. This shows at least that
the choice of the "right" approach to this problem is not trivial.

Best regards,

Michael
Received on Mi Dez 02 1998 - 12:29:00 CET

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:02 CEST