## The Inequality That Governs Round-Trip Conversions: A Partial ProofBy Rick Regan (Published May 11th, 2015) I have been writing about the spacing of decimal and binary floating-point numbers, and about how their relative spacing determines whether numbers round-trip between those two bases. I’ve stated an inequality that captures the required spacing, and from it I have derived formulas that specify the number of digits required for round-trip conversions. I ## Base Conversion TheoremDavid W. Matula states and proves this theorem, which governs round-trip conversions: Given The inequality specifies the precision required of both bases to make the gaps in the original base ( Proof of the theorem requires two steps: - If
*B*^{n}<*v*^{m-1}, then conversions from*B*round-trip through*v*. - If conversions from
*B*round-trip through*v*, then*B*^{n}<*v*^{m-1}.
The first step shows that the inequality is a (Matula states his theorem in different terms and symbols than I’ve used. For example, he uses the phrase ## Decimal/Binary Round-TripsFor our purposes, we want to apply this theorem to decimal/binary conversions, so I will restate it concretely as two separate theorems: **Decimal-binary-decimal:***d*-digit decimal numbers round-trip through*b*-bit binary numbers if and only if 10^{d}< 2^{b-1}.**Binary-decimal-binary:***b*-bit binary numbers round-trip through*d*-digit decimal numbers if and only if 2^{b}< 10^{d-1}.
## Existing Proofs of The Sufficient ConditionSeveral authors have done partial proofs of the theorem, for the sufficient condition only: I. Goldberg, Kahan, D. Goldberg, and Muller et al. (p. 41-3). I. Goldberg does it for decimal-binary-decimal round-trips, and Kahan, D. Goldberg, and Muller et al. do it for binary-decimal-binary round-trips. D. Goldberg’s proof is limited to IEEE single-precision binary floating-point. Muller et al., though they state that the inequality is “a necessary and sufficient condition”, only prove the sufficient condition. I like the proofs of D. Goldberg and Muller et al; they use a simple gap-based argument. (Frankly, I could not follow the other proofs in detail.) I will give my own proof, based on D. Goldberg’s and Muller et al.’s technique, for both decimal-binary-decimal and binary-decimal-binary round-trips, and for any precision. ## Gap Size Determines Round-TripA number is said to round-trip if it converts back to itself after being converted to an intermediate base. This can only happen when the gaps in the original base are greater than or equal to the gaps in the intermediate base. (Gap size can only be equal for integers, where the gaps line up exactly and thus conversion is exact; I won’t consider this special case of equal gap size any further.) To see why, consider what happens during a conversion; let’s use decimal-binary-decimal conversion as an example. Let gap ## What Matula Has To Say About Gap Size and Round-TripsIn his paper Base Conversion Mappings Matula says
## My Proof of The Sufficient Condition: Decimal-Binary-DecimalLet Consider the interval [10 In [10 Starting with 10 Combining powers, this simplifies to 2 ## My Proof of The Sufficient Condition: Binary-Decimal-BinaryThis proof is symmetric to the one above, so will read similarly. Consider the interval [10 In [10 Starting with 2 Combining powers, this simplifies to 10 ## Open Question: Proving The Necessary ConditionI would like to see a proof of the D. Goldberg uses a counterexample to prove the necessary condition for binary-decimal-binary conversion from IEEE single-precision binary floating-point, but I am looking for a general proof (Matula’s proof is general but not in the above style). What seems to make this direction harder is that there are some ranges where less precision than called for by the inequality will work. Any takers? |