Unification is a generalization of pattern matching that attempts to find a mapping between two expressions that may both contain variables. The unify function implements unification via a recursive process, which performs unification on corresponding parts of two expressions until a contradiction is reached or a viable binding to all variables can be established.

Let us begin with an example. The pattern (?x ?x) can match the pattern ((a ?y c) (a b ?z)) because there is an expression with no variables that matches both: ((a b c) (a b c)). Unification identifies this solution via the following steps:

1. To match the first element of each pattern, the variable ?x is bound to the expression (a ?y c).
2. To match the second element of each pattern, first the variable ?x is replaced by its value. Then, (a ?y c) is matched to (a b ?z) by binding ?y to b and ?z to c.

As a result, the bindings placed in the environment passed to unify contain entries for ?x, ?y, and ?z:

>>> e = read_line("(?x ?x)")
    >>> f = read_line(" ((a ?y c) (a b ?z))")
    >>> env = Frame(None)
    >>> unify(e, f, env)
    True
    >>> env.bindings
    {'?z': 'c', '?y': 'b', '?x': Pair('a', Pair('?y', Pair('c', nil)))}
    

The result of unification may bind a variable to an expression that also contains variables, as we see above with ?x bound to (a ?y c). The bind function recursively and repeatedly binds all variables to their values in an expression until no bound variables remain.

>>> print(bind(e, env))
    ((a b c) (a b c))
    

In general, unification proceeds by checking several conditions. The implementation of unify directly follows the description below.

1. Both inputs e and f are replaced by their values if they are variables.
2. If e and f are equal, unification succeeds.
3. If e is a variable, unification succeeds and e is bound to f.
4. If f is a variable, unification succeeds and f is bound to e.
5. If neither is a variable, both are not lists, and they are not equal, then e and f cannot be unified, and so unification fails.
6. If none of these cases holds, then e and f are both pairs, and so unification is performed on both their first and second corresponding elements.

>>> def unify(e, f, env):
            """Destructively extend ENV so as to unify (make equal) e and f, returning
            True if this succeeds and False otherwise.  ENV may be modified in either
            case (its existing bindings are never changed)."""
            e = lookup(e, env)
            f = lookup(f, env)
            if e == f:
                return True
            elif isvar(e):
                env.define(e, f)
                return True
            elif isvar(f):
                env.define(f, e)
                return True
            elif scheme_atomp(e) or scheme_atomp(f):
                return False
            else:
                return unify(e.first, f.first, env) and unify(e.second, f.second, env)