# Narrowing by a call of a number function

[Narrowing](../narrowing.md) › number functions. The names in the examples are those of [section 2](../narrowing.md#2-the-names-in-the-examples).

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](number.md#operations-in-the-comparison), 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](../narrowing.md#10-correctness-obligations-and-checks):

- **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)`.

| Expression | Type | Warnings |
| --- | --- | --- |
| `if floor(x) = 2.5 then 5 else 7` | `number = 7` | `unreachable_branch` |

## `abs`

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

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `abs(x) < 100` | `number in (-100..100)` | `number in [-max..-100], [100..max] \| Null` |
| `abs(x) <= 100` | `number in [-100..100]` | `number in [-max..-100), (100..max] \| Null` |
| `abs(x) > 3` | `number in [-max..-3), (3..max]` | `number in [-3..3] \| Null` |
| `abs(x) >= 3` | `number in [-max..-3], [3..max]` | `number in (-3..3) \| Null` |
| `abs(x) = 3` | `number in -3, 3` | `number in [-max..-3), (-3..3), (3..max] \| Null` |
| `abs(x) = 0` | `number = 0` | `number in [-max..0), (0..max] \| Null` |
| `3 > abs(x)` | `number in (-3..3)` | `number in [-max..-3], [3..max] \| Null` |
| `abs(x) < 0` | — | `number \| Null` |
| `abs(x + 1) < 5` | `number in (-6..4)` | `number \| Null` |
| `abs(x) in [1..5]` | `number in [-5..-1], [1..5]` | `number \| Null` |

| Condition | `dd` when true | `dd` when not true |
| --- | --- | --- |
| `abs(dd) < @"PT1H"` | `days and time duration in (-PT1H..PT1H)` | `days and time duration in [-max..-PT1H], [PT1H..max] \| Null` |
| `abs(dd) = @"PT1H"` | `days and time duration in -PT1H, PT1H` | `days and time duration in [-max..-PT1H), (-PT1H..PT1H), (PT1H..max] \| Null` |

| Condition | `v` when true | `v` when not true |
| --- | --- | --- |
| `abs(v) < 100` | `number in (-100..100) \| list<Any \| Null>` | `Any \| Null` |

## `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.

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `floor(x) = 3` | `number in [3..4)` | `number in [-max..3), [4..max] \| Null` |
| `floor(x) < 3` | `number in [-max..3)` | `number in [3..max] \| Null` |
| `floor(x) <= 3` | `number in [-max..4)` | `number in [4..max] \| Null` |
| `floor(x) > 3` | `number in [4..max]` | `number in [-max..4) \| Null` |
| `floor(x) >= 3` | `number in [3..max]` | `number in [-max..3) \| Null` |
| `ceiling(x) = 3` | `number in (2..3]` | `number in [-max..2], (3..max] \| Null` |
| `ceiling(x) >= 3` | `number in (2..max]` | `number in [-max..2] \| Null` |
| `round up(x) = 3` | `number in (2..3]` | `number in [-max..2], (3..max] \| Null` |
| `round up(x) = -3` | `number in [-3..-2)` | `number in [-max..-3), [-2..max] \| Null` |
| `round down(x) = 3` | `number in [3..4)` | `number in [-max..3), [4..max] \| Null` |
| `round down(x) = 0` | `number in (-1..1)` | `number in [-max..-1], [1..max] \| Null` |
| `round half up(x) = 3` | `number in [2.5..3.5)` | `number in [-max..2.5), [3.5..max] \| Null` |
| `round half down(x) = 3` | `number in (2.5..3.5]` | `number in [-max..2.5], (3.5..max] \| Null` |
| `decimal(x, 0) = 2` | `number in [1.5..2.5]` | `number in [-max..1.5), (2.5..max] \| Null` |
| `decimal(x, 0) = 3` | `number in (2.5..3.5)` | `number in [-max..2.5], [3.5..max] \| Null` |

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `round half up(x, 1) = 2.5` | `number in [2.45..2.55)` | `number in [-max..2.45), [2.55..max] \| Null` |
| `floor(x, 2) = 3.14` | `number in [3.14..3.15)` | `number in [-max..3.14), [3.15..max] \| Null` |
| `floor(x, -1) = 30` | `number in [30..40)` | `number in [-max..30), [40..max] \| Null` |
| `decimal(x, 2) > 1.5` | `number in (1.505..max]` | `number in [-max..1.505] \| Null` |
| `floor(x, y) = 3` | `number` | `number \| Null` |
| `floor(x) = 2.5` | — | `number \| Null` |
| `floor(abs(x)) = 3` | `number in (-4..-3], [3..4)` | `number \| Null` |

| Condition | `n` when true | `n` when not true |
| --- | --- | --- |
| `floor(n) = 3` | `number in [3..4)` | `number in [0..3), [4..10] \| Null` |
| `ceiling(n) = 12` | — | `number in [0..10] \| Null` |
| `round half up(n) >= 5` | `number in [4.5..10]` | `number in [0..4.5) \| Null` |

`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.

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `sqrt(x) < 10` | `number in [0..100)` | `number in [-max..0), [100..max] \| Null` |
| `sqrt(x) > 3` | `number in (9..max]` | `number in [-max..9.000000000000000000000000000000003] \| Null` |
| `sqrt(x) <= 10` | `number in [0..100.0000000000000000000000000000001]` | `number in [-max..0), (100..max] \| Null` |
| `sqrt(x) >= 10` | `number in [100..max]` | `number in [-max..100) \| Null` |
| `sqrt(x) = 10` | `number in [100..100.0000000000000000000000000000001]` | `number in [-max..100), (100..max] \| Null` |
| `sqrt(x) >= 3` | `number in [8.999999999999999999999999999999998..max]` | `number in [-max..9) \| Null` |
| `sqrt(x) < 0` | — | `number \| Null` |
| `sqrt(x) >= 0` | `number in [0..max]` | `number in [-max..0) \| Null` |
| `exp(x) > 1` | `number in (0..14149.38539644841072829055748903541]` | `number in [-max..0.0000000000000000000000000000000009999999999999999999999999999999996], (14149.38539644841072829055748903541..max] \| Null` |
| `exp(x) < 3` | `number in (-14221..1.098612288668109691395245236922527)` | `number in [-max..-14144.78022626242263692252150612604), [1.098612288668109691395245236922526..max] \| Null` |
| `log(x) < 0` | `number in (0..1)` | `number in [-max..0], [1..max] \| Null` |
| `log(x) >= 0` | `number in [1..max]` | `number in [-max..1) \| Null` |
| `log(x) = 1` | `number = 2.718281828459045235360287471352663` | `number \| Null` |
| `log(x) < 3` | `number in (0..20.08553692318766774092852965458173)` | `number in [-max..0], [20.08553692318766774092852965458171..max] \| Null` |

`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](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/edge_bounds_test.exs) 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.

| Condition | `n` when true | `n` when not true |
| --- | --- | --- |
| `modulo(n, 7) = 3` | `number in 3, 10` | `number in [0..10] \| Null` |
| `modulo(n, 7) < 2` | `number in [0..2), [7..9)` | `number in [0..10] \| Null` |
| `modulo(n, 4) = 1` | `number in 1, 5, 9` | `number in [0..10] \| Null` |
| `modulo(n, -7) = -3` | `number = 4` | `number in [0..10] \| Null` |
| `modulo(n, 2.5) = 0` | `number in 0, 2.5, 5, 7.5, 10` | `number in [0..10] \| Null` |
| `modulo(n, 20) = 3` | `number = 3` | `number in [0..10] \| Null` |

| Condition | `age` when true | `age` when not true |
| --- | --- | --- |
| `modulo(age, 50) = 10` | `number in 10, 60, 110` | `number in [0..150] \| Null` |
| `modulo(age, 1000) = 10` | `number = 10` | `number in [0..150] \| Null` |

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `modulo(x, 7) = 3` | `number` | `number \| Null` |

## With `and` and `or`

The facts are those of the comparisons, met and joined ([5](../narrowing.md#5-and-and-or)).

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `abs(x) < 100 and x > 0` | `number in (0..100)` | `number in [-max..0], [100..max] \| Null` |
| `abs(x) < 100 and abs(x) > 10` | `number in (-100..-10), (10..100)` | `number in [-max..-100], [-10..10], [100..max] \| Null` |
| `abs(x) < 1 or floor(x) = 5` | `number in (-1..1), [5..6)` | `number in [-max..-1], [1..5), [6..max] \| Null` |
| `floor(x) < 3 and floor(x) > 1` | `number in [2..3)` | `number in [-max..2), [3..max] \| Null` |

| Condition | `v` when true | `v` when not true |
| --- | --- | --- |
| `floor(v) = 3` | `number in [3..4) \| list<Any \| Null>` | `Any \| Null` |
| `sqrt(v) < 10` | `number in [0..100) \| list<Any \| Null>` | `Any \| Null` |

| Expression | Type | Warnings |
| --- | --- | --- |
| `if abs(x) < 100 then x else null` | `number in (-100..100) \| Null` | — |
| `if abs(k) < 100 then abs(k) else null` | `number in [0..100) \| Null` | — |
| `if floor(x) = 3 then x + 1 else null` | `number in [4..5] \| Null` | — |
| `if sqrt(x) < 10 then sqrt(x) else null` | `number in [0..10] \| Null` | — |
| `if modulo(n, 7) = 3 then n else null` | `number in 3, 10 \| Null` | — |
| `if floor(x, 6177) = 3 then x else null` | `Null` | `decided_condition` |

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`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/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`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/images/number/preimage.ex).