An optimised decision algorithm for stratified context unification
- Context unification is a variant of second order unification. It can also be seen as a generalization of string unification to tree unification. Currently it is not known whether context unification is decidable. A specialization of context unification is stratified context unification, which is decidable. However, the previous algorithm has a very bad worst case complexity. Recently it turned out that stratified context unification is equivalent to satisfiability of one-step rewrite constraints. This paper contains an optimized algorithm for strati ed context unification exploiting sharing and power expressions. We prove that the complexity is determined mainly by the maximal depth of SO-cycles. Two observations are used: i. For every ambiguous SO-cycle, there is a context variable that can be instantiated with a ground context of main depth O(c*d), where c is the number of context variables and d is the depth of the SO-cycle. ii. the exponent of periodicity is O(2 pi ), which means it has an O(n)sized representation. From a practical point of view, these observations allow us to conclude that the unification algorithm is well-behaved, if the maximal depth of SO-cycles does not grow too large.
Author: | Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30-9017 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/schauss/strat2000.ps |
Parent Title (German): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 13 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (13) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
Place of publication: | Frankfurt [am Main] |
Document Type: | Working Paper |
Language: | English |
Year of Completion: | 2000 |
Year of first Publication: | 2000 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2005/05/12 |
Source: | Technical Report Frank 13, Institut für Informatik, Johann Wolfgang Goethe-Universität Frankfurt am Main |
HeBIS-PPN: | 11521349X |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Licence (German): | Deutsches Urheberrecht |