Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 16:35
    cfarm6 starred JuliaReach/LazySets.jl
  • 11:14

    schillic on gh-pages

    build based on ee357e0 (compare)

  • 11:02
    schillic updated the wiki
  • 11:01

    schillic on commutative

    (compare)

  • 11:01

    schillic on master

    move binary operation methods t… use commitative macro in minkow… use commitative macro in isdisj… and 2 more (compare)

  • 11:01
    schillic closed #2808
  • 08:38
    uzaynagme starred JuliaReach/LazySets.jl
  • 04:14
    schillic review_requested #2809
  • 02:14
    hugefiver starred JuliaReach/LazySets.jl
  • Aug 04 21:28
    schillic edited #544
  • Aug 04 21:26
    schillic opened #2809
  • Aug 04 21:25

    schillic on 2741

    better cartesian_product for hy… (compare)

  • Aug 04 21:25
    schillic assigned #2741
  • Aug 04 20:52
    schillic opened #544
  • Aug 04 20:52

    schillic on 543

    use commutative macro from Lazy… (compare)

  • Aug 04 19:52
    schillic review_requested #2808
  • Aug 04 18:45
    schillic opened #2808
  • Aug 04 18:44

    schillic on commutative

    use commitative macro in isdisj… use commitative macro in inters… (compare)

  • Aug 04 18:43

    schillic on commutative

    move binary operation methods t… use commitative macro in minkow… use commitative macro in isdisj… and 1 more (compare)

Marcelo Forets
@mforets
i hope he will watch our talk :p
Marcelo Forets
@mforets
i found this review article by him https://sld.cs.columbia.edu/pubs/carloni_now06.pdf
it contains a bunch of interesting hybrid models
Gustavo Goretkin
@goretkin
I have had something about symbolic computation / laziness on my mind for a while, and when I came across LazySets.jlI 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
Gustavo Goretkin
@goretkin

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.

Marcelo Forets
@mforets
Thanks! I should do some reading before I can comment, because I don't know about Base.Fix.. to begin with :smile:
We do have some discussions in the lines of convenience macros for making lazy or concrete opertaions
there is a proof of principle somewhere

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

there is already a LazySets.concretize method
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