...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >Productive corecursion in logic programming
【24h】

Productive corecursion in logic programming

机译：逻辑编程中的生产性Corecursion

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/ coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property -of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper, we strengthen these recent results. We propose a method that semi-decides productivity of individual derivations for regular formulae. Thus, we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.
机译：逻辑编程是一种图灵完整的语言。结果，设计决定程序终止和不终止或确定公式的归纳/共归合理性的算法是一项艰巨的任务。例如，现有的最新算法只能在常规公式的逻辑编程中半确定查询的合计合理性。生产力是另一个不太出名，但同样基本且重要的无法确定的属性。如果推导是无限的并且相称地合理，则我们可能会问，它确定的计算出的答案是否实际上在计算无限公式。如果是这样，则无限计算将产生成果。这种直觉最初是在80年代以无穷大计算的名称表达的。在当今的Internet和流处理中，其重要性在于与无限数据结构处理有关。近来，提出了一种算法，其半确定逻辑程序的生产率的较弱属​​性。如果逻辑程序可以产生生产性推导，则它是生产性的。在本文中，我们加强了这些最新结果。我们提出了一种半确定规则公式的单个导数生产力的方法。因此，我们最后给出了与逻辑编程中的推导效率概念相对应的算法。自30年前提出以来，这是该问题的第一个算法解决方案。我们还提出了该算法的实现。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号