[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #98

Originator: Dan Dougherty (Talk at RTA 2000)
Date: July 2000

Summary: Is unification modulo the theory of allegories decidable?

Let ALL be the equational theory of Allegories. Is unification modulo ALL decidable?

Background:

The notion of "Allegory" has defined by Peter Freyd and Andre Scedrov in their monograph [FS90]. Allegories are to binary relations between sets as categories are to functions between sets. By ALL we refer to the untyped version of the theory (see page 195 of [FS90]).

Validity in this equational theory is decidable (Gutiérrez’ dissertation, Wesleyan University 1999, also see [DG00]). The universal-existential theory over these axioms is undecidable (reduction from the universal-existential theory of free semigroups with constants).

References

[DG00]

Dan Dougherty and Claudio Gutiérrez. Normal forms and reduction for theories of binary relations. In Leo Bachmair, editor, Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 95–109, Norwich, UK, July 2000. Springer-Verlag.

[FS90]

Peter Freyd and Andre Scedrov. Categories and Allegories, volume 39 of North Holland Mathematical Library. North-Holland, 1990.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]