收敛无穷计算的一个逻辑框架
A Logical Framework for Convergent Infinite Computations
摘要：
经典计算不能很好地捕捉无限计算的本质。本文主要研究一类称为收敛无穷计算的无穷计算。利用柯西序列对一阶理论进行推广，提出了一种收敛无穷计算逻辑，它比一阶逻辑具有更强的表达能力。一类刻画极限逻辑性质的不动点可以用柯西序列定义的无限长项来表示。我们将证明一阶理论序列的极限可以用距离来定义，类似于实分析中极限的$ε-N$式定义。在无穷项的基础上，提出了收敛无限计算的计算模型。最后，通过引入逻辑程序的实Herbrand模型，扩展了对逻辑程序的解释，并给出了用收敛无穷计算计算Horn逻辑程序的实Herbrand模型的一个充分条件.
英文摘要：
Classical computations can not capture the essence of infinite computations very well. This paper will focus on a class of infinite computations called convergent infinite computations}. A logic for convergent infinite computations is proposed by extending first order theories using Cauchy sequences, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite-length terms defined by Cauchy sequences. We will show that the limit of sequence of first order theories can be defined in terms of distance, similar to the $ε-N$ style definition of limits in real analysis. On the basis of infinitary terms, a computation model for convergent infinite computations is proposed. Finally, the interpretations of logic programs are extended by introducing real Herbrand models of logic programs and a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation is given.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
