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

[Richard A. O'Keefe]

	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
	
I note that if you start with a halfway decent approximation (like
taking the exponent, so 2**n <= x < 2**n+1, and then taking
	2**(n div 2)*(if n even then 1 else sqrt 2)
) a small fixed number of Newten iterations will polish it off amazingly
quickly.  I think 7 Newten iterations should be good enough for IEEE 754,
just off the top of my head.

I also note that Mercury is typeful, so it _is_ possible to deduce a
square root algorithm from that definition:
    try each non-negative floating-point number in turn until you
    find a solution.
For single-precision floating-point arithmetic, you'll even get an answer
in less than a day.

However, that "definition" just plain doesn't work for floating-point numbers,
because almost no floating-point numbers _have_ exact square roots.

There are programs around (have been since the 70s) that could derive things
like square root algorithms, but they needed things like "square root is
monotone non-decreasing" so that binary search will work.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------