用丰富的Lawvere理论表示操作语义
Representing operational semantics with enriched Lawvere theories
摘要：
许多术语演算，如λ演算或pi演算，涉及名称的绑定器，并且绑定变量名称的数学是微妙的。Schoenfinkel在1924年引入了SKI组合子演算，通过消除量化变量来澄清它们在直觉逻辑中的作用。Yoshida演示了如何在异步pi演算中消除来自输入前缀的绑定名称，但她的组合子仍然依赖于new运算符来绑定名称。最近，Meredith和Stay展示了如何修改Yoshida的组合子，用反射算子替换new和replication，以提供第一个没有绑定名称的组合子演算，异步pi演算可以忠实地嵌入其中。在这里，我们提供了一组替代的组合子，它由SKI加上反射构建，也消除了所有的标称现象，但提供了一个忠实的嵌入反射高阶π演算。我们表明，有效地消除了语法糖的名义功能，多分类的Lawvere理论丰富的图形足以捕捉的操作语义的演算。
英文摘要：
Many term calculi, like lambda calculus or pi calculus, involve binders for names, and the mathematics of bound variable names is subtle. Schoenfinkel introduced the SKI combinator calculus in 1924 to clarify the role of quantified variables in intuitionistic logic by eliminating them. Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculus, but her combinators still depend on the new operator to bind names. Recently, Meredith and Stay showed how to modify Yoshida's combinators by replacing new and replication with reflective operators to provide the first combinator calculus with no bound names into which the asynchronous pi calculus has a faithful embedding. Here we provide an alternative set of combinators built from SKI plus reflection that also eliminates all nominal phenomena, yet provides a faithful embedding of a reflective higher-order pi calculus. We show that with the nominal features effectively eliminated as syntactic sugar, multisorted Lawvere theories enriched over graphs suffice to capture the operational semantics of the calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
