 # Homework Assignments Week 1.8: Constraint Resolution (Answers)

## Unification

• 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`.

• 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