Unification is an algorithm for comparing terms with holes (called unification variables) for equality, discovering substitutions for the unification variables which make those terms equal. Unification of LF terms is used in a variety of ways in Twelf:
- During type and term reconstruction, unification is used to infer omitted type and term information.
- In the logic programming operational semantics of LF, unification is used to find solutions to unification variables in queries.
Unification for LF terms requires higher-order unification, which is undecidable. However, many instances of unification that arise in Twelf fall into the pattern fragment, which is decidable. Those that are not in the pattern fragment are postponed as constraints; unresolved constraints are reported to the user.
This page is incomplete. We should expand it.