Homework Assignments Week 1.8: Constraint Resolution (Answers)
Unification

The answer should include:

multiple unifiers may satisfy equalities

all possible unifiers can be created from a mostgeneral 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))
ora > h(y))
respectively.


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()))

A possible unifying substitution is:
a > c, b > f(c), d > f(h()), e > h()

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 typeInt > Int
orString > String
, but its principal type isforall 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