交集类型与任意扩展变量的完全可实现性语义
逻辑
2009-05-12 v1
摘要
扩展（Expansion）于 1970 年代末被引入，用于在交集类型系统中计算 λ-项的主类型。扩展变量（E-variables）于 1990 年代末被引入，以简化并帮助机械化扩展。最近，扩展变量被进一步简化和推广，也允许计算除交集之外的其他类型算子。关于交集类型系统的语义已有大量工作，但关于带扩展变量的交集类型系统的语义仅有一项工作。该工作表明，为扩展变量构建语义极具挑战性。由于不清楚如何为扩展变量设计意义空间，该工作转而开发了一种分层的类型意义空间，该空间具有多个层级（由索引表示）。然而，尽管带索引的演算有助于识别为扩展变量赋予语义的严重问题，但可靠的可实现性语义仅在仅使用单个扩展变量且不允许使用通用类型 ω 时才是完全的。在本文中，我们克服了这些挑战。我们开发了一种可实现性语义，允许任意（可能无限）数量的扩展变量，并且 ω 存在。我们证明了所提出语义的可靠性和完全性。
引用
@article{arxiv.0905.1566,
title = {A complete realisability semantics for intersection types and arbitrary expansion variables},
author = {Fairouz Kamareddine and Karim Nour and Vincent Rahli and J. B. Wells},
journal= {arXiv preprint arXiv:0905.1566},
year = {2009}
}
备注
5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008, 1-3 September 2008, Istanbul : Turquie (2008)