mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
2.04k stars 120 forks source link

Arithmetic & Prolog conundrum #1013

Closed jacobfriedman closed 3 years ago

jacobfriedman commented 3 years ago

I'm looking for a system which solves ?- 1.21 =:= 1.1*1.1. ... scryer yields false.

How can this be made true?

@triska please feel free to jump in here as I am at a significant roadblock in my platform of choice.

triska commented 3 years ago

1.1 cannot be exactly represented as a floating point number, since 0.1 is periodic in base 2:

$ bc -l
obase=2
1/10
.0001100110011001100110011001100110011001100110011001100110011001100

Consider using Scryer Prolog's rational numbers to reason about fractions exactly:

?- (1 + 21 rdiv 100) =:= 11 rdiv 10 * 11 rdiv 10.
   true.
UWN commented 3 years ago

What Every Computer Scientist Should Know About Floating-Point Arithmetic

jacobfriedman commented 3 years ago

Right, but this assumes I would want a fraction as output (or an input)

This same problem occurs in every computer language.

I was discussing epsilon with others (their idea) as a symbolic representation of the infinitesimally small complement. Andrew Dougherty pointed me to hyperreals. Well-known hyperreals seem to be matched well for DCGs!

The BNR library assumes a float output and can handle the calculation with the similar output "style" (type). That's just where I simply took this simple example from. There's an epsilon example in a BNR manual which I must look into further.

I also asked on gprolog, and Daniel Diaz suggested clpr - and to move to SWI - which can handle with a GNU arithmetic library. But this doesn't account for the hyperreals.

I want to reason as much as I can over finite, and perhaps infinite domains. One example is bigger than a max integer (which I would not be able to express here!) On a time axis, I should be able to do that. If we have a stream, why not handle a huge number. SWI does this very well, but I'm unable to reason about this in any other prolog system.

How would such symbols be adequately reasoned about, with infinity in mind?

How can we perform CLP over hyperreals?

On Tue., Aug. 3, 2021, 4:41 p.m. Markus Triska, @.***> wrote:

1.1 cannot be exactly represented as a floating point number, since 0.1 is periodic in base 2:

$ bc -lobase=21/10 .0001100110011001100110011001100110011001100110011001100110011001100

Consider using Scryer Prolog's rational numbers to reason about fractions exactly:

?- (1 + 21 rdiv 100) =:= 11 rdiv 10 11 rdiv 10.* true.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mthom/scryer-prolog/issues/1013#issuecomment-892151280, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFKHXXWJNU7FOAM364QQ2LT3BH7JANCNFSM5BPR2QHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

jacobfriedman commented 3 years ago

This was a good read, thank you!

Say X = Π

``` X ≈ 3; X ≈ 3.1; X ≈ 3.14 ... ```

Of course, the best-fit for the bit would be a representation in 32/64, however the system works; which we have already (pi/0).

The approximation is chosen with the system we have, but the accurate method of symbolic expression we like to use is lost. It's precise, but on a completely different scale.

How can the accuracy be retained for such computations?

On Wed., Aug. 4, 2021, 4:10 a.m. UWN, @.***> wrote:

What Every Computer Scientist Should Know About Floating-Point Arithmetic https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mthom/scryer-prolog/issues/1013#issuecomment-892458332, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFKHXS27WOSZN3SAVGWKGLT3DYZHANCNFSM5BPR2QHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

UWN commented 3 years ago

Note that current CLPR implementations have the same floating point problems. They have some rounding epsilon to hide problems most of the time, but not always.

Here is the one based on Christian Holzbaur's CLP(QR) implementation in SWI:

?- {X= 1.21, Y = 1.1*1.1}, X = Y.
false.

?- {X= 1.21, Y = 1.1*1.1}, {X = Y}.
X = 1.21,
Y = 1.2100000000000002 ;
false.

Hyperreal/surreal numbers are about infinite and infinitesimal quantities. That is not the problem here. The quantities by which these numbers differ are regular quantities. That is epsilon in R, it's even in Q.

Rationals are probably the best way, but be warned, over time they tend to get larger and larger. Floats cut off that part. That is, the size of a number remains constant with floats. With some interval arithmetics - ideally based on unum arithmetic - things could remain manageable. But that's my speculation only.

jacobfriedman commented 3 years ago

Thank you for the insight. I ran into unums a very long time ago but didn't have the perspective I do today to fully realise a practical implementation.

I am looking at the iso8601 time-spec. Given an interval of 0.1 seconds on an infinite axis, with the problems that exist here, we would not have a "good time".

Perhaps in prolog unums could be implemented with typed variables to include range/precision (and such other methods). From my quick glance, unum posits perform well. I'll look into this further; such a library would be great.

On Wed., Aug. 4, 2021, 5:07 a.m. UWN, @.***> wrote:

Note that current CLPR implementations have the same floating point problems. They have some rounding epsilon to hide problems most of the time, but not always.

Here is the one based on Chrisitian Holzbaur's CLP(QR) implementation in SWI:

?- {X= 1.21, Y = 1.1*1.1}, X = Y. false.

?- {X= 1.21, Y = 1.1*1.1}, {X = Y}. X = 1.21, Y = 1.2100000000000002 ; false.

Hyperreal/surreal numbers are about infinite and infinitesimal quantities. That is not the problem here. The quantities by which these numbers differ are regular quantities. That is epsilon in R, it's even in Q.

Rationals are probably the best way, but be warned, over time they tend to get larger and larger. Floats cut off that part. That is, the size of a number remains constant with floats. With some interval arithmetics - ideally based on unum arithmetic - things could remain manageable. But that's my speculation only.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mthom/scryer-prolog/issues/1013#issuecomment-892494996, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFKHXUBD4G3Q6RMKWBOERDT3D7NBANCNFSM5BPR2QHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

UWN commented 3 years ago

0.1 seconds? Here is one prominent example how this rounding error caused fatalities. The easiest way to circumvent this problem is to take a decimal fraction of a second as a base unit. Like a millisecond.

jacobfriedman commented 3 years ago

Yes, so on and so forth (centuries, pico, etc.). I don't see why time should be granted such a capability over any other unit of measure. The base unit of iso8601 is expressed as seconds — I would like to be able to use that in absolutely ANY case.

My solution will be to use BNR and SWI for now, if only to complete my simple tasks in this way. It is not easy to make such a choice. The easiest isn't always the best. I hope Scryer, and other implementations, along with the ISO, could work toward a truly symbolic representation of these conundrums.

On Wed., Aug. 4, 2021, 6:45 a.m. UWN, @.***> wrote:

0.1 seconds? Here is one prominent example https://www.google.com/search?channel=fs&client=ubuntu&q=rounding+error+patriot+missile how this rounding error causes fatalities. The easiest way to circumvent this problem is to take a decimal fraction of a second as a base unit. Like a millisecond.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mthom/scryer-prolog/issues/1013#issuecomment-892556574, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFKHXXZ6P2R4WGGAKELEQ3T3EK3VANCNFSM5BPR2QHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

UWN commented 3 years ago

why time should be granted such a capability over any other unit of measure

Because we expect to add up one-by-one small increments of time much more frequently than other units. (And, if I am at it, you could change the base ("radix") from 2 to 10, that would solve this problem and is even conforming (See 7.1.3). Yet, you would get greater numerical instabilities.)

I cannot see how BNR will help you in this respect, but good luck anyway.

(Unums would help you detect the rounding error. But they cannot solve this problem as fundamentally as you expect.)

UWN commented 3 years ago

BTW, did you in the meantime investigate other programming languages? I am sure they have already solutions we could copy cheaply.

jacobfriedman commented 3 years ago

Thanks for the follow-up! Floating-point precision is exactly that... 'precision'. It's inaccurate. Truth lies in symbolic representations. If we want to do error calculations, it's easy to start with ± in utf-8. BNR uses an interval such as ⟨0.100000000, 0.100000001〉. Unums are a solution, but there can still be representational errors. hyperreal calculus should solve this problem. "Floating-point is a [mere] approximation of R*" (Goldberg 1991, pp. 21-22) ...

I believe a solution can be found in the symbolic expression of hyperreals. Here's an excerpt "On the Strength of Nonstandard Analysis", C. Henson, H. Keisler, from the journal of symbolic logic in 1986. Is Prolog a language equipped to handle such expressions? It must be!

I'm sure you don't need more info for the perspective, but as a future reference for myself and others:

UWN commented 3 years ago

Seriously, that's all over the top. Non-standard analysis related notions might be of interest for re-formulating calculus. And could (cough cough) be of relevance to some program analysis tools. But that is extremely far-fetched.

What is more down-to-earth is ISO 8601 as you mentioned it before and how it is used and represented in various other programming languages. That is a way to go. I hoped you would go in that direction.

jacobfriedman commented 3 years ago

I've already started integrating clpBNR into ISO8601; I agree it's, more practical. I asked about the initial problem because I was curious about how the inaccuracy was handled.

If we're being serious, I don't think it's right to say that area of research is over-the-top. If ISO8601 can be used to position satellites, it's literally not looking for a down-to-earth solution. I asked this because of the precision that was required. You may ask why I assertz(time_axis(real, 'wgs84'('G1762'))).

In all fairness, something being far-fetched is just a matter of time.

UWN commented 3 years ago

@triska suggested rationals that solve all these issues related to precision.