Concrete categories and higher-order recursion
Concrete categories and higher-order recursion
复制标题
具体类别和高阶递归
DOI：
10.1145/3531130.3533370
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Matache C
中科院分区：
文献类型：
--
作者：
Matache C
我们研究具体层模型的调用值高阶语言递归。我们的家庭层模型是一个推广的许多例子，从文献中，如模型的概率和可微规划，完全抽象的逻辑关系模型。我们以综合域理论的精神来对待递归。我们提供了一个一般的建设提升单子从一类允许的单态在现场的层范畴。这样，我们得到了一个家庭的模型参数化的具体网站和一类单态，我们证明了一个一般的计算充分性定理。
We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.