Advanced Namespace Tools blog

28 January 2020

Choice Principles in Logic and Code

This post is 5th in a series describing research into infinitary mathematical objects and their possible computational interpretation. The first second third and fourth posts described motivations, experiments, goals, and foundations. This post focuses on choice principles.

Termination Assertion

After our last past examined the basic logic of dependent types and Agda, we return to study of the Escardo 'impossible' searches, which can perform exhaustive searches over Cantor space in finite time and determine equality of functions from the Cantor type to a type with decidable equality. Here is a simple Agda translation of the core pieces, adapted from Martin Escardo Seemingly Impossible Functional Programs. Note the annotation TERMINATING for the cfind function.

open import Agda.Builtin.Bool renaming (Bool to Bit; true to ■; false to □)
open import Agda.Builtin.Nat
open import Data.Bool renaming (Bool to Bit; true to ■; false to □)

Cantor : Set
Cantor = Nat → Bit

_⋉_ : Bit → Cantor → Cantor
(b ⋉ c) zero = b
(b ⋉ c) (suc x) = c x

forsome : (Cantor → Bit) → Bit
forevery : (Cantor → Bit) → Bit

cfind : (Cantor → Bit) → Cantor
{-# TERMINATING #-}
cfind p = if forsome (λ a → p (□ ⋉ a))
          then (□ ⋉ cfind (λ a → p ( □ ⋉ a)))
          else (■ ⋉ cfind (λ a → p ( ■ ⋉ a)))

forsome p = p (cfind (λ a → p a))

forevery p = not (forsome (λ a → not (p a)))

equal : (Cantor → Nat) → (Cantor → Nat) → Bit
equal f g = forevery (λ a → f a == g a)

In Agda, by default all functions are required to be total (provide an output for all inputs) and provably terminating (always reduce to a value after a finite amount of computation). The TERMINATING annotation is here because Agda's system of logic doesn't 'see' the cfind function as being guaranteed to ever return a value, it thinks it might recurse into itself endlessly. The Escardo blog post about the original Haskell states "What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single n such that for all inputs it is enough to look at depth n to get the answer (which in this case is always finite, because it is an integer)."

More recent work of Escardo in Agda in his TypeTopology development is divided into a large majority of safe modules and a tiny amount of unsafe. Within the unsafe modules is CountableTychonoff which is used to prove the compactness of Cantor space. The countable-Tychonoff proof here also requires TERMINATING. There is a comment explaining the need for the termination annotation and a remark about 'LPO' - the Limited Principle of Omniscience - in the context of noting that perhaps a strict constructivist won't be convinced the program terminates.

Let's take a step back to establish context. Agda is based on Martin-Löf type theory, which was created for the purpose of constructive mathematics in the tradition of Bishop. The intuitionism of Brouwer is another notable member of the more constructive, non-classical approaches to mathematical foundations. Classical mathematics is happy to 'say' that something exists even if it cannot provide an effective method to produce a concrete example. Constructivism is about what can actually be calculated and computed using effective methods by humans and machines - at least in theory, given sufficient pencils and paper or arbitrarily long but still finite Turing machine runtime.

As a result, we expect that in general, if we do possess a provably effective computational method - such as the 'impossible' search algorithm - which can be run on real computers and gives definite output, we can encode this into a constructive proof-oriented language. However, in this case, even though we have mathematical principles that explain the searchability and compactness of Cantor space, and computer programs that provide effective computational methods we can calculate specific examples with - there is an issue that prevents Agda from being 'convinced' that these proofs are valid and the algorithms terminate, that relates to how constructive mathematics differs from classical. What is the nature of these specific issues?

Axioms : take your Choice

And now we enter the tangled forest of Branching Paths which may or may not ever reach an end. We have Choices to make. Do we walk step-by-step, with no knowledge or belief of where our choices may take us? Or can we fix our eyes on a point on the horizon and walk toward it, confident that as long as we take the correct branch, a Pathway exists? Is there always a pattern to the way the trees of the forest grow to shape the path, or are the choices we may be faced with completely unknown? König's Lemma :

The wikipedia article contains a section of utmost interest, titled "Relationship to constructive mathematics and compactness". It explains the relation to Brouwer's fan theorem and some forms of bar induction and the topological compactness interpretation. The next section tells us that König's lemma is a weaker form of the Axiom of Choice, mentions the dependent (not the same as dependent types!) and countable forms, references Tychonoff's theorem, and now we have the end of the thread in our hands and it leads into the labyrinthine heart of the woods.

A standardized framework for most mathematics is Zermelo-Fraenkel set theory with the Axiom of Choice, aka ZFC. The controversy about this axiom is most famously typified by the Banach-Tarski decomposition and reassembly of one solid ball into two solid balls. This example has been kicked to death in dozens of other semitechnical blog posts so I will comment only that the richness of math supports far stranger abstract operations and math is not physics and doesn't need to be. Choice-related principles can manifest in computer code we can actually run, how our physical brains model reality, and in the logical structure of the world of our experience.

There are finitistic programs we can run, such as impossible.hs, which concretize infinitary logical structure. We will study other examples and applications, and we will often encounter a core principle at the heart, manifested in code or pure logic. The continuation monad is the prototypical example. It looks like this in my Hugs Haskell install in Plan 9:

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

instance Monad (Cont r) where
	return a = Cont ($ a)
	m >>= k  = Cont $ \c -> runCont m $ \a -> runCont (k a) c

For reasons that are still a topic of active research, continuation-like constructions provide a computationally meaningful implementation of choice principles that are strong enough to provide constructive versions of countable and dependent choice. Martin Escardo and Paul Oliva prove this for their 'Selection Monad' in Selection Functions, Bar Recursion, and Backward Induction.

The termination annotations required by the code at the start of this blog are required because the basic type-logic of Agda does not encode a choice principle of strength sufficient to prove the compactness results that guarantee termination of the Cantor space search. In upcoming blog posts, we will explore how the line between constructive and non-constructive and how Church-Turing limits apply to real-world computers is still unclear. Some seemingly non-constructive applications of choice principles in classical math have constructive translations. The continuation monad, the Escardo-Oliva selection monad, the codensity monad, the ultrafilter monad, and others are all related. A general principle of transition between the discrete and continuous is involved. It may be possible to extend real world computation to analogs of even more powerful logical principles similar to embeddings related to strong axioms of infinity in set theory.

Cantor Set Compactness, Recursive Trees, Choice

In pursuit of conceptual understanding, we may find it useful to have a large scale meaning-intuition for families of mathematical concepts even (or especially!) if there is rich technical detail and additional structure. Many results we are studying can be understood in the context of a prototypical object - the Cantor set, which can be seen as an infinite tree of binary choices expressible as the space of infinite strings of binary digits. The concepts of choice, recursion, and transformation of finite to infinite and from discrete to continuous are all manifested in this construction. The interpretation as binary bitstrings connects to Boolean algebra and the real world implementation of computers. The work of 20th century mathematicians in formalization and creation of abstractions such as Turing machines and the lambda calculus and set theoretic logic in general follows on the foundational work of Boole in providing a precise symbolic formalism for classical logic.

König's lemma and Tychonoff's theorem as applications of Choice have an analog in binary logic - the Boolean Prime Ideal which is equivalent to the Ultrafilter Lemma. The conceptual significance of ideals and filters is carriers of information about possible classifications. The easiest intuition for this is simply generalizing a single finite yes/no choice to an infinite series of yes/no choices. We can take the logical principle of making a single choice, project that principle forward in time to a potentially infinite sequence of future choices, and we may also apply the principle that at any given time in the future, only an arbitrarily large yet still finite amount of choices will have been made.

The spatial visualization of a physical tree helps build intuition. The binary choice sequence can be visualized as a root stem that branches in two, then each branch again branches, each sub-branch branches - and so forth onward as far as we wish to continue. Any given binary sequence is following a path from the root upward into the canopy, making choices as we go. This process of iterative recursive self-similar branching - the tree rule is that every branch of a tree is also a sub-tree - produces an uncountable infinity of points at its limit. The final outermost layer of the tree canopy is almost-continuous but divided into the uncountable yet separated set of branch-tips.

The Cantor set choice-tree is our prototypical choice-structure. Every compact metric space is a continuous image of the Cantor set. If we have this topology, we can use the Stone space duality with Boolean algebras. If our data is expressible within a Boolean algebra, we can construct the compact space of ultrafilters on its elements. As a result, the process of transferring data to computer manipulable binary form automatically compact-ifies things in a sense, becase we are encoding into representation in the context of a digital Boolean-algebra based cpu instruction set. There is a risk of layer confusion here; the point is that the physical realization of our computations is accomplished via switching algebra of logic gates.

Mathematical principles such as the ultrafilter lemma and Brouwer's fan and bar constructions dance along the line between constructive and non-constructive. They transfer our knowledge of the overall possibility structure to specific finite cases, and vice versa. This relates to the conceptual core of the inductive family of mathematical principles and compactness. Induction allows us to move from a specific finite proof to an infinite chain of proofs. The logical compactness theorem can be seen as a generalization of this - a set of first-order sentences has a model if and only if every finite subset of it has a model. These relations between the finite/discrete and infinite/continuous manifest in ultrafilter based constructions as a generalization of the limit concept. Terry Tao has an excellent blog post on Ultraproducts as a Bridge Between Discrete and Continuous Analysis.

Compactness is perhaps the prototype of the family of reflection principles that bridge the mathematical and metamathematical. Viewed in the context of the ultrafilter lemma and its topological consequences, choice principles are an assertion that we can generalize from the finite toward the infinite and vice versa and thus create compactness in our constructions. The continuation monad and its specializations such as the selection monad, codensity monad, ultrafilter monad, and others, provides a computational tool for choice based constructions.

Possibilities, Power Sets, and Brouwer

A central study of mathematical logic is understanding the space of possibilities generated by the infinite production rule for the natural numbers and the possible logical relationships describing collections of naturals - aka sets of naturals aka the real numbers, aka the powerset of any countably infinite collection. The classical study of the possibility space often makes use of the law of excluded middle to reason about the structure of these collections. These results can be seen in a way which is not contradictory to constructive principles. There is a double-negation translation from classical to intuitionistic logic, in which many classical results are understood as proving not-not-X rather than X itself. The constructive view of the possibility space distinguishes this from the effectively constructible possible objects for whose existence we can produce a witness via a definite finitistic method. To quote Bell from the SEP entry linked previously: "The true depth of the connection between the Axiom of Choice and logic emerges only when intuitionistic or constructive logic is brought into the picture. It is a remarkable fact that, assuming only the framework of intuitionistic logic together with certain mild further presuppositions, the Axiom of Choice can be shown to entail the cardinal rule of classical logic, the law of excluded middle."

Brouwer's mathematical concepts spring from a philosophical idea of the mathematician as the 'creating subject', building mental constructions which include sequences of choices, some of which may be defined by an algorithmic rule but may also be random or free. This Brouwerian intuitionistic view of the creating subject making choices which may or may not be given by a set rule points toward a synthesistic understanding of the power of constructive object formation within a larger possibility space that might not be rule-defined, and this corresponds well with the potential capacities of computers situated in physical reality. We can make use of continuation control structures, user input, and true environmental entropy to push the limits of our computationally realizable possibilities and richness of input/output space across which we may construct logical compactness or other applications of infinitary reflection and choice principles. It is my hope that this means real world computer software can make use of ultrafilter-analogous constructive computations to assist with practical applications of mathematical principles related to fairness and globally optimized choice in voting and economics and communication networks.

Further Reading

Future blog posts will gloss some of this material, but the interested reader is encouraged to dig into the vast literature on choice principles in constructive type theory and the axiom of choice in general. A few recommendations:

I'd like to especially recommend that a reader interested in the overlap of type, set, and categorical foundations take the time to survey the publications of Maria Maietti who has developed a sophisticated framework for handling the use of choice principles in constructive type theoretical foundations.

A preview of additional topics and many links to primary sources are found in /lib/CubeRead.agda on the recent ANTS release:

Future posts in this series will continue to explore aspects of this material in contexts such as type theoretical forcing and the long awaited (?) technical details of ultrafilters and their derivative constructions.