MATH.12:5.3 - Extract a case decision and its answer

For a rational input r=p/q, with integer p and positive integer q, construct either an indication that r=0 or a rational y such that r*y=1.

The proof examines the decidable integer condition p=0:

• If p=0, return Zero with the equality r=0.
• Otherwise return Inverse(q/p). Since p is nonzero, the fraction is defined, and (p/q)*(q/p)=1.

The result includes which case holds. At p=4,q=6 it returns Inverse(3/2). At p=0,q=5 it returns Zero. This tag lets a receiving calculation choose its continuation.

Merely reporting that one of the two conclusions holds loses the branch information the continuation needs. The construction obtains that information by testing an integer, then carries it with the result.

Now replace the rational representation by access to successively narrower rational intervals enclosing an arbitrary real number. The rational procedure’s test p=0 is no longer available. A nondegenerate rational interval containing zero does not by itself establish that the represented real is zero, because it also contains nonzero values. An interval [0,0] would establish equality, but the representation does not guarantee reaching such an interval. The previous proof does not supply a terminating zero test for this representation.

The next move is to obtain an appropriate decision procedure under additional input conditions, change the requested output to allow an unresolved case, or retain the existence conclusion without claiming the obtaining operation. The rational construction remains usable on its stated inputs.