向量空间计算性定义的范畴构造
计算机科学中的逻辑
2020-10-23 v2 范畴论
逻辑
摘要
Lambda-S 是一阶 lambda 演算的扩展，统一了量子 lambda 演算中两种非克隆方法。其一为禁止变量复制，其二为将所有 lambda 项视为代数线性函数。Lambda-S 的类型系统含有一构造子 S，使得类型 A 被视为向量空间的基，而 S(A) 为其张成空间。Lambda-S 亦可视为一种用于向量空间计算操作的语言：向量空间公理以重写系统给出，描述了待执行的计算步骤。本文给出 Lambda-S*（Lambda-S 的片段）的抽象范畴语义，表明 S 可解释为笛卡尔范畴与加法对称幺半范畴之间伴随关系里两个函子的复合。右伴随为一遗忘函子 U，它在语言中隐藏，并在计算推理中起核心作用。
引用
@article{arxiv.1905.01305,
title = {A categorical construction for the computational definition of vector spaces},
author = {Alejandro Díaz-Caro and Octavio Malherbe},
journal= {arXiv preprint arXiv:1905.01305},
year = {2020}
}
备注
39 pages. Applied Categorical Structures (2020). arXiv admin note: text overlap with arXiv:1806.09236