简单类型论的代数模型：一种多项式方法
计算机科学中的逻辑
2020-07-01 v1 范畴论
摘要
我们发展了简单类型论的代数模型，铺开一个将泛代数扩展以纳入代数排序与变量绑定的框架。简单类型论的例子包括单类型与简单类型 -演算、计算 -演算，以及谓词逻辑。简单类型论在预层范畴中获得模型，其结构由对应于自然演绎规则的多项式内函子的代数所规定。我们构造的初始模型抽象地描述了简单类型论的语法。考虑到代换结构，我们进一步在结构化的笛卡儿多范畴中提供可靠且完备的语义。这一发展将 Lambek 关于简单类型 -演算与笛卡儿闭范畴之间的对应推广到任意简单类型论。
引用
@article{arxiv.2006.16949,
title = {Algebraic models of simple type theories: a polynomial approach},
author = {Nathanael Arkor and Marcelo Fiore},
journal= {arXiv preprint arXiv:2006.16949},
year = {2020}
}
备注
14 pages