关于语法上避免捕获的替换、上下文应用、命名替换、偏微分等结构定义的统一处理
计算机科学中的逻辑
2022-04-11 v1 编程语言
范畴论
摘要
我们引入一种带辅助函数的语法的范畴论抽象，称为可容许单子态射。依赖于结构递归的一种抽象形式，我们进而设计了从基本数据构造可容许单子态射的通用工具。这些工具将 ubiquitous 标准模式自动化，例如（1）在连续的、可能相互依赖的层次中定义辅助函数，以及（2）通过对语法的归纳证明辅助函数的性质。我们涵盖了文献中重要的例子，包括带避免捕获的替换的标准 lambda 演算、带绑定求值上下文的 lambda 演算、带命名替换的 lambda-mu 演算，以及微分 lambda 演算。
引用
@article{arxiv.2204.03870,
title = {A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on},
author = {Tom Hirschowitz and Ambroise Lafont},
journal= {arXiv preprint arXiv:2204.03870},
year = {2022}
}