Understanding constraint formula concept in Java JLS defined a concept called "constraint formula". There is a formal definition:


  Constraint formulas are assertions of compatibility or subtyping that
  may involve inference variables. The formulas may take one of the
  following forms:
  
  
  ‹Expression → T›: An expression is compatible in a loose invocation context with type T (§5.3).
  ‹S → T›: A type S is compatible in a loose invocation context with type T (§5.3).
  ‹S &lt;: T›: A reference type S is a subtype of a reference type T (§4.10).
  ‹S &lt;= T›: A type argument S is contained by a type argument T (§4.5.1).
  ‹S = T›: A reference type S is the same as a reference type T (§4.3.4), or a type argument S is the same as type argument T.
  ‹LambdaExpression →throws T›: The checked exceptions thrown by the body of the LambdaExpression are declared by the throws clause of the
  function type derived from T.
  ‹MethodReference →throws T›: The checked exceptions thrown by the referenced method are declared by the throws clause of the function
  type derived from T.
  


I have some misunderstanding about it. As far as I've understood we have a set of all Java types, denote it by M. Could we say, that any constraint formula defines a subset of M, for instance 

‹S &lt;: T› = {S | (S belongs to M) and (S is a subtype of T) }
First, not all of the constraint formulas work with types, some of them work with expressions, or other objects. For example, what would be the set for the formula ‹1+1 → Integer›?

Second, a formula might contain zero, one (at either position) or two inference variables (denoted by Greek letters). What would be the set for ‹String → Object›, ‹α → Object›, ‹String → α›, or ‹α → β›?

Third, I think you should think about constraint formulas as predicates, not as sets. For example, the formula ‹String &lt;: Object› is satisfied, while ‹Object &lt;: String› isn't.

And when you have a constraint formula with inference variables, you can start talking about sets of types (or sets of pairs of types for formulas with two variables) that satisfy the formula.

This means that I think that the closest you can get to your equation would be something like:

{α | ‹α &lt;: T› } = {α | (α belongs to M) and (α is a subtype of T) }

(Though the second part is unnecessarily verbose, "α is a subtype of T" already implies "α belongs to M".)