Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 12:26
    schillic edited #2736
  • 12:25
    JuliaRegistrator commented #1332
  • 12:25
    mforets commented #1332
  • 12:24

    mforets on mforets-patch-9

    (compare)

  • 12:24

    mforets on master

    Update Project.toml (#2740) (compare)

  • 12:24
    mforets closed #2740
  • 08:09

    mforets on gh-pages

    build based on 60fb29d (compare)

  • 08:05

    mforets on gh-pages

    build based on a85d7df (compare)

  • 07:52

    github-actions[bot] on v0.14.14

    (compare)

  • 07:51
    JuliaTagBot commented #376
  • 07:37
    mforets opened #2740
  • 07:37

    mforets on mforets-patch-9

    Update Project.toml (compare)

  • 07:31
    JuliaRegistrator commented #111
  • 07:31
    mforets commented #111
  • 07:31

    github-actions[bot] on gh-pages

    delete history (compare)

  • 07:30

    mforets on master

    Update Project.toml (compare)

  • 07:30

    mforets on cluster_deco

    (compare)

  • 07:30

    mforets on master

    add cluster decompose zono Merge pull request #514 from Ju… (compare)

  • 07:30
    mforets closed #514
  • 07:14

    mforets on gh-pages

    build based on e25033f (compare)

Marcelo Forets
@mforets
i have to go now, cu
Gustavo Goretkin
@goretkin

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.

Gustavo Goretkin
@goretkin

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.

Marcelo Forets
@mforets
ok, thanks for example. i didn't know such things were available!
i recall unevaluated expressions is very useful in symbolic algebra. as in SageMath'shold argument of the symbolic ring (https://doc.sagemath.org/html/en/reference/calculus/sage/symbolic/expression.html).
Marcelo Forets
@mforets
can you explain a bit what do you want to show in
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")
Marcelo Forets
@mforets
"Dispatch is not tenable with anonymous functions:" -- ok, i see
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
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
Marcelo Forets
@mforets
that method is used to overapproximate the intersection between an n-ary cartesian product (.. of any array of lazysets, it could be made of sets or operation or both), and a polyhedron, and the output should be an n-ary cartesian product
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
Marcelo Forets
@mforets
here is one case where @fix would be nice:
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
Marcelo Forets
@mforets
This is even more convenient for cases with several terms eg. inv(A)^2 * (exp(A) - I) * X
then the idea is to dispatch on the support function of that beast; it works by composing the support function rule of every lazy operator
Gustavo Goretkin
@goretkin

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 Discs. 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?

Marcelo Forets
@mforets
yes, i guess that's what i have in mind , that the construction helps with dispatch. for example suppose there's a new operation 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 ρ(d,F)=maxxFoo(...)dTx\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.
This includes, say overapproximate(::Foo, something), or composing eg. ρ(d,AFoo(..)Foo(...))\rho(d, A * Foo(..) \oplus Foo(...))
note that A * Foo(..) just works and is again a lazyset (the lazy linear map of a Foo object)
Gustavo Goretkin
@goretkin

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

Gustavo Goretkin
@goretkin

I am not sure if there are places where the annotation ::LazySet prevents an ambiguity (current or future). For example:

https://github.com/JuliaReach/LazySets.jl/blob/53f21cb9c26355e7f218578e5b4036c3ff0091fe/src/Approximations/overapproximate.jl#L81-L96

written instead as

overapproximate(S,
                         ::Type{<:HPolygon},
                         ε::Real=Inf)
Gustavo Goretkin
@goretkin

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
Marcelo Forets
@mforets
I am not sure if there are places where the annotation ::LazySet
This sometimes prevents piracy eg Plots and Polyhedra export several names that are also used in LazySets
Gustavo Goretkin
@goretkin

This sometimes prevents piracy eg Plots and Polyhedra export several names that are also used in LazySets

Oh, of course, good point.

Gustavo Goretkin
@goretkin
well, wait. To make sure I understand, it's not because of name collisions, right? We're talking about controlling dispatch, which is the only thing that types in julia are arguably for
So e.g. defining RecipesBase.@recipe function somefunction(arg1::LazySet) end)

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}

Gustavo Goretkin
@goretkin
I mentioned them before. The only solution to this is "traits". In fact, if plot recipes used traits, then you probably don't even need 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. So
isoperationtype(::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)
Gustavo Goretkin
@goretkin
Marcelo Forets
@mforets
:thumbsup: LazySets does not use traits, but we have planned to do so for extending the type hierarchy with sets representations which are not convex
Marcelo Forets
@mforets
what is a good way to write a list of equations with documenter?
it uses aligned
Marcelo Forets
@mforets
Christian Schilling
@schillic
:+1:
Marcelo Forets
@mforets
FYI yesterday I added some mathematical details on LGG09 algorithm : https://juliareach.github.io/ReachabilityAnalysis.jl/dev/lib/algorithms/LGG09/#Homogeneous-case-1
Marcelo Forets
@mforets
Christian Schilling
@schillic
:+1:
Peng Yu
@yupbank
image.png
hello firends, wondering if i get some help around understanding this operation
Marcelo Forets
@mforets
hi
Peng Yu
@yupbank

For a discrete set GRnG \subset \mathbb{R}^n .
It is testing condition: zG\forall z \in G if zz spans a ray of cone(G)\operatorname{cone}(G).

Isn't it always true for all elements of GG ?

Marcelo Forets
@mforets
im not familiar with all the details of the paper (i think we have it referenced in a LazySets issue, but the method hasn't been implemented)
i see that line 8 comes from applying Proposition 4.3