用图丰富的Lawvere理论表示操作语义
计算机科学中的逻辑
2017-04-12 v1
摘要
许多项演算，如λ演算或π演算，涉及名字的绑定器，而绑定变量名的数学是微妙的。Schoenfinkel在1924年引入SKI组合子演算，通过消除量化变量来澄清直觉主义逻辑中量化变量的作用。Yoshida展示了如何消除异步π演算中输入前缀带来的绑定名，但她的组合子仍然依赖于new算子来绑定名。最近，Meredith和Stay展示了如何通过用反射算子替换new和复制来修改Yoshida的组合子，从而提供第一个无绑定名且异步π演算可忠实嵌入的组合子演算。这里我们提供另一组由SKI加反射构建的组合子，同样消除了所有名义现象，却提供了对反射高阶π演算的忠实嵌入。我们展示了随着名义特征作为语法糖被有效消除，在图之上丰富的多排序Lawvere理论足以捕获该演算的操作语义。
引用
@article{arxiv.1704.03080,
title = {Representing operational semantics with enriched Lawvere theories},
author = {Michael Stay and L. G. Meredith},
journal= {arXiv preprint arXiv:1704.03080},
year = {2017}
}
备注
arXiv admin note: text overlap with arXiv:1703.07054