## Research

NEWS! (2021 Feb 12) The Agda Universal Algebra Library is undergoing a makeover to make it more concise and elegant and to correct some flaws in the previous version. Stay tuned for an announcement of the release of version 2.03 of the Agda UALib, which will appear here in late February 2021.

(2021 Jan 26) The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory, documentation for the Agda UALib.

(2021 Jan 20) I am very pleased to announce that on 12 January 2021 I achieved my goal of constructing a formal, machine-checked proof of Birkhoff's variety theorem in dependent type theory using the Agda programming language.

Birkhoff's celebrated theorem asserts that a class K of algebraic structures is closed under the taking of homomorphic images, subalgebras, and arbitrary products if and only if K is defined by a set of equations.

To the best of my knowledge, this is the first time Birkhoff's Theorem has been formulated and proved in dependent type theory and verified with a proof assistant.

The main project webpage (ualib.org) has been updated with documentation, and one can download and install the source code by visiting the Agda Universal Algebra Library's gitlab repository.

## Summary of Research Activities

### Research areas

These are the areas I'm most passionate about.
1. Logic, universal algebra, model theory, category theory;
2. Formalization of mathematics in Agda and Lean;
3. Computational complexity of constraint satisfaction problems and deciding properties of general structures;
4. Functional programming in Scala/Spark for algebra, machine learning, and Big Data.

### Current projects

• Logic and Foundations. The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory (PREPRINT)
• Computational Complexity. The Complexity of the Homomorphism Problem for Boolean structures, with Libor Barto and Antoine Motet (PREPRINT)

### Recent projects

• Lattice Theory. Bounded homomorphisms and finitely generated fiber products of lattices, with Peter Mayr and Nik Ruskuc (PREPRINT)
• Equational Logic. Polynomial-time Tests for Difference Terms in Idempotent Varieties, with Ralph Freese and Matt Valeriote (PREPRINT)
• Computational Complexity. Universal Algebraic Methods for Constraint Satisfaction Problems, with Cliff Bergman (PREPRINT)

## Formal Foundations for Informal Mathematics Research

I am fascinated by the connections between programming languages and mathematics, and one of my most active current research projects is the development of a library of all core definitions and theorems of universal algebra in the Agda proof assistant and programming language. The project title is Formal Foundations for Informal Mathematics Research and two significant outputs of the project are the paper The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory and the software library that paper describes.

## Bounded Lattices and Fiber Products

In 2018 I began collaborating with Peter Mayr (CU Boulder) and Nik Ruskuc (University of St. Andrews) who were interested in knowing when a homomorphism $\varphi \colon \mathbf{F} \to \mathbf{L}$ from a finitely generated free lattice $\mathbf{F}$ onto a finite lattice $\mathbf L$ has a kernel $\ker \varphi$ that is a finitely generated sublattice of $\mathbf{F}^2$. We conjectured that this could be characterized by whether or not the homomorphism is *bounded*. (See the book by Freese, Jezek and Nation for the definition of a bounded lattice homomorphism.) and I presented a proof of one direction of the conjecture at the Algebras and Lattices in Hawaii conference in 2018. By early 2019 we proved the converse and thus confirmed our conjecture. Mayr and Ruskuc had in mind an application for the fact that our new result is equivalent to a characterization of fiber products of lattices. A paper presenting our theorem characterizing bounded lattices was published in January of 2020 in the International Journal of Algebra and Computation, 30 (4):693--710, 2020. (PREPRINT)

## Equational Logic and Complexity

Among my most significant research accomplishments is a discovery we made in 2018 that a certain decision problem about equations in varieties of algebraic structures, that previously seemed computationally out of reach is actually tractable. In collaboration with Ralph Freese (Univ Hawaii) and Matthew Valeriote (McMaster Univ), we considered the following practical question: Given a finite algebra $\mathbf{A}$ in a finite language, can we efficiently decide whether the variety generated by $\mathbf{A}$ has a so called difference term? We answered this question (positively) in the idempotent case and then describe an algorithm for constructing difference term operations in polynomial-time. These discoveries were published in the International Journal of Algebra and Computation, 29 (6):927--949, 2019. (PREPRINT)

## Algebras and Algorithms, Structure and Complexity

Algorithms & Algorithms Meeting
Boulder, CO

In 2015, I joined a group of 8 other scientists to form a universal algebra research group and secure a 3-year NSF grant for the project, Algebras and Algorithms, Structure and Complexity Theory. Our focus is on fundamental problems at the confluence of logic, algebra, and computer science, and our main goal is to deepen understanding of how to determine the complexity of certain types of computational problems. We focus primarily on classes of algebraic problems whose solutions yield new information about the complexity of CSPs. These include scheduling problems, resource allocation problems, and problems reducible to solving systems of linear equations. CSPs are theoretically solvable, but some are not solvable efficiently. Our work provides procedures for deciding whether a given instance of a CSP is tractable or intractable, and we develop efficient algorithms for finding solutions in the tractable cases.

My work on this project culminated in a 40-page manuscript co-authored with Cliff Bergman (Iowa State Univ) and entitled Universal Algebraic Methods for Constraint Satisfaction Problems. This was recently accepted for publication in the journal Logical Methods in Computer Science (LMCS) (PREPRINT)

## The Universal Algebra Calculator

See this post