一阶草图条件与约束——一种范畴无关方法
计算机科学中的逻辑
2021-03-16 v1
摘要
在图谓词框架(DPF)中推广“图条件与约束”以及“全称约束”和“否定全称约束”的不同变体,我们针对任意范畴 与“语句”函子 引入通用的一阶草图条件与约束。草图在 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