Global optimisation with constructive reals

Dan R. Ghica, Todd Waugh Ambridge

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We draw new connections between deterministic, complete, and general global optimisation of continuous functions and a generalised notion of regression, using constructive type theory and computable real numbers. Using this foundation we formulate novel convergence criteria for regression, derived from the convergence properties of global optimisations. We see this as possibly having an impact on optimisation-based computational sciences, which include much of machine learning. Using computable reals, as opposed to floating-point representations, we can give strong theoretical guarantees in terms of both precision and termination. The theory is fully formalised using the safe mode of the proof assistant AGDA. Some examples implemented using an off-the-shelf constructive reals library in JAVA indicate that the approach is algorithmically promising.

Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages13
ISBN (Electronic)9781665448956
ISBN (Print)9781665448963 (PoD)
Publication statusPublished - 7 Jul 2021
Event36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 - Virtual, Online
Duration: 29 Jun 20212 Jul 2021

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871
ISSN (Electronic)2575-5528


Conference36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
CityVirtual, Online

Bibliographical note

Funding Information:
Acknowledgement. We thank Martín Escardó for helping improve the mathematical content and presentation; and Jon Rowe for suggestions and ideas in the early stages of this research. Todd Waugh Ambridge thanks the School of Computer Science’s Agda Club for their feedback and fellowship. Dan R. Ghica acknowledges the support of UK EPSRC Grant EP/V001612/1.

Publisher Copyright:
© 2021 IEEE.


  • Java
  • Machine learning algorithms
  • Machine learning
  • Search problems
  • Libraries
  • Data models
  • Regression analysis

ASJC Scopus subject areas

  • Software
  • Mathematics(all)


Dive into the research topics of 'Global optimisation with constructive reals'. Together they form a unique fingerprint.

Cite this