From: Paco Lopez Fraguas <fraguas_at_eucmax.sim.ucm.es>
Date: Tue, 04 Feb 1997 09:30:29 +0100

Dear Sergio,

thanks for your interest. Let's continue the discussion.

>
> So may question is: Given the program (in Michael's notation)
>
> data nat = o ; s(nat).
>
> coin = o.
> coin = s(o).
>
>
>
> What's wrong with computing
>
> double(coin) --> s(o)
>

Let us apply to this example the arguments of my previous message:

The universe of 'values' for this program is {0,s(0),s(s(0)),...}
(technically, it is better to add free variables to the universe,
but this is not important here}.
The rules for 'coin' indicates that 'coin' can be reduced to
'0' or to 's(0)'. We can think that '0' and 's(0)' are the two
possible values of 'coin'. Another way of stating this is that 'coin'
denotes the set {0,s(0)}. In general, expressions (involving
non-constructor symbols) denote (some kind of) sets of values.

You can read the definition of the (deterministic, as you pointed
out) function 'double' as:
For any VALUE X, any possible value of 'add(X,X)' gives one possible
value of 'double(X)'.
For this particular case, given X, both 'add(X,X)' and 'double(X)' have
a unique value.

Now, for extending the reading of the rule for 'double' to cover the
case
that X is an expression (i.e., a set of values) in general, you
simply use the 'usual mathematical sense' for applying a function to
a set (i.e., the notion of image of a set by a function). With this
you would not say that 'double({0,s(0)})' is '{0,s(0),s(s(0))}',
but rather '{0,s(s(0))}'. That is, 0 and s(s(0)) -- but not s(0) -- are
the
possible values of 'double(coin)'.
Yet another formulation (closer to the terminology 'call-time-choice'):
for obtaining a possible value of 'double(coin)', pick up a possible
value
of 'coin', say x, and compute a possible value of 'add(x,x)'.
According with this point of view, 'double(coin)' and 'add(coin,coin)'
are not
the same (the same happens with 'mathematical functions',
where from the equation 'f(x) = g(x,x)' for _values_ x we do not deduce
'f(A)=g(A,A)' for sets A, at least if we understand g(A,A) as g(AxA)).

> I am troubled by the fact that one should
> compute
>

> Right?

Right, we have now two coins.

> Moreover, double is a well-behaved, deterministic function,
> thus for every t, one should compute
>
>

Yes, but for every value t, not for every expression (set of values).

> My reason to use a non-deterministic function
> such as permute is that if I have to solve, say, the n_queens
> problem, then I am able to code a simpler program if I can use a
> non-deterministic permute, than if I can't

This is also my reason.

>
> To be the devil's advocate, suppose that I want to know whether
> there is more than one solution to my problem. I define a
> (polymorphic) function
>
> many_solutions x -> not (x = x)
>
> and I solve
>
> many_solution n_queens = true
>
> What's wrong with that?

I hope it is clearer now that you cannot consider different values for
the x's
in the right hand side, so this definition does'nt work.

Best,

Paco

```--
Francisco J. Lopez-Fraguas
Dep. Informatica y Automatica
Fac. Matematicas Av. Complutense s/n