Unification source-tracking with application to diagnosis of type inference.

摘要

Prior diagnoses in unification-based type reconstruction systems have either missed information that is relevant, presented irrelevant details, or both.; We use a framework based on the Unification Logics of Le Chenadec to define, derive and simplify proof-based source-tracking for term unification. The objects of source-tracking are proofs in this deduction system, and correspond to path expressions over a unification graph whose labels form a semi-Dyck language of balanced parentheses. Simplification of source-tracking information is implemented as proof normalization in the rewrite system for free groups. Subject-reduction properties guarantee that normalization preserves the semantics of deductions. The presentation of the logic facilitates proof construction by a simple extension to standard unification algorithms.; We apply unification source-tracking to type inference in the Curry-Hindley type system. Programs are represented as systems of syntax equations. Program slices correspond to weakenings of syntax and type equations. A constraint generation function maps weakenings of type equations to weakenings of syntax equations. Source-tracking information is defined in terms of the inverse of this generating function.; Unification is central to many applications of symbolic computation and artificial intelligence, including computer algebra, automated theorem proving, expert systems, and programming language type systems. Source-tracking is a debugging technique based on tracing the execution of a program to identify those subparts that contribute to the result of the execution.