Please use this identifier to cite or link to this item: doi:10.22028/D291-25201
Title: String unification is essentially infinitary
Author(s): Hoche, Michael
Siekmann, Jörg
Szabo, Peter
Language: English
Year of Publication: 2008
SWD key words: Künstliche Inteligenz
Free key words: E-unification
equational theory
universal algebra
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: A unifier of two terms s and t is a substitution sigma such that ssigma=tsigma and for first-order terms there exists a most general unifier sigma in the sense that any other unifier delta can be composed from sigma with some substitution lambda, i.e. delta=sigmacirclambda. This notion can be generalised to E-unification , where E is an equational theory, =_{E} is equality under E andsigmaa is an E-unifier if ssigma =_{E}tsigma. Depending on the equational theory E, the set of most general unifiers is always a singleton (as above), or it may have more than one, either finitely or infinitely many unifiers and for some theories it may not even exist, in which case we call the theory of type nullary. String unification (or Löb's problem, Markov's problem, unification of word equations or Makanin's problem as it is often called in the literature) is the E-unification problem, where E = {f(x,f(y,z))=f(f(x,y),z)}, i.e. unification under associativity or string unification once we drop the fs and the brackets. It is well known that this problem is infinitary and decidable. Essential unifiers, as introduced by Hoche and Szabo, generalise the notion of a most general unifier and have a dramatically pleasant effect on the set of most general unifiers: the set of essential unifiers is often much smaller than the set of most general unifiers. Essential unification may even reduce an infinitary theory to an essentially finitary theory. The most dramatic reduction known so far is obtained for idempotent semigroups or bands as they are called in computer science: bands are of type nullary, i.e. there exist two unifiable terms s and t, but the set of most general unifiers is not enumerable. This is in stark contrast to essential unification: the set of essential unifiers for bands always exists and is finite. We show in this paper that the early hope for a similar reduction of unification under associativity is not justified: string unification is essentially infinitary. But we give an enumeration algorithm for essential unifiers. And beyond, this algorithm terminates when the considered problem is finitary.
Link to this record: urn:nbn:de:bsz:291-scidok-42939
Series name: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Series volume: 08-01
Date of registration: 25-Nov-2011
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
RR_08_01.pdf5,36 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.