# Taking abstract domains seriously
**URL:** https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890
**Category:** Specific Domains
**Created:** [November 23, 2018, 4:36am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890 "2018-11-23T04:36:52Z")
**Posts on this page:** 8
**Page:** 1
### Author:  [@HarrisonGrodin](https://discourse.julialang.org/u/HarrisonGrodin)
#### Post date: [November 23, 2018, 4:36am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/1 "2018-11-23T04:36:52Z")
Hi, everyone!
I’ve been planning a redesign for `SpecialSets.jl` to target use cases needed by `Rewrite.jl`, but figured that using representations of abstract/infinite sets shouldn’t require reinventing the wheel. I found the following packages which include relevant features:
- [AbstractDomains.jl](https://github.com/zenna/AbstractDomains.jl) (by @zennatavares)
- [ChainRules.jl](https://github.com/JuliaDiff/ChainRules.jl/blob/master/src/domain.jl) (by @jrevels)
- [SpecialSets.jl](https://github.com/HarrisonGrodin/SpecialSets.jl) (by @HarrisonGrodin)
- [IntervalSets.jl](https://github.com/JuliaMath/IntervalSets.jl) (cc: @tim.holy, @dlfivefifty)
- [IntervalArithmetic.jl](https://github.com/JuliaIntervals/IntervalArithmetic.jl) (cc: @dpsanders)
In this post and the discussion following, I’m hoping to compare the existing packages and come up with a list of necessary features in hopes of developing a common API or central package.
* * *
# Features
Throughout the remainder of this post, sets will be represented using set-builder notation:
\{\ x \mid \ p\_1(x),\ p\_2(x),\ \dots\ \}, where p\_n is a predicate on x
## Elementwise Operations
There should be some way to apply standard functions to each element in a set.
- \{\ y \mid (f(x) = y), p\_1(x),\ p\_2(x),\ \dots\ \}
It’s not entirely clear how operations between multiple sets should behave. The most natural interpretation I came up with is as follows:
```julia
A = {a::Int | a ≥ 0} # pseudocode
@assert A - A == {0} # interpreting as {a-a | a ≥ 0}
@assert A - copy(A) == ℤ # interpreting as {a-a' | a ≥ 0, a' ≥ 0}
```
## Set Operations
Common set operations should obviously be supported: \in, \subseteq, \cup, \cap, set equality, set difference.
There should be default representations of combinations and opportunities to define custom combination rules:
- `{x | isprime(x)} ∪ {x | x < -10}` → `{x | (isprime(x) || x < -10)}` (default union)
- `{x | x > 5} ∩ {x | x > 7}` → `{x | x > 7}` (custom intersection of `>` predicates)
- `{y | (y = 2x), x ∈ ℝ} ∩ {y | (y = 3x), x ∈ ℝ}` → `{y | (y = 6x), x ∈ ℝ}` (custom intersection of operations)
It’s possible that the logic behind this could be derived from an existing SMT solver (e.g. [Z3](https://github.com/zenna/Z3.jl)). Also, we should probably consider how cross-type predicates behave (e.g. `{x | x > 3} ⊆ {x | x > 2.0}`?).
Implicit algebraic properties about these operations (e.g. associativity/commutativity of `∪` and `∩`, transitivity of `⊆`) would also be rather convenient.
## Clear Connection With Julia Types
It seems reasonable to connect set elements with Julia types. There are many ways this could be done:
- `{x | x isa Int, x < 10}` (interpreting types as predicates)
- `{x::Int | x < 10}` (requiring that the most general type of `x` be asserted, drawing inspiration from LiquidHaskell)
We may also want to consider support for more complex typing rules, such as `{xs::AbstractVector{<:Number} | length(xs) > 7}`.
## More…
I neglected to discuss support for dealing with function signatures and variable domains (e.g. `ℝ×ℝ → ℝ`, `x ∈ ℤ⁻ ∪ ℙ`), since it seems like that might belong in an adjacent tool. I’m open to discussing that here as well, though, if people are interested. 🙂
* * *
I doubt this is a comprehensive list, but hopefully it can serve as a starting point for discussion. Looking forward to making headway on this key part of symbolic mathematics in Julia!
-Harrison
---
### Author:  [@Azamat](https://discourse.julialang.org/u/Azamat)
#### Post date: [November 23, 2018, 5:14am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/2 "2018-11-23T05:14:01Z")
> [@HarrisonGrodin](#):
>
> `@assert A - copy(A) == A # interpreting as {a-a' | a ≥ 0, a' ≥ 0}`
Did you mean `A + copy(A) == A`, because the set `A` the way you defined it is not closed under subtraction?
---
### Author:  [@HarrisonGrodin](https://discourse.julialang.org/u/HarrisonGrodin)
#### Post date: [November 23, 2018, 5:16am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/3 "2018-11-23T05:16:47Z")
Ah, my mistake! I meant `A - copy(A) == ℤ`, but your statement should hold, as well.
---
### Author:  [@Azamat](https://discourse.julialang.org/u/Azamat)
#### Post date: [November 23, 2018, 6:29am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/4 "2018-11-23T06:29:32Z")
This also might be of relevance to folks at [NemoCAS](https://github.com/Nemocas) (@wbhart, @jlapeyre)
---
### Author:  [@dlfivefifty](https://discourse.julialang.org/u/dlfivefifty)
#### Post date: [November 23, 2018, 9:23am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/5 "2018-11-23T09:23:24Z")
There’s also DomainSets.jl with @daanhb
---
### Author:  [@jlapeyre](https://discourse.julialang.org/u/jlapeyre)
#### Post date: [November 23, 2018, 10:42am UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/6 "2018-11-23T10:42:25Z")
> [@HarrisonGrodin](#):
>
> Two proposed ways to represent abstractly-defined sets are…
I somehow am missing the motivation for \{f(x) | p\_1(x),\ldots\} rather than just \{x | p\_1(x),\ldots\}. Also, in the case that f is many-to-one, the two representations you give are not equivalent. What is the significance of this ?
---
### Author:  [@HarrisonGrodin](https://discourse.julialang.org/u/HarrisonGrodin)
#### Post date: [November 23, 2018, 4:02pm UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/7 "2018-11-23T16:02:21Z")
The advantage I saw with the f strategy would be purely practical, in that we wouldn’t have to handle backsolving for such complex cases. However, the more I consider it, that isn’t a solution, but instead just delaying the problem; we would still need to backsolve for \in checking and other explicitly complicated cases. Good call - I’ve updated the original post.
---
### Author:  [@zennatavares](https://discourse.julialang.org/u/zennatavares)
#### Post date: [November 23, 2018, 5:20pm UTC](https://discourse.julialang.org/t/taking-abstract-domains-seriously/17890/8 "2018-11-23T17:20:21Z")
I am not entirely sure of the use case of SpecialSets.jl but most of what you wrote looks reasonable.
I’d add:
A key idea (finding?) behind abstract domains is that there are different representations, which capture different properties. Technically they make different approximations. For example the interval domain is more coarse than the polyhedral domain. Any generic package for abstract domains should support that.
You used `copy(A)` to denote seemingly a variable of identical to A but somehow different. I think you need to be rigorous about the identities of variables and what they mean, otherwise you’ll fall into trouble.
When I first designed AbstractDomains i wanted to fit it into the Julia type system, such that I could for example execute real valued functions with real valued abstract domains. You can get this to work some of the time but there is a fundamental incompatibility. It’s a similar incompatibility that people in the autodiff world find when using Dual numbers as Real numbers. For the same reason I find missing values a bit problematic (see [Union{T,Null} inference in structs · Issue #6 · JuliaData/Missings.jl · GitHub](https://github.com/JuliaData/Missings.jl/issues/6#issuecomment-341934836) for my opinion on that). However, with Cassette (@jrevels), some or all of these issues may be circumventable.