Compiler Construction bio photo

Compiler Construction

Twitter Github

Edit on GitHub

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