# Search over uniformly continuous decidable predicates on infinite collections of types

Todd Waugh Ambridge, 15th December 2021 and 1st February 2022

I explore, in the following two blog posts, two key concepts: searchable types and closeness functions.

The blog posts are written in literate Agda, meaning that everything is both explained in text and fully-foramlised in Agda. I use Martín Escardó’s Agda library TypeTopology as a framework.

## Introduction

```module InfiniteSearch where
```

A type X is searchable if, given any predicate ```p : X → {tt,ff}```, we can find some `x : X` such that if there is some x₀ such that `p(x₀) ≡ tt` then also ```p(x) ≡ tt```.

In Haskell, or Agda with the termination checker turned off, we can write a program that searches Cantor space (infinitary binary sequences) ─ in fact, Martín Escardó wrote both programs, in 2007 and 2011 respectively.

The latter program goes further than just the Cantor space, it in fact shows that searchable types are closed under countable (`ℕ`-indexed) products. Given that searchable types coincide with the topological notion of compact types, this program – along with the proof that it terminates – are tantamount to the Tychonoff theorem for searchable types.

The proofs that these programs terminate rely on classical logic; they assume that the given predicates are continuous, and they use classical logic to determine that they are uniformly continuous. We wish to give a constructive formulation of the the Tychonoff theorem for searchable types by explicitly restricting to uniformly continuous predicates.

Intuitively, a predicate `p : X → {tt,ff}` is uniformly continuous if there is some notion of precision `δ` such that, for all `x,y : X` that are `δ`-close if `p(x) ≡ tt` then also `p(y) ≡ tt`.

We find it convenient to formulate uniform continuity using the notion of a closeness function. If a type `X` has a closeness function `c : X × X → ℕ∞`, where `ℕ∞` is the natural numbers extended with a point at infinity, then we can define a version of uniform continuity on predicates of that type. Using this version of uniform continuity, the notion of precision is a natural number `δ : ℕ`, and two elements `x,y : X` are `δ`-close if `δ ≼ c(x,y)`.

If a type has a canonical closeness function such that we can search the type for the answer to any predicate that is uniformly continuous with respect to the closeness function, then it is called (uniformly) continuously searchable.

We prove the Tychonoff theorem for continuously searchable types in constructive mathematics.

## Part I

```open import InfiniteSearch1
```

In the first part, we introduce the type theory and the concepts of closeness functions and continuously searchable types formally.

Then, we show that: 1. Every discrete type has a canonical closeness function, and that every such type is continuously searchable with respect to this closeness function if it is searchable in the traditional sense. 1. Every sequence type of discrete types has a canonical closness function, and that every such type is continuously searchable with respect to this closeness function.

## Part II

```open import InfiniteSearch2
```

In the second part, we show that types equipped with closeness functions are closed under countable products. Further, and chiefly, continuously searchable types themselves are closed under countable products.

`````` Escardo, Martin. (2007).