变量绑定下的语法与操作语义的签名与模型
计算机科学中的逻辑
2019-12-19 v4
摘要
本论文研究编程语言语法与操作语义的规约与构造。我们采用一种通用的签名概念，用于将给定范畴的对象规约为合适模型范畴中的初始对象。这种表征遵循初始语义的精神，给出了递归原理的合理性证明。具有变量绑定的语言，如纯 lambda 演算，是通过经典代数签名在集合范畴上指定的单子。我们考虑的对带等式语法的首次扩展是这些代数签名的商。它们允许例如指定一个二元交换运算。但某些等式，如结合律，似乎仍难以触及。因此我们引入 2-签名的概念，由两部分组成：如前通过通常签名对运算的规约，以及它们之间的一组等式。我们确定了保证相关语法存在的代数 2-签名类。最后，我们着手处理如带 beta 归约的 lambda 演算等编程语言操作语义的规约。为此，我们引入归约单子及其签名的概念，然后将其推广得到操作单子的概念。
引用
@article{arxiv.1910.09162,
title = {Signatures and models for syntax and operational semantics in the presence of variable binding},
author = {Ambroise Lafont},
journal= {arXiv preprint arXiv:1910.09162},
year = {2019}
}
备注
doctoral thesis