Abstract Effects and Proof-Relevant Logical Relations
Abstract Effects and Proof-Relevant Logical Relations
复制标题
DOI：
10.1145/2535838.2535869
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Nigam, Vivek
中科院分区：
文献类型：
--
作者：
Benton, Nick;Hofmann, Martin;Nigam, Vivek
我们为基于区域的效应系统提供了一种典型的语义，该系统仅需要跟踪外部可见效果，以支持类型的抽象：不可观察的内部修改，例如搜索树的重组或懒惰的初始化，可以算作“纯”或“仅读”。这种“虚构的纯度”使模块的客户能够验证比以前的语义相比，基于效果的等效性更高。我们的语义使用了一种新颖的逻辑关系变体，这些变体不仅映射到值的部分等价关系，就像通常这样做的那样，而是与其相关的概括（即setoids）。 setoid的对象确定价值居住在语义类型的同时，而其形态被理解为语义对等的证明。向证据 - 相关的过渡解决了由于在Kripke逻辑关系中天真地使用存在量化而引起的两个尴尬问题，即接受可受理性和虚假功能依赖性。
We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as 'pure' or 'read only'. This 'fictional purity' allows clients of a module to validate soundly more effect-based program equivalences than would be possible with previous semantics. Our semantics uses a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves two awkward problems caused by naive use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.