Two Views on Unification: Terms as Strategies

Abstract

In [Furio Honsell et al., 2024], the authors have shown that linear application in Geometry of Interaction (GoI) models of λ-calculus amounts to resolution between principal types of linear λ-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. In particular, we show that two terms σ and τ unify if and only if R(σ) ⊆̂(τ) ;̂ ({R}(σ) ;̂ {R}(τ))^* and (τ) ⊆̂(σ) ;̂ ({R}(τ) ;̂ {R}(σ))^*, where {R}(σ) denotes the set of pairs of paths leading to the same variable in the term σ, ⊆̂ denotes "inclusion up to substitution" and ;̂ denotes "composition up to substitution".