带证据的积范畴：具有图示约束与广义草图的数据与系统建模

Zinovy Diskin

带证据的积范畴：具有图示约束与广义草图的数据与系统建模

计算机科学中的逻辑 2023-06-29 v1 范畴论

作者: Zinovy Diskin

摘要

数据约束对于实际数据建模至关重要，而数据实例对安全关键约束的可验证符合（满足关系）是安全保证的基石。图示约束作为理论概念和实践便利工具都很重要。本文表明，基本的形式化约束管理完全可以在有限完备范畴内发展（因此标题中提及积性）。在数据建模语境中，此类范畴的对象可视为图，而其态射扮演双重角色：数据实例以及（当被额外标记时）约束。具体而言，广义草图 $S$ 由图 $G_S$ 和声明于 $G_S$ 上的一组约束 $C_S$ 组成，并作为典型数据模式（数据库、XML和UML类图中的）的一种范式出现。数据建模框架（及基于它们的工具）的互操作性在很大程度上依赖于当模式图改变时调控数据实例与模式之间满足关系转换的规律：此时约束协变翻译而实例逆变翻译。探究这一转换模式是本文的主要数学主题。

关键词

积范畴图示约束广义草图数据建模满足关系互操作性

引用

@article{arxiv.2306.16284,
  title  = {Cartesian institutions with evidence: Data and system modelling with diagrammatic constraints and generalized sketches},
  author = {Zinovy Diskin},
  journal= {arXiv preprint arXiv:2306.16284},
  year   = {2023}
}

备注

35 pages. The paper will be presented at the conference on Applied Category Theory, ACT'23

带证据的积范畴：具有图示约束与广义草图的数据与系统建模

摘要

关键词

引用

备注

相关论文