Taking abstract domains seriously

Specific Domains
1

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:

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:

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). 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. :slight_smile:

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

5 Likes
2

Did you mean A + copy(A) == A, because the set A the way you defined it is not closed under subtraction?

3

Ah, my mistake! I meant A - copy(A) == ℤ, but your statement should hold, as well.

4

This also might be of relevance to folks at NemoCAS (@wbhart, @jlapeyre)

5

There’s also DomainSets.jl with @daanhb

1 Like
6

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 ?

2 Likes
7

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.

8

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 for my opinion on that). However, with Cassette (@jrevels), some or all of these issues may be circumventable.

2 Likes