We know that first-order unification is decidable. More generally, if there exists a unifier for a first-order unification problem, then there exists a most general unifier.
I'm interested in the following generalization to second-order unification:
Given a second-order unification problem with a unifier $\sigma$, when can we find a "most general generalization" of $\sigma$?
Fix a second-order theory with a single base sort $\mathrm{tm}$ and without equations. It consists of a collection of function symbols with second-order types. (More generally I'm interested in this question for free dependently-sorted second-order algebraic theories, i.e. dependent type theories without definitional equalities.)
For example we can consider the signature of unityped lambda calculus with two constants $a,b$:
- $\mathrm{app} : \mathrm{tm} \to \mathrm{tm} \to \mathrm{tm}$
- $\mathrm{lam} : (\mathrm{tm} → \mathrm{tm}) → \mathrm{tm}$
- $a : \mathrm{tm}$
- $b : \mathrm{tm}$
Note that I only consider theories without equations, so the $\beta$- and $\eta$-rules are not included in this signature.
A metacontext is a context whose variables (called metavariables) have first-order types.
A unification problem $t \doteq u$ is a pair $(t,u)$ of terms over a metacontext $\Gamma$.
An unifier is a substitution $\sigma : \Delta \to \Gamma$ such that $t[\sigma] = u[\sigma]$, where $\Delta$ is also a metacontext.
I'd like to know if given an unifier $\sigma : \Delta \to \Gamma$, we can always find another unifier $\rho : \Theta → \Gamma$ such that $\sigma$ factors through $\rho$ and every other such factorization of $\sigma$ factors through $\rho$.
Here are some examples:
Consider the unification problem $P(a) \doteq Q(b)$ over the metacontext $(P : \mathrm{tm} \to \mathrm{tm}, Q : \mathrm{tm} \to \mathrm{tm})$.
It has several unifiers. For instance $\sigma_{1} = [P := x \mapsto \mathrm{app}(x,b), Q := x \mapsto \mathrm{app}(a,x)]$ and $\sigma_{2} = [P := x \mapsto \mathrm{app}(a,a), Q := x \mapsto \mathrm{app}(a,a)]$ are two unifiers (both over the empty metacontext). The unifier $\sigma_{3} = [P := x \mapsto R(x,b), Q := x \mapsto R(a,x)]$ over the metacontext $(R : \mathrm{tm} \to \mathrm{tm} \to \mathrm{tm})$ is a common generalization of $\sigma_{1}$ and $\sigma_{2}$, and should be the most general unifier of this unification problem.
Another example is the unification problem $P(a) \doteq a$ over the metacontext $(P : \mathrm{tm} \to \mathrm{tm})$. It has two incomparable unifiers $[P := x \mapsto x]$ and $[P := x \mapsto a]$. Every other unifier should factor through one of these two.
We can also consider $P(Q(a),b) \doteq b$ over $(P : \mathrm{tm} \to \mathrm{tm}, Q : \mathrm{tm} \to \mathrm{tm})$. We have three unifiers $\sigma_{1} = [P := (x,y) \mapsto x, Q := x \mapsto b]$, $\sigma_{2} = [P := (x,y) \mapsto y, Q := x \mapsto R(x)]$ and $\sigma_{3} = [P := (x,y) \mapsto b, Q := x \mapsto R(x)]$. I believe that every other unifier factors through one of these three.
I can also rephrase the question in category theory:
Let $\mathcal{C}$ be a freely generated cartesian category with an exponentiable object. Given two maps $f,g : \Gamma \to \Delta$, an unifier of $f$ and $g$ is a morphism $\rho : \Theta \to \Gamma$ such that $f \circ \rho = g \circ \rho$.
Unifiers of $f$ and $g$ form a category. The terminal object in this category, when it exists, is the equalizer of $f$ and $g$.
Then the question becomes: do all connected components of the category of unifiers have a terminal object?