## 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 be a language of function symbols and constants. We write for an element of . Let be the set of ground terms in language .

### Syntax of Set Constraints

where

- - set variable
- - standard set operations and relations
- - function symbol
- in , is an integer between 1 and arity of

### Semantic

- - set variable, subset of
- - standard set operations and relations

#### Example1

#### Example2

#### Example3

What is the least solution of constraints

where is constant and is unary function symbol.

#### Example4

What is the least solution of constraints

where is constant, are unary function symbols.

#### Example5

Let where

- are constants representing propositional constants
- is unary function symbol representing negation in abstract syntax tree
- are binary function symbols representing in syntax tree

Then the set of ground terms represents propositional formulas.

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

## Existence of Solutions

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

where is a -morphism (and therefore monotonic and -continuous). The least solution can therefore be computed by fixpoint iteration (but it may contain infinite sets).