使用模式确保带子类型的类型逻辑程序的主语约化
计算机科学中的逻辑
2009-09-25 v2
摘要
我们考虑一种具有参数多态性和子类型关系的通用规范类型系统，用于逻辑程序。主语约化属性表达了类型系统相对于执行模型的一致性：如果一个程序是“类型正确”的，那么所有以“类型正确”目标开始的演绎仍是“类型正确”的。在没有子类型的情况下，已知对于逻辑程序及其标准（无类型）执行模型可轻易获得这一属性。本文给出确保在存在类型构造函数之间的一般子类型关系时也能获得主语约化的语法条件。其思想是考虑具有固定数据流（由模式给定）的逻辑程序。
引用
@article{arxiv.cs/0010029,
title = {Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping},
author = {Jan-Georg Smaus and Francois Fages and Pierre Deransart},
journal= {arXiv preprint arXiv:cs/0010029},
year = {2009}
}
备注
27 pages; Research Report of INRIA Rocquencourt, long version of paper in FSTTCS 2000 conference, New Delhi