[Agda] Hanging out with the Lean crowd

[Martin Escardo]

Your answer below seems provocative enough for me to want to answer. :-)

So here we go.

On 22/08/2020 00:11, mechvel at scico.botik.ru wrote:
> On 2020-08-21 23:21, Martin Escardo wrote:
>> You don't think the model in which types are spaces and functions are
>> continuous convincing enough? Excluded middle is not continuous.
>
>
> Too abstruse, unnatural.

It is actually quite natural: continuity says that "a finite amount of
information about the value of a function depends only on a finite
amount of information about the argument of the function". A finite
amount of output depends only on a finite amount of input. Finitely
many digits of the output of a function f : ℝ → ℝ depend only on
finitely many digits of its input. This is precisely what the ε-δ
formulation of continuity says. There is also an interpretation of
this phenomenon in terms of open sets, which are seen as "observable
properties" of points of the space. Continuity captures a fundamental
aspect of computation without mentioning Turing machines. Continuity
is a finiteness condition, at least for most spaces that arise
naturally in analysis. And in computation, too, such as the Cantor
space.

> To perceive this I need to study attentively in what precisely way
> types correspond to (topological? metric?) spaces, and so on.  An
> artificial thing.

Would I convince you if I used topological intuition and machinery to
prove a theorem in computation that would seem outrageous to both
Computer Scientists and Constructive Mathematicians?

We can write the following unlikely functional program in Agda (and in
Martin-Loef Type Theory of any variety):

 (1) Consider the type of decreasing infinite sequences of digits 0 and 1.

     Call this type ℕ∞, because

      - The sequence of n-many ones followed by infinitely many zeros
        encodes the natural number n.

      - The sequence of infinitely many ones encodes ∞,

     So we have an embedding ℕ → ℕ∞ and a new point ∞ in ℕ∞.

 (2) There is an Agda program that decides, for a given p : ℕ∞ → Bool,
     whether or not there is x : ℕ∞ with p x ≡ True.

     Clearly such a program *does not* exist if we replace ℕ∞ by ℕ.
     This non-existence is a theorem of computability theory.

     But it does exist with ℕ∞.

The intuition (if you develop it) is that the type ℕ∞ constructed in
(1) is the one-point compactification of the discrete space of natural
numbers, and that compactness is the topologist's notion of
finiteness. So although there are infinitely many cases to check to
perform the decision (2), there are only "compactly many" cases to
check, and this is possible. Still surprising, perhaps, but less so
when we consider the world in which ℕ∞ is compact and all functions
are continuous. We don't need to add any continuity axioms to Agda,
but, when we conceive such a program, we do need to think of types as
spaces.

Without topological intuition and techniques, people are unlikely to
come up with the idea of proving (2), that is, writing an Agda program
that checks infinitely many cases and answers "yes" or "no" without
using excluded middle: after all we seem to have learned from
computability theory that we can't perform such decisions on infinite
spaces. Actually we haven't. The above is a counter-example.

> It has sense to consider this only if simpler explanations are not found.

Oh, with this I agree fully. There are suitations, indeed, such as the
above, where simple explanations are not available.

> I mean a philosophical question about nature, to which it is applied our
> basic intuition.

Regarding mathematics, I only believe in mathematically justified
philosophy. Philosophy would presumably tell you that you can't
perform algorithmic decisions that depend on checking infinitely many
cases. But there you have a counter-example above. Built from
topological intuition and techniques.

Best,
Martin