Clarify user interface for applying lazy and concrete operations

[schillic]

In #148 we added functions like minkowski_sum. (The following is copied from the discussion started in #174.)

Why did we not add a MinkowskiSum constructor for Zonotopes? Answer: Because we wanted to reserve the MinkowskiSum constructor for the lazy operation.

I think that currently the design is inconsistent. For some lazy operations we actually do a concrete operation (like LinearMap(lm::LinearMap), MinkowskiSum(E::EmptySet, S::LazySet)) and for some concrete operations and only some types we have another function (like minkowski_sum). Why should the user know what to use? (in particular in an application where you do not know the set type in advance!)

I was thinking if we should have this:

minkowski_sum(S1::LazySet, S2::LazySet)
    return MinkowskiSum(S1, S2)
end
minkowski_sum(Z1::Zonotope, Z2::Zonotope)
    # what we did here
end
minkowski_sum(E::EmptySet, S::LazySet)
    return S
end
minkowski_sum(T1::Type1, T2::Type2) # other type combinations where concrete implemenations are simple
    ...
end

Then we could remove the specific MinkowskiSum constructors like MinkowskiSum(E::EmptySet, S::LazySet). The user would use this new function instead and "under the hood" we decide what happens (lazy or concrete).

But now I realized that this is a design decision and I do not have an opinion here. Previously you had to call the constructor MinkowskiSum and it either created a lazy MinkowskiSum object or, in special cases, skipped it (EmptySet). Now we have the mixture (sometimes you have to call the constructor and sometimes it is concrete; sometimes you have to call this function to get the concrete implementation).

The question is if we want to give the user the freedom to choose between lazy and concrete set operations. I see three options for who decides between lazy and concrete operations:

1. We decide: We only provide one interface (namely the MinkowskiSum constructor). In that case we should remove the function minkowski_sum wrote and add a respective constructor.
2. The user decides: The constructor MinkowskiSum is always lazy; the function minkowski_sum is always concrete if possible (and lazy otherwise).
3. The user can decide but we provide also a default choice.

We currently prefer the most general answer (3.), but it requires some discussion. Example implementation: The constructor MinkowskiSum is always lazy; the function minkowski_sum gets a new argument from the domain {"lazy", "concrete", "default"} with default value "default". Alternative: Have three functions minkowski_sum_lazy, minkowski_sum_concrete, and minkowski_sum.

[mforets]

i like option 3 as well. maybe a macro can be used like @concrete begin ... end, such that A ⊕ B -> minkowski_sum(A, B, lazy=false).

[schillic]

Good idea 👍

[mforets]

This issue should resolve the lazy/concrete intersection usage. Currently we have:

julia> begin
E = Ellipsoid(ones(2), diagm([2.0, 0.5]))
B = Ball1([2.5, 1.5], .8)

import LazySets.Approximations.overapproximate
polyoverapprox(x) = HPolytope(overapproximate(x, 1e-3).constraints)

Epoly = polyoverapprox(E)
Bpoly = polyoverapprox(B)
X = intersect(Epoly, Bpoly)
end

julia> @which intersect(Epoly, Bpoly)
intersect(X, Y) in LazySets at /Users/forets/.julia/v0.6/LazySets/src/Intersection.jl:36

julia> using Polyhedra

julia> @which intersect(Epoly, Bpoly)
intersect(P1::LazySets.HPolytope{N}, P2::LazySets.HPolytope{N}) where N<:Real in LazySets at /Users/forets/.julia/v0.6/LazySets/src/HPolytope.jl:272

I think it is better to reserve Intersection(Epoly, Bpoly) for the lazy intersection, compare e.g. to LinearMap, while reserving intersect, or intersection, for the concrete operations.

Meanwhile, @concrete Intersection(Epoly, Bpoly) should trigger the concrete function, if it exists.

[schillic]

Proposal: add a function concretize which, given a set, constructs a concrete set by applying the concrete counterpart (e.g., minkowski_sum for a MinkowskiSum object) and (recursively!) calling concretize on the operands.

Then the proposed @concrete X ∩ Y ⊕ Z would just translate to concretize(X ∩ Y ⊕ Z). There is of course the overhead of creating the lazy objects but this macro should not be used in library code anyway.

[mforets]

The following techniques are relevant to this discussion: https://github.com/JuliaIntervals/IntervalArithmetic.jl/issues/355#issuecomment-582638887 and https://github.com/JuliaIntervals/IntervalArithmetic.jl/issues/355#issuecomment-582649415

EDIT. This is a proof of principle using Cassette:

using LazySets, Cassette
Cassette.@context ConcreteMinkowskiSumCtx
const concrete_minkowski_sum_ctx = Cassette.disablehooks(ConcreteMinkowskiSumCtx())

Cassette.overdub(::ConcreteMinkowskiSumCtx, ::typeof(+), X::LazySet, Y::LazySet) = LazySets.minkowski_sum(X, Y)

concrete_minkowski_sum(f) = Cassette.overdub(concrete_minkowski_sum_ctx, f)

concrete_minkowski_sum() do
    X, Y = rand(VPolygon), rand(VPolygon)
    X + Y
end

VPolygon{Float64,Array{Float64,1}}(Array{Float64,1}[[-4.387680426840783, 2.877203090673391], [...]]

[schillic]

concretize was added in #2228.

concretize can be thought as an expression transformation from CamelCase to underscore (the module StringCases.jl contains such transformations). so i would suggest to consider using a generated function (or a macro, @concretize) that implements such rule once (ie. dispatch on LazySet)

Originally posted by @mforets in https://github.com/JuliaReach/LazySets.jl/pull/2228#issuecomment-660794543

[mforets]

Here are other suggestions (from slack):

• make lazy the default and move all other functions into a LazySets.Eager module where it could be used manually.

• use materialize or collect (which kinda act like the Base operations for evaluating the lazy operations).

• pass a keyword argument which would make a call eager if wanted.