# Taking abstract domains seriously

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.

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

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

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

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

There’s also DomainSets.jl with @daanhb

1 Like

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

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.

I am not entirely sure of the use case of SpecialSets.jl but most of what you wrote looks reasonable.

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.