Not Elimination and Witness Generation for JSON Schema

TL;DR

This paper introduces an algebraic framework for JSON Schema to address complex logical problems like not-elimination and witness generation, which are crucial for schema analysis and validation.

Contribution

It proposes an algebraic characterization of JSON Schema and algebra-based methods for not-elimination and witness generation, advancing schema reasoning techniques.

Findings

Algebraic characterization of JSON Schema developed.

Approaches for not-elimination problems introduced.

Methods for witness generation proposed.

Abstract

JSON Schema is an evolving standard for the description of families of JSON documents. JSON Schema is a logical language, based on a set of assertions that describe features of the JSON value under analysis and on logical or structural combinators for these assertions. As for any logical language, problems like satisfaction, not-elimination, schema satisfiability, schema inclusion and equivalence, as well as witness generation, have both theoretical and practical interest. While satisfaction is trivial, all other problems are quite difficult, due to the combined presence of negation, recursion, and complex assertions in JSON Schema. To make things even more complex and interesting, JSON Schema is not algebraic, since we have both syntactic and semantic interactions between different keywords in the same schema object. With such motivations, we present in this paper an algebraic characterization of JSON Schema, obtained by adding opportune operators, and by mirroring existing ones. We present then algebra-based approaches for dealing with not-elimination and witness generation problems, which play a central role as they lead to solutions for the other mentioned complex problems.