## Research

Notes about my work

**NEWS!** (2021 Nov 30) The **unabridged version** of our TYPES2021 submission is now available on the arXiv (preprint link). The paper describes our *new* formal proof of Birkhoff's variety theorem in Martin-Löf type theory using the Agda proof assistant.

More complete documentation of the Agda Universal Algebra Library (agda-algebras) is available on the main ualib.org website.

The library is open source and downloadable from the ualib/agda-algebras GitHub repository.

(2021 Jan 20) I'm 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 Agda Universal Algebra Library has undergone a makeover to make it more concise and elegant and to correct some flaws in the previous version. The latest release is version 2.03.

The main project webpage (ualib.org) is the best source for up-to-date documentation.

the Agda Universal Algebra Library gitlab repository is where one can download (clone or fork) and install the source code of the Agda UALib.

## 🔗 Publications

- The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory; (CoRR) available on arXiv [cs.LO] abs/2101.10166.
- Constraint Satisfaction Problems over Finite Structures, with Libor Barto and Antoine Mottet; (submitted to LICS 2021) available on arXiv [cs.LO] abs/2010.04958.
- Bounded homomorphisms and finitely generated fiber products of lattices, with Peter Mayr and Nik Ruskuc;
*International Journal of Algebra and Computation*, (30):693--710, 2020; available on arXiv [math.LO] abs/1907.08046. - Polynomial-time tests for difference terms in idempotent varieties, with Ralph Freese and Matthew Valeriote;
*International Journal of Algebra and Computation*, (29):927--949, 2019; available on arXiv [math.LO] abs/2011.07879. - Universal algebraic methods for constraint satisfaction problems, with Clifford Bergman; (accepted for publication in
*Logical Methods in Computer Science*) available on arXiv [cs.LO] abs/1611.02867. - Isotopic algebras with nonisomorphic congruence lattices;
*Algebra Universalis*, (72):295--298, 2014; available on arXiv [math.RA] abs/1301.7481 - Expansions of finite algebras & their congruence lattices;
*Algebra Universalis*, (69):257--278, 2013; available on arXiv [math.RA] abs/1205.1106. - Proceedings of Algebras and Lattices in Hawaii 2018, (editor) with Kira Adaricheva, Jennifer Hyndman; available at Lulu.com
- Topics in nonabelian harmonic analysis and dsp applications; (best paper award)
*Proceedings of the International Symposium on Musical Acoustics*, Nara, Japan 2004. - Characterizing musical signals with Wigner-Ville interferences;
*Proceedings of the International Computer Music Conference*, Gothenburg, Sweden 2002. - Approximating eigenvalues of large stochastic matrices;
*Proceedings of the 8th Copper Mt. Conference on Iterative Methods*, Colorado, 1998.

## Summary of Research Activities

### Research areas

These are the areas I'm most passionate about.-
**Logic**,**universal algebra**,**model theory**,**category theory**; -
**Formalization of mathematics**in**Agda**and**Lean**; -
**Computational complexity**of constraint satisfaction problems and deciding properties of general structures; -
**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

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,

My work on this project culminated in a 40-page manuscript co-authored with*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.**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