JSON模式的不可约性消除和见证点生成
Not Elimination and Witness Generation for JSON Schema
摘要：
JSON Schema是描述JSON文档族的一个不断发展的标准。JSON Schema是一种逻辑语言，基于一组描述分析中JSON值特征的断言，以及这些断言的逻辑或结构组合子。对于任何一种逻辑语言，满足、不消除、模式可满足性、模式包含与等价以及证明生成等问题都具有重要的理论和实际意义。虽然满足是微不足道的，但所有其他问题都相当困难，因为JSON模式中同时存在否定、递归和复杂断言。为了使事情变得更加复杂和有趣，JSON模式不是代数的，因为我们在同一模式对象中的不同关键字之间有语法和语义交互。有了这样的动机，我们在本文中提出了一个代数表征的JSON模式，通过添加适当的运营商，并通过镜像现有的。然后，我们提出了基于代数的方法来处理不消除和证人生成问题，发挥了核心作用，因为它们导致其他提到的复杂问题的解决方案。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
