Category Archives: Computation

Intuitionistic Mathematics and Realizability in the Physical World

This is a draft version of my contribution to “A Computable Universe: Understanding and Exploring Nature as Computation”, edited by Hector Zenil. Consider it a teaser for the rest of the book, which contains papers by an impressive list of authors.

Abstract: Intuitionistic mathematics perceives subtle variations in meaning where classical mathematics asserts equivalence, and permits geometrically and computationally motivated axioms that classical mathematics prohibits. It is therefore well-suited as a logical foundation on which questions about computability in the real world are studied. The realizability interpretation explains the computational content of intuitionistic mathematics, and relates it to classical models of computation, as well as to more speculative ones that push the laws of physics to their limits. Through the realizability interpretation Brouwerian continuity principles and Markovian computability axioms become statements about the computational nature of the physical world.

Download: real-world-realizability.pdf

The topology of the set of all types

It is well known that, both in constructive mathematics and in programming languages, types are secretly topological spaces and functions are secretly continuous. I have previously exploited this in the posts Seemingly impossible functional programs and A Haskell monad for infinite search in finite time, using the language Haskell. In languages based on Martin-Löf type theory such as Agda, there is a set of all types. This can be used to define functions $\mathbb{N} \to \mathrm{Set}$ that map numbers to types, functions $\mathrm{Set} \to \mathrm{Set}$ that map types to types, and so on.

Because $\mathrm{Set}$ itself is a type, a large type of small types, it must have a secret topology. What is it? There are a number of ways of approaching topology. The most popular one is via open sets. For some spaces, one can instead use convergent sequences, and this approach is more convenient in our situation. It turns out that the topology of the universe $\mathrm{Set}$ is indiscrete: every sequence of types converges to any type! I apply this to deduce that $\mathrm{Set}$ satisfies the conclusion of Rice’s Theorem: it has no non-trivial, extensional, decidable property.

To see how this works, check:

The Agda pages can be navigated be clicking at any (defined) symbol or word, in particular by clicking at the imported module names.

A puzzle about typing

While making a comment on Stackoverflow I noticed something: suppose we have a term in the $\lambda$-calculus in which no abstracted variable is used more than once. For example, $\lambda a b c . (a b) (\lambda d. d c)$ is such a term, but $\lambda f . f (\lambda x . x x)$ is not because $x$ is used twice. If I am not mistaken, all such terms can be typed. For example:

# fun a b c -> (a b) (fun d -> d c) ;;
- : ('a -> (('b -> 'c) -> 'c) -> 'd) -> 'a -> 'b -> 'd = <fun>

# fun a b c d e e' f g h i j k l m n o o' o'' o''' p q r r' s t u u' v w x y z ->
    q u i c k b r o w n f o' x j u' m p s o'' v e r' t h e' l a z y d o''' g;;
  - : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j ->
    'k -> 'l -> 'm -> 'n -> 'o -> 'p -> 'q -> 'r -> 's -> 't ->
    ('u -> 'j -> 'c -> 'l -> 'b -> 'v -> 'p -> 'w -> 'o -> 'g ->
     'q -> 'x -> 'k -> 'y -> 'n -> 't -> 'z -> 'r -> 'a1 -> 'e ->
     'b1 -> 'c1 -> 'i -> 'f -> 'm -> 'a -> 'd1 -> 'e1 -> 'd -> 's
     -> 'h -> 'f1) -> 'v -> 'b1 -> 'z -> 'c1 -> 'u -> 'y -> 'a1
     -> 'w -> 'x -> 'e1 -> 'd1 -> 'f1 = <fun>

What is the easiest way to see that this really is the case?

A related question is this (I am sure people have thought about it): how big can a type of a typeable $\lambda$-term be? For example, the Ackermann function can be typed as follows, although the type prevents it from doing the right thing in a typed setting:

# let one = fun f x -> f x ;;
val one : ('a -> 'b) -> 'a -> 'b =
# let suc = fun n f x -> n f (f x) ;;
val suc : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c =
# let ack = fun m -> m (fun f n -> n f (f one)) suc ;;
val ack :
  ((((('a -> 'b) -> 'a -> 'b) -> 'c) ->
   (((('a -> 'b) -> 'a -> 'b) -> 'c) -> 'c -> 'd) -> 'd) ->
   ((('e -> 'f) -> 'f -> 'g) -> ('e -> 'f) -> 'e -> 'g) -> 'h) -> 'h = <fun>

That’s one mean type there! Can it be “explained”? Hmm, why does ack compute the Ackermann function in the untyped $\lambda$-calculus?

Definability and extensionality of the modulus of continuity functional

In an earlier post I talked about the modulus of continuity functional, where I stated that it cannot be defined without using some form of computational effects. It is a bit hard to find the proof of this fact so I am posting it on my blog in two parts, for Google and everyone else to find more easily. In the first part I show that there is no extensional modulus of continuity. In the second part I will show that every functional that is defined in PCF (simply-typed $\lambda$-calculus with natural numbers and recursion) is extensional.  Continue reading

Running a classical proof with choice in Agda

As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together.

Using

for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).

As a corollary, we get the finite pigeonhole principle, using Friedman’s trick to make the existential quantifiers intuitionistic.

This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.

The main Agda files are

These are Agda files converted to html so that you can navigate them by clicking at words to go to their definitions. A zip file with all Agda files is available. Not much more information is available here.

The three little modules that implement the Berardi-Bezem-Coquand, Berger-Oliva and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift.