[TYPES] Unification within a quantifier prefix

[Alwen Tiu]

You might want to check the following paper. It addresses the type of
unification problem you mentioned.

Dale Miller. Unification Under a Mixed Prefix. Journal of Symbolic 
Computation 14(4), 1992.

-Alwen

Tim Sweeney wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>