LARA

Definition of Set Constraints

Set constraints are a logic used in program analysis. In set constraints, each variable denotes a set of ground terms.

Let $L$ be a language of function symbols and constants. We write $f \in L$ for an element of $L$. Let $GT$ be the set of ground terms in language $L$.

Syntax of Set Constraints

\begin{equation*}
\begin{array}{l}
  S ::= v | S \cap S | S \cup S | S \setminus S | f(S, ..., S) | f^{-i}(S) \\
  F ::= S \subseteq S \mid F \land F
\end{array}
\end{equation*}

where

  • $v$ - set variable
  • $\cap,\cup,\setminus,\subseteq$ - standard set operations and relations
  • $f \in L$ - function symbol
  • in $f^{-i}$, $i$ is an integer between 1 and arity of $f$

Semantic

  • $v$ - set variable, subset of $GT$
  • $\cap,\cup,\setminus,\subseteq$ - standard set operations and relations
  • $f(S_1,\ldots,S_n) = \{ f(t_1,\ldots,t_n) \mid t_1 \in S_1,\ldots, t_n \in S_n \}$
  • $f^{-i}(S) = \{ t_i \mid f(t_1,\ldots,t_n) \in S \}$

Example1

\begin{equation*}
    f(\{a,f(b,b)\},\{b,c\}) = \{ f(a,b),f(a,c),f(f(b,b),b), f(f(b,b),c) \}
\end{equation*}

Example2

\begin{equation*}
    f^{-2}(\{a,f(a,b),f(f(a,a),f(c,c))\}) = \{b,f(c,c)\}
\end{equation*}

Example3

What is the least solution of constraints

\begin{equation*}
\begin{array}{l}
  a \subseteq S \\
  f(f(S)) \subseteq S 
\end{array}
\end{equation*}

where $a$ is constant and $f$ is unary function symbol.

Example4

What is the least solution of constraints

\begin{equation*}
\begin{array}{l}
  a \subseteq S \\
  black(S) \subseteq S \\
  red(black(S)) \subseteq S
\end{array}
\end{equation*}

where $a$ is constant, $red,back$ are unary function symbols.

Example5

Let $L = \{a_1,\ldots,a_n, not, and, or, implies\}$ where

  • $a_1,\ldots,a_n$ are constants representing propositional constants
  • $not$ is unary function symbol representing negation in abstract syntax tree
  • $and,or,implies$ are binary function symbols representing $\land,\lor,\rightarrow$ in syntax tree

Then the set of ground terms $GT$ represents propositional formulas.

What does the least solution of these constraints represent (where $S$,$P$ are set variables):

\begin{equation*}
\begin{array}{l}
  a_1 \subseteq P \\
  \ldots \\
  a_n \subseteq P \\
  P \subseteq S \\
  not(P) \subseteq S \\
  and(S,S) \subseteq S \\
  or(S,S) \subseteq S
\end{array}
\end{equation*}

Existence of Solutions

We were able to talk about “the least solution” because previous examples can be rewritten into form

\begin{equation*}
  (S_1,\ldots,S_n) = F(S_1,\ldots,S_n)
\end{equation*}

where $F (2^{S})^n \to (2^{S})^n$ is a $\sqcup$-morphism (and therefore monotonic and $\omega$-continuous). The least solution can therefore be computed by fixpoint iteration (but it may contain infinite sets).

Example

Previous example can be rewritten as

\begin{equation*}
\begin{array}{l}
  P = P \cup a_1 \cup \ldots a_n \\
  S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S)
\end{array}
\end{equation*}

Is every set expression in set constraints monotonic?

Conditional Constraints

Let us simplify this expression:

\begin{equation*}
    f^{-1}(f(S,T)) =
\end{equation*}

\begin{equation*}
   = f^{-1}(\{ f(s,t) \mid s \in S, t \in T \}) 
\end{equation*}

\begin{equation*}
   = \{ s_1 \in S \mid \exists t_1 \in T \}
\end{equation*}

\begin{equation*}
   = \left\{ \begin{array}{rl} 
       S, \mbox{ if } T \neq \emptyset \\
       \emptyset, \mbox{ if } T = \emptyset
              \end{array}
     \right.
\end{equation*}

Consider conditional constraints of the form

\begin{equation*}
    T \neq \emptyset \rightarrow S_1 \subseteq S_2
\end{equation*}

We can transform it into

\begin{equation*}
    f(S_1,T) \subseteq f(S_2,T)
\end{equation*}

for some binary function symbol $f$. Thus, we can introduce such conditional constraints without changing expressive power or decidability.