Andrew Swan: Computable and non-computable 2-groups

Abstract

The idea behind computable structures is to study which algebraic structures can be directly and completely implemented by computers, and which cannot. We say an algebraic structure is *computable* if its carrier set is a computable subset of the naturals and any algebraic operations are computable functions. Amongst the earliest results on computable structures is Rabin's work on computable (1-)groups, and in particular the existence of finitely generated groups that are *not* computable.

By working in realizability models and using ideas from synthetic computability theory, we can simplify the definition of computable structure by only requiring the carrier set to be a decidable subset of N. In this setting any algebraic structure is automatically computable and algebraic structure that is *not* necessarily computable is the non trivial definition, but can nonetheless be defined cleanly using higher modalities (as studied by Rijke, Shulman and Spitters).

I'll combine the above ideas with the simplest example of higher algebraic structure: 2-groups. As shown by Buchholtz, Van Doorn and Rijke, 2-groups can be characterised elegantly in HoTT as pointed, connected, 2-truncated types. We can define computable 2-groups as 2-groups (BG, base) where ∥Ω(BG, base)∥₀ and Ω²(BG, base) are both equivalent to decidable subsets of N. I'll discuss how this definition can be phrased in terms of algebraic structure, using some recent work of Owen Milner, and give a direct construction in HoTT of a non computable finitely generated 2-group with computable underlying 1-group.