Regular Real Analysis

Journal Title
Journal ISSN
Volume Title
Association for Computing Machinery

We initiate the study of regular real analysis, or the analysis of real functions that can be encoded by automata on infinite words. It is known that ω-automata can be used to represent {relations} between real vectors, reals being represented in exact precision as infinite streams. The regular functions studied here constitute the functional subset of such relations. We show that some classic questions in function analysis can become elegantly computable in the context of regular real analysis. Specifically, we present an automata-theoretic technique for reasoning about limit behaviors of regular functions, and obtain, using this method, a decision procedure to verify the continuity of a regular function. Several other decision procedures for regular functions-for finding roots, fix points, minima, etc.-are also presented. At the same time, we show that the class of regular functions is quite rich, and includes functions that are highly challenging to encode using traditional symbolic notation.

Conference paper

Chaudhuri, Swarat, Sankaranarayanan, Sriram and Vardi, Moshe Y.. "Regular Real Analysis." LICS '13 Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, (2013) Association for Computing Machinery: 509-518.

Forms part of
This is an author's peer-reviewed final manuscript, as accepted by the publisher. The published article is copyrighted by the Association for Computing Machinery.
Link to license
Citable link to this page