A Logical Framework for Convergent Infinite Computations

TL;DR

This paper introduces a logical framework for modeling convergent infinite computations using Cauchy sequences, extending first-order logic to better capture the properties of infinite processes.

Contribution

It proposes a new logic based on Cauchy sequences and fixed points, providing a formal model for convergent infinite computations and extending logic program semantics.

Findings

Defined a logic for convergent infinite computations using Cauchy sequences

Established a model for limits of theories via a distance metric

Extended logic program semantics with real Herbrand models

Abstract

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.