English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The real numbers are important in both mathematics and computation theory.Computationally, real numbers can be represented in several ways; most commonlyusing inexact floating-point data-types, but also using exactarbitrary-precision data-types which satisfy the expected mathematicalproperties of the reals. This thesis is concerned with formalising propertiesof certain types for exact real arithmetic, as well as utilising themcomputationally for the purposes of search, optimisation and regression.  We develop, in a constructive and univalent type-theoretic foundation ofmathematics, a formalised framework for performing search, optimisation andregression on a wide class of types. This framework utilises Mart\'inEscard\'o's prior work on searchable types, along with a convenient version ofultrametric spaces -- which we call closeness spaces -- in order toconsistently search certain infinite types using the functional programminglanguage and proof assistant Agda.  We formally define and prove the convergence properties of type-theoreticvariants of global optimisation and parametric regression, problems related tosearch from the literature of analysis. As we work in a constructive setting,these convergence theorems yield computational algorithms for correctoptimisation and regression on the types of our framework.  Importantly, we can instantiate our framework on data-types from theliterature of exact real arithmetic, allowing us to perform our variants ofsearch, optimisation and regression on ternary signed-digit encodings of thereal numbers, as well as a simplified version of Hans-J. Boehm's functionalencodings of real numbers. Furthermore, we contribute to the extensive work onternary signed-digits by formally verifying the definition of certain exactreal arithmetic operations using the Escard\'o-Simpson interval objectspecification of compact intervals.

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics