Author name cluster

Val Tannen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

CSL Conference 2021 Conference Paper

Semiring Provenance for Fixed-Point Logic

Katrin M. Dannert
Erich Grädel
Matthias Naaf
Val Tannen

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Details

TCS Journal 2005 Journal Article

XML queries and constraints, containment and reformulation

Alin Deutsch
Val Tannen

Starting from the XQuery language we define XBind, an XML analog of relational conjunctive queries as well as a related class of XML integrity constraints (dependencies). We identify a fragment of XBind for which containment is decidable, in fact Π 2 p -complete, and a further fragment for which containment is NP-complete. We extend the containment algorithm to take XML dependencies into account. We give an algorithm for the reformulation of XBind queries under combinations of GAV and LAV XQuery views, as well as additional dependencies. We prove a completeness theorem which guarantees that under certain conditions, our algorithm will find a minimal reformulation if one exists. Moreover, we identify conditions when this algorithm achieves optimal complexity bounds. Our results on containment and reformulation depend on certain restrictions on the query and constraint languages. We calibrate the results by showing that lifting these restrictions significantly changes the complexity of the problems.

Details DOI

I&C Journal 1996 Journal Article

A Typed Pattern Calculus

Delia Kesner
Laurence Puel
Val Tannen

The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. We present a typed functional calculus that emphasizes the strong connection between the structures of whole pattern definitions and their types. In this calculus, type-checking guarantees the absence of runtime errors caused by non-exhaustive pattern-matching definitions. Its operational semantics is deterministic in a natural way, without the imposition of ad hoc solutions such as clause order or “best fit”. In the spirit of the Curry–Howard isomorphism, we design the calculus as a computational interpretation of the Gentzen sequent proofs for the intuitionistic propositional logic. We prove the basic properties connecting typing and evaluation: subject reduction and strong normalization. We believe that this calculus offers a rational reconstruction of the pattern-matching features found in successful functional languages.

Details DOI

TCS Journal 1995 Journal Article

Principles of programming with complex objects and collection types

Peter Buneman
Shamim Naqvi
Val Tannen
Limsson Wong

We present a new principle for the development of database query languages that the primitive operations should be organized around types. Viewing a relational database as consisting of sets of records, this principle dectates that we should investigate separately operations for records and sets. There are two immediate advantages of this approach, which is partly inspired by basic ideas from category theoryl. First, it provides a language for structures in which record and set types may be freely combined: nested relations or complex objects. Second, the fundamental operations for sets are closely related to those for other “collection types” such as bags or lists, and this suggests how database languages may be uniformly extended to these new types. the most general operation on sets, that of structural recursion, is one in which not all programs are well-defined. In looking for limited forms of this operation that always give rise to well-defined operations, we find a number of close connection with exiting database languages, notably those developed for complex objects. Moreover, even though the general paradigm of structural recursion is shown to be no more expressive than one of the existing languages for complex objects, it possesses certain properties of uniformity that make it a better candidate for an efficient, practical language. Thus rather than developing query languages by extending, for example, relational calculus, we advocate a very powerful paradigm in which a number of well-known languages are to be found as natural sublanguages.

Details DOI