中文

一阶草图条件与约束——一种范畴无关方法

计算机科学中的逻辑 2021-03-16 v1

摘要

在图谓词框架(DPF)中推广“图条件与约束”以及“全称约束”和“否定全称约束”的不同变体,我们针对任意范畴 Cxt\mathbf{Cxt} 与“语句”函子 Stm:CxtSet\mathtt{Stm}:\mathbf{Cxt}\to\mathbf{Set} 引入通用的一阶草图条件与约束。草图在 DPF 中用于形式化不同种类的图示化软件模型。我们讨论了草图约束在描述草图句法结构中的使用。我们概述了利用草图约束推导草图中隐式给出的知识,以及从给定草图约束推导草图约束的过程。我们以简单但具范式的建模形式体系“范畴论”作为贯穿示例。

关键词

引用

@article{arxiv.2103.07558,
  title  = {First-Order Sketch Conditions and Constraints -- A Category Independent Approach},
  author = {Uwe Wolter},
  journal= {arXiv preprint arXiv:2103.07558},
  year   = {2021}
}

备注

16 pages, submitted to ICGT 2021