Feel.Analysis.Preimage (feel v0.1.0)

Copy Markdown View Source

The numbers an operand can be when the result of an operation is in a set (D-122).

Feel.Analysis.Intervals goes from the operands to the result. This goes the other way, for x + 1 > 5: the comparison says the sum is in (5..max] (Feel.Analysis.TestSets), so x is in (4..max]. Given the set that the result is in, the set that the other operand can be, the operator and the side that the operand is on, operand/4 gives the set that the operand is in.

The run rounds a result to 34 digits, to the nearest, so the set is of results after the rounding, and an operand can be a little outside the set that the exact result would give:

  • A bound of the set that a result is above (x + 1 > 5, an open bound of a number of 34 digits) is exact: the rounding keeps the order, and a bound is a number the rounding does not change, so an exact result at or below it is rounded to a number at or below it. The preimage has the same bound, open.
  • A bound that a result may be (x + 1 >= 5, x + 1 = 5) is the bound the exact result can be half a unit of its last digit short of, and still be rounded to it: 9.999999999999999999999999999999999 + 1 is 10.99999999999999999999999999999999|9, which is rounded to 11. The exact preimage is taken of that wider set.
  • The run takes operands of at most 34 digits (more are null with an error, so the condition is not true for them), so the operand is one of the numbers that have that many digits. The wide bound is brought in to the first of them: where no number of 34 digits is in the strip that the rounding adds, as it is for x + 1 >= 5, the bound is 4, as it would be without the rounding.

The operand of a product or a quotient is found from the corners of the intervals (an operation is monotonic in each operand where the other has a sign), and a divisor that gets near zero makes the quotient as large as numbers go. Where zero is in the other operand and in the result a product is zero for any operand, so any number is possible.

iex> alias Feel.Type.NumberSet
iex> result = NumberSet.interval({Decimal.new(5), :open}, NumberSet.max_value())
iex> one = NumberSet.point(Decimal.new(1))
iex> result |> then(&Feel.Analysis.Preimage.operand(:add, :left, &1, one)) |> NumberSet.format()
"(4..max]"
iex> exactly = NumberSet.point(Decimal.new(5))
iex> exactly |> then(&Feel.Analysis.Preimage.operand(:add, :left, &1, one)) |> NumberSet.format()
"4"
iex> two = NumberSet.point(Decimal.new(2))
iex> exactly |> then(&Feel.Analysis.Preimage.operand(:multiply, :left, &1, two)) |> NumberSet.format()
"2.5"

Summary

Types

The operations that an operand can be read back from.

result: :exact says that the result is not rounded (the sum of two whole numbers of months, a number of days); and operand: :whole that the operand is a whole number (months, days), so its bounds are whole numbers.

The side of the operation that the operand is on.

Functions

The set the operand can be: the numbers x for which x <operator> y (side: :left) or y <operator> x (side: :right) is in result, for some y in other. It holds every number that the run can give a result in result for, and no more than the intervals show.

Types

operator()

@type operator() :: :add | :subtract | :multiply | :divide

The operations that an operand can be read back from.

options()

@type options() :: [result: :rounded | :exact, operand: :number | :whole]

result: :exact says that the result is not rounded (the sum of two whole numbers of months, a number of days); and operand: :whole that the operand is a whole number (months, days), so its bounds are whole numbers.

side()

@type side() :: :left | :right

The side of the operation that the operand is on.

Functions

operand(operator, side, result, other, options \\ [])

The set the operand can be: the numbers x for which x <operator> y (side: :left) or y <operator> x (side: :right) is in result, for some y in other. It holds every number that the run can give a result in result for, and no more than the intervals show.