mforets on mforets-patch-9
mforets on master
Update Project.toml (#2740) (compare)
mforets on gh-pages
build based on 60fb29d (compare)
mforets on gh-pages
build based on a85d7df (compare)
github-actions[bot] on v0.14.14
mforets on mforets-patch-9
Update Project.toml (compare)
github-actions[bot] on gh-pages
delete history (compare)
mforets on master
Update Project.toml (compare)
mforets on cluster_deco
mforets on master
add cluster decompose zono Merge pull request #514 from Ju… (compare)
mforets on gh-pages
build based on e25033f (compare)
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