Резюме
Да, если:
a и a2 - 32-разрядные целые числа, b и b2 являются ненулевыми значениями Java double, а a / b = a2 / b2,
тогда a / b равно a2 / b2. (Обратите внимание, что a / b обозначает арифметику действительных чисел, тогда как a / b обозначает арифметику с плавающей точкой. 4 / 3 точно равно 1 is, а 4./3 равно 1,3333333333333332593184650249895639717578887939453125.)
Доказательство
Согласно комментарию автора, это для Java, которая использует IEEE 754, включая базовую 64-битную двоичную с плавающей точкой IEEE-754 для double.
Основным свойством большинства операций с плавающей запятой является то, что вычисляемый результат представляет собой результат действительного числа, округленный до ближайшего значения, представляемого в формате с плавающей запятой. Следствием этого является:
- Если две операции имеют одинаковый результат с действительным числом и используют одно и то же правило округления, они имеют одинаковый результат с плавающей запятой.
(Существуют различные правила округления. В Java используются округления до ближайших связей к четным, что означает использование ближайшего представимого значения, а при наличии связи - кандидата с четным младшим битом .)
Другое следствие:
- Если результат операции с действительным числом представлен в формате с плавающей запятой, это результат с плавающей запятой. (Ошибка округления отсутствует.)
Теперь давайте рассмотрим выражения a / b и a2 / b2. Из-за смешанных типов первым шагом в каждом из них является преобразование a или a2 соответственно из целочисленного типа в double. Вопрос подсказывает нам, что целочисленный тип имеет 32 бита. Все 32-битные целые числа точно представимы в double (потому что double имеет 53-битные значения). Математическим результатом преобразования значения, конечно же, является само значение, поскольку преобразование предназначено для изменения типа, а не значения. Следовательно, результат преобразования a или a2 в double в точности равен a или a2, соответственно.
Далее идет деление, a / b или a2 / b2. Нам говорят, что a / b = a2 / b2. Это говорит нам о том, что результат действительного числа a / b равен результату действительного числа a2 / b2. Поскольку эти две операции имеют одинаковый результат вычисления действительного числа и используют одно и то же правило округления, их результаты с плавающей запятой одинаковы.
Обсуждение
Некоторые ограничения вышеперечисленного:
- Если
a или a2 может превышать 53 бита, оно может иметь значение, не представляемое в double. Тогда операция преобразования его в double должна будет округлить его. Округление может по-разному влиять на a и a2, и тогда коэффициенты a / b и a2 / b2 могут отличаться.
- Некоторые языки программирования не являются строгими в отношении того, как выполняются операции с плавающей запятой, и они не соответствуют правилам IEEE-754. Я считаю, что вышеизложенное относится к Java, но могут быть проблемы в C или C ++.
Обратите внимание, что b и b2 могут быть настолько малы (включая ноль), что частное переполняется, и вычисляемый результат равен бесконечности. Тем не менее, тот факт, что a / b = a2 / b2 потребует, чтобы оба результата были бесконечными или нет - правило о том, что результаты с плавающей точкой равны действительным числам равны, все еще сохраняется.
Если a, a2, b и b2 являются нулями, то обе операции будут создавать NaN, но два NaN не будут сравниваться как равные.
Если a и a2 не равны нулю, а b и b2, то обе операции приведут к бесконечности. Знак будет XOR знаков числителя и делителя. Это означает, что a / b и a2 / b2 могут создавать разные бесконечности (одну положительную, одну отрицательную), даже если a = a2 и b = b2, потому что IEEE-754 имеет + + и -0 , которые сравнивают равные, но имеют разные знаки.