Skip to main content

Everything is just so small

Often in mathematics, we have trouble talking about the sizes of things and understanding whether a thing is small enough to handle or too big to examine fully. In the most basic and natural form, a collection of objects is pretty small if it's finite because there's a computable way to list all of the objects of the collection, exhaust them, and witness that there are objects you can no longer fit into the collection. It is remarkable that, with reasonable though controversial assumptions, 'everything' is really tiny, and you can always count past all of its elements, and I mean count.

In the following, I present my informal description of the process of transfinite recursion and the astonishing implications of the axiom of choice on the notion of size.

Read more…

Monads: just a monoid in the category of endofunctors!

In computer science, and especially in functional programming, monads appear a lot! When one wants to understand them, however, it seems all explanations are either a fully categorical definition that is way too abstract or a hand-wavy intuition of 'boxes' and pipes and whatnot. In this post, I attempt to reconcile the two into a rigorous, but intuitive explanation.

Intuition

Monads are to seen, intuitively, as a way to nicely (functorially) extend objects in a certain universe (category) into other objects of that universe in a monoidal way, that is, there is a unit: a natural way to 'plainly' extend an object \(A\) into \(T A\) and there is a multiplication: there is a natural and unique way to combine higher level extensions \(T \cdots T A\) into a single layer \(T A\). The vagueness of the terms involved reflects the generality of applications of category theory. A monad is a purely categorical construct and therefore, so many categories reflecting so many different 'universes' of things could make use of monads, and the concrete intuition for each case can be quite different.

Read more…

Logic in Type Theory II: Identity Types

NOTE: This post needs JavaScript to show LaTeX expressions using MathsJax.

This is the second post on a series on logic as formulated in the language of type theory.

Identity types, some of the cornerstones of the new revolution in type theory and logic, are surprisingly simple, and surprisingly complex!

Definitional equality and path equality

Unlike in usual set theory, in type theory, equality is of two forms. The first form is definitional equality, which is a judgement, and the other is a binary relation \(a = b\), which is simply a type dependent over two parameters. The two kinds of equalities are different in nature as one belongs to the metalanguage, while the other to the language itself.

Judgemental equality asserts -- as a judgement -- that two terms are definitionally the same. For instance \(1 \equiv S\ 0\). Likewise, if one follows the definition of addition, one can always get \(3 + 5 \equiv 8\) definitionally, that is, purely in the metalanguage. However, although the addition of natural numbers is commutative, it is impossible to definitionally get \(n + m \equiv m + n\) for variable terms \(n\) and \(m\).

On the other hand, path equality -- whose naming will be clear when the path structure of types is discussed -- is a type which may or may not be inhabited. For instance, there is a way to prove that \(\forall x, y : \mathbb N, x + y = y + x\) by finding a term of type \(\prod_{x, y : \mathbb N} x + y = y + x\) (by recursion).

Read more…

Leap years and continued fractions

As a year is not precisely 365 days in length and as it is most favorable for calendars to preserve years as integer multiples of days, the technique of leap years balances the offset. The most primitive form of leap years would be to add a day to every 4th year, resulting in an average year length of 365.25 days, close enough to the ‘real’ year for daily calendar purposes and over the span of anyone’s lifetime. However, more elaborate systems have been introduced to account for a greater accuracy in this regard. In this article, I discuss a system based on the continued fraction expansion of the length of the year, and I prove a small optimality theorem about it.

Read more…

'Shape': a generalization of topological countability axioms

NOTE: This post needs JavaScript to show LaTeX expressions using MathsJax.

Motivation

The concept of countable bases for a topological space and its ramifications in terms of the power of sequences (allowing us to prove continuity of functions and that for every point of the closure \(\bar A\) of a set \(A\), there is a sequence of points of \(A\) converging to it) can be generalized into classes of nets of different levels of generality and produces fruitful results. The problem with the usual generalization to completely general nets is that it leaves no use for intermediate structures between first-countable spaces and completely general spaces. Introducing the concept of 'shape' solves that.

If you know the definitions and results presented before "\(I\)-shaped local basis", then just skip to that part.

Read more…

Logic in Type Theory I: Concepts

Intuistionistic logic and constructivism

The key insight of the Curry-Howard correspondence or the concept of 'propositions as types' is that there is a direct correspondence between logic and its operators and type theory and its operators.

This may at first seem strange and quite exotic (and it kind of is), but that's only because when one thinks of 'logic', it is most common -- by far -- to think of classical logic whereby every proposition (a statement which can be argued to be true or false) is assigned a truth value which mathematicians attempt to discover. A rather different logic is actually necessary to understand the Curry-Howard correspondence, namely: intuistionistic logic.

Intuitionism is the philosophical approach (in the philosophy of mathematics) whereby mathematical objects, including theorems and proofs are seen as human constructions instead of human discoveries. In other words, a group for instance is a lot more like a machine made up of pieces put together than Newton's second law of motion discovered based on empirical evidence of such law being respected in the Universe (there is obviously a lot more to be said about mathematics, technology, and physics, but for a layman in philosophy, this should get the point across).

Read more…