How should strict enclosure of interval boxes be defined?

[lucaferranti]

Currently,

julia> a = (1..2) × (3..4)
[1, 2] × [3, 4]

julia> b = (1.5..1.9) × (3..4)
[1.5, 1.90001] × [3, 4]

julia> b ⊂ a
false

That is currently it returns true if all intervals in the first box are strictly contained in the corresponding intervals in the second box.

I wonder whether this is correct, as generally b ⊂ a means that b is a subset of a but is not equal to it, so according to this the example above should return true.

edit: swapped a and b, as they were in the wrong order in the original example

[lbenet]

In your example, both a[1] ⊂ b[1] and a[2] ⊂ b[2] return false, so I think the result is correct.

Perhaps you meant

julia> b ⊂ a
false

In this case we get false because of the evaluation b[2] ⊂ a[2], which is false precisely because b should be properly contained (without being identic) to a.

[mforets]

I also find the definition confusing; from a set perspective: all intervals should be included and at least one of them should be strictly included.

[lucaferranti]

Yes I meant b ⊂ a sorry for the confusion.

Indeed it's not clear to me what "b properly contained in a" means in this case. Considering interval boxes as hyperrectangles, I would think that in this case b ⊂ a holds, see picture below.

[dpsanders]

Usually things like the interval Newton method require that $N(X)$ is in the interior of $X$ for the conclusion to hold.

[lucaferranti]

but ⊂ doesn't check that, for example

julia> (1..2) ⊂ (0..2)
true

apparently there's the function isinterior (or the symbol ⪽, typed \subsetdot+TAB) to check if an interval (intervalbox) is in the interior of another

julia> (1..2) ⪽ (0..2)
false

julia> isinterior(1..2, 0..2)
false

(this actually made me realise I should fix this also in ILA.jl, since there I check all(x .⊂ y) to check if an interval vector is in the interior of the other).

[lbenet]

Let's call a = 1..2 and b= 0..2. Then, a ⊂ b returns true because all elements in a are in b and you can find elements in b which are not in a (e.g., 0). (Is interior checks more or less the same, without including the boundaries of the interval.)

[lucaferranti]

Exactly, so returning to the original example

julia> a = (1..2) × (3..4)
[1, 2] × [3, 4]

julia> b = (1.5..1.9) × (3..4)
[1.5, 1.90001] × [3, 4]

julia> b ⊂ a
false

shouldn't in this case b ⊂ a return true? all elements in b are in a but there are elements in a which are not in b, see picture above.

[lbenet]

I see your point, and have no answer 😬.

Interval boxes are usually though as intervals in many dimensions, and functions such as ⊂ are taken as the element-by-element application of ⊂, i.e. .⊂ in the usual sense of broadcasting, in which case false should be expected.

If, on the other hand, we use the "set perspective" (correct me if this is not the correct expression), b ⊂ a should be interpreted as "all elements of b are inside a, and there exist elements in a which are not in b, in which case i have to agree with you and then b ⊂ a should return true.

I don't recall what the standard says on this, but we should stick to it.

[lucaferranti]

From what I can tell, the standard defines ⊆ and ⪽ but does not say anything about ⊂. The following table is from section 10.5 "Required operations", subsection 10.5.10 "Boolean operations"

[lucaferranti]

which is pretty funny, since both precedes and less have both strict and nonstrict version 🤔

[mforets]

FWIW, enclosure between interval boxes is also used in Picard iteration (see TaylorModels.iscontractive). That said, I think that the (less strict) idea in my previous comment also applies.

[lucaferranti]

Does picard iteration need elementwise (strict) enclosure to work?

[lbenet]

Does picard iteration need elementwise (strict) enclosure to work?

Regarding "element-wise" part, yes, so the enclosure is checked element by element.

Regarding the enclosure part, to prove existence it suffices ⊆, but to prove uniqueness I think ⊂ is required... but I may be wrong. As an example (of a fixed point theorem, or @dpsanders remark), consider the map T(x)=x^2 defined in the (compact) interval X=0..1, which has two fixed points (x=0 and x=1) in X. It is easy to see that T(X) ⊆ X (actually, equality ==) holds; so existence is guaranteed (but not uniqueness). But, for the interval X'=[0,1/2] we have T(X') ⊂ X', and existence and uniqueness follow.

[Kolaru]

as generally b ⊂ a means that b is a subset of a but is not equal to it, so according to this the example above should return true.

I think whether ⊂ is strict depends on the textbook you are using and there is no universally accepted version. That's probably why the standard avoid it entierely.

Regarding the enclosure part, to prove existence it suffices ⊆, but to prove uniqueness I think ⊂ is required... but I may be wrong.

The unicity of the solution for multidimensional Newton and Krawczyk needs the interior, but it relies on consideration about the derivative of the function and not directly on the fixpoint theorem.

For the one dimension Newton method, N(X) ⊆ X and 0 ∉ f'(X) is sufficient to imply unicity.

[schillic]

I think there are some confusions here. Some observations:

1. With the current implementation, a ⊂ b is not equivalent to a ⊆ interior(b), even in 1D. Hence I think the discussion about interior is misleading here.
   Example: a = [1, 2), b = [1, 2]. Clearly a ⊂ b because 2 ∉ a and 2 ∈ b. But 1 ∈ a and 1 ∉ interior(b).
2. In 1D everybody agrees that a ⊂ b iff a ⊆ b ∧ a ≠ b. This is also the implementation for Interval. And indeed this is the common definition of strict subsets in general.
3. According to the documentation, IntervalBox is the Cartesian product of intervals. A Cartesian product typically describes a set.
   

   IntervalArithmetic.jl/src/multidim/intervalbox.jl

   Lines 3 to 6 in df97cdd

   	"""An `IntervalBox` is an `N`-dimensional rectangular box, given
   	by a Cartesian product of a vector of `N` `Interval`s.
   	"""
   	struct IntervalBox{N,T}

From 2. and 3. I conclude that the current result is confusing (I find the picture in #490 (comment) compelling) and I would suggest to use a different function if you need the current implementation (dimension-wise strict subset) (which in fact is just one more symbol in Julia, so maybe a separate function is not needed).