一句话：提出归约单子与归约签名，统一代数地呈现λ演算等系统的替换结构与有向归约规则。
本文研究归约单子（reduction monads），它本质上是相对于从集合到多重图的自由函子的单子。归约单子同时刻画λ演算的两个方面：从单子观点看，λ演算带有良行为的替换；从图观点看，它是有向多重图，顶点为项、边为项之间的归约。作者研究归约单子的呈现问题，提出归约签名（reduction signature）概念：签名如同虚拟呈现，规定生成运算的元数（可带方程）以及生成归约规则的元数。对每个签名定义模型范畴，模型本身也是归约单子；若模型范畴存在初始对象，则称该初始对象为签名呈现的归约单子。主要结果识别出一类能按上述意义呈现归约单子的归约签名，并通过例子说明该方法覆盖若干标准λ演算变体。
In this work, we study reduction monads , which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph whose vertices are terms and whose edges witness the reductions between two terms. We study presentations of reduction monads. To this end, we propose a notion of reduction signature . As usual, such a signature plays the role of a virtual presentation, and specifies arities for generating operations—possibly subject to equations—together with arities for generating reduction rules. For each such signature, we define a category of models; any model is, in particular, a reduction monad. If the initial object of this category of models exists, we call it the reduction monad presented (or specified) by the given reduction signature . Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. We show in the examples that our approach covers several standard variants of the lambda calculus.
@article{paperbot544,
title = {Reduction monads and their signatures},
author = {Benedikt Ahrens and André Hirschowitz and Ambroise Lafont and Marco Maggesi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371099}
}