## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Jul 23 23:41

mforets on gh-pages

build based on 93cbffa (compare)

• Jul 23 23:04

mforets on flowpipe_ops

• Jul 23 23:04

mforets on master

generalize reach-set constructo… update exp docstring erge branch 'master' into mfore… and 3 more (compare)

• Jul 23 23:04
mforets closed #533
• Jul 23 22:20

mforets on gh-pages

• Jul 23 21:44
mforets opened #533
• Jul 23 21:44

mforets on flowpipe_ops

fix docstring more function overloads (compare)

• Jul 23 19:21

mforets on gh-pages

build based on fa3d68c (compare)

• Jul 23 18:57

github-actions[bot] on gh-pages

delete history (compare)

• Jul 23 18:57

schillic on plots

• Jul 23 18:57

schillic on master

do not import Plots functions t… Merge pull request #244 from Ju… (compare)

• Jul 23 18:57
schillic closed #244
• Jul 23 18:57

mforets on gh-pages

• Jul 23 18:55

mforets on gh-pages

build based on 46803fd (compare)

• Jul 23 18:53

mforets on gh-pages

build based on b657986 (compare)

• Jul 23 18:32
schillic opened #244
• Jul 23 18:32

schillic on plots

do not import Plots functions t… (compare)

• Jul 23 18:29

github-actions[bot] on gh-pages

delete history (compare)

• Jul 23 18:29
schillic review_request_removed #243
• Jul 23 18:29

github-actions[bot] on gh-pages

delete history (compare)

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 $\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. $\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

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)
Gustavo Goretkin
@goretkin

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}

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
hello firends, wondering if i get some help around understanding this operation