Two Views on Unification: Terms as Strategies

In previous works, the authors have shown that linear application in Geometry of Interaction (GoI) models of lambda-calculus amounts to resolution between principal types of linear  lambda-terms. This analogy also works in the reverse direction. Indeed, an alternative definition of unification between algebraic terms can be given by viewing the terms to be unified as strategies, i.e. sets of pairs of occurrences of the same variable, and verifying the termination of the GoI interaction obtained by playing the two strategies. In this paper we prove that such a criterion of unification is equivalent to the standard one. It can be viewed as a local, bottom-up, definition of unification. Dually, it can be understood as the GoI interpretation of unification. The proof requires generalizing earlier work to arbitrary algebraic constructors and allowing for multiple occurrences of the same variable in terms.