arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2205.15917cs.PLcs.LOmath.CT
收藏

具体范畴和高阶递归(应用包括概率、可微性和完全抽象)

Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)

Cristina Matache, Sean Moss, Sam Staton

摘要:

我们研究具体层模型的调用值高阶语言递归。我们的家庭层模型是一个推广的许多例子,从文献中,如模型的概率和可微规划,完全抽象的逻辑关系模型。我们以综合域理论的精神来对待递归。我们提供了一个一般的建设提升单子从一类允许的单态在现场的层范畴。这样,我们得到了一个家庭的模型参数化的具体网站和一类单态,我们证明了一个一般的计算充分性定理。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑