This repository contains the text and source code for my Bachelor’s thesis, presented at the University of Granada on the 21st of June, 2018. I would like to thank my advisors for this project, Pedro A. García Sánchez and Manuel Bullejos Lorenzo.
1. Lambda calculus.
- Untyped λ-calculus.
- Simply typed λ-calculus.
- The Curry-Howard correspondence.
- Other type systems.
2. Mikrokosmos.
- Implementation of λ-expressions.
- User interaction.
- Usage.
- Programming environment.
- Programming in untyped λ-calculus.
- Programming in the simply typed λ-calculus.
3. Category theory.
- Categories.
- Functors and natural transformations.
- Constructions on categories.
- Universality and limits.
- Adjoints, monads and algebras.
4. Categorical logic.
- Presheaves.
- Cartesian closed categories and lambda calculus.
- Working in cartesian closed categories.
- Locally cartesian closed categories and dependent types.
- Working in locally cartesian closed categories.
- Topoi.
5. Type theory.
- Martin-Löf type theory.
- Homotopy type theory.
- Verified formal proofs.
6. Conclusions and further work.
7. Appendices.
Assuming A∨¬A for any arbitrary proposition A may lead to an unnecessarily narrow view of mathematics and its relationship with computation. This principle, called the law of excluded middle, was the subject of much debate during the beginning of the 20th century. Constructive mathematics is mathematics done without assuming excluded middle: Brouwer’s intuitionism and Bishop’s constructive analysis are examples of this school of thought. However, constructivism did never attract the interest of the majority of mathematicians during the foundational crisis.
Some years after, in 1945, the notion of categories originated with Eilenberg and Mac Lane’s work on cohomology theory. Nowadays, functors, natural transformations and universal properties are used in all the different branches of mathematics. While we generally still prefer to rely on set-theoretical foundations, many axiomatizations of mathematics based on category theory have been proposed. It was observed that any category with enough structure is able to interpret most of mathematics in an internal logic; and remarkably, this internal logic does not satisfy in general the law of excluded middle.
How does all of this relate to programming? Suppose we want to design a programming language. A possible path is to follow the functional paradigm that revolves around composition and inductive data structures. We would borrow ideas from λ-calculus, a collection of formal systems Alonzo Church proposed in the 1930s. They can be seen as models of computation, and many modern programming languages are heavily influenced by them, specially in the typed variants of the calculus. But then, we have the realizability interpretation of logic without excluded middle by Heyting and Kolmogorov, that regards proofs as programs and propositions as types. Under this interpretation, the simply typed lambda calculus is precisely a language for constructive logic that loses its computational nature when excluded middle is added.
Categories are the framework in which we can make sense of this. A cartesian closed category is a category that has exponential objects (whose elements can be regarded as functions) and all finite products. These two constructions are particular cases of adjunctions, a purely categorical description of how certain transformations in mathematics relate. It is easy to see how these adjunctions translate into computations in lambda calculus, thus encoding a language for logic and programming inside categories.
The logic we first obtain this way is a propositional logic. This identification suffices to prove some theorems that have many known results as corollaries, such as the Lawvere’s diagonal theorem: a surjective morphism g : A → Bᴬ implies the existence of a fixed point for each f : B → B. However, we want to extend this logic with universal and existential quantifiers, and locally closed cartesian categories are the tool for this task. They are categories in which every slice generated by the morphisms to a particular object has the cartesian closed structure. Quantifiers are adjoints on this setting, and they provide, inside the type theoretical interpretation, dependent pairs, written with Σ, and dependent functions, written with Π. These correspond to the existential and universal quantifier respectively and they define types that can depend on elements of other types. Now we can prove more complex results, and the example we study is Diaconescu’s theorem: the Axiom of Choice implies the law of excluded middle.
Finally, Martin-Löf type theory helps to synthesize all these ideas into a formal system that is active subject of research. This is the environment in which Voevodsky’s Univalence Axiom gives rise to Homotopy Type Theory, a recent development relating type theory and topological constructions. As an example, we will prove that the fundamental group of the circle is Z with a computer verified mathematics library. Our first objective is to build an interpreter for untyped and simply typed lambda calculus. Results on the first section of this text provide solid theoretical grounds for this purpose. We want the interpreter to be a didactic tool, useful for experimentation and with a clear theoretical basis in which to interpret the constructions and programs we can write on it. Our second main objective is to understand how dependent type theory works internally and to develop libraries of computer verified mathematics, proving simple theorems, undertaking the project of constructing the real numbers from scratch and formulating homotopy types within this structure.
The Mikrokosmos lambda interpreter has its documented code published under a GNU General Public License v3.0 at the following link.
A previous stable version on the Hackage platform can be found at https://hackage.haskell.org/package/mikrokosmos. An HTML version of the documented code can be accessed at https://mroman42.github.io/mikrokosmos/haddock/.
Code for the Agda-mltt and Agda-hott libraries can be downloaded from the main repository. The easily-navigable HTML versions can be found at the following links.