Research

Notes about my work

Reading time: about 10 minutes (2039 words).

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

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)

    Brief research summary (pdf)

    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