A higher-order unification algorithm for inductive types and dependent types

This paper presents a method to define a set of mutually recursive inductive types, and develops a higher-order unification algorithm for λΠΣ extended with inductive types. The algorithm is an extension of Elliott's algorithm for λΠΣ. The notation of normal forms plays a vital role in higher-order unification. The weak head normal forms in the extended type theory is defined to reveal the ultimate “top level structures” of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algorithm can construct recursive functions automatically.