<story><title>Now I’m calculating with constructive reals</title><url>https://aperiodical.com/2022/03/now-im-calculating-with-constructive-reals/</url></story><parent_chain><item><author>giomasce</author><text>It&amp;#x27;s unfortunate there is no an equality decision procedure. If two numbers are equal you will see that the difference is zero no matter how much precision you request, but of you always see zero difference you will never know if the numbers are equal or you just have to keep searching.&lt;p&gt;I know that such a decision procedure exists for algebraic number (i.e., you can allow roots of any orders and general polynomial root extraction), but I don&amp;#x27;t know about transcendental functions like exponential and logarithm. And frankly it smells a lot of undecidability. Computational things tend to become undecidable just a little bit after they become interesting, and sometimes even before.</text></item></parent_chain><comment><author>fdej</author><text>There is an algorithm by Richardson to prove equality of real and complex numbers composed from exponentials and logarithms. (It doesn&amp;#x27;t have a complete proof of correctness, but it never returns a wrong result: it will loop forever iff it encounters a counterexample to Schanuel&amp;#x27;s conjecture.)&lt;p&gt;It can also be extended to higher transcendental functions, but it gets harder to guarantee termination.&lt;p&gt;I have a library for exact reals&amp;#x2F;complexes with an incomplete implementation of Richardson&amp;#x27;s algorithm: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;fredrikj.net&amp;#x2F;calcium&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;fredrikj.net&amp;#x2F;calcium&amp;#x2F;&lt;/a&gt;</text></comment>
<story><title>Now I’m calculating with constructive reals</title><url>https://aperiodical.com/2022/03/now-im-calculating-with-constructive-reals/</url></story><parent_chain><item><author>giomasce</author><text>It&amp;#x27;s unfortunate there is no an equality decision procedure. If two numbers are equal you will see that the difference is zero no matter how much precision you request, but of you always see zero difference you will never know if the numbers are equal or you just have to keep searching.&lt;p&gt;I know that such a decision procedure exists for algebraic number (i.e., you can allow roots of any orders and general polynomial root extraction), but I don&amp;#x27;t know about transcendental functions like exponential and logarithm. And frankly it smells a lot of undecidability. Computational things tend to become undecidable just a little bit after they become interesting, and sometimes even before.</text></item></parent_chain><comment><author>chriswarbo</author><text>This technique can&amp;#x27;t be applied to equality, since equality &amp;quot;collapses&amp;quot; the entire decimal expansion down to a single bit: we can&amp;#x27;t make closer and closer approximations, since that first bit requires an infinite amount of work.&lt;p&gt;In fact, talking about &amp;quot;Nth decimals&amp;quot; &lt;i&gt;also&lt;/i&gt; requires an infinite amount of work. For example, what&amp;#x27;s the first digit of &amp;#x27;0.99999... + 0.00000...&amp;#x27;? Note that this is &lt;i&gt;not&lt;/i&gt; the same as &amp;#x27;rounded to one significant digit&amp;#x27;. Let&amp;#x27;s call the numbers x and y; there are a few possibilities:&lt;p&gt;- If y = 0, then the sum is equal to x:&lt;p&gt;- If x eventually has a non-9 digit, then the first digit is 0; e.g. if the third digit is a 3, then the result is 0.993...&lt;p&gt;- If x repeats 9 forever, the first digit can be either 1 or 0, depending on taste&lt;p&gt;- If y &amp;gt; 0, then the result depends on the relative magnitudes of y and (1 - x). The first digit could be 0 (if y &amp;lt; 1 - x), or 1 (if y &amp;gt; 1 - x). If these differences only occur after billions of decimal places, we must go that far through the calculation to determine whether the first digit is 0 or 1!&lt;p&gt;Most computable real representations will actually calculate to within some epsilon, e.g. a power of 10 if we&amp;#x27;re rounding the final decimal when displaying the result. That ensures all of these problems disappear, but of course it introduces uncertainty.&lt;p&gt;We can likewise ask whether two numbers are equal &lt;i&gt;to some precision&lt;/i&gt;; but not necessarily in general.&lt;p&gt;(There might be tricks&amp;#x2F;identities for the particular functions being used in this calculator; but the above applies to &amp;quot;computable reals&amp;quot; in the strictest sense; i.e. where each function is a Universal Turing Machine)</text></comment>