单型类型的逻辑关系
计算机科学中的逻辑
2009-09-29 v2
摘要
逻辑关系及其推广是证明 lambda 演算属性的基本工具，例如，可产生观察等价的可靠原则。我们提出了一种能够处理莫格比(Moggi)计算 lambda 演算中单型类型的自然逻辑关系概念。该方法是范畴化的，基于子连、单射分解系统和单子态射的概念。我们的做法具有诸多有趣的应用，包括 lambda 演算的非确定性情况（在逻辑关系中意味着双仿射）、动态名称创建以及概率系统。
关键词
引用
@article{arxiv.cs/0511006,
title = {Logical Relations for Monadic Types},
author = {Jean Goubault-Larrecq and Slawomir Lasota and David Nowak},
journal= {arXiv preprint arXiv:cs/0511006},
year = {2009}
}
备注
83 pages