JSON Schema 的取反消除与见证生成
数据库
2021-05-10 v2
摘要
JSON Schema 是用于描述 JSON 文档族的一个不断演进的标准。JSON Schema 是一种逻辑语言，基于一组描述待分析 JSON 值特征的断言，以及用于这些断言的逻辑或结构组合子。与任何逻辑语言一样，满足性、取反消除、模式可满足性、模式包含与等价，以及见证生成等问题都具有理论和实际意义。虽然满足性是平凡的，但由于 JSON Schema 中同时存在否定、递归和复杂断言，所有其他问题都相当困难。更使问题复杂且有趣的是，JSON Schema 不是代数的，因为同一模式对象中不同关键字之间存在句法和语义上的交互。基于这些动机，本文通过添加适当的算子并镜像现有算子，给出了 JSON Schema 的一种代数刻画。接着我们提出了基于代数的方法来处理取反消除和见证生成问题，这两个问题居于核心地位，因为它们可导出上述其他复杂问题的解。
引用
@article{arxiv.2104.14828,
title = {Not Elimination and Witness Generation for JSON Schema},
author = {Mohamed-Amine Baazizi and Dario Colazzo and Giorgio Ghelli and Carlo Sartiani and Stefanie Scherzinger},
journal= {arXiv preprint arXiv:2104.14828},
year = {2021}
}