Function Symbols in Tuple-Generating Dependencies: Expressive Power and Computability

Tuple-generating dependencies -- for short tgds -- have been a staple of database research throughout most of its history. Yet one of the central aspects of tgds, namely the role of existential quantifiers, has not seen much investigation so far. When studying dependencies, existential quantifiers and -- in their Skolemized form -- function symbols are often viewed as two ways to express the same concept. But in fact, tgds are quite restrictive in the way that functional terms can occur. In this paper, we investigate the role of function symbols in dependency formalisms that go beyond tgds. Among them is the powerful class of SO tgds and the intermediate class of nested tgds. In addition, we employ Henkin quantifiers -- a well-known concept in the area of logic -- and introduce Henkin tgds to gain a more fine-grained understanding of the role of function symbols in dependencies. For members of these families of dependency classes, we investigate their expressive power, that is, when one dependency class is equivalently representable in another class of dependencies. In addition, we analyze the computability of query answering under many of the well-known syntactical decidability criteria for tgds as well as the complexity of model checking.