高阶理论
计算机科学中的逻辑
2008-09-09 v2
摘要
我们通过模和线性性扩展了关于抽象语法（含绑定构造）的方法。首先我们给出了元数的新的一般定义，从而得到签名的伴随概念。然后我们获得了 Ghani 和 Uustalu (2003) 所要求的模性结果：在我们的框架中，合并语法的两个扩展对应于构建融合和。最后我们定义了关于签名的方程的自然概念，并证明了所谓可表示签名配备方程组时初始语义的存在性。
引用
@article{arxiv.0704.2900,
title = {Higher-order theories},
author = {Andre' Hirschowitz and Marco Maggesi},
journal= {arXiv preprint arXiv:0704.2900},
year = {2008}
}
评论
12 pages