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