替代非良基文法的绑定语法
摘要：一种涉及变量绑定和单子替换操作的非好基语法的通用构建被描述。我们的语法和替换操作的构建发生在范畴论中，尤其是通过使用单子范畴和它们之间的强函子。一个语言由一个多重排序的绑定签名{Sigma}来指定。首先，我们通过{omega} -连续性为{Sigma}提供了生成可能的无限术语的语言的充分条件。其次，我们构建了由{Sigma}生成的语言的单子替换操作。该构建的基石是Matthes和Uustalu开发的异构替换系统概念的轻微泛化；这样的系统封装了实现替换所需的核递归方案。这些结果在Coq证明助手中通过UniMath库的同伦数学进行了形式化。
作者：Ralph Matthes and Kobe Wullaert and Benedikt Ahrens
论文ID：2308.05485
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-11