International audience

JSON Schema is an important, evolving standard schema language for families of JSON documents. It is based on a complex combination of structural and Boolean operators, including negation, as well as mutually recursive variables. The static analysis of JSON Schema documents comprises practically relevant problems, including schema satisfiability, inclusion, and equivalence. These three can be reduced to witness generation: given a schema, generate an element of the schema — if it exists — otherwise report unsatisfiability. Schema satisfiability, inclusion, and equivalence have been shown to be decidable, by reduction to reachability in alternating tree automata. However, no witness generation algorithm has yet been formally described. We contribute a first, direct algorithm for JSON Schema witness generation. We study its effectiveness and efficiency, in experiments over several schema collections, including thousands of real-world schemas. Our focus is on the completeness of the language (where we only exclude the "uniqueItems" operator), on the ability of the algorithm to run in reasonable time on a large set of real-world examples, despite the exponential complexity of the problem, and on proving its correctness and completeness.

International audience

JSON Schema is the de-facto standard schema language for JSON data. The language went through many minor revisions, but the most recent versions of the language, starting from Draft 2019-09, added two novel features, dynamic references and annotation-dependent validation , that change the evaluation model. Modern JSON Schema is the name used to indicate all versions from Draft 2019-09, which are characterized by these new features, while Classical JSON Schema is used to indicate the previous versions. These new “modern” features make the schema language quite difficult to understand and have generated many discussions about the correct interpretation of their official specifications; for this reason, we undertook the task of their formalization. During this process, we also analyzed the complexity of data validation in Modern JSON Schema, with the idea of confirming the polynomial complexity of Classical JSON Schema validation, and we were surprised to discover a completely different truth: data validation, which is expected to be an extremely efficient process, acquires, with Modern JSON Schema features, a PSPACE complexity. In this paper, we give the first formal description of Modern JSON Schema, which we have discussed with the community of JSON Schema tool developers, and which we consider a central contribution of this work. We then prove that its data validation problem is PSPACE-complete. We prove that the origin of the problem lies in the Draft 2020-12 version of dynamic references, and not in annotation-dependent validation. We study the schema and data complexities, showing that the problem is PSPACE-complete with respect to the schema size even with a fixed instance but is in P when the schema is fixed and only the instance size is allowed to vary. Finally, we run experiments that show that there are families of schemas where the difference in asymptotic complexity between dynamic and static references is extremely visible, even with small schemas.

JSON Schema is a schema language for JSON documents, based on a complex combination of structural operators, Boolean operators (negation included), and recursive variables. The static analysis of JSON Schema documents comprises practically relevant problems, including schema satisfiability, inclusion, and equivalence. These problems can be reduced to witness generation: given a schema, generate an element of the schema --- if it exists --- and report failure otherwise. Schema satisfiability, inclusion, and equivalence have been shown to be decidable. However, no witness generation algorithm has yet been formally described. We contribute a first, direct algorithm for JSON Schema witness generation, and study its effectiveness and efficiency in experiments over several schema collections, including thousands of real-world schemas.

International audience

International audience

International audience

In this paper we present the first JSON type system that provides the possibility of inferring a schema by adopting different levels of precision/succinctness for different parts of the dataset, under user control. This feature gives the data analyst the possibility to have detailed schemas for parts of the data of greater interest, while more succinct schema is provided for other parts, and the decision can be changed as many times as needed, in order to explore the schema in a gradual fashion, moving the focus to different parts of the collection, without the need of reprocessing data and by only performing type rewriting operations on the most precise schema.

The last few years have seen the fast and ubiquitous diffusion of JSON as one of the most widely used formats for publishing and interchanging data, as it combines the flexibility of semistructured data models with well-known data structures like records and arrays. The user willing to effectively manage JSON data collections can rely on several schema languages, like JSON Schema, JSound, and Joi, as well as on the type abstractions offered by modern programming and scripting languages like Swift or TypeScript. The main aim of this tutorial is to provide the audience (both researchers and practitioners) with the basic notions for enjoying all the benefits that schema and types can offer while processing and manipulating JSON data. This tutorial focuses on four main aspects of the relation between JSON and schemas: (1) we survey existing schema language proposals and discuss their prominent features; (2) we analyze tools that can infer schemas from data, or that exploit schema information for improving data parsing and management; and (3) we discuss some open research challenges and opportunities related to JSON data.

With the widespread diffusion of social networks and the dawn of data-intensive scientific applications, graphs became one of the foundations for modern data management applications. A key role in graph querying and analysis is played by Regular Path Queries, their extensions, and, in particular, GXPath. In this demo we will present PathGraph, a distributed GXPath query processor, and its web-based graphical interface.

In the recent years JSON affirmed as a very popular data format for representing massive data collections. JSON data collections are usually schemaless. While this ensures sev- eral advantages, the absence of schema information has im- portant negative consequences: the correctness of complex queries and programs cannot be statically checked, users cannot rely on schema information to quickly figure out the structural properties that could speed up the formulation of correct queries, and many schema-based optimizations are not possible. In this paper we deal with the problem of inferring a schema from massive JSON datasets. We first identify a JSON type language which is simple and, at the same time, expressive enough to capture irregularities and to give com- plete structural information about input data. We then present our main contribution, which is the design of a schema inference algorithm, its theoretical study, and its implemen- tation based on Spark, enabling reasonable schema infer- ence time for massive collections. Finally, we report about an experimental analysis showing the effectiveness of our ap- proach in terms of execution time, precision, and conciseness of inferred schemas, and scalability.

Regular Expressions (REs) are ubiquitous in database and programming languages. While many applications make use of REs extended with interleaving ( shuffle ) and unordered concatenation operators, this extension badly affects the complexity of basic operations, and, especially, makes membership NP-hard, which is unacceptable in most practical scenarios. In this article, we study the problem of membership checking for a restricted class of these extended REs, called conflict-free REs , which are expressive enough to cover the vast majority of real-world applications. We present several polynomial algorithms for membership checking over conflict-free REs. The algorithms are all polynomial and differ in terms of adopted optimization techniques and in the kind of supported operators. As a particular application, we generalize the approach to check membership of Extensible Markup Language trees into a class of EDTDs (Extended Document Type Definitions) that models the crucial aspects of DTDs (Document Type Definitions) and XSD (XML Schema Definitions) schemas. Results about an extensive experimental analysis validate the efficiency of the presented membership checking techniques.

Pig Latin is a popular language which is widely used for parallel processing of massive data sets. Currently, subexpressions occurring repeatedly in Pig Latin scripts are executed as many times as they appear, and the current Pig Latin optimizer does not identify reuse opportunities. We present a novel optimization approach aiming at identifying and reusing repeated subexpressions in Pig Latin scripts. Our optimization algorithm, named PigReuse, identifies subexpression merging opportunities, selects the best ones to execute based on a cost function, and reuses their results as needed in order to compute exactly the same output as the original scripts. Our experiments demonstrate the effectiveness of our approach.

XQuery is a general-purpose programming language for processing semi-structured data, and as such, it is very expressive. As a consequence, optimizing and parallelizing complex analytics XQuery queries is still an open, challenging problem.

Increasing volumes of data are being produced and exchanged over the Web, in particular in tree-structured formats such as XML or JSON. This leads to a need of highly scalable algorithms and tools for processing such data, capable to take advantage of massively parallel processing platforms. This work considers the problem of efficiently parallelizing the execution of complex nested data processing, expressed in XQuery. We provide novel algorithms showing how to translate such queries into PACT, a recent framework generalizing MapReduce in particular by supporting many-input tasks. We present the first formal translation of complex XQuery algebraic expressions into PACT plans, and demonstrate experimentally the efficiency and scalability of our approach.

The development of Semantic Web (RDF) brings new requirements for data analytics tools and methods, going beyond querying to semantics-rich analytics through warehouse-style tools. In this work, we fully redesign, from the bottom up, core data analytics concepts and tools in the context of RDF data, leading to the first complete formal framework for warehouse-style RDF analytics. Notably, we define i) analytical schemas tailored to heterogeneous, semantics-rich RDF graph, ii) analytical queries which (beyond relational cubes) allow flexible querying of the data and the schema as well as powerful aggregation and iii) OLAP-style operations. Experiments on a fully-implemented platform demonstrate the practical interest of our approach.

In this demo we will showcase a research prototype for processing queries and updates on large XML documents. The prototype is based on the idea of statically and dynamically partitioning the input document, so to distribute the computing load among the machines of a Map/Reduce cluster. Attendees will be able to run predefined queries and updates on documents conforming to the XMark schema, as well as to submit their own queries and updates.

An increasing part of the world's data is either shared through the Web or directly produced through and for Web platforms, in particular using structured formats like XML or JSON. Cloud platforms are interesting candidates to handle large data repositories, due to their elastic scaling properties. Popular commercial clouds provide a variety of sub-systems and primitives for storing data in specific formats (files, key-value pairs etc.) as well as dedicated sub-systems for running and coordinating execution within the cloud.

XML data projection (or pruning) is a natural optimization for main memory query engines: given a query Q over a document D , the subtrees of D that are not necessary to evaluate Q are pruned, thus producing a smaller document D' ; the query Q is then executed on D' , hence avoiding to allocate and process nodes that will never be reached by Q . In this article, we propose a new approach, based on types, that greatly improves current solutions. Besides providing comparable or greater precision and far lesser pruning overhead, our solution—unlike current approaches—takes into account backward axes, predicates, and can be applied to multiple queries rather than just to single ones. A side contribution is a new type system for XPath able to handle backward axes. The soundness of our approach is formally proved. Furthermore, we prove that the approach is also complete (i.e., yields the best possible type-driven pruning) for a relevant class of queries and Schemas. We further validate our approach using the XMark and XPathMark benchmarks and show that pruning not only improves the main memory query engine's performances (as expected) but also those of state of the art native XML databases.

Type inclusion is a fundamental operation in every type-checking compiler, but it is quite expensive for XML manipulation languages. A polynomial inclusion checking algorithm for an expressive family of XML type languages is known, but it runs in quadratic time both in the best and in the worst cases. We present here an algorithm that has a linear-time backbone, and resorts to the quadratic approach for some specific parts of the compared types. Our experiments show that the new algorithm is much faster than the quadratic one, and that it typically runs in linear time, hence it can be used as a building block for a practical type-checking compiler.

We present AMADA, a platform for storing Web data (in particular, XML documents and RDF graphs) based on the Amazon Web Services (AWS) cloud infrastructure. AMADA operates in a Software as a Service (SaaS) approach, allowing users to upload, index, store, and query large volumes of Web data. The demonstration shows (i) the step-by-step procedure for building and exploiting the warehouse (storing, indexing, querying) and (ii) the monitoring tools enabling one to control the expenses (monetary costs) charged by AWS for the operations involved while running AMADA.

This paper presents an XML partitioning technique that allows main-memory query engines to process a class of XQuery queries, that we dub iterative queries, on arbitrarily large input documents. We provide a static analysis technique to recognize these queries. The static analysis is based on paths extracted from queries and does not need additional schema information. We then provide an algorithm using path information for partitioning the input documents of iterative queries. This algorithm admits a streaming implementation, whose effectiveness is experimentally validated.

This paper presents a novel static analysis technique to detect XML query-update independence, in the presence of a schema. Rather than types, our system infers chains of types. Each chain represents a path that can be traversed on a valid document during query/update evaluation. The resulting independence analysis is precise, although it raises a challenging issue: recursive schemas may lead to inference of infinitely many chains. A sound and complete approximation technique ensuring a finite analysis in any case is presented, together with an efficient implementation performing the chain-based analysis in polynomial space and time.

While projection techniques have been extensively investigated for XML querying, we are not aware of applications to XML updating. This paper investigates a projection based optimization mechanism for XQuery Update Facility expressions in the presence of a schema. This paper includes a formal development and study of the method as well as experiments testifying its effectiveness.

Schemas have always played a crucial role in database management. For traditional relational and object databases, schemas have a relatively simple structure, and this eases their use for optimizing and typechecking queries. In the context of XML databases, things change. Several different schema languages have been defined, tailored for different application classes. Moreover, XML schema languages are inherently more complex, as they host mechanisms for describing highly irregular and flexible structures. In this tutorial we will describe the theoretical models behind these languages, their formal properties, and will also present the complexity of the basic decision problems. We will explore some theoretical and practical applications of schemas for query processing; finally, we will discuss how decision problems can be efficiently solved, at the price of some restrictions on the expressible types.

A key feature of XQuery is its type system. Any language expression is statically typed and its type is used during program type-checking.

The management of temporal data is a crucial issue in many applications. Recently, XML has become the standard for data exchange and representation. Consequently, important efforts have been made on the development of temporal extensions for XML. This paper investigates how to generate or maintain space-efficient time-stamped documents. We formally define a notion of compactness which allows for comparing documents. Then, we present two methods. For the first one, called general method, no restriction is made on the evolution of the XML documents whereas for the second one, called update-based method, changes are assumed to be specified by updates. For both methods, the issue is to enable processing very large documents, to use existing engines and to comply to Xquery Update Facility. The two methods are compared in terms of space-efficiency. The update-based method produces time-stamped XML documents that are more satisfactory wrt space-efficiency than the general method. This goes to show that the update-based method effectively takes advantage of the updates.

Type inclusion is a fundamental operation in every type-checking compiler, but it is quite expensive for XML manipulation languages. We recently presented an inclusion checking algorithm for an expressive family of XML type languages which is polynomial, but runs in quadratic time both in the best and in the worst cases. We present here an algorithm that has a linear-time backbone, and resorts to the quadratic approach for some specific parts of the compared types. Our experiments show that the new algorithm typically runs in linear time, hence can be used as a building block for a practical type-checking compiler.

The inclusion of Regular Expressions (REs) is the kernel of any subtype checking algorithm for XML schema languages. XML applications would benefit from the extension of REs with interleaving and counting, but this is not feasible in general, since inclusion is EXPSPACE-complete for such extended REs. In [9] we introduced a notion of "conflict-free REs", which are extended REs with excellent complexity behaviour, including a cubic inclusion algorithm [9] and linear membership [10]. Conflict-free REs have interleaving and counting, but the complexity is tamed by the "conflict-free" limitations, which have been found to be satisfied by the vast majority of the content models published on the Web.

Discretionary Access Control (DAC) systems provide powerful resource management mechanisms based on the selective distribution of capabilities to selected classes of principals. We study a type-based theory of DAC models for a process calculus that extends Cardelli, Ghelli and Gordon's pi-calculus with groups (Cardelliet al. 2005). In our theory, groups play the role of principals and form the unit of abstraction for our access control policies, and types allow the specification of fine-grained access control policies to govern the transmission of names, bound the (iterated) re-transmission of capabilities and predicate their use on the inability to pass them to third parties. The type system relies on subtyping to achieve a selective distribution of capabilities to the groups that control the communication channels. We show that the typing and subtyping relationships of the calculus are decidable. We also prove a type safety result, showing that in well-typed processes all names: (i) flow according to the access control policies specified by their types; and (ii) are received at the intended sites with the intended capabilities. We illustrate the expressive power and the flexibility of the typing system using several examples.

In modern data integration scenarios, many remote data sources are located on the Web and are accessible only through forms or Web services, and no guarantee is given about their stability. In these contexts the detection of corrupted mappings, as a consequence of a change in the source or in the target schema, is a key problem. A corrupted mapping fails in matching the target or the source schema, hence it is not able to transform data conforming to a schema S into data conforming to a schema T, nor it can be used for effective query reformulation. This article describes a novel technique for maintaining schema mappings in XML data integration systems, based on a notion of mapping correctness relying on the denotational semantics of mappings.

Regular Expressions (REs) form the basis of most XML type languages, such as DTDs, XML Schema types, and XDuce types (Thompson et al. 2004; Hosoya and Pierce 2003). In this context, the interleaving operator would be a natural addition to the language of REs, as witnessed by the presence of limited forms of interleaving in XSD (the all group), Relax-NG, and SGML. Unfortunately, membership checking for REs with interleaving is NP-hard in general. We present here a restricted class of REs with interleaving and counting which admits a linear membership algorithm. This restricted class is known to be expressive enough for the vast majority of the content models used in real-world DTDs and XSD schemas; moreover, we have proved in (Ghelli et al. 2007) that the same class admits a polynomial algorithm for subtyping and typeequivalence, problems which are EXPSPACE-complete for the full language of REs with interleaving. We first present an algorithm for membership of a list of words into a RE with interleaving and counting, based on the translation of the RE into a set of constraints. We generalize the approach in order to check membership of XML trees into a class of EDTDs with interleaving and counting, which models the crucial aspects of DTDs and XSD schemas. Finally, we extend the approach to REs with intersection. 1.

We present Pattern-by-Example (PBE), a graphical language that allows users with little or no knowledge of pattern-matching and functional programming to define complex and optimized queries on XML documents. We demonstrate the key features of PBE by commenting an interactive session and then we present its semantics by formally defining a translation from PBE graphical queries into CQL ones. The advantages of the approach are twofold. First, it generates queries that are provably correct with respect to types: the type of the result is displayed to the user and this constitutes a first and immediate visual check of the semantic correctness of the resulting query. The second advantage is that a semantics formally-thus, unambiguously-defined is an important advancement over some current approaches in which standard usage and learning methods are based on "trial and error" techniques

In the contexts of data integration and data exchange, schema mappings are primarily used for query answering. As a consequence, their maintenance and, in particular, the detection of corrupted mappings, i.e., mappings that fail in matching the source and/or the target schema, is crucial.Corruption checking can be automatically performed by relying on an operation called type projection. This work describes an efficient algorithm for checking XML type projection, based on a characterization of type projection in terms of type simulation.

A part of a query that will never contribute data to the query answer should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition for this class of errors, and define a type system that is sound and complete, in its search for such errors, for a core language, under mild restrictions on the use of recursion in type definitions. In the process, we describe a dichotomy among existential and universal type systems, which is essential to understand some specific features of our type system.

If a subexpression in a query will never contribute data to the query answer, this should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition for this class of errors, and define a type system that is sound and complete, in its search for such errors, for a core language, under mild restrictions on the use of recursion in type definitions. In the process, we describe a dichotomy among existential and universal type systems, which is useful to understand some unusual features of our type system.

Abstract XML is nowadays considered the standard meta‐language for document markup and data representation. XML is widely employed in Web‐related applications as well as in database applications, and there is also a growing interest for it by the literary community to develop tools for supporting document‐oriented retrieval operations. The purpose of this article is to show the basic new requirements of this kind of applications and to present the main features of a typed query language, called Tequyla‐TX, designed to support them.

The problem of defining and checking a subtype relation between recursive types was studied in Armadio and Cardelli (1993) for a first order type system, but for second order systems, which combine subtyping and parametric polymorphism, only negative results are known. This paper studies the problem of subtype checking for recursive types in system kernel Fun, a typed /spl lambda/-calculus with subtyping and bounded second order polymorphism. Along the lines of Armadio and Cardelli (1993), we study the definition of a subtype relation over kernel Fun recursive types, and then we present a subtyping algorithm which is sound and complete with respect to this relation. We show that the natural extension of the techniques introduced in Armadio and Cardelli (1993) to compare first order recursive types gives a non complete algorithm. We prove the completeness and correctness of a different algorithm, which also admits an efficient implementation.