Computable analysis with applications to dynamic systems. (English) Zbl 1478.03072
Summary: Numerical computation is traditionally performed using floating-point arithmetic and truncated forms of infinite series, a methodology which allows for efficient computation at the cost of some accuracy. For most applications, these errors are entirely acceptable and the numerical results are considered trustworthy, but for some operations, we may want to have guarantees that the numerical results are correct, or explicit bounds on the errors. To obtain rigorous calculations, floating-point arithmetic is usually replaced by interval arithmetic and truncation errors are explicitly contained in the result. We may then ask the question of which mathematical operations can be implemented in a way in which the exact result can be approximated to arbitrary known accuracy by a numerical algorithm. This is the subject of computable analysis and forms a theoretical underpinning of rigorous numerical computation. The aim of this article is to provide a straightforward introduction to this subject that is powerful enough to answer questions arising in dynamic system theory.
MSC:
| 03D78 | Computation over the reals, computable analysis |
| 03F60 | Constructive and recursive analysis |
| 54B30 | Categorical methods in general topology |
| 54A05 | Topological spaces and generalizations (closure spaces, etc.) |
| 93B03 | Attainable sets, reachability |
| 93B24 | Topological methods |
References:
| [1] | Aberth, O. (2007). Introduction to Precise Numerical Methods, 2nd edn., Amsterdam, Elsevier/Academic Press. With 1 CD-ROM (Windows). · Zbl 1127.65001 |
| [2] | Ariadne: A C++ library for formal verification of cyber-physical systems, using reachability analysis for nonlinear hybrid automata (Release 1.9, 2018). http://www.ariadne-cps.org/. |
| [3] | Asarin, E., Bournez, O., Dang, T., Maler, O. and Pnueli, A. (2000). Effective synthesis of switching controllers for linear systems. Proceedings of the IEEE881011-1025. |
| [4] | Asarin, E., Maler, O. and Pnueli, A. (1995). Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science138 (1) 35-65. · Zbl 0884.68050 |
| [5] | Aubin, J.-P. and Cellina, A. (1984). Differential Inclusions, Grundlehren der Mathematischen Wissenschaften, vol. 264, Berlin, Springer-Verlag. · Zbl 0538.34007 |
| [6] | Aubin, J.-P., Lygeros, J., Quincampoix, M. and Sastry, S. (2002). Impulse differential inclusions: a viability approach to hybrid systems. IEEE Transactions on Automatic Control47 (1) 2-20. · Zbl 1364.49018 |
| [7] | Battenfeld, I. (2008). Topological Domain Theory. Phd thesis, University of Edinburgh. · Zbl 1273.68202 |
| [8] | Battenfeld, I., Schröder, M. and Simpson, A. (2007). A convenient category of domains. In: Cardelli, L., Fiore, M. and Winskel, G. (eds.) Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science, vol. 172, Amsterdam, Elsevier, 69-99. · Zbl 1277.68113 |
| [9] | Bauer, A. (2000). The Realizability Approach to Computable Analysis and Topology. Phd thesis, Carnegie Mellon University. |
| [10] | Beggs, E. J. and Tucker, J. V. (2009). Computations via Newtonian and relativistic kinematic systems. Applied Mathematics and Computation215 (4) 1311-1322. · Zbl 1400.70002 |
| [11] | Bishop, E. and Bridges, D. (1985). Constructive Analysis, Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 279, Berlin, Springer-Verlag. · Zbl 0656.03042 |
| [12] | Blanck, J. (2000). Domain representations of topological spaces. Theoretical Computer Science247 (1—2) 229-255. · Zbl 0949.68096 |
| [13] | Blondel, V. D. and Tsitsiklis, J. N. (2000). The boundedness of all products of a pair of matrices is undecidable. Systems & Control Letters41 (2) 135-140. · Zbl 0985.93042 |
| [14] | Bournez, O., Campagnolo, M. L., Graça, D. S. and Hainry, E.. (2006). The general purpose analog computer and computable analysis are two equivalent paradigms of analog computation. In: Cai, J.-Y., Barry Cooper, S. and Li, A. (eds.) Proceedings of the Third International Conference on Theory and Applications of Models of Computation (TAMC), Springer, 631-643. · Zbl 1178.68253 |
| [15] | Bournez, O., Graça, D. S. and Pouly, A. (2013). Turing machines can be efficiently simulated by the general purpose analog computer. In: Hubert Chan, T.-H., Lau, L. C. and Trevisan, L. (eds.) Theory and Applications of Models of Computation, Springer, 169-180. · Zbl 1382.68067 |
| [16] | Brattka, V. (1998). Recursive and Computable Operations over Topological Structures. Phd thesis, FernUniversität Hagen. |
| [17] | Brattka, V., Hertling, P. and Weihrauch, K. (2008). A tutorial on computable analysis. In: Barry Cooper, S., Löwe, B. and Sorbi, A. (eds.) New Computational Paradigms: Changing Conceptions of What is Computable, New York, NY, Springer, 425-491. · Zbl 1145.03037 |
| [18] | Brattka, V. and Presser, G. (2003). Computability on subsets of metric spaces. Theoretical Computer Science30543-76. · Zbl 1071.03027 |
| [19] | Bresolin, D., Geretti, L., Villa, T. and Collins, P. (2015). An introduction to the verification of hybrid systems using Ariadne. In: Jan Van Schuppen, H. and Villa, T. (eds.) Coordination Control of Distributed Systems, Lecture Notes in Control and Information Sciences, vol. 456, Cham, Springer International, 339-346. · Zbl 1403.93108 |
| [20] | Clementino, M. M., Giuli, E. and Tholen, W. (2004). A functional approach to general topology. In: Pedicchio, M. C. and Tholen, W. (eds.) Categorical Foundations, Encyclopedia of Mathematics and its Applications, vol. 97, Cambridge, Cambridge University Press, 103-163. · Zbl 1059.54012 |
| [21] | Collins, P. (2005). Continuity and computability of reachable sets. Theoretical Computer Science341 (1-3) 162-195. · Zbl 1154.93351 |
| [22] | Collins, P. (2007). Optimal semicomputable approximations to reachable and invariant sets. Theory of Computing Systems41 (1) 33-48. · Zbl 1118.93320 |
| [23] | Collins, P. (2008). Computability of controllers for discrete-time semicontinuous systems. In: Proceedings of the 18th International Symposium on the Mathematical Theory of Networks and Systems, Blacksburg, Virginia. |
| [24] | Collins, P. (2011). Semantics and computability of the evolution of hybrid systems. SIAM Journal on Control and Optimization49 (2) 890-925. · Zbl 1217.93024 |
| [25] | Collins, P. (2014). Computable stochastic processes. arXiv:1409.4667. |
| [26] | Collins, P. and Graça, D. (2008). Effective computability of solutions of ordinary differential equations — the thousand monkeys approach. In: Proceedings of the 5th International Conference on Computability and Complexity in Analysis (CCA’08), Electronic Notes in Theoretical Computer Science, Amsterdam, The Netherlands, Elsevier, 53-64. · Zbl 1262.03081 |
| [27] | Collins, P. and Graça, D. S. (2009) Effective computability of solutions of differential inclusions: the ten thousand monkeys approach. J.UCS15 (6) 1162-1185. · Zbl 1201.03031 |
| [28] | Dahlgren, F. (2007). Partial continuous functions and admissible domain representations. Journal of Logic and Computation17 (6) 1063-1081. · Zbl 1155.03029 |
| [29] | Daniel, J. W. and Moore, R. E. (1970). Computation and Theory in Ordinary Differential Equations, San Francisco, W. H. Freeman & Co Ltd. · Zbl 0207.08802 |
| [30] | Edalat, A. (2009). A computable approach to measure and integration theory. Information and Computation207 (5) 642-659. · Zbl 1169.03032 |
| [31] | Edalat, A. and Sünderhauf, P. (1999). A domain-theoretic approach to computability on the real line. Theoretical Computer Science210 (1) 73-98. · Zbl 0912.68031 |
| [32] | Engelking, R. (1989). General Topology, Sigma Series in Pure Mathematics, vol. 6, Berlin, Heldermann. · Zbl 0684.54001 |
| [33] | Ershov, Ju. L. (1973). Theorie der numerierungen i. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik19 (4) 289-388. · Zbl 0295.02025 |
| [34] | Ershov, Ju. L. (1975). Theorie der numerierungen ii. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik21 (6) 473-584. · Zbl 0344.02031 |
| [35] | Ershov, Ju. L. (1977). Theorie der numerierungen iii. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik23 (4) 289-371. · Zbl 0374.02028 |
| [36] | Escardó, M. (2004). Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science8721-156. · Zbl 1270.68082 |
| [37] | Escardó, M. and Heckmann, R. (2002). Topologies on spaces of continuous functions. Topology Proceedings26 (2) 545-564. · Zbl 1083.54009 |
| [38] | Escardó, M., Lawson, J. and Simpson, A. (2004). Comparing Cartesian closed categories of (core) compactly generated spaces. Topology and its Applications143 (1-3) 105-145. · Zbl 1066.54028 |
| [39] | Filippov, A. F. (1988). Differential Equations with Discontinuous Righthand Sides, Mathematics and Its Applications, Dordrecht, Kluwer Academic Publishers. · Zbl 0664.34001 |
| [40] | Franklin, S. P. (1965). Spaces in which sequences suffice. Fundamenta Mathematicae57 (1) 107-115. · Zbl 0132.17802 |
| [41] | Fränzle, M. (1999). Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: Flum, J. and Rodriguez-Artalejo, M. (eds.) Computer Science Logic, Lecture Notes in Computer Science, vol. 1683, Berlin, Heidelberg, New York, Springer-Verlag. · Zbl 0944.68119 |
| [42] | Gabor, G. (2007). Continuous selection of the solution map for one-sided Lipschitz differential inclusions. Nonlinear Analysis66 (5) 1185-1197. · Zbl 1121.34018 |
| [43] | Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. W. and Scott, D. S. (1980). A Compendium of Continuous Lattices, Berlin, Springer-Verlag. · Zbl 0452.06001 |
| [44] | Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (2003). Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications, vol. 93, Cambridge, Cambridge University Press. · Zbl 1088.06001 |
| [45] | Goebel, R. and Teel, A. R. (2006). Solutions to hybrid inclusions via set and graphical convergence with stability theory applications. Automatica - A Journal of IFAC42 (4) 573-587. · Zbl 1106.93042 |
| [46] | Grzegorczyk, A. (1957). On the definitions of computable real continuous functions. Fundamenta Mathematicae4444-61. · Zbl 0079.24801 |
| [47] | Hansen, E. and William Walster, G. (2004). Global Optimization using Interval Analysis, 2nd edn., Monographs and Textbooks in Pure and Applied Mathematics, vol. 264, New York, Marcel Dekker Inc. · Zbl 1103.90092 |
| [48] | Hauck, J. (1980). Konstruktive Darstellungen in topologischen Räumen mit rekursiver Basis. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik26565-576. · Zbl 0455.03025 |
| [49] | Hauck, J. (1981). Berechenbarkeit in topologischen Räumen mit rekursiver Basis. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik27473-480. |
| [50] | Hertling, P. (1999). A real number structure that is effectively categorical. Mathematical Logic Quarterly45 (2) 147-182. · Zbl 0946.03050 |
| [51] | Hofmann, K. H. and Lawson, J. D. (1978). The spectral theory of distributive continuous lattices. Transactions of the American Mathematical Society246285-310. · Zbl 0402.54043 |
| [52] | Hofmann, K. and Mislove, M. (1981). Local compactness and continuous lattices. In: Continuous Lattices, vol. 871, Lecture Notes in Mathematics, Berlin, Heidelberg, Springer, 209-248. · Zbl 0464.06005 |
| [53] | Isbell, J. R. (1975). Function spaces and adjoints. Mathematica Scandinavica36317-339. · Zbl 0309.54016 |
| [54] | Jaulin, L., Kieffer, M., Didrit, O. and Walter, É. (2001). Applied Interval Analysis, London, Springer-Verlag London Ltd. With examples in parameter and state estimation, robust control and robotics, With 1 CD-ROM (UNIX, Sun Solaris). · Zbl 1023.65037 |
| [55] | Johnstone, P. T. (2002a). Sketches of an Elephant: a Topos Theory Compendium. Volume 1, Oxford Logic Guides, vol. 43. New York, The Clarendon Press, Oxford University Press. · Zbl 1071.18001 |
| [56] | Johnstone, P. T. (2002b). Sketches of an Elephant: a Topos Theory Compendium. Volume 2, Oxford Logic Guides, vol. 44, Oxford, The Clarendon Press, Oxford University Press. · Zbl 1071.18001 |
| [57] | Katok, A. and Hasselblatt, B. (1995). Introduction to the Modern Theory of Dynamical Systems, Encyclopedia of Mathematics and its Applications, vol. 54. Cambridge, Cambridge University Press. · Zbl 0878.58020 |
| [58] | Keimel, K. and Paseka, J. (1994). A direct proof of the Hofmann-Mislove theorem. Proceedings of the American Mathematical Society120 (1) 301-303. · Zbl 0789.54030 |
| [59] | Kleene, S. C. (1936). General recursive functions of natural numbers. Mathematische Annalen112 (1) 727-742. · JFM 62.0044.02 |
| [60] | Ko, K.-I. (1991). Complexity Theory of Real Functions, Progress in Theoretical Computer Science, Boston, MA, Birkhäuser Boston Inc. · Zbl 0791.03019 |
| [61] | Kushner, B. A. (1999). Markov’s constructive analysis; a participant’s view. Theoretical Computer Science219 (1-2) 267-285. Computability and complexity in analysis (Castle Dagstuhl, 1997). · Zbl 0916.68053 |
| [62] | Luckhardt, H. (1977). A fundamental effect in computations on real numbers. Theoretical Computer Science5 (3) 321-324. · Zbl 0374.02018 |
| [63] | Martin-Löf, P. (1984). Intuitionistic Type Theory, Napoli, Bibliopolis. · Zbl 0571.03030 |
| [64] | Mazur, S. (1963). Computable Analysis, Razprawy Matematyczne, vol. 33, Warszawa, Państwowe Wydawnictwo Naukowe. · Zbl 0113.24306 |
| [65] | Moore, R. E., Baker Kearfott, R. and Cloud, M. J. (2009). Introduction to Interval Analysis, Philadelphia, PA, Society for Industrial and Applied Mathematics (SIAM). · Zbl 1168.65002 |
| [66] | O’Connor, R. and Spitters, B. (2010). A computer-verified monadic functional implementation of the integral. Theoretical Computer Science411 (37) 3386-3402. · Zbl 1209.68108 |
| [67] | Pauly, A. (2016). On the topological aspects of the theory of represented spaces. Computability5 (2) 159-180. · Zbl 1401.03087 |
| [68] | Pauly, A. and De Brecht, M. (2015). Descriptive set theory in the category of represented spaces. In: Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE, 438-449. · Zbl 1395.03021 |
| [69] | Pour-El, M. B. and Ian Richards, J. (1989). Computability in Analysis and Physics, Perspectives in Mathematical Logic, Berlin, Springer-Verlag. · Zbl 0678.03027 |
| [70] | Puri, A., Varaiya, P. and Borkar, V. (1996). Epsilon-approximation of differential inclusions. In: Alur, R., Henzinger, T. A. and Sontag, E. D. (eds.) Hybrid Systems III, LNCS, vol. 1066, Berlin, Springer, 362-376. |
| [71] | Ruohonen, K. (1996). An effective Cauchy-Peano existence theorem for unique solutions. International Journal of Foundations of Computer Science7 (2) 151-160. · Zbl 0854.34010 |
| [72] | Saint-Pierre, P. (1994). Approximation of the viability kernel. Applied Mathematics & Optimization29 (2) 187-209. · Zbl 0790.65081 |
| [73] | Schröder, M. (2002a). Admissible Representations for Continuous Computations. Phd thesis, Fachbereich Informatik, FernUniversitöt Hagen. · Zbl 1020.18005 |
| [74] | Schröder, M. (2002b). Extended admissibility. Theoretical Computer Science284 (2) 519-538. Computability and complexity in analysis (Castle Dagstuhl, 1999). · Zbl 1042.68050 |
| [75] | Sipser, M. (1996). Introduction to the Theory of Computation, Boston, Course Technology, International Thomson. · Zbl 1191.68311 |
| [76] | Steen, L. A. and Seebach, J. A. (1978). Counterexamples in Topology, 2nd edn., New York, Springer-Verlag. · Zbl 0386.54001 |
| [77] | Taylor, P. (2008). A lambda calculus for real analysis. http://www.monad.me.uk/. |
| [78] | Tomlin, C., Lygeros, J. and Sastry, S. (2000). A game theoretic approach to controller design for hybrid systems. Proceedings of the IEEE88 (7), 949-970. |
| [79] | Turing, A. M. (1937) On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2)43 (1) 230-265. · JFM 62.1059.03 |
| [80] | Troelstra, A. S. and Van Dalen, D. (1988). Constructivism in Mathematics: An Introduction, Volume 1, Studies in Logic and the Foundations of Mathematics, vol. 121, Amsterdam, North-Holland. · Zbl 0661.03047 |
| [81] | Van Stigt, W. P. (1990). Brouwer’s Intuitionism, Studies in the History and Philosophy of Mathematics, vol. 2, Amsterdam, North-Holland Publishing Co. · Zbl 0707.03001 |
| [82] | Vickers, S. (1989). Topology via Logic, Cambridge Tracts in Theoretical Computer Science, vol. 5, Cambridge, Cambridge University Press. · Zbl 0668.54001 |
| [83] | Weihrauch, K. (2000). Computable Analysis: An Introduction, Texts in Theoretical Computer Science. An EATCS Series, Berlin, Springer-Verlag. · Zbl 0956.68056 |
| [84] | Weihrauch, K. and Grubba, T. (2009). Elementary computable topology. J.UCS15 (6) 1381-1422. · Zbl 1201.03039 |
| [85] | Ziegler, M. (2009). Physically-relativized Church-Turing Hypotheses: physical foundations of computing and complexity theory of computational physics. Applied Mathematics and Computation215 (4) 1431-1447. · Zbl 1192.68268 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
