[mercury-users] Computing a square root from its definition

[Fergus Henderson]

On 26-Apr-2001, Terrence Brannon <princepawn at earthlink.net> wrote:
> I am working on a functional means of approximating square roots that
> I will post once I am have my final efforts with it. 
> 
> But for the moment, is there a short Mercury program which might
> deduce a square root from its definition:
> 
> sqrt(x) == Y | Y >= 0 and Y*Y = x

The short answer here is no.
Mercury is a programming language, not a theorem prover.
The above equation is a fine specification for sqrt,
but it does not define an algorithm for computing sqrt.

You can easily express that specification in Mercury,
either via a direct translation

	sqrt(X) = Y :- Y >= 0, Y*Y = X.

or even slightly more concisely

	sqrt(Y * Y) = Y :- Y >= 0.

but since it is only a specification, not an algorithm,
it will type check, but it won't pass mode-checking.
If you want to have a program that will compile and
run and that will compute square roots, then you need
to give a different definition for sqrt, one that is
mode-correct, otherwise the Mercury compiler won't know
what algorithm to use.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------