A Logical Framework for Convergent Infinite Computations
<|reference_start|>A Logical Framework for Convergent Infinite Computations: 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 $\epsilon-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.<|reference_end|>
@article{li2001a,
    title={A Logical Framework for Convergent Infinite Computations},
    author={Wei Li, Shilong Ma, Yuefei Sui, Ke Xu},
    journal={arXiv preprint arXiv:cs/0105020},
    year={2001},
    archivePrefix={arXiv},
    eprint={cs/0105020},
    primaryClass={cs.LO cs.PL}
}