mforets on gh-pages
build based on 93cbffa (compare)
mforets on flowpipe_ops
mforets on master
generalize reach-set constructo… update exp docstring erge branch 'master' into mfore… and 3 more (compare)
mforets on gh-pages
build based on ad11bb2 (compare)
mforets on flowpipe_ops
fix docstring more function overloads (compare)
mforets on gh-pages
build based on fa3d68c (compare)
github-actions[bot] on gh-pages
delete history (compare)
schillic on plots
schillic on master
do not import Plots functions t… Merge pull request #244 from Ju… (compare)
mforets on gh-pages
build based on 4cad9c1 (compare)
mforets on gh-pages
build based on 46803fd (compare)
mforets on gh-pages
build based on b657986 (compare)
schillic on plots
do not import Plots functions t… (compare)
github-actions[bot] on gh-pages
delete history (compare)
github-actions[bot] on gh-pages
delete history (compare)
LazySets.jl
I tried to make sense of how it might relate. I don't know how to explain it well, but I tried to briefly mention it here: goretkin/FixArgs.jl#21
Perhaps in summary, instead of making new "human" names for things like MinkowskiSum
, instead have a generic family of types that represents that in terms of an existing type. In julia, every function (not method) has its own type, and so if there is a minkowski_sum
function, then minkowski_sum(a,b)
performs some computation, and @fix minkowski_sum(a,b)
represents doing that computation, even if there is no method defined for typeof(a)
and typeof(b)
. The overall hope I have is that using something like FixArgs.jl
in LazySets.jl
would be a benefit, either by reducing the lines of code, or by enforcing a constraint that e.g. Translation
is directly tied to translate
, not just because of the definition of the concretize
method, but because Translation
is just a alias for something like FixArgs{typeof(translate), ... }
.
There is a readability problem to try to address because types in julia can be hard to see at a glance. And there's also a chance it puts a big burden on the compiler. I don't know for sure the risks, but I know that it's not a 100% straightforward idea. I would love to chat about it if there's any interest in the idea.
would be a benefit, either by reducing the lines of code
yes, i think something along those lines can be a benefit. i'll share the issue when i find it
LazySets.concretize
method
about the macro, at some point i played with https://github.com/JuliaReach/LazySets.jl/issues/175#issuecomment-583594153
oh thanks for linking to this! I'll take a look.
because I don't know about
Base.Fix..
to begin with :smile:
This is an excerpt from the README that I included to try to explain what I see as the "big win" of Base.Fix{1/2}
:
Dispatching on the Fix
type enables a certain form of symbolic computation.
For example, take a specific method of the findfirst
function:
findfirst(p::Union{Fix2{typeof(isequal),Int},Fix2{typeof(==),Int}}, r::OneTo{Int}) =
1 <= p.x <= r.stop ? p.x : nothing
The fallback for findfirst
(triggered by e.g. findfirst(x->x==3, 1:10)
instead of findfirst(==(3), 1:10)
) would produce the same (correct) answer, but the method above will be quicker.
hold
argument of the symbolic ring (https://doc.sagemath.org/html/en/reference/calculus/sage/symbolic/expression.html).
julia> f1 = x -> x == 0
#1 (generic function with 1 method)
julia> f2 = Base.Fix1(==, 0)
(::Base.Fix1{typeof(==),Int64}) (generic function with 1 method)
julia> f3 = x -> x == 0
#3 (generic function with 1 method)
julia> f4 = Base.Fix1(==, 0)
(::Base.Fix1{typeof(==),Int64}) (generic function with 1 method)
julia> typeof(f2) === typeof(f4)
true
julia> typeof(f1), typeof(f3)
(var"#1#2", var"#3#4")
julia> @which findfirst(x->x==3, 1:10)
findfirst(testf::Function, A::Union{AbstractString, AbstractArray}) in Base at array.jl:1861
julia> @which findfirst(==(3), 1:10)
findfirst(p::Union{Base.Fix2{typeof(==),T}, Base.Fix2{typeof(isequal),T}}, r::AbstractUnitRange) where T<:Integer in Base at array.jl:1867
julia> using LazySets, SparseArrays, Expokit
julia> A = sprandn(1000, 1000, 0.1); X = rand(Hyperrectangle, dim=1000);
julia> typeof(A * X)
LinearMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},Float64,SparseMatrixCSC{Float64,Int64}}
julia> typeof(exp(Matrix(A)) * X) # computes exp(A) eagerly
LinearMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},Float64,Array{Float64,2}}
julia> typeof(SparseMatrixExp(A) * X) # lazy matrix exponential on sets
ExponentialMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}}}
julia> @fix exp(A) * X # should have the same effect
what i don't see is.. if the approach is composable? one of the key advantages of using lazy set types is that we can dispatch on a composition of operations, for example
If I understand what you mean about composing, then it's something I'm trying to figure out now. There's a PR that gives one solution. And I wrote a small book (:-/) about it with a geometric set example here: https://github.com/goretkin/FixArgs.jl/issues/16#issuecomment-738457696 . In summary: a "ring" (annulus) is a setdiff
of two Disc
s. In LazySets.jl
you would probably introduce a LazyDiff
struct.
also, having sets to be on the same footing as lazy operations (in the sense that both subtype LazySet) has turned out to be extremely useful
Yeah, that's probably something you would have to give up. I think giving it up might not be so bad if you wanted to use a trait like IsLazySet
. But now we're talking about adding even more generality.
Both being a subtype of LazySet
helps somewhere with dispatching? Or does it help in a different way?
Foo(A, B, X, ..)
where the arguments are arrays or lazysets. if we let Foo <: LazySet
and we know how to compute the support function, i.e. implement ρ(d::AbstractVector, F::Foo)
where $\rho(d, F) = \max_{x \in Foo(...)} d^T x$, then we can reuse a lot of code that has been written generically using support functions.
overapproximate(::Foo, something)
, or composing eg. $\rho(d, A * Foo(..) \oplus Foo(...))$
A * Foo(..)
just works and is again a lazyset (the lazy linear map of a Foo object)
https://github.com/JuliaReach/LazySets.jl/blob/master/src/Approximations/overapproximate.jl#L1202
I dug into this at https://github.com/goretkin/FixArgs.jl/issues/21#issuecomment-739122718 There are some features that FixArgs.jl
needs still, but I hope it helps to see what the composition looks like
I am not sure if there are places where the annotation ::LazySet
prevents an ambiguity (current or future). For example:
written instead as
overapproximate(S,
::Type{<:HPolygon},
ε::Real=Inf)
Binding the value of N
is a separate problem, but I think fixable. Same with constraints, like ensuring two LazySets
have the same N
.
Alternatively, maybe there could be something like
struct LazySet2{N, T<:FixArgs.Fix} <: LazySet{N}
_::T # it is possible to avoid naming a field when there is only one. access with `lazyset2._`.
end
RecipesBase.@recipe function somefunction(arg1::LazySet) end)
an actual example: https://github.com/JuliaReach/LazySets.jl/blob/53f21cb9c26355e7f218578e5b4036c3ff0091fe/src/Plotting/plot_recipes.jl#L228
So, yes, I agree.
So assuming that something like LazySet2
(but with a better name) is the right solution (I am not sure), then there is still a need to encode the information that is encoded by the type hierarchy now, e.g.
abstract type AbstractAffineMap{N, S<:LazySet{N}} <: LazySet{N} end
and
struct LinearMap{N<:Real, S<:LazySet{N}, NM, MAT<:AbstractMatrix{NM}} <: AbstractAffineMap{N, S}
LazySets
. I'm not sure if LazySets.jl
uses anything traits-like already. I (and lots of other julia people) use "traits" specifically to mean things that can control dispatch. Soisoperationtype(::Type{<:AbstractAffineMap}) = true
is not a trait by this definition, since julia can't dispatch on true
or false
. But it can, however, dispatch on Val{true}
and Val{false}
(and for that matter, Val{true}()
and Val{false}()
as well)
aligned