构造系统中的重写和缩小带有调用时选择语义
摘要：非连续和非终止的基于构造函数的术语重写系统对于规范和编程非常有用。特别是，现有的函数逻辑语言使用这种重写系统来定义可能是非严格的非确定性函数。采用的非确定性的语义是调用时选择，其与非严格性的组合是一个非平凡问题，年前从语义观点上从语义观点上讨论了Constructor-based Rewriting Logic (CRWL)解决了这个问题，这是一个广泛接受的现代函数逻辑语言的合适的语义基础。CRWL的一个缺点是它没有恰当的一步缩减概念，它对于理解和推理计算如何进行非常有用。在本文中，我们深入发展了一阶版本的let-rewriting理论，这是一种与经典术语重写相近的简单的缩减概念，但通过添加let-binding结构扩展以适当地表达调用时选择和非严格语义的组合。let-rewriting可以被看作是术语图重写的一种特定的文本表示。我们研究了let-rewriting的性质，尤其是它们与处理let-bindings的CRWL语义的保守扩展的等价性，并通过一些案例研究表明，拥有两个可互换的形式视图（缩减/语义）的相同语言是一种强大的推理工具。之后，我们提供了一种适用于调用时选择的let-narrowing概念，并通过对于let-rewriting的soundness和completeness结果，将其与let-rewriting的关系（以及CRWL）与普通术语重写和缩减联系起来。
作者：Francisco J. L''opez-Fraguas, Enrique Martin-Martin, Juan Rodr''iguez-Hortal''a, Jaime S''anchez-Hern''andez
论文ID：1209.2617
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-10-11