[TYPES] Unification within a quantifier prefix

[Tim Sweeney]

I'm looking for insight into general unification problems of the
following form:

A unification problem consists of an equation within a quantifier
prefix.  The goal is to characterize the solutions to the unification
problem: whether there are none, one, or many possible values for the
existential variables which satisfy the equation.  (This arises as the
core of a typechecking algorithm.)

A quantifier prefix is an ordered list of existential and universal
quantifiers without explicit bounds.  Example: Ex.Ay.Ez.<equation> means
"There exists an x such that, for all y, there exists a z such that
<equation>".

An equation is one of:
- An equality between two terms (t1 = t2)
- A conjunction of two equations (e1 and e2)
- A disjunction of two equations (e1 or e2)
- A negation of an equation (not e1)

A term is one of:
- A variable (x, y, z, ...) bound by the quantifier prefix.
- A lambda expression taking one term to another term (t1->t2).

We can also add constants (0, 1, 2...) to terms, without changing the
expressive power (else we can encode them as Church numerals).

Example unification problems:

- Ex.x=1 - one solution
- Ex.x=1 and x=2 - no solution
- Ay.Ex.x=y - infinitely many solutions
- Ex.Ay.x=y - no solutions
- Ex.Ey.not x=y - infinitely many solutions
- Ef.Ay.f=(y->y) -- one solution (f is the identity function)
- Ef.f=(2->3) -- infinitely many solutions (f comprises all functions
  taking 2 to 3)
- Ef.f=(0->1) & (2->7) -- infinitely many solutions (all functions
  taking 0 to 1, and 2 to 7)
- Ef.Ay.f=(y->y) and f=(2->3) -- no solutions (the identity function
  doesn't take 2 to 3)
- Ex.Ay.x=1 or x=y - one solution
- Ef.Ax.not f=(0->x) -- f is all functions that don't have 0 in their
  domain

Since the resulting system is Turing-complete, we can't expect to find a
decision procedure.  But a partial decision procedure would be very
useful, and it seems (intuitively) like we could define a well-founded
subset of the problem and give a decision procedure over it.  Better yet
would be a decision algorithm which happens to always terminate for
well-founded problems, and diverge for (some) others.

Any references, or suggestions on how to proceed?

Thanks!

Tim Sweeney
Epic Games