Algorithmic solution of higher type equations

Martín Escardó*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


In recent work, we developed the notion of exhaustible set as a higher type computational counter part of the topological notion of compact set. In this article, we give applications to the computation of solutions of higher type equations. Given a continuous functional f: X → Y and y ∈ Y, we wish to compute x ∈ X such that f(x)=y, if such an x exists. We show that if x is unique and X and Y are subspaces of Kleene-Kreisel spaces of continuous functionals with X exhaustible, then x is computable uniformly in f, y and the exhaustibility condition. We also establish a version of this for computational metric spaces X and Y, where is X computationally complete and has an exhaustible set of Kleene-Kreisel representatives. Examples of interest include evaluation functionals defined on compact spaces X of bounded sequences of Taylor coefficients with values on spaces Y of real analytic functions defined on a compact set. A corollary is that it is semi-decidable whether a function defined on such a compact set fails to be analytic, and that the Taylor coefficients of an analytic function can be computed extensionally from the function.

Original languageEnglish
Pages (from-to)839-854
Number of pages16
JournalJournal of Logic and Computation
Issue number4
Publication statusPublished - Aug 2013


  • admissible representation
  • computationally compact set
  • exhaustible set
  • Higher type computability
  • Kleene-Kreisel spaces of continuous functionals
  • QCB space
  • searchable set
  • topology in the theory of computation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic


Dive into the research topics of 'Algorithmic solution of higher type equations'. Together they form a unique fingerprint.

Cite this