Back to Search
Start Over
Source-tracking unification
- Source :
- Information and Computation. (2):121-159
- Publisher :
- Elsevier Inc.
-
Abstract
- We propose a path-based framework for deriving and simplifying source-tracking information for first-order term unification in the empty theory. Such a framework is useful for diagnosing unification-based systems, including debugging of type errors in programs and the generation of success and failure proofs in logic programming. The objects of source-tracking are deductions in the logic of term unification. The semantics of deductions are paths over a unification graph whose labels form the suffix language of a semi-Dyck set. Based on this idea of unification paths, two algorithms for generating proofs are presented: the first uses context-free labeled shortest-path algorithms to generate optimal (shortest) proofs in time O(n3) for a fixed signature, where n is the number of vertices of the unification graph. The second algorithm integrates easily with standard unification algorithms, entailing an overhead of only a constant factor, but generates non-optimal proofs. These non-optimal proofs may be further simplified by group rewrite rules.
- Subjects :
- Unification
Mathematical proof
Logic programming
Theoretical Computer Science
Term unification
Formal language
Path problems
Type inference
Mathematics
Graph theory
Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing)
Computer Science Applications
Algebra
Formal languages
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Shortest path problem
Graph (abstract data type)
Computer Science::Programming Languages
Debugging
Algorithms
Information Systems
Subjects
Details
- Language :
- English
- ISSN :
- 08905401
- Issue :
- 2
- Database :
- OpenAIRE
- Journal :
- Information and Computation
- Accession number :
- edsair.doi.dedup.....05debb4ebc5acf0fe0bf0e90d3a89023
- Full Text :
- https://doi.org/10.1016/j.ic.2004.10.013