Complexity and Real Computation Laboratory

This shows you the differences between two versions of the page.

--- home [2020-09-11] – Martin Ziegler
+++ home [2023-03-18] (current) – [Mission] Martin Ziegler
@@ Line 1: / Line 1: @@
-====== Complexity and Computing with Continuous Data ======
+====== Computer Science for Continuous Data: Algorithmic Foundations of Numerics ======
-Building on Mathematical Logic,
+===== Motivation =====
-Theoretical Computer Science provides the foundation,
+Digital Computers naturally process discrete data, such as bits or integers or strings or graphs. From bits to advanced data structures, from a first semi-conducting transistor to billions in wafer-scale integration, from individual Boolean connectives to entire CPU circuits, from kB to TB memories, from 10<sup>2</sup> to 10<sup>9</sup> instructions per second, from assembly code to high-level programming languages: \\
-concepts, and approaches to modern software development:
+the success story of digital computing arguably is due to (1) hierarchical layers of abstraction and (2) the ultimate reliability of each layer for the next one to build on ― for processing discrete data.
-from problem specification via algorithm design and analysis,
-proof of optimality (aka Complexity Theory)
-to implementation and formal verification.
-It usually evolves around discrete data such as bits, integers, graphs.
+Continuous data on the other hand commonly arises in Physics, Engineering and Science: //natura non facit saltus//.
-"Discrete" can be understood to mean "in steps": there is no integer between 21 and 22.
+Such data mathematically corresponds to real numbers, smooth functions, bounded operators, or compact subsets of some abstract metric space.
-However data in Engineering or Mathematical applications is usually continuous:
-temperature does not 'jump' from 21 to 22 degrees Celsius,
-electricity from 21 to 22 volt, velocity from 21 to 22 km/h.
-Floating point numbers try to approximate continuous with discrete data;
+The rise of digital (over analog) computers led a stagnation in the realm of continuous (=//non//-discretized) data processing:
-but they thus violate many mathematical laws, such as distributivity.
+years after introduction and hardware standardization of IEEE 754 floating point numbers, mainstream Numerics is arguably still dominated by this forcible discretization of continuous data ― in spite of violating associative and distributive laws, breaking symmetries, introducing and propagating rounding errors, in addition to an involved (and incomplete) axiomatization including NaNs and denormalized numbers.
-Standardized in 1985 with IEEE754, they are an anachronistic data type
--- like assembly language is an outdated approach to programming,
-long superceded by more convenient and less error-prone
-object-oriented high-level programming languages.
-We develop a new and elegant high-level approach
+{{https://cs4contidat.eu/floatingpoints.png}}
-to algorithmically processing continuous data:
+Figure 1: Floating Point Number Line, from https://courses.engr.illinois.edu/cs357/fa2019/assets/images/figs/floatingpoints.png. See also https://www.jasss.org/9/4/4.html#2.1
-  * multivalued problem specification in first-order logic over two-sorted structure
-  * algorithm design over exact arithmetic primitives with partial tests
+\\
-  * algorithm analysis w.r.t. realistic bit-cost in dependence on the output precision
-  * proof of optimality by sensitivity/adversary argument or relating to NP-hard problems
+Deviations between mathematical structures and their hardware counterparts are common also in the discrete realm,
-  * implementation in newly devised imperative object-oriented paradigm "Exact Real Computation"
+such as the “integer” wraparound 255+1=0 occurring in bytes that led to the //[[https://en.wikipedia.org/wiki/Nuclear_Gandhi|Nuclear Gandhi]]// programming bug.
-  * formal verification in extension of Floyd-Hoare Logic
+Similarly, deviations between exact and approximate continuous data underlie infamous failures such as the  [[https://en.wikipedia.org/wiki/Ariane_flight_V88|Ariane 501 flight V88]] or the [[https://en.wikipedia.org/wiki/Sleipner_A|Sleipner-A oil platform]].
+Nowadays high-level programming languages (such as Java or Python) provide a user data type (called for example ''BigInt'' or ''mpz_t'') that fully agrees with mathematical integers, simulated in software using a variable number of hardware bytes.
+This additional layer of abstraction provides the reliability for advanced discrete data types (such as weighted or labelled graphs) to build on, as mentioned above.
+===== Mission =====
+We develop Computer Science for continuous data, to catch up with the discrete case: from foundations via practical implementation to commercial applications.
+In fact some object-oriented software libraries, such as [[http://irram.uni-trier.de/|iRRAM]] or [[https://cs.nyu.edu/exact/core_pages/intro.html|Core III]] or [[https://store.fmi.uni-sofia.bg/fmi/logic/theses/lambov/|realLib]] or [[http://ariadne-cps.org/|Ariadne]] or [[https://michalkonecny.github.io/aern/|Aern]], have long been providing general (=including all transcendental) real numbers as exact encapsulated user data type.
+Technically they employ finite but variable precision approximations: much like ''BigInt'', but with the added challenge of choosing said precision automatically and adaptively sufficient for the user program to appear as indistinguishable from exact reals. This requires a new (namely partial) semantics for real comparison: formalizing the folklore to “avoid” testing for equality, in terms of [[https://en.wikipedia.org/wiki/Three-valued_logic|Kleene's ternary logic]].
+   *  [[http://sewonpark.com/sewon_park|Sewon Park]] in [[http://realcomputation.asia/THESES/21Sewon.pdf|his PhD Thesis]] has extended that semantics to composite expressions, and further to command sequences aka programs, whose correctness can then be symbolically verified using an extension of [[https://en.wikipedia.org/wiki/Hoare_logic|Floyd-Hoare Logic]];
+see also the preprint [[http://arXiv.org/abs/1608.05787|arXiv:1608.05787]].
+     * Thus reliably building on single real numbers leads to higher (but finite) dimensional data types, such as vectors or matrices.
+[[http://sewonpark.com/sewon_park|Sewon Park]] has designed and analyzed and implemented a [[https://github.com/realcomputation/irramplus/tree/master/GAUSSELIM|reliable variant of Gaussian Elimination]], in particular regarding pivot search.
+[[https://slee3379.math.gatech.edu/|Seokbin Lee]] has designed and analyzed and implemented a [[https://github.com/realcomputation/irramplus/tree/master/GRASSMANN|reliable variant of the Grassmannian]], i.e., the orthomodular lattice of subspaces of some fixed finite-dimensional Euclidean or unitary vector space.
+  * Infinite sequences of real numbers arise as elements of ℓ<sup>p</sup> spaces; and as coefficients to analytic function germs.
+[[http://www.holgerthies.com/|Holger Thies]] has implemented [[https://github.com/holgerthies|analytic functions for reliably solving ODEs and PDEs]].
+See the references below for this and more [[https://github.com/realcomputation/irramplus|continuous data types on GitHub]].
+Like discrete data, processing continuous data on a digital computer eventually boils down to processing bits: finite sequences of bits in the discrete case, in the continuous case infinite sequences, approximated via finite initial segments.
+Coding theory of discrete data is well-established since Claude Shannon’s famous work.
+Encoding real numbers as infinite sequences of bits is non-trivial: the binary expansion for example renders addition uncomputable.
+  *  [[https://www.donghyunlim.com/|Donghyun Lim]] in [[http://realcomputation.asia/THESES/19Donghyun.pdf|his MSc Thesis]] has investigated encoding more advanced (such as function) spaces;
+see also the [[https://arxiv.org/abs/2002.04005|preprint arXiv:2002.04005]].
+  *  [[https://www.comp.nus.edu.sg/programmes/pg/phdcs/directory/|Ivan Koswara]] and [[http://www.lix.polytechnique.fr/Labo/Gleb.POGUDIN/|Gleb Pogudin]] and [[https://www.researchgate.net/profile/Svetlana-Selivanova|Svetlana Selivanova]] have [[http://cs4contidat.eu/yjcom101727.pdf|related the bit-complexity intrinsic to approximate solutions of linear partial differential equations]] to discrete complexity classes #P and PSPACE.
+  * [[http://informatik.uni-trier.de/~brausse/personal/index.xhtml|Franz Brauße]] and [[https://www.maastrichtuniversity.nl/pieter.collins|Pieter Collins]] envision a Computer <del>Algebra</del>//Analysis// System
+===== References =====
+  * [[http://youtube.com/playlist?list=PLvcvykdwsGNE9HyG46aT6aqCvvJBZgKZh|30h online lecture series]] in [[https://youtube.com/channel/UCSehZy20EPRqgV0uiTzJkEA|YouTube channel]]
+  *  C++ classes for continuous data types: [[https://github.com/realcomputation|RealComputation]], [[https://github.com/holgerthies|Holger Thies]]
+  * [[https://doi.org/10.1007/978-3-031-14788-3_5|Vision paper]]
+  * [[https://doi.org/10.1016/j.jco.2022.101727|Recent publication characterizing the bit-complexity of Partial Differential Equations in terms of discrete complexity classes P/NP/#P/PSPACE/EXP]]
+  * [[https://arxiv.org/abs/2002.04005|Preprint on quantitative coding theory of continuous data]]
+  * [[https://arxiv.org/abs/1608.05787|Preprint on semantics and formal verification of programs processing real numbers exactly with partial semantics of comparison]]
+  * [[http://stoimenov.net/stoimeno/homepage/ckt/index.html|Workshop on Computational Knot Theory]] organized by [[http://stoimenov.net/stoimeno/homepage/|Alexander Stoimenow]]
+  * [[https://www.fiff.de/publikationen/fiff-kommunikation/fk-2022/fk-2022-2/fk-2022-2-content/fk-2-22-p25.pdf|Vision paper (in German) about Artificial Intelligence]], written jointly with [[https://www.fernuni-hagen.de/philosophie/lg1/team/andrea.reichenberger.shtml|Andrea Reichenberger]]
-More on our [[https://www.youtube.com/channel/UCSehZy20EPRqgV0uiTzJkEA|YouTube-Channel]]...

Differences