Logical Relations for Monadic Types
Logical Relations for Monadic Types
复制标题
Monadic 类型的逻辑关系
DOI：
10.1007/3-540-45793-3_37
复制
发表时间：
2002
影响因子：
0.5
通讯作者：
Yu Zhang
中科院分区：
文献类型：
--
作者：
S. Lasota;David Nowak;Yu Zhang
逻辑关系和继承人的概括是证明lambda-calculi的性质的基本工具，例如，产生了观察等效性的声音原理。我们提出了一个自然的逻辑关系概念，能够处理Moggi的计算Lambda-Calculus的单调类型。该治疗是分类的，并且基于单调的亚规范和分布定律的概念。我们的方法有许多有趣的应用程序，包括具有非确定性的lambda-calculi病例（逻辑关系意味着是双仿），动态名称创建和概率系统。
Logical relations andt heir generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with the monadic types of Moggi's computational lambda-calculus. The treatment is categorical, and is based on notions of subsconing and distributivity laws for monads. Our approach has a number of interesting applications, including cases for lambda-calculi with non-determinism (where being in logical relation means being bisimilar), dynamic name creation, and probabilistic systems.