Constraint normalization

A minimal solution for an arbitrary set of constraints is found by normalization to a form where the solution is obvious. Figure 16 shows the normalization rules. Constraint set C rewrites to C' in one labeled transition step ( ) if there is a rule , , and . The label is a variable substitution, here the identity substitution.

A labeled transition rule propagates equalities between constraint variables:

We define the reflexive and transitive closure of labeled transitions by: , and if and then . The normalization rules are sound and complete: Finite application of transition rules to a constraint set does not change the set of solutions.

Theorem 1   Let . Substitution solves C iff solves C'.

Proof:

By inspection of the rules in Fig. 16 against the semantics of constraints in Fig. 13.

As an example we consider rule (25):

which is the most complicated rule. Let be a solution for the antecedent. Let us consider the three possibilities for the initial to hold.

• : We have , , and , so solves the consequent.
• : The vcons constraints force and . Obviously, solves the consequent.
• : In this case we must have as well. Therefore, the constraints in the consequent are all solved by .

For the reverse direction we start with the possible solutions of :

• : If we have by dependency and vcons. By equality, we have , too. cannot be D because is not D. Therefore, .
• : Here, and cannot be D, hence and as required.
• : The dependency constraints force and hence as well.

Therefore, the above rule is correct and complete as it neither adds nor removes solutions.

Normalization of an initial constraint set C is the exhaustive application of the normalization rules.

Theorem 2   Constraint normalization terminates for an arbitrary initial constraint set C.

Proof:

For the constraint set C define the tuple (a,b,c,d) as follows:

• a is the sum of the number of function constraints, lift constraints, structure constraints, S-dependencies, M-dependencies, and L-dependencies.
• b is the sum of the number of base value dependencies, non-static dependencies, and memo constraints.
• c is the sum of the number of equality and dependency constraints.
• d is the sum of the number of constraints and the number of clashes ( where the constraint constructors of c and c' differ) not resolved by .

Each application of a rule decreases (a,b,c,d) in the lexicographic order, except rules (25) and (23). If we restrict the applicability of (23) to and apply rule (25) only once to each pair we obtain termination.

The normalized constraint set determines a substitution by ignoring all dependency constraints, interpreting the constraints of the form as equalities, resolving cycles introduced through function and structure constraints by recursive types, and mapping the remaining variables to .

Theorem 3   is a minimal solution of .

Proof:

By construction of the substitution .

From a solution of we can easily construct a completion. We call the completion constructed from the minimal solution a minimal completion. The minimal completion is the result of the binding-time analysis which is passed on to the specializer.

Type reconstruction can be implemented by term graph manipulation of constraint terms similar to Henglein's implementation in quasi-linear time [19]. However, in our case the complexity is at least quadratic in the size of the program: The number of constraints generated is quadratic in the size of the program because we need to relate the free variables of a function to the function itself. The formal presentation of the algorithm and its complexity is beyond the scope of the present paper.