具有调用时选择语义的构造函数系统的重写和收缩
Rewriting and narrowing for constructor systems with call-time choice semantics
摘要：
非融合和非终止的基于构造函数的术语重写系统对于规范和编程的目的是有用的。特别地，现有的函数逻辑语言使用这种重写系统来定义可能不严格的非确定性函数。非确定性采用的语义是调用时间选择，其与非严格性的结合是一个重要的问题，多年前从语义的角度用基于构造器的重写逻辑（CRWL）解决，CRWL是一个众所周知的语义框架，通常被接受为现代函数逻辑语言的合适语义基础。CRWL的一个缺点是它没有一个正确的一步约简的概念，这对于理解和推理计算如何进行是非常有用的。在本文中，我们彻底发展的理论，一阶版本的让重写，一个简单的减少概念，接近经典的长期重写，但扩展了让绑定建设，充分表达结合调用时间的选择与非严格的语义。字母重写可以被看作是术语图重写的一种特殊的文本表示。我们调查的属性，让重写，最显着的等价性相对于一个保守的扩展的CRWL语义处理让绑定，我们通过一些案例研究表明，有两个可互换的正式意见（减少/语义）相同的语言是一个强大的推理工具。在此之后，我们提供了一个概念，让缩小，这是足够的调用时间的选择，证明了健全性和完整性的结果，让缩小让重写。此外，我们将这些let重写和let缩小关系（以及因此CRWL）与普通项重写和缩小（...）逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
英文摘要：
Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper we develop thoroughly the theory for the first order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing (..) To appear in Theory and Practice of Logic Programming (TPLP).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
