Master Thesis Impredicative Encodings of Inductive and Coinductive Types

TL;DR

This work extends impredicative encodings in System F to recover induction and coinduction principles for a range of data types. By embedding inductive structures as initial algebras and coinductive ones via quotients (and existential types for coinduction), the thesis shows η-rule compliance and establishes induction, coinduction, and bisimulation principles for lists, quotients, streams, W-types, and M-types. A general framework is developed to transport these encodings to arbitrary (non-higher) inductive and coinductive types, linking category-theoretic notions with type-theoretic encodings. The results advance foundational beyond-predicative encoding techniques and open avenues for formalization in proof assistants and exploration of higher inductive types.

Abstract

In the impredicative type theory of System F (λ2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the \b{eta}-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight (2018) used an extension of λC with sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras. In this thesis, we extend their results. We create a list and quotient type that have the desired induction principles. We show that we can use the technique for general inductive types by defining W-types with an induction principle. We also take the dual notion of their technique and create a coinductive stream type with the desired coinduction principle (also called bisimulation). We finish by showing that this dual approach can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.

Figures (16)

• Figure 1: Commutative diagram of a $\mathcal{L}$-morphism.
• Figure 2: Commutative diagram of the initial $\mathcal{L}$-algebra.
• Figure 3: Diagram of the uniqueness requirement of an initial $\mathcal{L}$-algebra.
• Figure 4: Commutative diagram of the $\beta$-rule for quotient types.
• Figure 5: Uniqueness rule for quotients.

Theorems & Definitions (186)

• Definition 3.2.1
• Definition 3.2.2
• Lemma 3.2.3
• proof
• Lemma 3.2.4
• proof
• Theorem 3.2.5
• proof
• Definition 3.2.6
• Proposition 3.2.7