4
$\begingroup$

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?

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.