Narrowing by a call of a number function

Narrowing › number functions. The names in the examples are those of section 2.

A comparison of a call of abs, floor, ceiling, round up, round down, round half up, round half down, decimal, sqrt, log, exp or modulo with a value says what the argument is, as the comparison of an arithmetic operation does (number, D-122): when abs(x) < 100 is true the call is a number, so x is too, and it is a number for which the call gives a result below 100, which is (-100..100). The else must also include failures: a null argument, a negative number for sqrt, or an invalid scale. Selected inverse rules keep those failure regions and can narrow both branches; unsupported cases leave the else broad (D-194). An allowed value is a condition on ? (D-161), so abs(?) < 100 as an allowed value narrows the name in the same way, and so does an in (abs(x) in [1..5]).

The rules use these principles, within the common budgets and correctness limits:

• The call is not null. An argument that is null, or of a kind the function does not take, is excluded (abs(s) < 100 leaves no string), and a list of one number is the number it holds, so a name that may be a list keeps the lists: floor(v) = 3 leaves number in [3..4) | list<Any | Null> for an Any.

• Inverse rules aim to keep exactly the inputs that give the result, within their budgets. Roots, logarithms and exponentials need additional approximation because the run rounds to 34 digits (below). Where nothing gives the result (floor(x) = 2.5), the fact leaves nothing. Selected call-preimage checks can detect this even if the branch never reads x: if floor(x) = 2.5 then 5 else 7 is number = 7 with unreachable_branch (D-194). Other impossible facts are detected when their subject is read. A condition whose own type already rules out true instead gets decided_condition.
• An argument that is an operation or a call is read in turn: abs(x + 1) < 5 leaves x in (-6..4), and floor(abs(x)) = 3 leaves (-4..-3], [3..4).

abs

The results and their negatives. A duration is the same, on its seconds or months.

floor, ceiling, round * and decimal

A call rounds a number to a scale, the number of digits after the point (0 if none is given), and the scale is cut to a whole number in -6111..6176. The result is a multiple of the step 10^-scale, so the numbers that give a set of results are those between the step before the first and the step after the last: floor(x) = 3 is [3..4), round half up(x) = 3 is [2.5..3.5) (a tie goes away from zero), round half down(x) = 3 is (2.5..3.5], decimal(x, 0) = 2 is [1.5..2.5] (a tie goes to the even number), round up(x) = 3 is (2..3] (away from zero) and round down(x) = 3 is [3..4) (toward it). The set is exact. The scale has to be one number (a literal, or a name that has only one); with a name that has many, the call says only that the argument is a number.

floor(x) = 2.5 leaves nothing of x (no number has that floor), so the branch where it is true cannot be taken (D-152); ceiling(n) = 12 is decided by the types, since the call is in [0..10].

sqrt, log and exp

The run rounds each to 34 digits, to the nearest, and the end of the argument has to allow for that:

• An end of the results that is not included (sqrt(x) < 10, sqrt(x) > 3) is exact: the rounding keeps the order, and a bound of 34 digits is not changed by it, so a number that gives a result below 10 has a root below 10. This gives x < 100 and x > 9.
• An end that is included (<=, >=, =) is one that the value can be half a unit of its last digit short of, and still be rounded to. The search moves inward from there, using the run itself, to the first number that gives a result in the set (a few numbers; the inverse is ln and exp, one unit of the last digit either way): sqrt(x) >= 10 is [100..max], where the root of the number just below 100 is 9.999…9; sqrt(x) <= 10 is [0..100.0000000000000000000000000000001], since that is a number whose root rounds to 10. sqrt(x) >= 3 is [8.999999999999999999999999999999998..max], the first number with the root 3. If the search finds none within 24 numbers, the number from the inverse is kept, which gives a larger set.
• Where the run has no result, the argument stops: exp(x) is a number for x up to 14149.38539644841072829055748903541 (found with the run, and held to it by the tests), so exp(x) > 1 is (0..14149.38…]; below -14221 the result is below the smallest number, and the numbers between that and -14144.78… give a representable result only when the digits of the result happen to be zeros.

log(x) = 1 is one number: the one just above e (2.718281828459045235360287471352662|4977…) is the only one of 34 digits whose logarithm the run rounds to 1.

Numeric endpoints and conservative fallback

A result interval is a hull, not an enumeration of the steps a rounding function can return. Rounding images cut their endpoints outward to representable 34-digit FEEL numbers (D-220). Near max, an exact integer step such as max - 1 need not itself be representable, so the bound can widen to max. Power inference stays total for an unsupported endpoint; root, logarithm and exponential images fall back to signature bounds if they cannot read an endpoint. Preparing such an expression must not raise or infer a smaller set by dropping the corner. The edge-bound regressions exercise these compositions at the range limits.

modulo by one number

modulo(x, m) is x - m * floor(x / m), which is in [0..m) for a positive m and in (m..0] for a negative one, and is exact. The numbers that give a remainder in a set are the remainders and the multiples of m added to them, as many as the multiples there are, so the fact is about the set of the name that it is applied to: it keeps the part of the set that is a remainder away from a multiple, if that is 16 intervals or fewer, and leaves the set as it was otherwise. A name without allowed values has all the numbers, so it is left as it is.

With and and or

The facts are those of the comparisons, met and joined (5).

The last row is a scale outside the range: the call is null, so the condition is never true.

What is left

• The else branch holds the arguments for which the comparison is false and those for which the call is null. abs, floor, ceiling, round * and decimal of a number are numbers that can be written, so abs(x) < 100 is not true for the numbers from 100 on, nor for null. sqrt, log and exp can be null, and Feel.Analysis.Failure says for which arguments: sqrt for the negative numbers, log for those and zero, exp for those above 14149.38… and below -14144.78… (past that the result is always written, see above). So sqrt(x) < 10 is not true for an x below 0 or from 100 on. The preimage of the results that make the comparison false is a hull for these three, as it is for the then (a unit of the last digit either way), which is an outer approximation and is what the else needs; @unread_else in Feel.Analysis.Narrowing is the list of names to leave unread, if a case turns up where it is not enough. If the other side may be null, the comparison may be unknown for any argument, so the not-true branch may have to keep them all.
• A call is not read as a set of the values it gives beyond the hull of its ends: floor(x) for x in [0.5..3.7] is [0..3], and not the whole numbers 0, 1, 2, 3 (the granularity of D-161, step D), so floor(x) = 2.5 is not decided.
• even and odd give a boolean that says the argument is whole, which a set cannot express.
• A scale or a divisor that is not one number (floor(x, k), modulo(x, m)) says that the argument is a number, and no more.

Tests: number_function_narrowing_test.exs has the types, the branches against the run for many values, and the numbers of each function against the run at the ends of the sets and the numbers next to them; the code is analysis/images/number/preimage.ex.