Homework Assignments Week 1.8: Constraint Resolution (Answers)

Unification

1. The answer should include:

   • multiple unifiers may satisfy equalities

   • all possible unifiers can be created from a most-general unifier, by applying a substitution to the mgu

   • an mgu’s for these equalities, is

     a -> b, c -> g(), d -> f(b, g()), e -> h(f(b, g())), x -> g()
     

     or

     b -> a, c -> g(), d -> f(a, g()), e -> h(f(a, g())), x -> g()
     

   • the unifier from the question is obtained from the mgu by applying b -> h(y)) or a -> h(y)) respectively.

2. A most general unifier is given by

   b -> i(), c -> g(a, i()), d -> h(h(i(), g(a, i())), a), e -> h(i(), g(a, i()))
   

3. A possible unifying substitution is:

   a -> c, b -> f(c), d -> f(h()), e -> h()
   

4. A given substitution s is a principal unifier if every other unifier s’ is an instance of s. A unifier s’ is an instance of s if a substitution s’‘ exists, such that s’‘ applied to s yields s.

   In the example, any substitution that fixes a term value t for c is still a unifier for the constraints. However, it would not be principal anymore. The substitution s’‘ in this scenario would be given by s -> t.

   Possible additions:

   • Principal unifiers are not necessarily unique. For example, the variables a and c could be swapped in our example solution and it would remain principle.
   • In type systems there is a similar concept: principle types. These are types that are supertypes of all other valid types for a program. For example, the identity function \x -> x may have type Int -> Int or String -> String, but its principal type is forall a. a -> a.

Constraint Semantics

Include the following:

• constraint semantics define when constraints are satisfied by a given solution
• constraint solver is an algorithm that finds a solution for a given constraint
• soundness, completeness, and principality are properties of the solver
• soundness states that every outcome of the solver is valid/correct according to the semantics
• completeness states that if the constraints are satisfiable according to the semantics, the solver returns a solution
• principality states that the solver returns a most general, or principal, solution