JSON Schema Inclusion through Refutational Normalization: Reconciling Efficiency and Completeness

Abstract

JSON Schema is the de facto standard for describing the structure of JSON documents. Deciding JSON Schema inclusion - whether every instance of a schema $S$ is also an instance of a schema $S^{\prime }$ - is a building block for version and API compatibility checks, schema refactoring, and large-scale corpus analysis. The problem is EXPTIME-complete, and the two existing families of algorithms fail in practice in complementary ways: rule-based algorithms are fast but incomplete by design, while witness-generation algorithms are complete but so slow that, under any reasonable timeout, they are incomplete in practice as well. We show that this specific problem admits a way out. We redesign the normalization core of the complete algorithm, so that, on the easy cases, it mimics the behavior of the fast rule-based algorithm, without losing completeness. We prove that it is exactly as efficient as the rule-based approach on every inclusion that approach can prove, while remaining complete on all others. We validate this on a vast collection of real-world schemas and hand-crafted schemas. We show that our algorithm advances the state of the art, making tractable a range of use cases that were out of reach for existing tools.